Диссертация (1150902), страница 7
Текст из файла (страница 7)
e] для терма A, у которого подтерм B, вершина “λx” и соотHB [Zветствующая вершина оператора применения помечены (вычеркнуты).36⟨(λ x . x) @ (λ y . y);⟨(λ x . x) @ (λ y . y);XXXH@(λy.Xy);⟨(λHx . x) @HX@XX HX@⟨ (λHx . λ y .y) @(λy .Xy);HX@XX H.Xy);⟨ (λHx . λ y .y) @@(λyXHX@[ ];[][ ];[((λ y . y), [ ])][x 7→ ((λ y . y), [ ])]; [ ][ ];[][ ];[]⟩⟩⟩⟩⟩→[App]→[Lam-Elim]→[BVar]→[Lam-Non-Elim]̸→(2.2)(2.3)(2.4)(2.5)(2.6)Рисунок 10.
Поведение системы переходов для головной линейной редукции напримере терма (λ x . x) @ (λ y . y)мента состояния (формально, выбор между правилами [Lam-*] зависит оттекущего состояния стека висячих аргументов, но это состояние также зависит отвходного терма). Единственным случаем, когда система переходов может достичьсвоего конечного состояния, является случай выделенной переменной, котораялибо свободна, либо не связана никаким простым редексом. Более того, правилагарантируют, что выделенной может быть лишь вершина, находящаяся на самомлевом пути абстрактного синтаксического дерева терма. Иными словами, еслисистема переходов достигает конечного состояния, вычисления завершаются,головное вхождение переменной (hoc-переменная) оказывается выделенным, асама переменная не связанна никаким простым редексом.Пример поведения системы переходов для головной линейной редукции натерме (λ x .
x)@(λ y . y) приведён на рисунке 10. Как и ожидалось, первым элементом конечного состояния (игнорируя вычеркивание вершин) является псевдоголовная нормальная форма входного терма, а именно терм (λx . λ y .y) @ (λ y . y).Головной же нормальной формой рассматриваемого терма является терм λy . y,получаемый в данном случае простым “выбрасыванием” вычеркнутых вершин изпервого элемента конечного состояния системы переходов. В общем случае нампотребуется определить специальную функцию расширения exp, которая будетвозвращать соответствующий терм из конечного состояния, а также необходимобудет установить согласованность этой функции с головной редукцией (см. раздел 2.1.2).■372.1.2.
Согласованность головной и головной линейной стратегий редукцииВ данном разделе приводится доказательство согласованности головной иголовной линейной стратегий редукции. Сначала определяется дополнительнаяфункция расширения — exp.Функция расширения.По данному состоянию системы переходов функцияexp возвращает λ-терм.
Эта функция производит последовательную редукциювсех простых редексов, накопившихся на данный момент времени. Поскольку этапоследовательность совпадает с последовательностью головных редексов, головная и линейная головная редукции оказываются согласованы.
Формально это выражается следующим образом14 :exp ⟨M [A]; Γ • [(x 7→ (B, Γ′ ))]; ∆⟩ = exp ⟨M [A[x/B[Γ′ ]]]; Γ; ∆⟩exp ⟨MB [A]; [ ]; (B,Γ′ ) : ∆⟩ = exp ⟨MB[Γ′ ] [A]; [ ]; ∆⟩exp ⟨M ; [ ]; [ ]⟩ = M ′ ,(2.7)(2.8)(2.9)где B[Γ′ ] = exp ⟨B; Γ′ ; [ ]⟩, а терм M ′ получается из терма M удалением всехвычеркнутых вершин.Согласно определению, сначала функция exp производит последовательностьподстановок согласно информации, накопленной в текущем окружении Γ (см.определение (2.7)). А именно, функция расширения производит подстановку терма B[Γ′ ] вместо всех вхождений переменной x в такое поддерево терма M , котороеимеет корнем выделенную вершину (т.е. поддерево A).
Далее функция exp производит последовательность подстановок в аргументах из стека висячих аргументов ∆, согласно сохранённым вместе с ними окружениям. А именно, каждый рекурсивный вызов, соответствующий определению (2.8), производит подстановкувсех переменных в соответствии с контекстом Γ′ исключительно в висячем аргументе B. Напомним, мы придерживаемся соглашения Барендрегта (см. главу 1),т.е.
предполагается, что все переменные имеют уникальные имена. Следование14α • β означает конкатенацию контейнеров α и β.38этой концепции в данном случае15 позволяет избежать захвата имён переменныхпри подстановке (см. главу 1). Далее мы будем называть расширением состояниясистемы переходов результат применения функции exp к этому состоянию.Отметим некоторые важные свойства системы переходов головной линейнойредукции.1.
По определению функции exp (уравнения (2.7) и (2.8)), единственное правило системы переходов, при применении которого расширения получаемого состояние не равны расширению исходного состояния, из которого онополучено, — это [Lam-Elim]; все остальные правила оставляют расширениенеизменным.2. Количество переходов системы без применения правила [Lam-Elim] конечно. Данный факт является прямым следствием определения контекста, конечности размера входного терма и того, что в силу определения толькоправило [Lam-Elim] может изменить контекст.
С этого момента мы будемобозначать последовательное применение правил без применения правила∗[Lam-Elim] через →.Пример.Ниже показан результат применения функции exp к каждому состоя-нию системы переходов для примера, приведённого на рисунке 10.exp((2.2)) = exp(⟨(λ x . x) @ (λ y . y); [ ]; [ ]⟩) = (λ x . x) @ (λ y . y)exp((2.3)) = exp(⟨(λ x . x) @ (λ y . y); [ ]; [((λ y . y), [ ])]⟩)= exp(⟨(λ x . x) @ (λ y . y); [ ]; [ ]⟩)= (λ x .
x) @ (λ y . y)XHXyX.exp((2.4)) = exp(⟨(λHx . x) @@(λXy);HX [(x 7→ ((λ y . y), [ ]))]; [ ]⟩)@XXXHXyX.= exp(⟨(λHx . λ y . y) @@(λXy);HX [ ]; [ ]⟩) = λ y . y@HXyX.exp((2.5)) = exp(⟨(λHx . λ y . y) @@(λXy);HX [ ]; [ ]⟩) = λ y . y@HXyX.λHx . λ y . y) @exp((2.6)) = exp(⟨(@(λXy);HX [ ]; [ ]⟩) = λ y . y@15Заметим, что следование соглашению Барендрегта не избавляет от неприятностей, связанных с переименованиемпеременных, при подставновке в общем случае. Тем не менее, при использовании окружений эта проблема откладывается до момента конструирования результата вычислений (Read-Out Function).
Для краткости изложения, мы будемигнорировать эту проблему. Заметим, что она может быть решена с помощью отдельного обхода по АСД результатавычислений, генерации новых имён и переименовании переменных на лету.39■Идея доказательства согласованности головной и линейной головной стратегий редукции состоит в следующем. Расширение не может быть измененоникаким правилом, кроме [Lam-Elim], следовательно, после применения функции расширения к состояниям системы переходов каждое применение правила[Lam-Elim] соответствует одному шагу головной редукции. Так, в примере выше(λ x . x) @ (λ y . y) соответствует первому шагу системы переходов, а λ y . yсоответствует трём оставшимся шагам.Теорема 2. Пусть ⟨.
. . ⟩ — некоторое состояние системы переходов, расширениекоторого обозначено троеточием . . . (см. иллюстрацию к теореме, рисунок 11),такое, что на следующем шаге должно быть применено правило [Lam-Elim]. Приэтом результатом его применения является состояние ⟨Mi ; Γi ; ∆i ⟩, расширениемкоторого является некоторый терм Mi′ . Далее система переходов делает некотороеконечное число шагов до следующего применения правила [Lam-Elim].
Обозначим ⟨Mi ; Γi ; ∆i ⟩ состояние, расширением которого является терм Mi′ . Тогда еслиможет быть применено правило [Lam-Elim], расширяющее окружение Γ новымсвязыванием (x 7→ (B,Γ′ )), и расширением результата применения которого яв′′получается из терма Mi за одним шаг, то терм Mi+1ляется некоторый терм Mi+1головной редукции.Доказательство. Теорема доказывается индукцией по количеству примененийправила [Lam-Elim].База индукции.
Первый элемент, добавляемый в Γ, является головным редексомпо определению, поэтому база индукции очевидна.Индукционный переход. Согласно индукционному предположению, после i-гоприменения правила [Lam-Elim], текущим состоянием будет ⟨Mi ; Γi ; ∆i ⟩, рас∗ширением которого является некоторый терм Mi . Как уже отмечалось ранее, →∗не изменяет расширения и число шагов → конечно. Таким образом, существуютследующие возможные случаи.⟨. . .
⟩[Lam-Elim]∗⟨A[λx.e]; Γ; (B, Γ′ ) : ∆⟩[Lam-Elim]Z⟨Aλx.e];(x 7→ (B, Γ′ )) : Γ; ∆⟩ZB [Zexpexp...⟨Mi ; Γi ; ∆i ⟩expexpHRMi′HRРисунок 11. Иллюстрация к теореме 2′Mi+1401. Система переходов достигла конечного состояния, и доказывать нечего.2. Система не достигла конечного состояния, и может быть применено правило [Lam-Elim]. В данном случае, согласно определению правила [LamElim], мы знаем вид исходного состояния: ⟨A[λx.e]; Γ; (B,Γ′ ) : ∆⟩.
Обозначим это состояние как (i), а результат применения к нему правила [LamZElim] обозначим как ⟨A@λx.e];(x 7→ (B, Γ′ )) : Γ; ∆⟩ или сокращенно (ii).ZB [Нам надо показать, что результат применения функции exp к состоянию (ii)совпадает с результатом одного шага головной редукции терма Mi′ , т.е. с′термом Mi+1. Применим функцию exp к состоянию (i):exp ⟨A[λx. e]; Γ; (B,Γ′ ) : ∆⟩(2.10)exp∗→ exp ⟨A[λx.
e[Γ]]; [ ]; (B,Γ′ ) : ∆⟩ по (2.7)exp→ exp ⟨AB[Γ′ ] [λx. e[Γ]]; [ ]; ∆⟩за одни шаг (2.8)exp→ ...(2.11)(2.12)(2.13)Теперь применим функцию exp к состоянию (ii):Z e]; (x 7→ (B,Γ′ )) : Γ; ∆⟩exp⟨A@λx.ZB [exp∗Z e[Γ]]; [(x 7→ (B,Γ′ )]; ∆⟩→ exp ⟨A@λx.ZB [expZ e[Γ][x/B[Γ′ ]]]; [ ]; ∆⟩→ exp ⟨A@λx.ZB [exp→ ...(2.14)согласно (2.7)(2.15)за шаг (2.7)(2.16)(2.17)Легко заметить, что терм, являющийся первым компонентом состояния(2.12), AB[Γ′ ] [λx.e[Γ]], имеет головной редекс (λx, B), поскольку контекстуже является пустым.
Таким образом, если применить шаг головной редук′Z]]]. Поции к данному терму, То результатом будет терм A@λx.e[Γ][x/B[ΓZB [определению головной редукции этот терм соответствует первой компоненте состояния (2.16). Согласно определениям (2.7) и (2.8), если продолжитьприменение функции exp к состояниям (2.12) и (2.16), то в обоих случаяходин и тот же стек висячих аргументов ∆ не произведёт никаких изменение ни в аргументе B, ни в выделенном поддереве e. Следовательно, редекс41(λx, B) является головным для терма Mi′ , а значит, расширением состояния′(ii) является терм Mi+1.■Теорема 2 сопоставляет каждому шагу головной редукции шаг системы переходов, соответствующий применению правила [Lam-Elim]. Таким образом, прямым следствием теоремы является тот факт, что головная линейная редукция завершается тогда и только тогда, когда завершается головная редукция.Более того, поскольку функция расширения не способна изменить путь от корня дерева терма до корня его выделенного поддерева, первая компонента конечного состояния системы переходов для головной линейной редукции содержиттакой терм, что самый левый путь в представляющем его дереве является частьюголовной нормальной формы, а значит, расширение конечного состояния является вершиной дерева Бёма.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
