2016-08-09

Лямбда Синтаксисы

В этом посте хочу собрать все лямбда синтаксисы. Навскидку есть несколько синтаксисов для лямбды:

λ x . B x — нетипизированная классика
λ x : A , B x — в научных статьях
λ (x: A) → B x — современный синтаксис, Morte, pts
λ (x: A) , B x — Lean
(x: A) B x — LISP синтаксис
[x: A] B(x) — AUTOMATH
fun (x: A) => B x — языки программирования, французкая школа
fun (X) -> B(X) — Erlang

Классика используется студентами, которые решают домашки, на википедии, и в HOL/Isabelle. Второй синтаксис используется в самых крутых статьях по лямбда исчислению, его использует например Страйхер, третий используется тоже часто в статьях, например Пфенинг. LISP синтаксис заюзал в своей работе по индуктивных семейставах Дыбьер. Но все это вариации AUTOMATH, где есть [], что есть там и квантор и лямбда. Есть еще логический синтаксис правил вывода, который заюзал МакБрайд в Эпиграмме, но это по-моему слишком. Синтаксис, который используется в современных языках программирования, так же приведен, тут по столько по скольку, так как статьи на нем писать неудобно. Мы выбрали в качестве синтаксиса лямбда исчисления в OM тот, где есть и скобочки и стрелочки. Нормальные формы лямбд мы выстраиваем вертикально так как это делал Дыбьер, чтобы видеть паттерн и глубину терма.

Отдельно хочется отметить семейство синтаксисов Caramel, авторства MaiaVictor, к сожалению фыйлы Карамели похоронены под мастером, но я вытащил. Еще этот сиснтаксис использовался в обзорной статье про кодировки лямбда исчисления CPS-кодирвка с континуатором.


 cons  = (x list cons nil -> (cons x (list cons nil)))
 nil   = (cons nil -> (id nil))
 foldr = (cons nil list -> (list cons nil))
 seq   = (foldr comp id)
 do    = (comp seq reverse)
 take  = (n -> (n (r l -> (cons (head l) (r (tail l)))) (const nil)))

То как выглядят индуктивные типы условно можно разделить на британскую школу LCF/ML/HOL/Hope/Miranda/Haskell/Agda/Idris и американскую LISP/ACL2/NuPRL/Lean школу.


 data List (A : Set) : Set where
      []  : List A
      _∷_ : (x : A) (xs : List A) → List A

 data List (A: *): * :=
      (Nil: List A)
      (Cons: A → List A → List A)

 data List (A: U): U :=
      nil
    | cons (x: A) (xs: List A)

 data List : (A: Type) -> Type
    | nil  : Nat
    | cons : (x:A, xs: List(A)) -> Nat