Диссертация (1150902), страница 14
Текст из файла (страница 14)
По определению,каждая переменная, зависящая от других динамических переменных, также классифицируется как динамическая. Таким образом, обход (т.е. история h с рисунка 19) также является динамическим. Также как динамические классифицируютсяи все значения, получаемые на основе обхода, например, его размер.Все рекурсивные вызовы функций в UNP, аргументами и результатом которых не являются подвыражения исходного лямбда-терма M , также классифицируются как динамические. Такой подход, возможно, не является наиболее точнымс точки зрения результата специализации, но является общепринятым (см.
[68])и безопасным — он позволяет избежать зацикливания процесса специализациииз-за бесконечного раскрытия вызовов функций. Все остальные вызовы функцийраскрываются в процессе специализации.Результат анализа времени связывания алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления приведён на рисунке 26. В “коробочки” (прямоугольники,как статическая, например:) заключена вся информация, классифицируемая79– Exp обозначает статический тип Exp;– Для каждой связанной переменной lookup i α обозначает остаточный вызов функции, который может быть специализирован для любых значенийстатических переменных i и α; например, для i = 2 и α = T остаточнымвызовом будет lookup2,T bh ch h;– При вызове функции lookup выражение i − 1 является статическим, а рекурсивные вызовы lookup i α внутри функции lookup являются статическими вызовами функции с двумя статическими переменными; эти вызовыбудут раскрыты во время специализации.Пусть функция f имеет тип D1 → D2 → · · · → Di → Di+1 → · · · → Dn , где n— общее число аргументов, а i — количество статических аргументов функцииf .
В таком случае тип функции f будет аннотирован следующим образом:f : D1 → . . . Di → Di+1 → . . . → Dn .Заметим, что у функций алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления статические параметры всегда образуют некоторыйпрефикс списка всех параметров функции.В телах определений функций статические вызовы вида f e1 . . . em будут также заключены в прямоугольники, например f e1 . . . em . Если такой вызов функции является ещё и остаточным, то вдобавок к выделению прямоугольником онбудет подчёркнут, например, f e1 . . .
em . В случае, если вызов заключён в прямоугольник, но не подчёркнут, он будет раскрыт частичным вычислителем во время специализации.На рисунке 26 приведена аннотированная версия алгоритма трассирующейнормализации для нетипизированного лямбда-исчисления. Помимо аннотациикода, приведенная версия содержит ещё одно изменение для лучшего разделения времён связывания — тип истории H развёртывается, а тип Item местамиразбивается на компоненты. До аннотации функция eval имела тип H ⇀ H, гдеH = [Item].
Ниже приведено вышеописанное преобразование типа функции eval80по шагам:eval : H ⇀ Hза шаг развёртки типа Heval : (Item : H) ⇀ Hприменяя каррированиеeval : Item → H ⇀ Hразбивая тип Item на компонентыeval : Exp → F lag → BH → CH → H ⇀ HПодобное преобразование позволяет отделить аргументы, классифицируемые какстатические, т.е. e и α, от остальных, динамических, аргументов функции.
Заметим, что история H всегда является непустым списком, поэтому вышеописанноепреобразование является корректным и не требует отдельного рассмотрения случая H = [ ].Приведённая на рисунке 26 аннотированная версия UNP не содержит средисемантических равенств функции evaloperand.
Аргументы этой функции возникают из истории, которая является динамическим параметром, и поэтому должны классифицироваться как динамические. Тем не менее, аргумент e является аргументом со статически ограниченным множеством значений, а именно,он является подвыражением исходного лямбда-терма M .
Поэтому к функцииmevaloperand применяется “The Trick”. Пусть e11 @e12 , . . . , em1 @e2 — список всехсинтаксических применений лямбда-термов терма M . На рисунке 27 приведёнрезультат применения “The Trick” к функции evaloperand и статическому аргументу e.evoperand e11 @e12 α bh ch h =eval e12 α bh ch (⟨e12 α bh ch⟩ : h)...mevoperand em1 @e2 αbh ch h =meval em2 α bh ch (⟨e2 α bh ch⟩ : h)Рисунок 27. Результат применения “The Trick” к функции evaloperand истатическому аргументу e81>hf_gue ∈ Exp= λ − \ujZ`_gb_α ∈ F lag= {T, F }h ∈ H, ch ∈ CH, bh ∈ BHit ∈ Item= [Item](Bklhjby)= hExp F lag BH CHiK_fZglbq_kdb_ nmgdpbbtraversal: Exp ⇀ Heval:Exp → F lag → BH → CH → H ⇀ Hapk:Exp → CH → H ⇀ Hevoperand:lookup:Exp → F lag → H → H → H ⇀ HInt → F lag → BH → CH → H ⇀ HK_fZglbq_kdb_ jZ\_gkl\Z :(M ² \oh^ghc λ l_jf )traversal = HYDO M F [ ] [ ] [ hM F [ ] [ ]i ]HYDO (F V x) B B ch h = apk (F V x) ch hHYDO (BV x i) α bh ch h = lookup i α bh ch hHYDOλx.eT bh ch h = apk λx.e ch hHYDOλx.eF bh ch h = HYDO e F bh ch he F bh chi : hHYDO (e1 #e2 ) α bh ch h = HYDO e1 T bh ch he1 T bh chi : hapk B[]h=hapk λx.e (hB α bh ch′ i : B) h = HYDO e h ch′ he α h ch′ i : hapk B(he α bh ch′ i : B) h = HYRSHUDQG e F bh ch′ hlookup 0 α (hB T B ch′ i : B) ch h = FDVH ch′ RIhe B bh Bi : B⇒ evoperand e α bh ch hB⇒FDVH ch RI[]⇒ h′′′′hap B bh ch i : B ⇒ evoperand ap F bh′′ ch′′ i hlookup 0 B (hB F B ch′ i : h′ ) ch h = apk (BV B 0) ch hlookup i α (hB B bh′ Bi : B) ch h = lookup (i − 1) α bh′ ch hРисунок 26.
Аннотированная версия алгоритма трассирующей нормализациидля нетипизированного лямбда-исчисления82Таким образом, специализированная программа U N PM будет содержатьстолько специализированных версий функции evaloperand, сколько операцийсинтаксического применения термов встречается в исходном терме M . Соответствующим образом аннотированная версия функции evaloperand приведена нарисунке 28.evoperand e α bh ch h = f M e wheref (e′ : es) e = case e′ ofe1 @e2 ⇒ if e = e′ then eval e2 α bh ch helse f es e_ ⇒ f es eРисунок 28. Аннотированная версия функции evaloperandРезультат специализация UNP на входной лямбда-терм.Как было описано впредыдущих разделах, при наличии самоприменимого частичного вычислителяна основе интерпретатора языка программирования возможно автоматически сгенерировать его компилятор.
Интерпретатором в данном случае является процедура трассирующей нормализации для нетипизированного лямбда-исчисления, реализованная на языке Haskell. Одним из распространённых способов достиженияэффекта специализации является использование генерирующих расширений вместо частичного вычислителя [65, 68, 98–100]. Именно этот подход и был использован для компиляции лямбда-термов в низкоуровневое представление, LLL. Поскольку алгоритм трассирующей нормализации для нетипизированного лямбдаисчисления был реализован на языке Haskell, то LLL является крошечным подмножеством этого языка, эквивалентным по своей выразительной силе языку Fиз [2].Результат специализации процедуры трассирующей нормализации на термmul ⃗2 ⃗2 приведён на рисунке 29. Каждая специализированная версия алгоритма трассирующей нормализации на некоторый входной терм M , U N PM , содержит множество операторов apply, bind, getV , .
. . , которые не зависят от входного терма. Эти функции манипулируют списками указателей висячих аргументов ch и динамических связываний bh. Они могут быть рассмотрены как встроенные операторы языка LLL. Заметим, что в общем случае размер обхода лямбда-83mul ⃗2 ⃗2 =(λm.λn.λS.λZ.m@2 (n@3 S)@1 Z)@01 (λs1 .λz1 .s1 @4 (s1 @5 z1 ))@02 (λs2 .λz2 .s2 @6 (s2 @7 z2 )а) Терм mul ⃗2 ⃗2mullmlnlSlZ@1@2@3ZSnm============lmbind lnbind lSbind lZb i n d @1a p p l y @2 Za p p l y m @3apply n SgetV 0getV 1getV 2getV 3ls1lz1@4s1@5z1ls2lz2@6s2@7z2============bind lz1b i n d @4apply s1getV 1apply s1getV 0bind lz2b i n d @6apply s2getV 1apply s2getV 0@5z1@7z2б) Результат компиляции терма mul ⃗2 ⃗2 в LLLРисунок 29.
Результат компиляции программытерма M может быть сильно больше его размера [101]. Тем не менее, используя частичные вычисления, результат специализации U N PM будет иметь размер|U N PM | = O(|M |). Иными словами, результат компиляции терма M в LLL имеетразмер, линейно зависящий от размера самого терма M . Исполнение скомпилированной программы с рисунка 29 приведено в приложении А.84Глава 6Трассирующая нормализацияи стратегии вычисленийСложность вычислений в лямбда-исчислении напрямую зависит от выбранной стратегии редукции.
Основные стратегии вычислений были описаны в разедле 1.3. Алгоритм трассирующей нормализации для нетипизированного лямбдаисчисления в той форме, в которой он был разработан и представлен в разедле 3.5,соответствует стратегии нормального порядка редукции. Стратегия нормальногопорядка редукции, также как и стратегия вызова по имени, часто проделывает одну и ту же работу несколько раз [102]. В этой главе мы покажем, как алгоритмтрассирующей нормализации может быть адаптирован для стратегии аппликативного порядка редукции, а также покажем, как семантика некоторых распространённых функциональных конструкции может быть представлена с помощьюподхода трассирующей нормализация на примере языка PCF.Заметим, что трассирующая нормализация может быть также адаптирована идля иных стратегий вычислений.
Так например, в разделе 6.2 описываются особенности адаптации алгоритма трассирующей нормализации для стратегии вызова по значению. Схожим образом27 трассирующая нормализация может бытьопределена и для стратегии вызова по необходимости.27Для этого потребуется распространить определение обобщённого связывающего указателя с целью перемещениявычисления значения аргументов в место первого вхождения соответствующей связанной переменной.856.1.
Алгоритм трассирующей нормализации, соответствующий аппликативному порядку редукцииПри аппликативном порядке редукции, также как и при стратегии вызова позначению, редукция функционального аргумента каждого применения редуцируется до абстракции, после чего происходит редукция аргумента, значение которого сохраняется и не перевычисляется в дальнейшем, даже при неоднократномиспользовании. Более того, результатом вычисления аргумента может быть терм,который уже не является подтермом исходного терма. Таким образом, для адаптации алгоритма трассирующей нормализации к аппликативному порядку редукции необходимо сохранять значения в обходе и переиспользовать их в случаенеобходимости.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
