Диссертация (1150902), страница 16
Текст из файла (страница 16)
Как консеквент применения этого правила может бытьсформировано новое выражение e′1 @e′2 , не являющееся подвыражением термаантецедента e′1 @e′2 . Тем не менее, известно, что семантика вызова по значению,в отличие от семантики аппликативного порядка редукции, в некоторых случаяхобладает свойством полукомпозициональности [102, 106].Теорема 6. Семантика вызова по значению для замкнутых30 строго нормализируемых термов является полукомпозицональной.Доказательство. Теорема может быть доказана индукцией по глубине деревавывода. Для случаев BVar, FVar, Lam и App − L утверждение теоремы следуетao⇓ означает шаг редукции согласно стратегии аппликативного порядка редукции.Естественная семантика также известна как натуральная или семантика большого шага (Natural Semantics, Big-StepSemantics, детали см.
в [31, 83, 103–105]).282930cbv⇓ означает шаг редукции согласно стратегии вызова по значению.Замкнутым называется лямбда-терм, не содержащий свободных переменных.92x ∈ D(ρ) e : ρ′ = ρ(x)aox:ρ⇓e:ρ′x ̸∈ D(ρ)BVaraox:ρ⇓x:ρaoe : ρ ⇓ e′ : ρ′ao′λx.e : ρ ⇓ λx.e : ρaoe1 : ρ′ ⇓ λx.e : ρ′′aoe : ρ′′ [x 7→ e′2 : ρ′′′ ] ⇓ e′ : ρ′′e1 @e2 : ρ ⇓ e : ρaoe1 : ρ ⇓ e′1 : ρ′′e′ ̸≡ λx.eaoe1 @e2 : ρ ⇓Lamaoe2 : ρ′′ ⇓ e′2 : ρ′′′ao′FVar′aoe2 : ρ′′ ⇓ e2′ : ρ′e′1 @e′2App − L:ρ′App − RРисунок 32.
Естественная семантика нетипизированного лямбда-исчисления,основанная на окружении и соответствующая аппликативному порядкуредукциинапрямую из индукционного предположения. Единственный случай, заслуживающий отдельного внимания, — случай App − R. Но применение этого правиланевозможно, если исходный терм замкнут. Базовым значением с точки зрения семантики вызова по значению является либо абстракция, что соответствует правилу App − L, либо переменная, окружение на которой не определено. Такая переменная может быть только свободной, поскольку если переменная является связанной, то либо её абстракция образует редекс, сохранённый в окружении, либосемантика вызова по значению рассматривает саму абстракцию как значение ине редуцирует её тело. Таким образом, единственное правило, нарушающее полукомпозициональность — App − R — неприменимо при редукции замкнутыхтермов.■Теорема 6 позволяет эффективно компилировать процедуру трассирующейнормализации для нетипизированного лямбда-исчисления, соответствующую семантике вызова по значению, для замкнутых лямбда-термов.
Отметим, что такаяверсия алгоритма трассирующей нормализации отличается от приведённой в разделе 6.1 лишь отсутствием правил, отвечающих за редукцию под абстракцией,указателя на текущий токен аргумента, а также правил следования этому указателю.936.3. ТрассирующаянормализациядляPCF-подобного языкаЛямбда-исчисление является одним из простейших Тьюринг-полных языков программирования. Тем не менее реализация даже простых функций может вызвать немало трудностей у программиста.
Например, все объекты лямбдаисчисления представляют собой термы, поэтому все данные должны быть закодированы в термы согласно некоторому заранее выбранному представлению, арезультат должен быть интерпретирован соответствующим образом. Далее мы покажем, как трассирующая нормализация может быть распространена на основныеязыковые конструкции языка типа PCF. Рассматриваемый далее язык являетсянадмножеством лямбда-исчисления, расширенного оператором потока управления if − then − else, комбинатором неподвижной точки Y , числовыми константами и бинарными операциями.Для обработки дополнительных языковых конструкций функция продолженияapk будет принимать ещё один аргумент.Сначала рассмотрим один из простейших случаев — числовую константу. Подобно случаю свободной переменной, её трассирующая семантика есть вызовфункции продолжения apk.Во-вторых, рассмотрим случай комбинатора неподвижной точки Y .
В процессе вычисления этот комбинатор раскрывает тело функции, обновляя окружение(связывающий указатель bh) и оставляя текущее продолжение ch неизменным.Функция lookup также претерпевает изменения: для имён функций она возвращает комбинатор неподвижной точки Y с исходным окружением, а для имён переменных действует прежним образом. Описанные изменения, очевидно, соответствуют классической семантике комбинатора неподвижной точки: [[Y M ]] =[[M (Y M )]].Оператор потока управления if − then − else также хорошо согласуется сподходом трассирующей нормализации: происходит вычисление тела условия доконстанты, а затем в функции применения окружения apk выбирается соответствующая ветвь вычислений.Наконец, рассмотрим случай бинарного оператора над значениями.
Дляпростоты ,мы рассмотрим только функцию сложения, трассирующая семан-94@ Y sum λx If x 1 + x 1 @ sum Y sum λx If x − x 1 1 0 0 1Рисунок 33. Обход терма sum 1тика остальных бинарных операторов определяется схожим образом. Существует несколько способов определить семантику бинарных операторов.Первый способ — “синтаксический сахар” над соответствующим лямбдатермом.
А именно, сложение может быть определено как псевдоним термаλm.λn.λx.(m@f )@((n@f )@x). В случае определения новых синтаксическихконструкций таким образом, трассирующая нормализация сохраняет все своисвойства, и в том числе, полукомпозициональность. С другой стороны, такой подход влечёт за собой неэффективность вычислений за счёт того, что результат вычислений не будет сохранён и будет каждый раз перевычисляться в процессе выполнения программы.
Другой способ определения трассирующей семантики бинарных операторов — сохрание (простых) значений в обходе подобно тому, какэто было сделано в случае аппликативного алгоритма трассирующей нормализации. В данном случае токен, представляющий простое значение (число), можетбыть динамическим, т.е. неизвестным на момент компиляции. Более того, мы позволим функции продолжения изменять аргумент бинарных операций в процессеисполнения, что сделает возможным сохранять промежуточные значения внутриобхода.
Заметим, что, сказанное выше применимо лишь для одиночных токеновзначений, представляющих числа, поэтому никаких дополнительных указателей,как в случае аппликативного порядка редукции, не требуется.Изменения по сравнению с трассирующей семантикой, представленной в разделе 3.5, приведены на рисунке 34. Обход функции sum(x) = Σxi=1 i, применённойк аргументу 1: Y sum (λx. if x then x + sum(x − 1) else 0) — приведён нарисунке 3331 .31Заметим, что Y sum является одним токеном, означающим вызов рекурсивной функции sum.95eval h = let ⟨ e bh α ch ⟩ : _ = h incase e of...Const n ⇒ apk ch e h αY f e1 ⇒ eval ⟨ e1 h α ch ⟩:hIf b e1 e2 ⇒ eval ⟨ b bh α ch ⟩:hAdd e1 e2 ⇒ eval ⟨ e1 bh T h ⟩:hapk ch e h α = case ch of...⟨ (If _ e1 e2 ) bh' α ch' ⟩ : _ ⇒if e == 0then eval ⟨ e2 bh' α ch' ⟩ : helse eval ⟨ e1 bh' α ch' ⟩ :⟨ (Add e1 e2 ) bh' α ch' ⟩ : ch'' ⇒let Const n = e in if αthen eval ⟨ e2 bh' F ⟨ (Add e e2 ) bh' α ch'): ch'' ⟩ ⟩ : helse let Const n1 = e1in eval ⟨ (Const (n1 + n)) bh' α ch' ⟩ : h⟨ (Pred _ e) bh' α ch' ⟩ : ch'' ⇒if e == 0then eval ⟨ e2 bh' F ch''' ⟩ : helse eval ⟨ (Const (e1 − e)) bh' α ch' ⟩ : hwhere ch''' = ⟨ (Sub e e2 ) bh α ch' ⟩ : ch''Рисунок 34.
Трассирующая семантика новых языковых конструкций96ЗаключениеВ ходе выполнения данной диссертационной работы был достигнуты следующие результаты.1. Разработан алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления, соответствующий нормальному порядку редукции.2. Представлена модель полной головной линейной редукции, являющаясярасширением известной модели головной линейной редукции. Предложенная модель формализована в виде системы переходов, доказана её корректность относительно головной редукции.3. Доказана корректность представленного алгоритма трассирующей нормализации относительно предложенной модели полной головной линейнойредукции путём его формализации в виде системы переходов и дальнейшей симуляции системы переходов для полной головной линейной редукции.
Таким образом, доказано, что процедура трассирующей нормализацииявляется нормализирующей.4. Предложенный алгоритм адаптирован для других, отличных от нормального порядка, стратегий вычислений: аппликативного порядка редукции ивызова по необходимости.5. Предложен новый метод компиляции функциональных языков программирования в низкоуровневое представление путём специализации представленного алгоритма трассирующей нормализации на входной терм.6. Разработана экспериментальная реализация алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления [107], а также ге-97нерирующего расширения, на ней основанного, для компиляции лямбдатермов в низкоуровневое представление, на языках Haskell и Racket.В качестве рекомендации по применению результатов работы в индустриии научных исследованиях указывается, что предложенный алгоритм трассирующей нормализации не преобразует исходный терм, а только посещает его в конечном числе точек, благодаря чему он успешно поддается специализации с помощью хорошо известных методов специализации программ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
