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

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

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

Для краткости инаглядности изложения, она симулирует все шаги вычислений, не возвращая реального результата. Для построения нормальной формы необходимо преобразовать результат (e, ρ) в лямбда-терм, раскрывая окружения и производя переименование переменных в случае необходимости.49Домены:e ∈ ExpEEρ ∈ Envρ0α ∈ F lagk∈K======∪λ − термыExp × EnvV ariable ⇀ EE ∪ {F ree}λx.F ree{T, F }(контекст применения){⟨Kend⟩}(продолжения){⟨Kapp e α ρ k⟩ | e ∈ Exp, ρ ∈ Env, k ∈ K}Семантические функции:R:Exp ⇀ {Succeed}[[ ]] : Exp → F lag → Env → K ⇀ {Succeed}apk : Exp → K → Env ⇀ {Succeed}Семантические равенства:R[[e]]= [[e]] F ρ0 ⟨Kend⟩[[x]] α ρ k= case ρ x of Free ⇒ apk x k ρ0(e′ , ρ′ ) ⇒ [[e′ ]] α ρ′ k[[e1 @e2 ]] α ρ =k [[e1 ]] T ρ ⟨Kapp e2 α ρ k⟩[[λx.e]] F ρ k= [[e]] F ρ[x 7→ F ree] k′′[[λx.e]] T ρ ⟨Kapp e α ρ =k⟩[[e]] α ρ[x 7→ (e′ , ρ′ )] k[[λx.e]] T ρ ⟨Kend⟩= Succeedapk e ⟨Kend⟩ρ = Succeed′′apk e ⟨Kapp e α ρ k⟩ ρ = case e ofλx.e′′ ⇒ [[e′′ ]] α ρ[x 7→ (e′ , ρ′ )] k_⇒ [[e′ ]] F ρ′ kРисунок 17.

Строгая хвосто-рекурсивная редукцияПриведённая семантика обладает свойством полукомпозициональности. Этосвойство является важным для эффективной компиляции лямбда-термов в целевой код. Согласно терминологии из [93], функция [[_]] применяется только к аргументам, которые являются синтаксическими подвыражениями исходного терма, что означает, что семантическая переменная является таковой “со статическиограниченным множеством значений” (Bounded Static Variation) (см. раздел 5.3.2и [68]).503.3. Хвосто-рекурсивная семантикаСледующимшагомявляетсяпреобразованиесемантикивхвосто-рекурсивную.

Для этого необходимо устранить все вложенные вызовы семантической функции, что возможно произвести в два этапа. Первый шаг— введение дополнительной функции продолжения, на вызов которой будутзаменены все вложенные вызовы семантической функции. Затем, применяетсяподход дефункционализации по Рейнолдсу [59], позволяющий заменить функцию продолжения на структуру данных. На рисунке 17 приведён результатприменения вышеописанных шагов к семантике, приведённой на рисунке 16. Нарисунке 17 κ ∈ K является дефункционализированным продолжением, функцияapk применяет κ к выражению. Результатом семантической функции являетсялибо значение “Succeed”, если вычисления завершились, либо семантическаяфункция расходится, и нормальной формы у исходного терма не существует.Данная семантика является одновременно хвосто-рекурсивной и обладаетсвойством полукомпозициональности.

Таким образом, согласно правилам, приведённым на рисунке 17, семантическая функция, будучи применённой ко входномулямбда-терму M , произведут следующую последовательность вызовов:[[e1 ]]α1 ρ1 κ1 → [[e2 ]]α2 ρ2 κ2 → · · · → [[ei ]]αi ρi κi → . . . ,где ∀i.ei является подтермом терма M .3.4. Семантика, основанная на истории и окруженииСледующим преобразованием является замена продолжения κ на указательв историю h. Подобно хвосто-рекурсивной семантике, семантика, основанная наистории и окружении, осуществляет в процессе вычисления следующую последовательность вызовов:[[e1 ]]h1 → [[e2 ]]h2 → . . . → [[ei ]]hi → .

