Редукционные стратегии

Функциональная программа представляет собой выражение, а выполнение ее означает вычисление этого выражения. Можно сказать, что начиная с некоторого подтерма (редекса от англ, redex (REDucible Expression)) мы последовательно применяем редукции до тех пор, пока это возможно. При этом возникает вопрос, какую редукцию применять на каждом конкретном шаге? Отношение редукции не детерминистично, т.е. для некоторого терма t существует несколько различных t_i, таких что t —> t_i. Иногда выбор между ними означает выбор между конечной и бесконечной последовательности редукций, т.е. между завершением и зацикливанием программы. Например, если мы начнем редукцию с самого внутреннего редекса в выражении (λх.у) ((λх.х х х) (λх.х х х)), то получим бесконечную последовательность редукций:

(λх.у) ((λх.х х х) (λх.х х х))

—> (λх.у) ((λх.х х х) (λх.х х х) (λх.х х х))

—> (λх.у) ((λх.х х х) (λх.х х х) (λх.х х х) (λх.х х х))

—>...

Однако если мы начнем с самого внешнего редекса, то сразу получим: y и больше нельзя применить никакую редукцию.

Следующая теорема утверждает, что это обстоятельство имеет место и в общем случае.

Теорема 1. Если S —> Т, где Т находится в нормальной форме, то последовательность редукций, начинающаяся с S, построенная таким образом, чтобы для редукции всегда выбирался самый левый и самый внешний редекс, гарантированно завершится и приведет терм в нормальную форму.

Понятие «самого левого и самого внешнего» редекса можно определить индуктивно: для терма (λx.S) Т это будет сам терм; для любого другого терма S Т это будет самый левый и самый внешний редекс в S, и для абстракции λx.S это будет самый левый самый внешний редекс в S. В терминах рассмотренного синтаксиса редуцируется редекс, чей символ λ находится левее всего.

Теорема Черча-Россера, утверждает, что если начиная с терма Т провести две произвольные конечные последовательности редукций, то существуют еще две последовательности редукций, которые приводят к одному и тому же терму (он может не находиться в нормальной форме).

Теорема 2. Если t —> s₁ и t —> s₂, то существует терм и, такой, что

s₁ —> u и s ₂ —> u.

Эта теорема имеет несколько важных следствий.

Следствие 1. Если t ₁ = t ₂, то существует терм и такой, что t ₁—> и

и t₂ —> и.

Следствие 2. Если t = t ₁ и t = t ₂, где t ₁ и t₂ находятся в нормальной форме, то t ₁≡ _а t ₂, т.е. t ₁ и t₂ равны с точностью до переименования переменных.

Следовательно, нормальная форма, если она существует, единственна с точностью до α -конверсии.

С вычислительной точки зрения это означает следующее. Стратегия редуцирования самого левого самого внешнего редекса (ее называют нормализованной стратегией) является наилучшей, поскольку она приводит к результату, если он достижим с помощью какой-либо стратегии. С другой стороны, любая завершающаяся последовательность редукций всегда приводит к одному и тому же результату.