Диссертация (1150902), страница 11
Текст из файла (страница 11)
Приведённыйвыше алгоритм восстановления состояния системы переходов для HLR из соответствующего состояния системы переходов для BUNP корректен.Пусть S и T — соответствующие состояния систем переходов для HLR иBUNP, а S ′ и T ′ получаются из S и T применением правил ruleS и ruleT соответственно, тогда правила ruleS и ruleT имеют одинаковые имена, а состояниеS ′ получается из состояния T ′ согласно вышеописанному алгоритму. Иными словами диаграмма, приведённая на рис. 23, является коммутативной.Доказательство. Доказательство выполним индукцией по количеству применений правила ruleT .База индукции. Тривиально.Индукционный переход.
Рассмотрим все возможные случаи для правила ruleT .– (App):. . . @ −→ @ = e_ −→... @ eСогласно индукционному предположению, S соответствует T . Более того,первой компонентой S является терм M [@]. Согласно правилам системыпереходов для HLR, правило [App] может быть применено к состоянию S,и никакое другое правило в данном случае применено быть не может.1. В обеих системах переходов правила требуют перейти к первому аргументу (левому ребёнку в смысле АСД терма) применения, таким об-63разом первый компонент S ′ в точности соответствует тому, которыйбудет восстановлен из T ′ — M [e].2. Согласно правилам восстановления состояния системы переходов дляHLR из обхода, окружение, восстановленное из состояния T ′ , совпадает с окружением, восстановленным из состояния T .
Действительно,если ∃x : e = λx, то по определению токен λx исключается из рассмотрения при восстановлении окружения. Если же ∀x.e ̸= λx, то, очевидно, список простых редексов обхода T и T ′ совпадают. Согласно жеправилу [App], окружение состояния S ′ является тем же самым, что иИПу состояния S. Таким образом, ρS ′ = ρS = ρT = ρT ′ .3. В обоих случаях стек висячих аргументов расширяется аргументомрассматриваемых применений, которые совпадают согласно индукционному предположению.nil– (Lam-Non-Elim):nil nil. . .
λx −→ λx = λx.e −→ . . . λxeПоскольку указатель стека висячих аргументов у токена λx является нулевым, то согласно индукционному предположению стек висячих указателейу S пуст. Следовательно, только правило [Lam-Non-Elim] может быть применено к S. По тем же соображениям, что и в случае (App), терм и окружение, восстанавливаемые из T ′ в точности совпадают с первыми двумя компонентами S ′ , а стек висячих аргументов в обоих случаях остаётся пустым.– (Lam-Elim):. . . @1 . . . @2 .
. . λx −→ λx = λx.e −→. . . @1 . . . @2 . . . λx eСогласно индукционному предположению, окружение в состоянии S непусто. Более того, его первым элементом является (A, ρ′ ), где A — аргумент @2 , а ρ′ – соответствующее окружение. Таким образом правило [LamElim] должно быть применено к состоянию S.
Как и в случае с правилом(App), терм, построенный из состояния T ′ , является первым компонентомсостояния S ′ . Окружения в обоих случаях расширяются простым редексом64(λx, A), где окружение терма A одинаково в обеих системах переходов. Также в обоих случаях ровно один элемент был снят со стека висячих аргументов.i– (BVar):. . . @ . . . λx . . . x −→ @ = _e −→i. . . @ .
. . λx . . . x eЕсли правило (BVar) может быть применено, то, во-первых, токен λx должен быть доступен по цепочке связывающих указателей из токена x, вовторых, токены λx и @ должны быть связаны указателем стека висячихаргументов (т.е. α(λx) = @). Согласно индукционному предположению Sвосстанавливается из T , а значит, (x,e) ∈ ρS , и правило [BVar] может бытьприменено к состоянию S, и никакое другое правило к S применено бытьне может, следовательно, термы, подставляемые вместо x в обоих случаях, совпадают между собой.
Таким образом терм, восстанавливаемый из T ′совпадает с первой компонентой состояния S ′ , а его окружение — с окружением S ′ . Наконец, стек висячих аргументов остаётся неизменным в обоихслучаях.■Следствие 1. Первой компонентой состояния, получающегося восстановлениемиз конечного состояния системы переходов для BUNP, согласно приведённымправилам, является терм в псевдо-головной нормальной форме.4.2.
Алгоритм трассирующей нормализации длянетипизированного лямбда-исчисления и полная головная линейная редукцияСистема переходов для полной головной линейной редукции (CHLR) приведена на рисунке 13. Для удобства чтения изменения по сравнению правилами система переходов для HLR выделены с помощью прямоугольников: выделение .
Система переходов для полной головной линейной редукции отличается от таковойдля головной линейной редукции наличием новых правил [FVar-*], отвечающих65за рекурсивное применение к аргументам, а также нового символа-разделителя $,запрещающего связывать абстракции и применения, не находящиеся на одном пути в абстрактном синтаксическом дереве терма, соответствующего текущему состоянию системы переходов. Более того, конечным состоянием может быть лишьтакое, в котором стек висячих аргументов пуст, а текущей выделенной вершинойявляется переменная, не определённая в текущем окружении.Далее приводится система переходов для UNP, согласованная с оригинальной формулировкой алгоритма трассирующей нормализации (см.
рис. 19 и [73]),и устанавливается соответствие между системами переходов для CHLR и UNPподобно тому, как это было сделано с соответствующими системами переходовдля HLR и BUNP в предыдущем разделе.4.2.1. UNP в виде системы переходовВ данном разделе приводится формальное представление UNP в виде системыпереходов. Заметим, что ниже представленная система переходов имеет в точности столько же правил переходов, сколько и система переходов для полной головной линейной редукции, предложенная в [95] и приведённая на рисунке 9. Болеетого, мы покажем, как состояния этих систем переходов связаны отношением симуляции.Подобно тому, как система переходов для полной головной линейной редукции является обобщением системы переходов для головной линейной редукции,так и система переходов для алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления является обобщением системы переходов дляограниченной версии алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления.
Как и в случае BUNP, в UNP каждый токен можетбыть снабжён указателями нижеследующих родов.– Указатель стека висячих аргументов. В отличие от BUNP, в UNP указательстека висячих аргументов бывает двух нижеследующих типов.– Внутриуровневый указатель. Изображается жирной коричневой стрелкой над обходом и имеет тот же смысл, что и указатель стека висячихаргументов в BUNP.66Новые обозначениямежуровневый и опциональный межуровневый указателистека висячих аргументоввнутриуровневый и опциональный внутриуровневый указателистека висячих аргументовопциональный указательстека висячих аргументов произвольного типа(BVar)i. .
. @ . . . λx . . . xi→@ = _e→j. . . @ . . . λx . . . x ej(Lam-Non-Elim). . . @ . . . λx→λx = λx.e→. . . @ . . . λx e→λx = λx.e→. . . @1 . . . @2 . . . λx e→@ = e_→... @ e→@2 = _e→. . . @1 . . . @2 . . . y e→@2 = _e→. . . @1 . . . @2 . . . y e→@2 = _e→. . . @1 . . . @2 . . . y e(Lam-Elim). .
. @1 . . . @2 . . . λx(App)... @(FVar-0). . . @1 . . . @2 . . . y(FVar-1). . . @1 . . . @2 . . . y(FVar-2). . . @1 . . . @2 . . . yРисунок 24. Правила переходов для UNP67– Межуровневый указатель. Изображается фиолетовой стрелкой с плоским началом над обходом. В то время как межуровневый указатель всёещё указывает на последний висячий аргумент, он запрещает формирование простого редекса. Интуитивно, он является аналогом символаразделителя $ системы переходов для CHLR.Мы также будем использовать пунктирный красный указатель над обходомдля обозначения указателя стека висячих аргументов в тех случаях, когданас не интересует его тип. При формулировке правил переходов красныепунктирные указатели должны быть согласованы: добавляемый к новомутокену указатель стека висячих аргументов, будучи изображённым краснойпунктирной стрелкой, имеет тот же тип, что и аналогичный ему указатель,уже представленный в левой части правила.– Обобщённый связывающий указатель.
Как и в случае с BUNP, связывающий указатель изображается на диаграммах зелёной стрелкой под обходом.Более того, его смысл и правила установки остаются неизменными.Правила переходов для UNP приведены на рисунке 24. Для обеспечения детерминированности системы переходов, мы будем считать, что правила упорядочены и в случае, когда несколько правил может быть применено, применяется то,что приведено раньше на рисунке 24.
В действительности, в конфликте могут находится лишь правило (BVar) и любое из правил (FVar-*), а наш порядок означает,что последние могут быть применены тогда и только тогда, когда не может бытьприменено первое, иными словами, правила для свободных переменных применяются, только если текущая переменная не связана никаким простым редексом.4.2.2. Соответствие между CHLR и UNPДля восстановления состояния системы переходов для полной головной линейной редукции из соответствующего состояния системы переходов для алгоритма трассирующей нормализации для нетипизированного лямбда-исчислениямы определим способ восстановления каждой из его компонент по отдельности.– Терм с выделенной вершиной.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