. . .История h является кумулятивным обходом, накапливающим последовательности вызовов семантических функций совместно с их аргументами. Каждая исто-51Домены:e ∈ ExpEEρ ∈ Envρ0α ∈ F lagh, ∈ H, ch ∈ CHit ∈ Item=======λ − ExpressionExp × EnvV ariable ⇀ EE ∪ {F ree}λx . F ree{T, F }[ Item ](История)⟨Exp F lag Env CH⟩Семантические функции:R : Exp ⇀ Heval : H ⇀ Hapk : Exp → Env → CH → H ⇀ HСемантические равенства:R[[e]] = eval [ ⟨ e F ρ0 [ ] ⟩ ]eval h = let it : _ = h in case it of⟨ x α ρ ch⟩ ⇒ apk x ρ0 ch hif ρ x = F ree′′⟨ x α ρ ch⟩ ⇒ eval ⟨e α ρ ch⟩ : h if ρ x = (e′ , ρ′ )⟨ λx.e T ρ ch⟩ ⇒ apk λx.e ρ ch h⟨ λx.e F ρ ch⟩ ⇒ eval ⟨e F ρ[x 7→ F ree] ch⟩ : h⟨e1 @e2 α ρ ch⟩ ⇒ eval ⟨e1 T ρ h⟩ : hapk e ρ ch h= case ch of[]⇒h′(⟨e1 @e2 α ρ0 ch ⟩ : _) ⇒ eval (f e) : hwheref (λx.e0 ) = ⟨e0 α ρ[x 7→ (e2 , ρ)] ch′ ⟩f e= ⟨e2 F ρ0 ch′ ⟩Рисунок 18.

Семантика, основанная на истории и окружениирия hi представляет собой список, элементами которого являются вызовами семантической функции [[ej ]], где j = 1, . . . ,i. ∀i > 0 элемент истории hi имеет следующий вид: hi = ⟨ei αi ρi chi ⟩ : hi−1 , где chi представляет κi .Суть рассматриваемого преобразования заключается в замене окружения изхвосто-рекурсивной семантики на структуру данных ⟨(Kapp e2 ) α ρ k⟩ на момент52времени ti , в который это продолжение было создано. Время ti представляетсяуказателем на соответствующий компонент chi , являющийся головой истории hi .Семантика, основанная на истории и окружении, отличается от хвосторекурсивной семантики тем, что, во-первых, история явно представляется кумулятивной записью, во-вторых, каждое значение κi ∈ K заменяется на историюуправления chi , являющуюся префиксом текущей истории, т.е.

указателем на ранний её элемент. Наконец, семантика, основанная на истории, не создаёт структур,представляющих продолжения, поскольку информация о продолжении содержится в каждом элементе истории ⟨e α ρ ch⟩. Семантика, основанная на истории иокружении, приведена на рисунке 18.3.5. Алгоритм трассирующей нормализации длянетипизированноголямбда-исчисленияилисемантика, основанная только на историиЗаключительным шагом является преобразование окружения в историю, являющуюся префиксом текущей истории и обозначаемую bh.

Появляется новая семантическая функция lookup, реализующая ту же функциональность, что и окружение ρ, путём поиска соответствующего значения в текущей истории bh. В данной главе предполагается, что входной лямбда-терм снабжён индексами де Брауна. Как правило, индексы де Брауна используются вместо имён переменных. Дляудобства изложения и компактности графического представления мы будем считать, что переменные представлены и их именами, и индексами одновременно.

