t ::= термы: true константа «истина» false константа «ложь» if t then t else t условное выражение 0 константа «ноль» succ t следующее число pred t предыдущее число iszero t проверка на ноль
множество термов T это наименьшее множество T:
1. {true, false, 0} ⊆ T;
2. t1 ∈ T ⇒ {succ t1, pred t1, iszero t1} ⊆ T;
3. t1 ∈ T, t2 ∈ T, t3 ∈ T ⇒ if t1 then t2 else t3 ∈ T
множество термов T это наименьшее множество T:
true ∈ T, false ∈ T, 0 ∈ T t1 ∈ T ------------ succ t1 ∈ T t1 ∈ T ------------ pred t1 ∈ T t1 ∈ T ------------- iszero t1 ∈ T t1 ∈ T t2 ∈ T t3 ∈ T ------------------------- if t1 then t2 else t3 ∈ T
type info = int * string (* каждый узел абстрактного синтаксического дерева снабжен значением типа info, в котором записано место в файле и имя файла, в котором определена эта вершина *) type term = | TmTrue of info | TmFalse of info | TmIf of info * term * term * term | TmZero of info | TmSucc of info * term | TmPred of info * term | TmIsZero of info * term let rec isnum t = match t with | TmZero(_) -> true | TmSucc(_,t1) -> isnum t1 | _ -> false let rec isval t = match t with | TmTrue(_) -> true | TmFalse(_) -> true | t when isnum t -> true | _ -> false (* определим сначала исключение, которое вызывается, если ни одно правило не применимо: *) exception NoRuleApplies (* в нескольких местах мы создаем новые термы, а не переделываем уже существующие. так как этих новых термов нет в пользовательских исходных файлах, то аннотации info в них не имеют смысла. в таких термах мы используем константу dummyinfo. для сопоставления с аннотациями в образцах всегда используется переменная fi (file info) *) let dummyinfo = (0 , "") ;; let rec eval1 t = match t with | TmIf(_,TmTrue(_),t2,t3) -> t2 | TmIf(_,TmFalse(_),t2,t3) -> t3 | TmIf(fi,t1,t2,t3) -> let t1' = eval1 t1 in TmIf(fi, t1', t2, t3) | TmSucc(fi,t1) -> let t1' = eval1 t1 in TmSucc(fi, t1') | TmPred(_,TmZero(_)) -> TmZero(dummyinfo) | TmPred(_,TmSucc(_,nv1)) when (isnum nv1) -> nv1 | TmPred(fi,t1) -> let t1' = eval1 t1 in TmPred(fi, t1') | TmIsZero(_,TmZero(_)) -> TmTrue(dummyinfo) | TmIsZero(_,TmSucc(_,nv1)) when (isnum nv1) -> TmFalse(dummyinfo) | TmIsZero(fi,t1) -> let t1' = eval1 t1 in TmIsZero(fi, t1') | _ -> raise NoRuleApplies let rec eval t = try let t' = eval1 t in eval t' with NoRuleApplies -> t (* помещать обработчик исключений try внутрь рекурсивного цикла не рекомендуется *)
процедурная (или функциональная) абстракция - ключевое свойство почти всех языков программирования
вместо того чтобы выписывать одно и то же вычисление раз за разом, мы пишем процедуру или функцию, которая проделывает это вычисление в общем виде, используя один или несколько именованных параметров, а затем при необходимости вызываем эту процедуру, каждый раз задавая значения параметров
лямбда-исчисление (lambda-calculus) воплощает такой способ определения и применения функций в наиболее чистой форме. в лямбда-исчислении всё является функциями: аргументы, которые функции принимают - тоже функции, и результат, который возвращают функции - опять-таки функция
синтаксис лямбда-исчисления состоит из трех видов термов
эти способы конструирования термов выражаются следующей грамматикой:
t ::= термы: x переменная λx . t абстракция t t применение
полезно различать два уровня структуры:
преобразование из конкретного в абстрактный синтаксис происходит в два этапа
сначала лексический анализатор (lexical analyzer) (или лексер, lexer) переводит последовательность символов, написанных программистом, в последовательность лексем (tokens) - идентификаторов, ключевых слов, комментариев, символов пунктуации и т. п. лексический анализатор убирает комментарии, обрабатывает пробелы, решает вопрос с заглавными и строчными буквами, а также распознает форматы числовых и символьных констант
после этого грамматический анализатор (парсер, parser) преобразует последовательность лексем в абстрактное синтаксическое дерево
переменная x называется связанной (bound), если она находится в теле t абстракции
вхождение x свободно (free), если оно не связано никакой вышележащей абстракцией переменной x
например, вхождения x в
и
свободны, а вхождения x в
и
связаны. В
первое вхождение x связано, а второе свободно
терм без свободных переменных называется замкнутым (closed); замкнутые термы называют также комбинаторами (combinators). простейший комбинатор, называемый функцией тождества (identity function),
не выполняет никаких действий, а просто возвращает свой аргумент
терм t находится в нормальной форме (normal form), если к нему не применимо никакое правило вычисления - т.е. если не существует такого t′, что t → t'. true и false - нормальные формы
Тh: если t находится в нормальной форме, то t - значение
Тh: если t →∗u и t →∗u′, причем как u, так и u′ - нормальные формы, то u = u'
каждый терм можно вычислить и получить значение. понятно, что это еще одна характеристика, которой могут не обладать более богатые языки, в которых, например, присутствуют рекурсивные определения функций.
Def: терм называется тупиковым (stuck), если он находится в нормальной форме, но не является значением
понятие «тупикового терма» представляет ошибки времени выполнения (run-time errors). оно описывает ситуации, когда операционная семантика не знает, что делать дальше, поскольку программа оказалась в «бессмысленном» состоянии. в более конкретной реализации языка такие состояния могут соответствовать различного рода ошибкам: обращениям по несуществующему адресу, попыткам выполнить запрещенную машинную команду и т.п.
в своей чистой форме лямбда-исчисление не содержит встроенных констант и элементарных операторов - ни чисел, ни арифметических операций, ни условных выражений, ни записей, ни циклов, ни последовательного выполнения выражений, ни ввода-вывода, и т.д. единственное средство для «вычисления» термов - применение функций к аргументам (которые сами являются функциями). каждый шаг вычисления состоит в том, что в терме-применении, в котором левый член является абстракцией, связанная переменная в теле этой абстракции заменяется на правый член. записывается это так:
(λx.t12) t2 → [x → t2] t12где [x → t2] t12 означает «терм, получаемый из t12 путем замены всех свободных вхождений x на t2».
например, терм (λx.x) y за один шаг вычисления переходит в y, а терм (λx. x (λx.x)) (u r) переходит в u r (λx.x)
вслед за Чёрчем, терм вида (λx. t12) t2 называется редексом (reducible expression, redex — «сокращаемое выражение»), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией (beta-reduction)
в большинстве языков используется стратегия вызова по значению (call by value). в соответствии с ней, сокращаются только самые внешние редексы, и, кроме того, редекс срабатывает только в том случае, если его правая часть уже сведена к значению (value) - замкнутому терму, который уже вычислен и не может быть редуцирован далее
стратегия вызова по имени (call by name) не позволяет проводить редукцию внутри абстракций
в Haskell используется оптимизированная версия, известная как вызов по необходимости (call by need), в которой вместо того, чтобы перевычислять аргумент при каждом использовании, при первом вычислении все вхождения аргумента заменяются значением, и таким образом пропадает необходимость вычислять его заново в следующий раз. при такой стратегии требуется во время выполнения совместно использовать структуры данных между представлениями термов - в сущности, получается отношение редукции на графах абстрактного синтаксиса, а не на синтаксических деревьях
в лямбда-исчислении отсутствует встроенная поддержка функций с несколькими аргументами. ее было бы нетрудно добавить, однако того же самого результата проще достичь через функции высшего порядка (higher-order functions), которые возвращают функции в качестве результата. преобразование функций с несколькими аргументами в функции высшего порядка называется каррированием (currying) - в честь Хаскелла Карри. несмотря на название, Карри не считал себя автором идеи каррирования. её открытие обычно приписывают Шёнфинкелю (Schönfinkel,1924), однако основная идея еще в XIX веке была известна некоторым математикам, в том числе Фреге и Кантору