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

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

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

Среди множества головных нормальных форм терма выделяют основную головную нормальную форму(Principal Head Normal Form, phnf), которая получается посредством головной редукции терма, записанного в виде (1), если редукция завершается.Деревом Бёма (Bëhm Tree) BT (M ) терма M называется дерево, которое строится по следующим правилам9Утверждение может быть легко доказано индукцией по структуре терма M .24xBT (I a xω(Ix)) = ωλf.fxffа) Конечное деревоBT (Y ) = BT (λf.(λx.f (xx))(λx.f (xx))) = . .

.aТерм I = λx.x является одиниз основных комбинторов исчисления комбинаторовб) Бесконечное деревоРисунок 6. Пример: деревья Бёма для термов, не имеющих нормальной формыBT (M ) :=ωλ⃗x.y BT (V1 ) . . . BT (Vn ), если M не имеет hnf, если phnf(M ) = λ⃗x.yV1 . . . VnКак уже отмечалось ранее, повторное применение головной редукции к аргументам головной нормальной формы нормализует терм.

Таким образом, еслитерм имеет нормальную форму, то дерево Бёма, представляющее этот терм, вычислимо и конечно, и наоборот [30,43,87]. Также отметим, что если терм нормальной формы не имеет, соответствующее ему дерево Бёма либо конечно, а процедура построения его следующего уровня расходится (см. рис. 6а)), либо являетсябесконечным (см. рис. 6б)).1.5. η-длинная форма термаη-длинной форма (η-long Form) терма получает путём его полного ηрасширения и заменой бинарного оператора применения на оператор длинного применения @long (Long Application). Заметим, что каждая переменная, непосредственным предком которой не является абстракция, также подлежит ηрасширению путём введения анонимной (Dummy) абстракции (x 7→ λ.x). Например, η-длинной формой терма λxι→ι→ι .x является терм λxι→ι→ι aι bι .x(λ.b)(λ.a).Заметим, что понятие η-длинной форм имеет смысл только в типизированном исчислении, т.к.

в нём η-расширение ограничено хотя бы размером типа терма, в товремя как в бестиповом случае η-расширять терм можно до бесконечности.25β-нормальной η-длинной является форма терма, не содержащая β-редексов,но являющаяся η-длинной. Например, β-нормальной η-длинной формой терма(λxι→ι .x) y является терм λaι . y (λ.a), η-редуцирующийся к терму y ι→ι , являющемуся, в свою очередь, нормальной формой исходного терма.Заметим, что абстрактный синтаксис, используемый в определении η-длиннойформы терма, отличается от стандартного абстрактного синтаксиса λ-исчисления,введённого в начале раздела 1.1.

А именно, он описывается нижеследующей грамматикой.τ1τp lfΛlfodd ::= λx1 . . . xp .ΛevenlflflflflfΛlfeven ::= x Λ1 odd . . . Λn odd | Λ0 odd @long Λ1 odd . . . Λm odd , где m ∈ N, n,p ∈ N0Иными словами, нечётные уровни в абстрактном синтаксическом дереве являются абстракциями по произвольному числу аргументов, а чётные — применением переменной к нулю или более аргументам, либо же применение другого ηдлинного терма к одному или более аргументам. Последнее применение получило название оператора длинного применения @long .Определение. Абстрактным синтаксическим деревом эта-длинной формы терма, АСД10 , называется Σ-помеченное дерево (Σ-Labelled Tree), гдеΣ ::=Λodd|{z}лямбда-вершины∪evenΛ| {z }другие вершины≡ {λξ⃗ : ξ⃗ ⊆ V ar} ∪ V ar ∪ {@Along : A ∈ T ypes}{z} ||{z}лямбда-вершиныдругие вершиныявляется ранжированным алфавитом таким, что ar(xA ) := ar(A), ar(λ⃗x) :=1, ar(@A ) := ar(A) + 1, V ar является бесконечным множеством переменных,T ypes ::= {τ : τ = o | τ → τ } — множество простых типов, ξ⃗ — вектор переменных, @Along — оператор длинного применения соответствующий типу A.

Попостроению в дереве эта-длинной формы вершинами нечётных уровней дереваявляются элементы множества Λodd , а элементами чётных уровней — элементымножества Λeven . Так, например, на рис. 7 приведено абстрактное синтаксическоедерево η-длинной формы терма mul ⃗2 ⃗2, которое задает умножение двух нумеролов Чёрча ⃗2 ≡ λs.λz.s@(s@z) в кодировке Чёрча.10Под аббревиатурой АСД мы будем понимать, в зависимости от контекста, как абстрактное синтаксическое деревоη-длинной формы терма, так и его стандартное абстрактное синтаксическое дерево.poλS o→oλs2o→oλz1oz2os2o→os1o→oλλs2o→o z2oλλs1o→o z1os1o→o@long((o→o)→o)→o→oλpoZoλλq o((o→o)→o)→(o→o)→o→o@longλS o→o Z o≡η−long λSZ.@long (λs1z1.s1(λ.s1(λ.z1)))(λq.@long (λs2z2.s2(λ.s2(λ.z2)))(λq.S(λP )))(λ.Z)mul ⃗2 ⃗2 ≡ λS.λZ.(((λs1.λz1.s1@(s1@z1))@((λs2.λz2.s2@(s2@z2))@S)))@Z26Рисунок 7.

