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

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

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

МакКаскером [40, 41]. Это было сделано посредством использования игровой семантики (Game Semantics). Последняя являетсяодним из способов задания формальной семантики языков программирования ирассматривает вычисления как игру (Game) между игроками: пропонентом (-ами)(Proponent, Player) и оппонентом(-ами) (Opponent) — программой и её окружением.

Семантикой программы а данном случае является стратегия (Strategy), которой пропонент должен придерживаться. Подробнее с игровой семантикой читатель может ознакомиться в следующих работах [39, 41, 42, 44, 45, 91]. В 2015 годуЛ. Онг заметил, что из игровой семантики программ для простого типизированного лямбда-исчисления естественным образом вытекает нестандартная процедура нормализации [6].

Отличительной особенностью данной процедуры является то, что вместо изменения терма посредствам β-редукции, используя стандартные приёмы, такие как окружения или замыкания11 , трассирующая нормализа11Замыканием (Closure) называется функция первого порядка, определяющая значения переменных, определённыхвне тела функции; в случае лямбда-исчисления эти переменные являются свободными. Использование замыканийявляется одним из стандартных способов реализации функциональных языков программирования.30ция (Traversal-Based Normalization, Normalization by Traversals, [6, 11, 12]) оставляет входной терм нетронутым, производя его нормализацию путём обхода егоабстрактного синтаксического дерева терма, запоминая историю этого обхода.Трассирующая нормализация в стиле Онга, ONP— оксфордская процедуранормализации (Oxford Normalization Procedure, ONP), определена для термов простого типизированного лямбда-исчисления, находящихся в η-длинной форме [6].Заметим, что поскольку рассматриваемое исчисление является простым типизированным, каждый терм имеет уникальную η-длинную форму, а процедура егонормализации, предложенная Онгом, всегда завершается.Определение.

Обоснованной последовательностью (Justified Sequence) называется последовательность, каждый элемент которой может быть обоснован(Sustified), т.е. снабжён указателем на ранний элемент последовательности(Backpointer).Определение. Обходом (Traversal) называется обоснованная последовательностьвершин абстрактного синтаксического дерева η-длинной формы терма.Каждому дереву некоторого корректного просто типизированного терма соответствует некоторое непустое множество обходов Trav, каждый из которых соответствует пути в абстрактном синтаксическом дереве η-длинной β-нормальнойформы исходного терма.

Таким образом, ONPстроит всё множество обходов данного терма, которое и определяет η-длинную β-нормальную форму терма, сводимую к нормальной форме путём η-редукции, которая, в свою очередь, всегдазавершается.Такой подход к нормализации термов оказался согласован с головной линейной редукцией. Заметим, что важной составляющей частью трассирующей нормализации в том виде, в котором она была предложена Онгом, является преобразование терма в η-длинную форму, которое, в свою очередь, существенно опираетсяна типы термов и не может быть непосредственно распространено до нетипизированного лямбда-исчисления. Последнее утверждение справедливо в силу того,что ввиду отсутствия типизации, неконтролируемое η-расширение терма, очевидно, расходится.

Тем не менее, последние работы Блюма показывают, что трассирующая нормализация в стиле Онга может быть распространена до нетипизированного лямбда-исчисления посредством эта-расширения на лету (On-the-FlyEta-Expansion). Последнее вместо построения эта-длинной формы терма и даль-31нейшей её нормализации производит эта-расширение терма по ходу самой нормализации тогда и только тогда, когда это необходимо [92].1.7.

Системы переходовОдним из подходов к изучению поведения дискретных систем являются системы переходов (Transition System, [57]) — суть четвёрка (S, I, F, →), где S —множество состояний системы, I ⊆ S — множество исходных состояний системы, F ⊆ S — множество конечных состояний системы, →⊆ S × S — отношение,означающее дискретный переход системы из одного состояния в другое, обозначаемое (s1 , s2 ) ∈→ или, для удобства чтения, s1 → s2 , где s1 , s2 ∈ S.Система переходов называется детерминированной, если её текущее состояние однозначно определяет последующее, в противном случае, она называетсянедетерминированной.Например, алгоритм Евклида может быть записан нижеследующей системойпереходов.S =N×NI=SF = {(n, n) | n ∈ N}→ = {((m,n), (m − n,n)) | m > n} ∪ {((m,n), (m,n − m)) | m < n}1.8.

ВыводыНа основе проделанного обзора сделаны следующие выводы.1. Существующие алгоритмы трассирующей нормализации определены лишьдля некоторых неполных по Тьюрингу исчислений. При этом ориентированность этих алгоритмов на системы типов и статические ограничения наструктуру исходного терма осложняют их обобщение для поддержки исчислений, полных по Тьюрингу.2.

Задача построения алгоритмов трассирующей нормализации для нетипизированного лямбда-исчисления для стратегий вычислений нормального и ап-32пликативного порядков, а также стратегии вызова по необходимости, является актуальной задачей в области анализа языков программирования.3. Алгоритмы трассирующей нормализации требуют формального операционного доказательства корректности.33Глава 2Полная головная линейнаяредукцияВ главе представлена модель головной линейной редукции (см. раздел 2.1),согласованная с известной оригинальной моделью, предложенной В.