Аименно, индексы де Брауна будут использоваться в определении семантическихравенств, в то время как имена переменных будут использоваться для обозначения переменных в текущем обходе.Алгоритм трассирующей нормализации приведён на рисунке 19. BV x i обозначает вождение связанной переменной xс индексом де Брауна, равным i, а F V xобозначает свободное вхождение переменной x.53Домены:e ∈ Expα ∈ F lagh ∈ H, ch ∈ CH, bh ∈ BHit ∈ ItemСемантические функции:Revalevoperandapklookup:::::====λ − Expression{T, F }[Item](История)⟨Exp F lag BH CH⟩Exp ⇀ HH⇀HItem → H ⇀ HExp → CH → H ⇀ HInt → F lag → BH → CH → H ⇀ HСемантические равенства:R[[e]] = eval [ ⟨e F [ ] [ ]⟩ ]eval h= let it : _ = h in case it of⟨ (F V x) α bh ch ⟩ ⇒ apk (F V x) ch h⟨ (BV x i)α bh ch ⟩ ⇒ lookup i α bh ch h⟨ λx.e T bh ch ⟩ ⇒ apk λx.e ch h⟨ λx.e F bh ch ⟩ ⇒ eval ⟨e F bh ch⟩ : h⟨ e1 @e2 α bh ch ⟩ ⇒ eval ⟨e1 T bh h ⟩ : hlookup 0 α(⟨_ T _ ch′ ⟩ : _) ch h = case ch′ of⟨e _ bh _⟩ : _ ⇒ evoperand ⟨e α bh ch⟩ h_ ⇒ case ch of[]⇒ h⟨ap _ bh′′ ch′′ ⟩ : _ ⇒ evoperand ⟨ap F bh′′ ch′′ ⟩ hlookup 0 _ (⟨_ F _ ch′ ⟩ : h′ ) ch h = apk (BV _ 0) ch hlookup i α (⟨_ _ bh′ _⟩ : _) ch h = lookup (i − 1) α bh′ ch hapk _ [ ] h = hapk λx.e(⟨_ α _ ch⟩ : _) h = eval ⟨e α h ch⟩ : hapk _ (⟨e α bh ch⟩ : _) h = evoperand ⟨e F bh ch⟩ hevoperand ⟨e1 @e2 α bh ch⟩ h = eval ⟨e2 α bh ch⟩ : hРисунок 19.

Алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления54@1@2Z@7λs1λz1λs2@3λz2s1@4s1S@5z1s2@6s2z2Рисунок 20. АСД терма mul ⃗2 ⃗2ПримерПриведём пример работы алгоритма трассирующей нормализации на терме mul ⃗2 ⃗2 = ((λs1 .λz1 .s1 @3 (s1 @4 z1 ))@2 ((λs2 .λz2 .s2 @5 (s2 @6 z2 ))@7 S))@1 Z, абстрактное синтаксическое дерево разбора которого приведено на рисунке 20. Обход представляет собой историю, каждый элемент которой может быть снабжёндвумя видами указателей: ch для история управления и bh для истории связываний переменных.

На диаграммах, представляющих обходы, bh изображается зелёным указателем под обходом, а ch красным указателем над ним же. Токен выделенподчёркиванием, если его флаг α имеет значение T . Начальным состоянием (исходной историей h0 ) является корень абстрактного синтаксического дерева входного терма с пустым множеством указателей, h = @1 .Первые два шага алгоритма похожи друг на друга: к текущему состоянию применяется функция eval, следующая по самому левому пути в абстрактном синтаксическом дереве терма, bh не изменяется (остаётся пустым), а ch выставляетсяравным текущей истории.@1 @2 λs1Следующие два шага также похожи: два токена–абстракции связываются ссоответствующими токенами–применениями посредством указателя ch, образуятем самым спинальные редексы.

Получается, что функция применения продол-55жения, apk, вызывается в обоих случаях. Функция apk расширяет текущий обход,снабжая новые токены указателями истории связывания, выставленными на самый поздний токен-абстракцию. Вершина bh снимается, а функция eval вызывается с не изменённым флагом α.@1 @2 λs1 λz1 @3Далее алгоритм выполняет шаг, аналогичных первым двум, после чего последним токеном становится токен–переменная s1.

Эта переменная является связанной, а соответствующая ей абстракция может быть найдена в истории по цепочке указателей bh, что и достигается посредством вызова функции lookup. Результатом вызова функции lookup будет токен @7 , являющийся аргументом спинального редекса, образованного абстракцией λs1 и применением @2 (абстракция образует спинальный редекс, если она связана указателем ch с токеном–применением). После этого функция eval вызывается с аргументом @7 .@1 @2 λs1 λz1 @3 s1 @7Следующим шагом построения обхода, заслуживающим внимания, являетсядвенадцатый шаг. На этом шаге функция eval вызывает функцию lookup на аргументах h1..12 S.

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

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