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

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

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

Эти рассуждения являются неформальным обоснованием того, что рекурсивное применение головной линейной редукции ко всемоставшимся аргументам, т.е. полная головная линейная редукция (см. раздел 2.2),нормализует терм. Теорема 3 является формальным доказательством это утверждения.2.2. Модель полной головной линейной редукцииПолная головная линейная редукция (Complete Head Linear Reduction, CHLR)является расширением головной линейной редукции, рекурсивно применяющимпоследнюю к аргументам при достижении конечного состояния. В данном разделе приводится разработанное автором формальное определение полной головнойлинейной редукции в виде системы переходов, являющийся расширением системы переходов для головной линейной редукции, приведённой в разделе 2.1.2.2.1.

Система переходов для полной головной линейной редукцииСистема переходов для CHLR является расширением системы переходов дляHLR тремя новыми правилами [FVar-*]. Эти правила предназначены для обра-42λx@1@2xBλy...Рисунок 12. Терм M [λy]ботки ситуации, когда система переходов для HLR достигла своего конечного состояния. А именно, если система переходов для HLR достигла своего конечного состояния, то его первой компонентой является некоторый терм, выделеннымподдеревом которого является вхождение головной переменной, которая либо является свободной, либо динамически несвязанной ни с каким аргументом. Поддинамически несвязанная с аргументом переменной понимается такая связаннаяпеременная, чья абстракция не применена ни к какому аргументу.

Другими словами, абстракция динамически несвязанной с аргументом связанной переменнойне участвует в формировании какого-либо простого редекса. Итак, система переходов для полной головной линейной редукции обладает нижеследующими изменениями по сравнению с системой переходов для головной линейной редукции.– Стек висячих аргументов ∆ расширяется специальным символом $. Этотсимвол играет роль разделителя, запрещающего связывать абстракцию саргументом, если путь от этого аргумента до соответствующей абстракциине является левым путём.

Мы будем именовать символ $ символом разделителем. Символ разделитель гарантирует, что все редексы в текущем контексте (окружении Γ) являются простыми для данного подтерма. Например,пусть дан некоторый входной терм, и в ходе полной головной линейной редукции получено состояние ⟨M [λy]; Γ; [$, (B, Γ0 )]⟩, где терм M [λy] изображён на рисунке 12.

В данном примере разделитель $ запрещает связываниевершины λy с висячим аргументом B, поскольку они не образуют простогоредекса.– Конечное состояния системы переходов также претерпевает изменения: теперь стек висячих аргументов в нём должен быть пустым. Конечным стано-43вится состояние следующего вида: ⟨M [x] ; Γ; [ ]⟩, где x ̸∈ dom(Γ). Начальное же состояние совпадает с начальным состоянием системы переходовголовной линейной редукции ⟨λ1 ; [ ]; [ ]⟩, где λ1 является входным термомс выделенным корнем.– Результатом CHLR является терм в нормальной форме.

В терминах системы переходов это означает, что он может быть получен из первой компоненты конечного состояния системы переходов путём удаления из неё всехвычеркнутых вершин.– На рисунке 13 приведены правила для переходов системы переходов дляCHLR. Для удобства чтения новые/измененные правила по сравнениюс системой переходов для HLR выделены с помощью прямоугольников:выделение .2.2.2. Корректность модели полной головной линейной редукцииКак и в случае HLR, определим функцию расширения состояний системы переходов exp до соответствующего лямбда-терма.

