Лямбда исчисление

Автор: Пользователь скрыл имя, 18 Марта 2012 в 20:08, реферат

Описание работы

Функциональные языки программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в качестве теоретической основы и "минимального" функционального языка программирования.

Работа содержит 1 файл

Лямбда исчисление.docx

— 147.45 Кб (Скачать)

Определение 5   [Подстановка]:

[x ↦ s]x

=

s

[x ↦ s]y

=

y

если y ≠ x

[x ↦ s](λy.t1)

=

λy. [x ↦ s]t1

если y ≠ x и y ∉ FV(s)

[x ↦ s](tt2)

=

([x ↦ s]t1)   ([x ↦ s]t2)

 

Операционная семантика

Операционная  семантика лямбда-термов вкратце представлена на рис. 5.3. Множество значений в этом исчислении более интересно, чем было в случае арифметических выражений. Поскольку вычисление (с вызовом по значению) останавливается, когда достигает лямбды, значениями являются произвольные лямбда-термы.

 

→ (бестиповое)

 

 

 

 

Синтаксис

t

::= термы:

 

x переменная

 

λx.t абстракция

 

t t применение

   

v

::= значения:

 

λx.t значение-абстракция


Вычислениеt → t′t → t′

 

t→ t′1

 

tt→ t′t2


 

 

t→ t′2

 

vt→ vt′2


 

 

(λx.t12) v→ [x ↦ v2]t12


 

 

 

 

Figure 5.3: Бестиповое лямбда-исчисление (λ)


 

Отношение вычисления показано в правом столбце  рисунка. Как и в случае арифметических выражений, имеется два типа правил: рабочее правило E-AppAbs и правила соответствия E-App1 и E-App2.

Обратите  внимание, как выбор метапеременных в этих правилах помогает управлять  порядком вычислений. Поскольку vможет относиться только к значениям, левая сторона правила E-AppAbsсоответствует всем применениям термов, в которых терм-аргумент является значением. Точно так же, E-App1 относится к тем применениям, в которых левая часть не является значением, посколькуtможет обозначать любой терм, но предпосылка правила требует, чтобы tмог совершить шаг вычисления. Напротив, E-App2 не срабатывает, пока левая часть не станет значением, которое может быть обозначено метапеременной v. Совместно эти правила полностью определяют порядок вычисления терма вида tt2: сначала работает E-App1, пока tне сведется к значению, затем E-App2применяется до тех пор, пока tне окажется значением, и, наконец, само правило E-AppAbs производит само применение.

Упражнение 6   [★★]: 
Модифицируйте эти правила так, чтобы описать три другие стратегии вычисления: полную бета-редукцию, нормальный порядок и ленивое вычисление.

Заметим, что в чистом лямбда-исчислении единственные возможные значения — это лямбда-абстракции, так что, если E-App1 доводит tдо значения, это значение должно быть лямбда-абстракцией. Разумеется, это утверждение перестает быть справедливым, как только мы добавляем в язык другие конструкции, скажем, элементарные булевские значения, поскольку при этом у нас появляются новые виды значений.

Упражнение 7   [★★,↛]: 
В упражнении 16 дается альтернативное представление операционной семантики булевских и арифметических выражений, в котором тупиковые термы дают при вычислении особую константуwrong. Распространите эту семантику на λNB.

Упражнение 8   [★★]: 
В упражнении 17 вводится стиль вычисления арифметических выражений <<с большим шагом>>, в котором базовое отношение вычисления означает <<терм t при вычислении дает окончательный результат v>>. Покажите, как сформулировать правила вычисления лямбда-термов в этом стиле.

5.4  Дополнительные замечания

Бестиповое  лямбда-исчисление было разработано  Чёрчем и его коллегами в 20-е  и 30-е годы (Church, 1941). Основополагающий труд по всем вопросам бестипового лямбда-исчисления — книга Барендрегта (Barendregt, 1984); работа Хиндли и Селдина (Hindley and Seldin, 1986) уже по охвату, но легче для чтения. Статья Барендрегта (Barendregt, 1990) в <<Справочнике по теоретической информатике>> представляет собой краткий обзор. Сведения о лямбда-исчислении можно найти также во множестве учебников по функциональным языкам программирования (Abelson and Sussman, 1985, Friedman, Wand, and Haynes, 2001, Peyton Jones and Lester, 1992) и по семантике языков программирования (напр., Schmidt, 1986, Gunter, 1992, Winskel, 1993, Mitchell, 1996). Систематический метод кодирования различных структур данных в виде лямбда-термов описан в статье Бёма и Берардуччи (Böhm and Berarducci, 1985).

Несмотря  на название, Карри не считал себя автором  идеи каррирования. Её открытие обычно приписывают Шёнфинкелю (Schönfinkel, 1924), однако основная идея еще в XIX веке была известна некоторым математикам, в том числе Фреге и Кантору.

Возможно, у этой системы найдутся приложения не только в роли логического исчисления. Алонсо Чёрч, 1932

 

 

  


Информация о работе Лямбда исчисление