часть первая - бестиповые системы

термы

  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) воплощает такой способ определения и применения функций в наиболее чистой форме. в лямбда-исчислении всё является функциями: аргументы, которые функции принимают - тоже функции, и результат, который возвращают функции - опять-таки функция

синтаксис лямбда-исчисления состоит из трех видов термов

  • переменная x сама по себе есть терм
  • абстракция переменной x в терме t1 (λx.t1) - тоже терм
  • применение терма t1 к терму t2 (t1 t2) - третий вид термов

    эти способы конструирования термов выражаются следующей грамматикой:

    t ::=                     термы:
       x                      переменная
       λx . t                 абстракция
       t t                    применение
    

    полезно различать два уровня структуры:

  • конкретный синтаксис (concrete syntax) языка относится к строкам символов, которые непосредственно читают и пишут программисты
  • абстрактный синтаксис (abstract syntax) - это намного более простое внутреннее представление программ в виде помеченных деревьев, которые называются абстрактными синтаксическими деревьями (abstract syntax trees, AST)

    преобразование из конкретного в абстрактный синтаксис происходит в два этапа

    сначала лексический анализатор (lexical analyzer) (или лексер, lexer) переводит последовательность символов, написанных программистом, в последовательность лексем (tokens) - идентификаторов, ключевых слов, комментариев, символов пунктуации и т. п. лексический анализатор убирает комментарии, обрабатывает пробелы, решает вопрос с заглавными и строчными буквами, а также распознает форматы числовых и символьных констант

    после этого грамматический анализатор (парсер, parser) преобразует последовательность лексем в абстрактное синтаксическое дерево

    переменная x называется связанной (bound), если она находится в теле t абстракции λx . t

    вхождение x свободно (free), если оно не связано никакой вышележащей абстракцией переменной x

    например, вхождения x в x y и λy . x y свободны, а вхождения x в λx . x и λz . λx . λy . x (y z) связаны. В (λx . x) x первое вхождение x связано, а второе свободно

    терм без свободных переменных называется замкнутым (closed); замкнутые термы называют также комбинаторами (combinators). простейший комбинатор, называемый функцией тождества (identity function), id = λx . x не выполняет никаких действий, а просто возвращает свой аргумент

    терм 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 веке была известна некоторым математикам, в том числе Фреге и Кантору