Диссертация (1150902), страница 10

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 10)

Переменная S является свободной, следовательно, вызываетсяфункция применения продолжения apk. Поскольку ch не пуст, вызывается функция eval на аргументе последнего применения, который ещё не был просмотрени не образует спинального редекса. В данном случае таковым является токен @6 .@1 @2 λs1 λz1 @3 s1 @7 λs2 λz2 @5 s2 S @6Наконец, обход завершится за тридцать шагов. Итоговый обход представленна рисунке 21а).Нормальная форма может быть получена из итогового обхода терма удалением из него всех токенов, участвующих в формировании спинальных редексов, атакже всех вхождений связанных переменных, вместо которых была произведе-56@1 @2 λs1 λz1 @3 s1 @7 λs2 λz2 @5 s2 S @6 s2 S z2 @4 s1 @7 λs2 λz2 @5 s2 S @6 s2 S z2 z1 Zа) Итоговый обход@5@6S@5S@6S@5 S @6 S @5 S @6 S Zб) Обход после “очистки”SZв) АСД терма соответствующегообходу после “очистки”Рисунок 21.

Результат работы UNP на терме mul ⃗2 ⃗2на подстановка. Результатом такой “очистки” обхода, полученного посредствомалгоритма трассирующей нормализации, будет обход абстрактного синтаксического дерева нормальной формы терма в глубину. Оба они приведены на рисунках16 21б) и 21в) соответственно. Как и ожидалось, им соответствует термS(S(S(S Z))), являющийся нормальной формой исходного терма, mul ⃗2 ⃗2.На рисунке видно, что некоторые токены (вершины АСД исходного терма mul ⃗2 ⃗2) могут встречаться в результатенесколько раз, хотя входить в исходный терм многие их них могли лишь один раз. Например, оба токена применения, @5 и @6 , встречаются дважды, а свободная переменная S встречается аж четыре раза.

В данной ситуации нетникакого противоречия: токены применения рассматриваются, игнорируя нумерацию, которая была нужна лишь длябольшей наглядности графических представлений обходов, также игнорируются и имена переменных. Напомним,что мы рассматриваем переменные сразу в двух представлениях: именованном и анонимном. Таким образом, послеуничтожения имён, переменные представляются индексами де Брауна, а абстракции становятся анонимными.1657Глава 4Корректность алгоритматрассирующей нормализациидля нетипизированноголямбда-исчисленияДанная глава посвящена доказательству17 корректности алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления, приведённого вразделе 3.5. Для этого вводится ограниченная версия алгоритма трассирующейнормализации, BUNP, в виде системы переходов (см.

раздел 4.1), и устанавливается соответствие между ней и системой переходов для головной линейной редукцией (см. теорему 4). Затем в раздел 4.1.1 и сам алгоритм трассирующей нормализации представляется в виде системы переходов, которая в свою очередь являетсярасширением системы переходов для BUNP, а также устанавливается соответствие между этой системой и системой переходов для полной головной линейнойредукции — см. теорему 5.58Обозначенияiiсоответствующий указатель на некоторую вершину i (в т.ч. и nil)указатель стека висячих аргументовопциональный указатель стека висячих аргументовобощённый связывающий указательдоступность по цепочке связывающих указателейСостояниеобходaНачальное состояниекорень AST входноготермаКонечное состояниеобходbПравила переходовii(BVar) .

. . @ . . . λx . . . x →@=_e→j. . . @ . . . λx . . . x ejnil nilnil(Lam-Non-Elim). . . λx→ λx = λx.e→→ λx = λx.e→ . . . @1 . . . @2 . . . λx ei→→. . . λx e(Lam-Elim). . . @1 . . . @2 . . . λxi(App)... @@=e_a... @ eДля удобства формального изложения мы будем считать, что состоянием системы переходов дляBUNP является тройка ⟨t; β; α⟩, где t : Σ → [1 .. |t|] является упорядоченной последовательностью,|t| — длина обхода t, a частичные функции α, β : [1 ..

|t|] ⇀ [1 .. |t| − 1] определяют множествауказателей стека висячих аргументов и связывающих указателей соответственно.bКонечным состоянием является обход, такой, что его последний токен является токеномпеременной, не имеющим указателя висячих аргументов, t = _ • x : α(x) = ⊥, являющейся либосвободной, ̸ ∃k ∈ N : α ◦ β k (x) = λx, либо связанной, чья абстракция не связана никаким простымредексом, ∢k ∈ N : β k (x) = λx => β k (x) = λx ∈/ D(α).Рисунок 22. Система переходов для BUNP594.1.

Головная линейная редукция и ограниченнаяверсия алгоритма трассирующей нормализацииВ этом разделе представлена ограниченная версия алгоритма трассирующейнормализации в виде системы переходов, и установлено соответствие между приведёнными системами переходов для головной линейной редукции (см. рис. 9) иограниченной версии алгоритма трассирующей нормализации (см. рис. 22).4.1.1.

Система переходов для BUNPBUNP, или базовый UNP, является ограниченной версией UNP (см. раздел 3.5, [73]). BUNP соответствует головной линейной редукции, являющейсяосновой для полной головной линейной редукции. Далее мы установим соответствие между системами переходов для BUNP и HLR, определив функцию преобразования состояний одной системы переходов в состояния другой. Более того,правила переходов рассматриваемых систем переходов напрямую отображаютсядруг в друга. В отличие от HLR, состояние системы переходов для BUNP является обоснованной последовательностью вершин входного лямбда-терма, снабжённых указателями на ранние вершины последовательности.

