Автор: Пользователь скрыл имя, 18 Марта 2012 в 20:08, реферат
Функциональные языки программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в качестве теоретической основы и "минимального" функционального языка программирования.
Определение 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](t1 t2) |
= |
([x ↦ s]t1) ([x ↦ s]t2) |
Операционная семантика лямбда-термов вкратце представлена на рис. 5.3. Множество значений в этом исчислении более интересно, чем было в случае арифметических выражений. Поскольку вычисление (с вызовом по значению) останавливается, когда достигает лямбды, значениями являются произвольные лямбда-термы.
→ (бестиповое)
Синтаксис
t |
::= термы: |
x переменная | |
λx.t абстракция | |
t t применение | |
v |
::= значения: |
λx.t значение-абстракция |
Вычислениеt → t′t → t′
|
|
|
|
Figure 5.3: Бестиповое лямбда-исчисление (λ) |
Отношение вычисления показано в правом столбце рисунка. Как и в случае арифметических выражений, имеется два типа правил: рабочее правило E-AppAbs и правила соответствия E-App1 и E-App2.
Обратите внимание, как выбор метапеременных в этих правилах помогает управлять порядком вычислений. Поскольку v2 может относиться только к значениям, левая сторона правила E-AppAbsсоответствует всем применениям термов, в которых терм-аргумент является значением. Точно так же, E-App1 относится к тем применениям, в которых левая часть не является значением, посколькуt1 может обозначать любой терм, но предпосылка правила требует, чтобы t1 мог совершить шаг вычисления. Напротив, E-App2 не срабатывает, пока левая часть не станет значением, которое может быть обозначено метапеременной v. Совместно эти правила полностью определяют порядок вычисления терма вида t1 t2: сначала работает E-App1, пока t1 не сведется к значению, затем E-App2применяется до тех пор, пока t2 не окажется значением, и, наконец, само правило E-AppAbs производит само применение.
Упражнение 6 [★★]:
Модифицируйте эти правила так, чтобы
описать три другие стратегии вычисления:
полную бета-редукцию, нормальный порядок
и ленивое вычисление.
Заметим, что в чистом лямбда-исчислении единственные возможные значения — это лямбда-абстракции, так что, если E-App1 доводит t1 до значения, это значение должно быть лямбда-абстракцией. Разумеется, это утверждение перестает быть справедливым, как только мы добавляем в язык другие конструкции, скажем, элементарные булевские значения, поскольку при этом у нас появляются новые виды значений.
Упражнение 7 [★★,↛]:
В упражнении 16 дается альтернативное
представление операционной семантики
булевских и арифметических выражений,
в котором тупиковые термы дают при вычислении
особую константуwrong. Распространите
эту семантику на λNB.
Упражнение 8 [★★]:
В упражнении 17 вводится стиль
вычисления арифметических выражений
<<с большим шагом>>, в котором базовое
отношение вычисления означает <<терм t при вычислении
дает окончательный результат v>>. Покажите,
как сформулировать правила вычисления
лямбда-термов в этом стиле.
Бестиповое лямбда-исчисление было разработано Чёрчем и его коллегами в 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