По сравнению с функцией расширения, определённой для системы переходов для HLR, новая функция расширения распространяется на ещё один случай — (2.20). А именно, этот случай обрабатывает ситуацию, при которой на вершине стека висячих аргументов оказалсясимвол разделитель.exp ⟨M [A]; Γ • (x 7→ (B, Γ′ )); ∆⟩ = exp ⟨M [A[x/B[Γ′ ]]]; Γ; ∆⟩(2.18)exp ⟨MB [A]; [ ]; (B,Γ′ ) : ∆⟩ = exp ⟨MB[Γ′ ] [A]; [ ]; ∆⟩(2.19)exp ⟨MB [A]; [ ]; $ : ∆⟩ = exp ⟨MB [A]; [ ]; ∆⟩exp ⟨M ; [ ]; [ ]⟩ = M ′(2.20)(2.21)Здесь B[Γ′ ] = exp ⟨B; Γ′ ; [ ]⟩, а M ′ получается из M удалением вычеркнутыхвершин.Начальное состояние⟨ A[A]; [ ]; [ ] ⟩Конечное состояние⟨ A[x]; Γ; [ ] ⟩⟨ []⟩Ae@e;Γ;∆12⟨⟩A [λx.e] ; Γ; $ : ∆Правила⟨ [переходов]⟩−→ ⟨A e1 @e2 ; Γ; (e2 , Γ):∆[App]⟩−→A [λx.e] ; Γ; $ : ∆[Lam-Non-Elim]⟨[]⟩′Z⟨A [λx.e] ; Γ; (B, Γ′ ) : ∆⟩−→ Aλx.e[Lam-Elim]Z ; (x 7→ (B, Γ )) : Γ; ∆B Z′′⟨A [x] ; [.

. . , (x 7→ (B, Γ )), . . . ]; ∆⟩ −→ ⟨A [B] ; Γ ; ∆⟩[BVar]−→ ⟨A [M [x]@B] ; Γ′ ; $ : ∆⟩,[F V ar − 0]⟨A [M [x] @B] ; Γ; (B, Γ′ ) : $ : ∆⟩x∈/ dom(Γ)NB: здесь B, как и во всех [FVar-*] правилах, является компонентом списка висячих аргументов.Более того, B должен быть аргументом некоторого вышестоящего в контексте A применения.⟨A [M [x] @B] ; Γ; (B, Γ′ ) : C : ∆⟩−→ ⟨A [M [x]@B] ; Γ′ ; $ : C : ∆⟩,[F V ar − 1]C ̸= $, x ∈/ dom(Γ)′′⟨A [M [x] @B] ; Γ; $ : (B, Γ ) : ∆⟩−→ ⟨A [M [x] @B] ; Γ ; ∆1 ⟩,[F V ar − 2]{∆, если ∆ = $ : ∆2x∈/ dom(Γ), ∆1 =$ : ∆, иначеСостояние⟨A[B]; Γ; ∆⟩ОбозначенияA[B]λ-терм с выделенным поддеревом BΓ := (var 7→ (t, Γ1 )) : Γокружение (список)∆ := (t, Γ) : ∆стек висячих аргументов[]пустой список либо пустой стек$символ-разделитель44Рисунок 13.

Система переходов для полной головной линейной редукцииТеорема 3. Полная головная линейная редукция завершается тогда и только то-гда, когда терм имеет нормальную форму. Более того, если M — некоторый терм,sf inal := ⟨M ′ ; Γ′ ; ∆′ ⟩ — конечное состояние системы переходов полной головнойлинейной редукции для терма M , и Mexp — расширение состояния sf inal , тогда:45– Mexp есть M ′ за исключением вычеркнутых поддеревьев;– Mexp не содержит редексов;– Mexp является нормальной формой терма M .Доказательство.

Заметим, что правила [FVar-*] не могут изменить расширениесостояния системы переходов. Следовательно, доказательство корректности полной головной линейной редукции является прямым следствием корректности головной линейной редукции (см. следствия к теореме 2). Это значит, полная головная линейная редукция завершается тогда и только тогда, когда завершается полная головная редукция терма, что, в свою очередь, эквивалентно конечности дерева Бёма, представляющего входной терм, а значит эквивалентно и существованиюнормальной формы входного терма.

Иными словами, полная головная линейнаяредукция завершается тогда и только тогда, когда у входного терма существуетнормальная форма.■46Глава 3Алгоритм трассирующейнормализации длянетипизированноголямбда-исчисленияВ главе представлен разработанный автором алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления. Алгоритм согласован снормальным порядком редукций и нормализует произвольный лямбда-терм, нормальная форма которого существует. Вместо изменения термов по правилам βредукции алгоритм строит обход абстрактного синтаксического дерева терма,оставляя сам терм неизменным.Определение.

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

Даная глава завершается примером работы алгоритмы трассирующей нормализации на терме mul ⃗2 ⃗2 = ⃗2(⃗2S)Z.473.1. Семантика, основанная на подстановкеПо определению (см. главу 1), терм находится в нормальной форме тогда итолько тогда, когда он не содержит редексов — подвыражений вида e1 @e2 , гдеe1 ≡ λx.e. Стандартная процедура нормализации сначала редуцирует выражениеe1 до функциональной абстракции, используя слабую редукцию, а затем применяет аксиому β-редукции. Семантика слабой редукции [86] приведена на рисунке 14.wnfwnfx ⇓ xλx.e ⇓ λx.ewnfwnfwnfe1 ⇓ λx.e e[e2 /x] ⇓ e′ e1 ⇓ e′ ̸≡ λx.ewnfwnfe1 @e2 ⇓ e′e1 @e2 ⇓ e′1 @e2Рисунок 14.

Слабая редукцияСильная редукция (нормальный порядок), приводящая терм в нормальнуюформу, если и только если последняя существует, может быть представлена в виде правил, приведённых на рисунке 15 [86]. Эта процедура нормализации является эффективной редуцирующей стратегией (в терминологии [30]). Отметим, чтопроцедура snf не является хвосто-рекурсивной, и, кроме того, использует именапеременных во во время исполнения.wnfsnfe1 ⇓ λx.e e[e2 /x] ⇓ e′snfsnfx ⇓ xe1 @e2 ⇓ e′snfe1 ⇓ e1′ ̸≡ λx.e e1′ ⇓ e1′′ e2 ⇓ e′2e ⇓ esnfsnfwnf′λx.e ⇓ λx.e′snfsnfe1 @e2 ⇓ e′′1 @e′2Рисунок 15. Строгая редукция3.2.

Вычисление с окружениемОперация подстановки, используемая в разделе 3.1 для определения обеихстратегий редукции, как отмечалось в главе 1, является нетривиальной и дорого-48Домены:e ∈ ExpEEρ ∈ Envρ0α ∈ F lag=====λ − термыExp × EnvV ariable → EE ∪ {F ree}λx.F ree{T, F } (контекст применения)Семантические функции:R : Exp ⇀ EE[[ ]] : Exp → F lag → Env ⇀ EEСемантические равенства:R[[e]]= [[e]] F ρ0[[x]] α ρ= case ρ x of (e′ , ρ′ ) ⇒ [[e′ ]] α ρ′Free ⇒ (x, ρ0 )[[λx.e]] T ρ = (λx.e, ρ)[[λx.e]] F ρ = [[e]] F ρ[x 7→ F ree][[e1 @e2 ]] α ρ = let (e′1 , ρ′ ) = [[e1 ]] T ρ incase e′1 ofλx.e0 ⇒ [[e0 ]] α ρ′ [x 7→ (e2 , ρ)]v⇒ [[e2 ]] F ρРисунок 16.

Строгая редукция, основанная на окружениистоящей. Стандартным приёмом является использование окружений, вместо явной подстановки. На рисунке 16 приведена семантика строгой редукции лямбдаисчисления, основанная на вычислении с окружением. [[_]] обозначает семантическую функцию, ρ — окружение, а A ⇀ B — частичную функцию, областьюопределения которой является домен A, а областью значений — домен B.Аргумент α (контекст применения) является логическим флагом, значение которого равно T в случае слабой редукции и F в случае строгой.Следует отметить, что семантика, приведённая на рисунке 16 завершается тогда и только тогда, когда нормальная форма терма существует.

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

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