Диссертация (1150902), страница 12
Текст из файла (страница 12)
Напомним, что обход (Traversal) представляет собой обход абстрактного синтаксического дерева в глубину. Таким об-68разом для восстановления соответствующего терма необходимо поочерёдно добавлять токены, соблюдая арность соответствующих конструкторов,при этом опуская связанные переменные, вместо которых была произведена линейная подстановка19 , за исключением тех случаев, когда последнимтокеном обхода является токен, представляющий связную переменную, ивычёркивая простые редексы — пары токенов (@, λx) : α(λx) = @20 . Последний токен текущего обхода определяет выделенную вершину, а стеквисячих аргументов является упорядоченным список аргументов, которыенеобходимо подставить, как соответствующие аргументы применений.– Окружение.
Окружение восстанавливается так же, как и в случае BUNP.Построение текущего окружения завершается при появлении первого межуровневого указателя.– Стек висячих аргументов восстанавливается напрямую из текущей цепочки указателей стека висячих аргументов: внутриуровневые указатели определяют текущий аргумент, окружение которого восстанавливается согласнопредыдущему пункту, а межуровневые, помимо вышеописанного, соответствуют добавлению в стек символа-разделителя $.Теорема 5 (Согласованность алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления с полной головной линейной редукцией).Приведённый выше алгоритм восстановления состояния системы переходов дляCHLR из соответствующего состояния системы переходов для UNP корректен.Пусть S и T — соответствующие состояния систем переходов для CHLR иUNP, а S ′ и T ′ получаются из S и T применением правил ruleS и ruleT соответственно, тогда правила ruleS и ruleT имеют одинаковые имена, а состояние S ′получается из состояния T ′ согласно вышеописанному алгоритму.
Иными словами, диаграмма, приведённая на рисунке 25, является коммутативной.19Заметим, что связанные переменные, вместо которых не была произведена линейная подстановка, т.е. было применено одно из правил (FVar-*), а не правило (BVar), не исключаются из обхода при восстановлении терма с выделенной вершиной.20Мы будем придерживаться следующих обозначений: α(λx) = @$ для межуровневых и α(λx) = @ для внутриуровневых указателей стека висячих аргументов.69T = ⟨t; β; α⟩ruleTT ′ = ⟨t′ ; β ′ ; α′ ⟩S = ⟨M ; ρ; σ⟩ruleSS ′ = ⟨M ′ ; ρ′ ; σ ′ ⟩Рисунок 25.
Иллюстрация к Теореме 5Доказательство. Доказательство проводится индукцией по количеству применений правила ruleT .База индукции. Тривиально.Индукционный переход. Рассмотрим все случаи для ruleT .ii. . . @ . . . λx . . . x → @ = _e → . . . @ . . . λx . . . x e(BVar)Итак, согласно индукционному предположению состояние S восстанавливается из состояния T , T ′ получается из T посредством правила (BVar). Докажем,что S ′ получается из S применением правила [BVar] и восстанавливается из T ′ .Поскольку S восстанавливается из T , то первой его компонентой является термс выделенной вершиной x, M [x]. Более того, x ∈ ρS поскольку согласно индукционному предположению, т.к.
∃k ∈ N : β k (x) = λx ∧ α(λx) = @ = _e. Такимобразом, правило [BVar] может быть применено к состоянию S, а посколькусистема переходов для CHLR является детерминированной, то применено можетбыть только оно. Согласно индукционному предположению, окружения висячегоаргумента e, которое становится текущим после применения соответствующегоправила, равны в обоих системах переходов, а стек висячих аргументов состоянияS равен тому, который восстанавливается из состояния T , и в обоих системахпереходов он остаётся неизменным.. . . @ . . . λx → λx = λx.e → . . .
@ . . . λx e(Lam-Non-Elim)Согласно индукционному предположению, S = ⟨M [λx.e]; ρ; $ : σ⟩, следовательно, S[Lam-Non-Elim]→S ′ = ⟨M [λx.e]; ρ; $ : σ⟩. Согласно же правиламвосстановления состояния системы переходов для CHLR из T ′ , как окружение,так и стек висячих аргументов остаётся неизменным, а выделенной вершиной70терма, очевидно, становится корень e.(Lam-Elim). . . @1 .
. . @2 . . . λx → λx = λx.e → . . . @1 . . . @2 . . . λx eПо индукционному предположению, S = ⟨M [λx.e]; ρ; (e1 ,ρ′ ) : (e2 ,ρ′′ ) : σ⟩,тогда S[Lam-Elim]→S ′ = ⟨M [λx.e]; (e1 ,ρ′ ) : ρ; (e2 ,ρ′′ ) : σ⟩. Согласно правилам вос-становления состояния системы переходов для CHLR из соответствующего состояния системы переходов для UNP, состояние, восстанавливаемое из состоянияT ′ , отличается от S переносом выделения на вершину e, расширением окруженияэлементом (e1 ,ρ′ ) и отсутствием последнего на стеке висячих аргументов.(App)Аналогично BUNP (см.
теорему 4).(FVar-0). . . @1 . . . @2 . . . y → @2 = _e →ИПS = ⟨A[M [x]@B]; ρ; (B,ρ′ ) : $ : σ⟩[FVar-0]→. . . @1 . . . @2 . . . y eS ′ = ⟨A[M [x]@B]; ρ′ ; $ : σ⟩.Пусть состояние, восстанавливаемое из T ′ , ST ′ ⇋ ⟨MT ′ ; ρT ′ ; σT ′ ⟩. Тогда, очевидно, MT ′ = A[M [x]@B], ρT ′ = ρ′ по ИП для токена @2 , σT ′ отличается отσT = (B,ρ′ ) : $ : σ снятием вершины последнего, т.е.
σT ′ = $ : σ.(FVar-1). . . @1 . . . @2 . . . y → @2 = _e →. . . @1 . . . @2 . . . y e/ D(ρ) соответствует состояS = ⟨A[M [x]@B]; ρ; (B,ρ′ ) : C : σ⟩, C ̸= $, x ∈нию, восстанавливаемому из T ⇋ ST , а S[FVar-1]→ S ′ = ⟨A[M [x]@B]; ρ′ ; $ : C : σ⟩.Тогда, очевидно, MT ′ = A[M [x]@B], ρT ′ = ρ′ по ИП для токена @2 , σT ′ отличается от σT = (B,ρ′ ) : C : σ снятием вершины последнего и добавлениемтокена-разделителя ввиду изменения типа указателя на межуровневый, т.е.σT ′ = $ : C : σ.(FVar-2)Аналогично двум предыдущим случаям.■Следствие 2 (UNP является эффективной нормализирующей процедурой). UNPзавершается тогда и только тогда, когда нормальная форма входного терма существует, и она же является первой компонентой состояния, восстановленного изконечного состояния системы переходов для UNP.71Глава 5Компиляция путёмспециализацииВ данной главе мы покажем, как алгоритм трассирующей нормализации может быть использован для генерации компилятора путём его специализации.
Известно, что компилятор из языка S в язык T (как и генератор компиляторов) можетбыть автоматически сгенерирован на основе интерпретатора языка S, реализованного на языке T , при наличии самоприменимого смешанного вычислителя mixдля языка T [64, 67, 68]. Существование смешанного вычислителя следует из такназываемых проекций Футамуры-Ершова-Турчина (см. раздел 5.2).5.1.
Частичные вычисленияЧастичнымвычислителемилиспециализаторомназываетсямета-программа, которая по некоторой другой программе и подмножеству её входныхданных порождает специализированную версию этой программы (см. [68]).При этом результат исполнения специализированной программы на оставшихся входных данных должен совпадать с результатом исполенения исходнойпрограммы на всём множестве входных данных. Обоснованием возможностиспециализации и существования специализаторов является широко известнаялемма о трансляции, или чаще s − m − n теорема Клини, доказанная С.
Клинив 1943 году. Частичные вычисления могут быть определены, как специальныйслучай s − m − n теоремы, а именно, s − 1 − 1.72Определение (Частичный вычислитель). Частичным вычислителем или специализатором называется программа mix, удовлетворяющая нижеследующему уравнению.∀p ∈ Programs . ∀s, d ∈ Data . [[[[mix]](p, s)]](d) = [[p]](s, d)В результате, в то время как классические вычисления [[p]](s, d) представляютсобой одношаговое вычисление, при частичных вычислениях исполнение программы разбивается на две стадии, [[[[mix]](p, s)]].В случае лямбда-исчисления частичным вычислителем можно называть такуюпрограмму mix, что для любых лямбда-термов p и x (программы и её данных) существует специализированная программа px такая, что справедливы следующиеутверждения.1.
Если mix p x имеет β-нормальную форму, то она равна px .2. ∀y . p x ≡β p x y.При этом p является представлением (кодировкой) терма p согласно некоторой фиксированной схеме представления (кодировки) данных. Согласно первому утверждению, частичный вычислитель может быть не всюду определенным— вычисления могут не заканчиваться, если нормальной формы у специализируемой на данных программы не существует. Если вычисления завершаются, торезультатом является представление специализированной программы px . Второеусловие является “критерием успеха”, т.е.
условием корректности специализатора: на любых данных y специализированная программа px должна иметь то жеповедение, что и программа p на данных x и y. Очевидно, определение частичного вычислителя может быть напрямую распространено до произвольного числа аргументов. Аргументы, по которым производится специализация, называются статическими, а остальные аргументы — динамическими.
Частичный вычислитель принимает представления статических аргументов программы, посколькуони могут стать частью специализированной программы. Это свойство являетсяобязательным в случае лямбда-исчисления [96].Важным в контексте специализации программ является понятие точками специализации. Идея соответствующего подхода к специализации заключается в построение программных точек специализированной программы на основе программных точек исходной (специализируемой) программы, объединённых со73статическими значениями в этой точке. Это означает, что каждая логическая единица специализируемой программы — программная точка — может быть специализирована несколько раз с учётом статических данных, доступных в даннойпрограммной точке. Результат каждой такой специализации программной точкиобразует новую программную точку уже в специализированной программе.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