Даносом иЛ. Ренье [8], а также предлагается модель полной головной линейной редукции(см. раздел 2.2), являющаяся расширением этой модели. Приводится формальное представление обеих моделей в виде систем переходов (см. рисунки 9 и 13),причём системы переходов для головной линейной редукции является частнымслучаем системы переходов для полной головной линейной редукции. Наконец,приводится доказательство корректности обеих моделей, а именно устанавливается их согласованность с головной редукцией лямбда-термов (см. теоремы 2 и 3).2.1. Модель головной линейной редукцииНиже приведена формальная модель головной линейной редукции в виде системы переходов, а также установлена корректность предложенной модели относительно модели головной редукции.2.1.1.

Головная линейная редукция как система переходовДля представления головной линейной редукции в виду системы переходов(см. раздел 1.7) мы определим каждую из компонент этой системы (множество34состояний, начальное состояние, множество конечных состояний, а также правила переходов) по отдельности.Множество состояний системы переходов.Состоянием системы переходовдля головной линейной редукции является тройка ⟨ A[B]; Γ; ∆ ⟩, где:– A[B] — это λ-терм, в котором вершина, являющаяся корнем поддерева B,выделена12 ;– Γ := (var 7→ (t, Γ1 )) : Γ | [ ] является окружением, иными словами, спискомсвязываний переменных, где var — переменная, t — λ-терм, Γ1 — сохранённое окружение, соответствующее терму t;– ∆ := (t, Γ) : ∆ | [ ] является стеком висячих аргументов и представляетсобой список пар вида (t, Γ), где t — λ-терм, а Γ — соответствующее емуокружение.Начальным является состояние ⟨ A[A]; [ ]; [ ] ⟩, где первое вхождение [ ] обозначает пустое окружение, второе — пустой стек висячих аргументов, A[A] обозначает входной терм с выделенным корнем.Конечным является состояние вида ⟨ A[x]; Γ; ∆ ⟩, где A[x] — исходный λ-термс выделенной переменной x, x ̸∈ Γ.Правила переходов.Формальное определение правил переходов приведено нарис.

9. Ниже дано описание каждого из этих правил, а также обозначений, используемых в определении на рис. 9.– Если выделенной вершиной в текущем состоянии является применение,(правило [App]), то выделенной вершиной следующего состояния системыпереходов является левый аргумент этого применения, а в стек висячих аргументов помещается аргумент с текущим окружением. В дальнейшем этотаргумент может быть использован для формирования простого редекса.12Выделение является синтаксической пометкой вершины абстрактного синтаксического дерева терма и обозначается подчёркиванием в примерах и правилах.35ОбозначенияA[B]λ-терм с выделенным поддеревом BΓ := (var 7→ (t, Γ1 )) : Γокружение (список)∆ := (t, Γ) : ∆стек висячих аргументов[]пустой список либо пустой стекСостояние⟨A[B]; Γ; ∆⟩Начальное состояние⟨ A[A]; [ ]; [ ] ⟩Конечное состояние⟨ A[x]; Γ; ∆ ⟩Правила переходов⟨ []⟩⟨ []⟩A e1 @e2 ; Γ; ∆→ A e1 @e2 ; Γ; (e2 , Γ) : ∆[App]⟨A [λx.e] ; Γ; [ ]⟩→ ⟨A[Lam-Non-Elim]⟩⟨ [λx.e][ ; ]Γ; [ ]⟩′′Z;(x→7(B,Γ)):Γ;∆[Lam-Elim]→ Aλx.e⟨A [λx.e] ; Γ; (B, Γ ) : ∆⟩ZBZ′′⟨A [x] ; [.

. . , (x 7→ (B, Γ )), . . . ]; ∆⟩ → ⟨A [B] ; Γ ; ∆⟩[BVar]Рисунок 9. Система переходов для головной линейной редукции– Если выделенной вершиной является абстракция, то следующей выделенной вершиной становится корень подтерма, представляющего тело этой абстракции. Если стек висячих аргументов пуст, то переменная абстракциине связывается ни с каким аргументом (правило [Lam-Non-Elim]). Если жестек висячих аргументов не пуст, эта абстракция формирует простой редекс с его вершиной (правило [Lam-Elim]). В последнем случае, абстракцияи соответствующие применение и его аргумент вычёркиваются13 из текущего дерева (первого компонента текущего состояния системы переходов),а простой редекс сохраняется в текущем окружении.

Очевидно, что правиланапрямую согласованы с определением простого редекса.– Если же выделенной вершиной текущего состояния является переменная,то, если она является свободной, система переходов достигла своего конечного состояния, ежели переменная является связанной, то либо существуетпростой редекс, аргумент которого может быть подставлен вместо вхождения этой головной переменной (правило [BVar]), либо такого редекса нет, иопять же система переходов достигла своего конечного состояния.Заметим,чтосистемапереходовявляетсядетерминированнойисинтаксически–управляемой, а выбор правила зависит лишь от первого эле13Вычёркивание является синтаксической пометкой вершин в дереве, а не полным удалением подтерма. С этогоHмомента мы будем использовать обозначение Aλx .

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

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