Лямбда Синтаксисы
В этом посте хочу собрать все лямбда синтаксисы. Навскидку есть несколько синтаксисов для лямбды:
λ 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