Диссертация (1150902), страница 15
Текст из файла (страница 15)
Также необходим некоторый новый способ ссылаться на токены значений аргументов в процессе переиспользования. Для этого будут введены↑↓дополнительные указатели, а также специальные символы i и i , обозначающиеначало и конец вычисления значения аргумента с уровнем вложенности i.Заметим, что обход может содержать множество избыточной информации, которая не является необходимой при повторном использовании агрумента. Например, спинальные редексы могут быть опущены, поскольку они не участвуют вформировании результата (и в том числе значений). Для итого, чтобы избавитьобход от излишней информации в тот момент, когда она более не является необходимой, вводится функция cleanup, вызываемая в момент окончания вычисленияочередного аргумента.
Понятие токена и обхода в случае аппликативного порядка усложняются.↓↑Определение. Токеном называется либо символ i , либо символ i , либо кортеж⟨e, ap, lp, bp, pp, underline, α⟩, где:– e — некоторая вершина абстрактного синтаксического дерева терма;– ap — указатель стека висячих аргументов (на диаграммах обозначаютсякрасными округлыми стрелками над обходом);86↑– lb — указатель на последнюю абстракцию перед последним токеном i (новый; на диаграммах обозначается фиолетовой ломаной стрелкой над обходом);– bp — связывающий указатель (на диаграммах изображается зелёной округлой стрелкой под обходом);– lb — указатель на текущий токен аргумента, при его использовании (новый;на диаграммах обозначается чёрной ломаной стрелкой под обходом);– underline — логический флаг, имеющий значением “истина” (T rue), еслиi токен не будет участвовать в формировании результата (значения), “ложь”(F alse) — иначе;– α — логический флаг, имеющий значением “истина” (T rue) если, и толькоесли в текущий момент происходит вычисление некоторого аргумента;↑↓– i и i обозначают начало и конец вычисления значения аргумента соответственно, а i ∈ N указывает на уровень вложенности.На диаграммах ниже пунктирным указателем обозначается таковой, значениекоторого может быть равно nil.
Иными словами, наличие этого указателя у соответствующего токена не обязательно, но если соответствующий указатель всё жеприсутствует, то он должен быть согласован с пунктирным указателем.Определение. Обходом называется список токенов, первым токеном которого яв↑ляется 0 , а вторым — ⟨e, 0, 0, 0, 0, F alse, F aslse⟩, где e — корень абстрактного синтаксического дерева исходного терма. Оставшаяся часть обхода строится согласно нижеследующим правилам. Если ни одно из правил не может быть↓применено, то токен 0 добавляется в конец обхода, после чего вызывается функция cleanup, которая по данному обходу строит новый обход, являющийся обходом абстрактного синтаксического дерева нормальной формы исходного терма.Напомним, что стратегия аппликативного порядка редукции не является эффективной нормализирующей стратегией.
Иными словами, как и все алгоритмы нормализации, соответствующие стратегии аппликативного порядка редукции, алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления,87Применение. . . @1• (App-Tree). . . @1 e . . . @2 −→• (App-Argument)@1 =e_−→. . .
@1 e. . . @1 e . . . @2 eАбстракция↑@1 =_e. . . @1 . . . λx −→ . . . @1 . . . λx i e• (Lam-Elim-Tree)• (Lam-Elim-Argument)↑@1 =_e. . . @1 e . . . @2 . . . @3 . . . λx −→ . . . @1 e . . . @2 . . . @3 . . . λx i e. . . λx• (Lam-Non-Elim-Tree)λx=λx.e−→. . . λx e. . . λx e . . . λx −→ .
. . λx e … λx e• (Lam-Non-Elim-Argument)Связанная переменная↑• (BVar)↓. . . λx i e . . .i↑. . . x −→ . . . λx i e . . .↓i... x e. . . @ . . . x −→ . . . @ . . . x eРисунок 30. Правила переходов для случаев применения, абстракции исвязанной переменнойей соответствующий, может расходится на некоторых термах, нормальная формакоторых существует.Рассмотрим теперь новые правила построения обхода. Напомним, что после↓каждого добавления токена i в обход вызывается функция cleanup. Сами правила88Свободная переменная• (FVar-I)↑↑.
. . λx i. . . S −→ . . . λx i↓... S i e↑↑↓. . . @1 . . . @2 . . . λx i . . . S −→ . . . @1 . . . @2 . . . λx i . . . S i e↓• (Free-II)↓@2 =_e. . . S i . . . @1 . . . @2 . . . S −→ . . . S i . . . @1 . . . @2 . . . S e• (Free-III)↓↓. . . @1 e . . . S i . .
. @2 . . . @3 . . . S −→ . . . @1 e . . . S i . . . @2 . . . @3 . . . S e• (Free-IV)↓↑↓↑↓. . . λxe . . . S i . . . λx j . . . S −→ . . . λxe . . . S i . . . λx j . . . S j e↑↑↓. . . @1 . . . @2 . . . λx j . . . S −→ . . . @1 . . . @2 . . . λx j . . . S j e• (Free-V)↑...i↓... S e ...i↑. . . S −→ . . .i↓... S e ...i... S e. . . @1 . . . @2 . .
. S −→ . . . @1 . . . @2 . . . S• (Free-VI)@2 =_e. . . @1 . . . @2 . . . S −→ . . . @1 . . . @2 . . . SeeРисунок 31. Правила переходов для случая свободной переменнойпостроения обхода для стратегии аппликативного порядка редукции приведенына рисунках 30 и 31. Для удобства, иногда правила выставления новых указателейразделяются на два.В случае, если последним токеном обхода является токен-применение, то либоуказатель на текущий токен аргумента у этого токена равен nil, и в обход добав-89ляется непосредственный первый (левый) аргумент этого токена, либо, если указатель на текущий токен аргумента у него отличен от nil, обозначим последнийза e, то в обход добавляется новая копия токена e, а указатель на текущий токенаргумента у новой копии токена e выставляется на исходный токен e.Если текущим последним токеном обхода является токен-абстракция λx, тосуществует четыре возможных дальнейших варианта построения обхода. Еслиуказатель на текущий токен аргумента у токена @1 равен nil (см.
правило (Lam↓Elim-Tree) на рис. 30), то в обход добавляется токен i , где i является текущимуровнем вложенности, а непосредственно за ним добавляется и токен e, представляющий аргумент (правого ребёнка) применения @2 . Токены @1 и λx выделяются подчёркиванием, как образующие постой редекс. Если же у токена λx существует ненулевой указатель стека висячих аргументов, указывающий на токенприменение @3 , указатель на текущий токен аргумента у которого указывает нанекоторый ненулевой токен-применение @1 (см. правило (Lam-Elim-Argument)↓на рис.
30), то добавляются токены i и e, где e является токеном, следующим затокеном e1 в текущем обходе. Токены @3 и λx опять же выделяются подчёркиванием, как образующие постой редекс. Если же как указатель на текущий токенаргумента, так и указатель стека висячих аргументов у рассматриваемого токенаабстракции являются нулевыми, то в обход просто добавляется токен, представляющий тело абстракции (его непосредственного ребёнка в смысле АСД; см. правило (Lam-Non-Elim) на рис. 30). Наконец, если указатель на текущий токен аргумента у рассматриваемого токена-абстракции λx не равен nil, а указывает на некоторое другое вхождение токена λx в текущий обход, а также либо α(λx) = T rue,либо ap(λx) = nil, то в обход добавляется токен e, являющийся копией токена,следующего за этим вхождением токена λx, а также на него выставляется указатель на текущий токен аргумента у добавляемого в обход токена (см.
правило(Lam-Non-Elim-Argument) на рис. 30).В случае, если последним токеном текущего обхода является токен x, представляющий вхождение связанной переменной, то применяется правило (BVar),приведённое на рисунке 30. Заметим, что если токен вида λx недоступен по цепочке связывающих указателей из токена x, применяются правила для свободнойпеременной, приведённые на рисунке 31.90Наконец, если последний токен текущего обхода является токеном, представляющим свободную переменную (или такую связанную переменную, токенабстракция которой не найдена в цепочке связывающих указателей), то применяется одно из шести правил, приведённых на рисунке 31.
Неформально говоря, всеправила для свободной переменной отвечают за продолжение построения обходапо завершению построения под-обхода, соответствующего вычислению какогото аргумента, либо какой-то ветки абстрактного синтаксического дерева терма.Отметим, также предполагается, что у токена S в правиле (FVar-VI) указатель натекущий токен аргумента равен nil, а в правиле (FVar-I) помимо этого нулевымявляется ещё и указатель стека висячих аргументов.Функция cleanup сжимает обход, удаляя из него информацию, которая более непотребуется.
В действительности, функция cleanup удаляет из обхода все под↑↓чёркнутые токены, расположенный между последними парными токенами i и i ,↑↓вместе со всеми под-обходами, заключёнными между токенами j и j , включаяпоследние, для всех j > i. В результате, под-обход, заключённый между токенами↑↓i и i , образует обход абстрактного синтаксического дерева значения вычисляемого аргумента.Пример работы системы переходов для алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления, соответствующего аппликативному порядку редукции, приведён в приложении Б.6.2.
Об адаптации алгоритма трассирующей нормализации для стратегии вызова по значениюКак уже отмечалось в обзор области исследования (глава 1), стратегия вызова по значению является слабой версией стратегии аппликативного порядка редукции. Напомним, что под слабой слабой стратегией редукции подразумеваетсятакая стратегия, которая рассматривает абстракцию как значение и не редуцирует её тело. Семантика большого шага нетипизированного лямбда-исчисления, основанная на окружении и соответствующая аппликативному порядку редукции,91приведена на рисунке 3228 . Соответствующая семантика для стратегии вызова поaocbvзначению отличается лишь заменой всех ⇓ на ⇓ , а также правилом вычислениязначения абстракции — Lam.
Соответствующее правило для случая вызова позначению имеет ниже следующий вид29 .cbvLamλx.e : ρ ⇓ λx.e : ρЗаметим, что значением с точки зрения описанной семантики вызова по значению является терм в некотором окружении, e : ρ. Произведение всех необходимых подстановок согласно окружению ρ приведёт его к слабую нормальная формаисходного терма.Приведённые семантики большого шага для аппликативного порядка редукции и стратегии вызова по значению, основанные на семантике, не являются полукомпозициональными, в смысле определения из раздела 3.2.
Именно ввиду отсутствия полукомпозициональности и требуется такое количество дополнительныхнакладных расходов (указателей в историю) при определении алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления, соответствующего стратегии аппликативного порядка редукции, приведённого в предыдущем разделе.Свойство полукомпозициональности нарушается из-за правила App − R, приведённого на рисунке 32.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