Терм mul ⃗2 ⃗2, его η-длинная форма и её АСД1.6. Головная линейная редукцияКак уже отмечалось ранее, лямбда-исчисление в первую очередь представляет собой модель вычислений. Соответственно, закономерным является вопросо сложности (Complexity) вычислений в лямбда-исчислении. Иными словами,пусть дан некоторый терм и зафиксирована стратегия вычислений. Какова сложность вычислений (нормализации) данного терма? Простейшей мерой сложностивычисления является количество шагов β-редукции, необходимых для нормали-27Терм TxUVUVλx.UУсловиеλh (U ) = [ ]λh (U ) = λx : lСписок головных абстракций λh (T ) Список простых редексов pr(T )[][][]pr(U )l(λx, V ) : pr(U )λx : λh (U )pr(U )Рисунок 8. Определение списков головных абстракций и простых редексовзации терма. К сожалению, такой подход не соответствует сложности вычисленийна реальных вычислителях, поскольку сложность операции подстановки находится в нелинейной зависимости от длины терма.

Работы [13–15,88–90] представляют различные подходы к описанию сложности вычислений в лямбда-исчислениии определению оптимальных стратегий редукции, основанных на той или иноймере сложности вычислений. Одним из таких подходов является головная линейная редукция (Head Linear Reduction) [8, 9], когда на каждом шаге вместо обычных подстановок производятся так называемые линейные подстановки (LinearSubstitution) — подстановки только одного вхождения переменной в терм. В этомразделе мы рассмотрим классические определения головной линейной редукции,трассирующей нормализации, также обсудим связь между ними.1.6.1. Головная линейная редукция: классическое определениеДля формального определения понятия головной линейной редукции нам понадобится ввести некоторое количество дополнительных определений.

Хребетными или спинальными подтермами (Spine Sub-Terms) терма T называются самтерм T , а также все спинные подтермы терма U , если T = U V или T = λx.Uсоответственно. Заметим, что любой лямбда-терм имеет ровно один спинальныйподтерм-переменную. Такое вхождение переменной, так же как и сам подтерм,называется головным (Head Occurrence, hoc). Ещё два понятия: список головныхабстракций (Head λ List, λh (T )) и простые редексы (Prime Redexes) — определяются индукцией по структуре терма T .

Простой редекс представляет собой пару(λx, N ), первый и второй элементы которой называются абстракцией и аргументом простого редекса соответственно. Индуктивное определение списков простых редексов и головных абстракций приведены на рис. 8, где pr(T ) обозначаетсписок простых редексов терма T .28Редексом головного вхождения переменной (hoc Redex) терма T называетсяпростой редекс (λx, V ), где x является головной переменной, если такой редекссуществует.Головная линейная редукция линеаризует последовательность подстановокпутём замены на каждом шаге лишь одного вхождения переменной — головного,оставляя сам головной редекс нетронутым.

Если же он не определён, то головная линейная редукция завершается в так называемой псевдоголовной нормальнойформе (Quasi-Head-Normal Form, qhn).Пусть r = (λx, . . . ) и s = (λy, . . . ) — два простых редекса терма T . Говорят,что некоторый простой редекс r содержит другой простой редекс s, если λy является вершиной поддерева, непосредственным предком которого является вершинаλx. Более того, простые редексы r и s называются последовательными, если r содержит s, и не существует такого простого редекса t, который содержится в r, ноне содержится в s.Пример.Пусть T = λs.(λx.(λy.(λw.w@s)@y)@x)@(λz.z), тогдаλh (T ) = [λs]pr(T ) = [(λx, (λz.z)), (λy, x), (λz, y)] ⇌ [r, s, t]Пары простых редексов r и s, и s и t образуют последовательные простые редексы.Теорема 1.

Пусть N – произвольный терм, а терм M является результатом применения к нему головной линейной редукции. Тогда:1. M ≡β N ;2. Головная линейная редукция завершается тогда и только тогда, когда завершается головная редукция.Первое утверждение может быть показано индукцией по числу шагов головной линейной редукции.Что же касается второго утверждения, то его необходимость устанавливаетсяв силу того, что головная редукция терма N завершиться за число шагов, равноеколичеству простых редексов терма M . Действительно, никакая β-редукция терма M не способна произвести подстановку головного вхождения переменной, а29значит и не способна создать новый простой редекс.

Таким образом, терм имеет головную нормальную норму, что в свою очередь гарантирует завершаемостьголовной редукции [30].Тем не менее, доказать достаточность этого утверждения не так просто. Дляэтого мы введём формальное определение головной линейной редукции в видесистемы переходов, с помощью которой формально и докажем утверждение теоремы (см. раздел 2.1).1.6.2. Трассирующая нормализацияВ 70-ых годах 20 века Г.

Плоткин [5] сформулировал проблему построения полностью абстрактной модели вычислений (Fully Abstract Modelof Computations) для языка программирования вычислимых функций PCF(Programming Computable Functions), заключающуюся в построении абстрактноймодели языка, являющейся одновременно полной (Complete) — каждый терм языка представим в его модели — и согласованной (Sound) — каждый элемент абстрактной модели имеет прообраз в языке. Эта проблема была решена в начале 90-ых годов независимо двумя группами исследователей: М. Хуландом, Л.Онгом [39] и С. Абрамски, Г.

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

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