Диссертация (1150902), страница 3
Текст из файла (страница 3)
Джонсу (N. D. Jones)за создание условий для изучения данной темы и руководство на начальных этапах, Л. Онгу (L. Ong), С. А. Романенко, Н. Н. Непейводе и А. М. Миронову заценные вопросы и комментарии к работе, позволившие уточнить ряд формулировок и улучшить изложение результатов, научному руководителю Д. В. Кознову занеоценимый вклад в работу над диссертацией и помощь по ходу исследований,компании ООО “ИнтеллиДжей Лабс” и А.
Иванову за поддержку исследований.Отдельную благодарность хочется выразить моей семье, особенно маме, котораяявляется моей опорой и верным спутником на протяжении всей моей жизни.13Глава 1Обзор области исследованияВ данной главе рассмотрены существующие подходы к нормализации лямбдатермов и, в том числе, к трассирующей нормализации.
Описывается алгоритмытрассирующей нормализации для простого типизированного лямбда-исчисленияи безопасного лямбда-исчисления, предложенные Л. Онгом и В. Блюмом соответственно.1.1. Лямбда-исчислениеЛямбда-исчисление было предложено А. Чёрчем в 30-х годах 20 века. В1935 году С.
Клини и Д. Б. Россер установили противоречивость первой модели исчисления. Спустя непродолжительное время А. Чёрч предложил новую модель, известную сейчас как чистое, нетипизированное или беспитовое лямбдаисчисление. Спустя 4 года, в 1940, он создал первую модель типизированного исчисления, ныне известную как простое-типизированное лямбда-исчисление [4].В 1960-х годах была установлена связь между лямбда-исчислением и языкамипрограммирования, а само лямбда-исчисление стало одной из основных моделей вычислений наряду с машинами Тьюринга, моделью частично-рекурсивныхфункций, алгорифмами Маркова и Поста и другими.Объекты модели лямбда-исчисления, называемые лямбда-термам, строятся спомощью трёх синтаксических конструкций: переменной, функциональной абстракции по переменной, т.е.
анонимной функции, и применения одного лямбдатерма к другому — функции к аргументу. Формально, лямбда-выражением14(лямбда-термом, λ-термом или просто термом, λ-term) называется выражение,удовлетворяющее следующей грамматикеΛ1 ::= V | Λ@2 Λ | λV.λ,где V — множество конечных строк, называемых переменными, над некоторымфиксированным алфавитом Σ \ { , . , @, λ}, выражение вида λx.e называетсялямбда-абстракцией (или просто абстракцией, λ-abstraction) по переменной x,а выражение вида e1 @e23— применением (application) терма e1 к аргументу —терму e2 .Выделяют два вида вхождения переменной в терм: свободное и связанное.Связанными называются такие вхождения переменных, по которым уже былапроизведена абстракция в дереве синтаксического разбора терма, все остальные вхождения переменных называются свободными.
Так, например, в термеλy.x@y@(λx.x) первое вхождение переменной x является свободным, а второе— связанным, также как и единственное вхождение переменной y.Основной формой эквивалентности лямбда-термов является так называемаяα-эквивалентность (α-конверсия, α-coercion), согласно которой термы, получаемые друг из друга посредством переименования одной или нескольких связанных переменных, являются α-эквивалентными. Так, термы λx.x и λy.y — αэквивалентны. Отношение α-эквивалентности обозначается знаком ∼α , например, λx.x ∼α λy.y.
Как правило, термы в лямбда-исчислении рассматриваютсяс точностью до α-эквивалентности, поэтому вместо терминов связанное и свободное вхождение переменной часто используют термины связанная и свободнаяпеременная, соответственно, подразумевая, что различные вхождения одной и тойже переменной не могут быть и связанными, и свободными одновременно. Далее мы будем придерживаться соглашения Барендрегта (Barendregt’s convention),подразумевающего, что различные переменные имеют различные имена. Формальные определения множеств свободных (F V ) и связанных (BV ) переменныхприведены на рисунке 1.1Мы также будем использовать скобки (“(”, “)”) как незначащие символы грамматики в тех ситуациях, когда изконкретного синтаксиса невозможно однозначное восстановление абстрактного.2Символ @ иногда опускается: Λ@Λ ≡ Λ Λ ≡ ΛΛ.3Мы будем считать, что приоритет оператора “@” выше чем у “.”, т.е.
λx.x@y ≡ λx.(x@y), а ассоциативность уоператора “@” — левая, т.е. x@y@z = (x@y)@z.15Основной аксиомой лямбда-исчисления является аксиома β-редукции. котораяпроизводит применение функции (лямбда-абстракции) к её аргументу путём синтаксической замены всех вхождений переменной, связанной этой абстракцией, натело аргумента:(λx.e1 ) e2 =β e1 [x/e2 ].Такая замена называется подстановкой аргумента e1 в терм e2 , а выражение вида(λx.e1 ) e2 — редексом. Снабжённое аксиомой β-редукции лямбда-исчисление является полным по Тьюрингу, определяя тем самым одну из простейших моделейвычислений. Термы, получаемые друг из друга по правилу β-редукции, называются β-эквивалентными. Запись s →β t означает, что терм t получается из термаs за один шаг β-редукции, а запись s →∗β t означает, что терм t получается изтерма s за ноль или более шагов β-редукции.Заметим, что подстановка не является тривиальной операцией.
Например, рассмотрим терм (λx.x y) x. Согласно правилу α-эквивалентности он эквивалентентерму (λz.z y) x, который, в свою очередь, β-эквивалентен терму λz.z x. Если произвести подстановку [x/y] непосредственно в терме λx.x y, то результатом будеттерм λx.x x, который уже не эквивалентен терму λz.z x.Таким образом, для подстановки важно, чтобы свободные переменные терма не связывались при подстановке. Такая подстановка называется свободной отсвязывания (Capture-Avoiding Substitution), далее будем называть ее просто подстановкой. Формальное определение подстановки приведено на рисунке 1.В начале 70-х годов Н. де Брауном (N. de Bruijn4 ) была предложена нотация, получившая название представление де Брауна или неименованное представление [81], позволяющая полностью избавиться от имён в лямбда-термах:вхождения переменных заменяются натуральными числами, называемыми индексами де Брауна (de Bruijn indexes), а абстракции становятся анонимными.Таким образом, термы в представлении де Брауна представляют собой классыэквивалентности именованных лямбда-термов, факторизованных по правилу αэквивалентности.
Индекс де Брауна — это натуральное число, которое обозначает вхождение переменной; оно равно количеству абстракций между этим вхождением и абстракцией, связывающей переменную, включительно. Например, терм4В русскоязычной литературе также встречаются и другие варианты перевода этой фамилии: “де Брюйн”, “деБрейн”, “де Бройн”.16СинтаксисΛ ::= V | Λ @ Λ | λV.ΛV ::= {x, y, . . . }Подстановкаx[x/r] = ry[x/r] = y, если x ̸= y(e1 e2 )[x/r] = (e1 [x/r])(e2 [x/r])(λx.e)[x/r] = λx.e(λy.e)[x/r] = λy.e[x/r], если x ̸= y и y ̸∈ F V (r)β-редукция(λx.e1 ) e2 =β e1 [x/e2 ]Множество свободных переменныхF V (x) = {x}F V (λx.e) = F V (e) \ {x}F V (e1 e2 ) = F V (e1 ) ∪ F V (e2 )Рисунок 1.
Именованное представление чистого лямбда-исчисленияλx.λy.λz.x z (y z), известный как S комбинатор, в нотации де Брауна имеет следующий вид: λ λ λ 3 1 (2 1). Заметим, что в представлении де Брауна при осуществлении подстановки может потребоваться пересчёт индексов. Формальноеопределение неименованного представления чистого лямбда-исчисления приведено на рисунке 2.Ещё одно преобразование иногда считается стандартным для лямбдаисчисления — η-конверсия (эта–конверсия, η-conversion), отождествляющеефункцию и абстракцию этой функции, применённой к переменной, по которой осуществлена абстракция.
Преобразование функции f к виду λx.f x получило название η-расширения (η-expansion), а преобразование, ему обратное, —η-редукции (η-reduction). Определения η-расширения и η-редукции приведены нарисунке 3.17СинтаксисΛd ::= N | Λd Λd | λ ΛdСдвиг в Λd{k, k < c↑dc (k) =k + d, k ≥ cПодстановка в Λd{r, k = jk[j/r] =k, иначе↑dc (λ e) = λ ↑dc+1 (e)(λ e)[j/r] = λ e[j + 1/ ↑10 r](e1 e2 )[j/r] = e1 [j/r]e2 [j/r]↑dc (e1 e2 ) =↑dc (e1 ) ↑dc (e2 )β-редукция в Λd1(λ e1 )e2 →↑−10 (e1 [0/ ↑0 (e2 )])Множество связанных переменныхBV (x) = ∅BV (λx.e) = BV (e) ∪ {x}BV (e1 e2 ) = BV (e1 ) ∪ BV (e2 )α-эквивалентностьλx.e ∼α λy.e[x/y], если y ̸∈ F V (e)Рисунок 2.
Неименованное представление чистого лямбда-исчисленияη-конверсияf ∼η λx.f x, если x ̸∈ F V (f )α-эквивалентностьλx.e ∼α λy.e[x/y], если y ̸∈ F V (e)Рисунок 3. η-конверсия1.2. Простое типизированное лямбда-исчислениеПростое типизированное лямбда-исчисление (Simply-Typed Lambda-Calculus,STLC) имеет такой же синтаксис, как и бестиповое. Тем не менее, не все термыбестипового исчисления являются допустимыми (Valid) термами простого типизированного. Типы в простом типизированном лямбда-исчислении описываются следующей грамматикой: τ ::= ι | τ → τ , где ι представляет собой некоторый базовый тип (Graund Type), а τ1 → τ2 — функциональный тип (стрелочныйтип, Arrow Type), ассоциативность у оператора стрелка → правая. Принято вы-18СинтаксисТипизацияΛCu ::= Λx:τ ∈ΓΓ ⊢Cu x : τТипыτ ::= ι | τ → τКонтекстыΓ ::= ∅ | Γ, V : τΓ, x : τ ⊢Cu e : σΓ ⊢Cu λx.e : τ → σΓ ⊢Cu e1 : τ1 → τ2Γ ⊢Cu e2 : τ2Γ ⊢Cu e1 e2 : τ2Рисунок 4. Простое типизированное лямбда-исчисление в стиле Карриделять два похода, два стиля типизации: стиль Карри (типизация по Карри, á laCurry) и стиль Чёрча (типизация по Чёрчу, á la Church).
Эти два подходя являютсяпринципиально разными: при типизации по Карри сначала задаётся грамматикатермов — синтаксис, затем определяется их поведение — семантика, и наконецвводится система типов — типизация, отвергающая термы, обладающие нежелательным поведением, в то время как в стиле Чёрча типизация предшествует семантике5 [23, 31, 82–85]. Иными словами, при типизации по Чёрчу семантикой —смыслом — наделены исключительно правильно типизированные (Well-Formed,Well-Typed) термы, а типизация по Карри даёт возможность рассуждать о поведении лямбда-термов вне зависимости от того, являются ли они правильно типизированными или нет. Синтаксис и типизации по Чёрчу и по Карри простого типизированного лямбда-исчисления в виде правил вывода (inference rules) приведенына рисунках 5 и 4 соответственно.
Суждение вида Γ ⊢ Λ : τ называется термом вконтексте (Term-in-Context), где контекст типизации Γ (Typing Context) является множеством текущих предположений о типах термов.Одним из основных отличий двух систем типизации является свойство единственности типа.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