В BUNP существуетдва следующих рода указателей.– Обобщённый связывающий указатель (generalised binder backpointer). Длякраткости мы часто будем упускать слово “обобщённый” и говорить просто — связывающий указатель. На диаграммах, представляющих обходы,он будет обозначаться зелёной стрелкой под последовательностью токенов.Связывающий указатель является BUNP-эквивалентом окружения: он позволяет построить соответствующее окружение на каждом шаге алгоритма.Для каждого токена он указывает на токен, представляющий последнююабстракцию, которую необходимо добавить в окружение при его формировании, если эта абстракция участвует в образовании какого-либо простогоредекса.17Доказательство опубликовано в [94].60– Указатель стека висячих аргументов. На диаграммах он будет представлен коричневой стрелкой, изображаемой над последовательностью токенов.Указатель стека висячих аргументов является BUNP-эквивалентом стека висячих указателей σ системы переходов для HLR.

Инвариантом этого указателя является то, что он всегда указывает либо на токен, представляющийприменение термов, либо отсутствует вовсе. Указатель стека висячих аргументов позволяет конструировать список спинальных аргументов терма накаждом шаге алгоритма. Заметим, что любое вхождение нижеследующегошаблона в обход формирует простой редекс (λx, A), где A — спинальныйаргумент (аргумент @ в АСД терма), а λx — головная абстракция.. . . @ . . .

λx . . .Таким образом, указатель стека висячих аргументов для токеновабстракций всегда указывает на токен-применение, с аргументом которогоон формирует простой редекс, а для остальных токенов — на применение,являющиеся непосредственным предком последнего спинального аргумента. В некоторых случаях, чтобы подчеркнуть, что некоторый токен неимеет указателя стека висячих аргументов, мы будем вводить специальнуювершину nil за пределами обхода, на которую соответствующий указательи будет указывать.Система переходов для BUNP приведена на рис. 2218 . Для краткости изложения и ясности графического представления, а также в виду их простоты, правила установки обобщённого связывающего указателя опущены во всех правилах,кроме (BVar). Для всех остальных правил применяется следующее правило установки обобщённого связывающего указателя: если последний токен обхода былабстракцией, то у добавляемого в обход токена обобщённый связывающий указатель выставляется на эту самую абстракцию, в противном случае он выставляетсятакой же, как у предыдущего токена.18Заметим, что правила (Lam-Elim) и (Lam-Non-Elim), вообще говоря, могут быть объедены в одно.

Тем не менее, для более наглядного представления и взаимной-однозначности соответствия между одноимёнными правиламисистем переходов для HLR и BUNP мы вводим правила именно в таком виде.614.1.2. Соответствие между головной линейной редукцией иограниченной версией алгоритма трассирующей нормализации для нетипизированного лямбда-исчисленияМы установим соответствие между приведёнными в предыдущих разделахсистемами переходов для HLR (см. рис.

9) и BUNP (см. рис. 22). Мы покажем, что как состояния систем переходов, так и их шаги находятся во взаимнооднозначном соответствии.Для того, чтобы восстановить состояние системы переходов для HLR из текущего обхода, необходимо определить каждую из его компонент: текущий терм свыделенной вершиной, текущее окружение ρ и корректный стек висячих аргументов σ. Итак, пусть дан обход t, тогда терм, окружение и стек висячих аргументовмогут быть восстановлены из него нижеследующим образом.– Терм. Обход t представляет собой подпоследовательность самого левого пути в абстрактном синтаксическом дереве терма. Таким образом, для восстановления соответствующего первого компонента системы переходов дляHLR необходимо снабдить токены-применения соответствующими висячими аргументами, игнорируя вхождения связанных переменных, и выделитьвершину, соответствующую последнему токену обхода.– Окружение.

Напомним, что каждое вхождение шаблона. . . @ . . . λx . . .определяет простой редекс (λx, A), где A является аргументом вершиныприменения @. Если последним токеном текущего обхода является абстракция, то при восстановлении окружения обход рассматривается без учётаэтой абстракции. Пусть R — множество всех простых редексов обхода t,Λ — список лямбда-абстракций, доступных из последнего токена по цепочке связывающих указателей, тогда текущее окружение ρ(t) = {x 7→(A, ρ′ ) | (λx,A) ∈ R} ↾ Λ, где ρ′ определено рекурсивно. Заметим, чтомы подразумеваем, что множество R упорядочено: пусть r1 = (λx,A), r2 =(λy, B) ∈ R, тогда r1 > r2 тогда и только тогда, когда токен λx входит вобход до токена λy.62– Висячие аргументы.

Стек висячих аргументов получается из обхода ограничением последнего на список токенов, доступных из него по цепочке указателей висячих аргументов, и снабжением их соответствующими окружениями, согласно предыдущему пункту.T = ⟨t; β; α⟩ruleTT ′ = ⟨t′ ; β ′ ; α′ ⟩S = ⟨M ; ρ; σ⟩ruleSS ′ = ⟨M ′ ; ρ′ ; σ ′ ⟩Рисунок 23. Иллюстрация к Теореме 4Теорема 4 (Согласованность систем переходов для BUNP и HLR).

Характеристики

Список файлов диссертации