Анотація
Мова програмування
Синтаксис
Терми
I = #identifier
O = I | ( O ) | O O | λ I -> O | O , O | O.1 | O.2 | 1type term =
| Var of string
| Lam of string * term
| App of term * term
| Pair of term * term
| Fst of term
| Snd of term
| UnitПравила обчислень
Основними правилами обчислень у
App (Lam (x, b), a) → subst x a b
Fst (Pair (t1, t2)) → t1
Snd (Pair (t1, t2)) → t2Підстановка
let rec subst x s = function
| Var y -> if x = y then s else Var y
| Lam (y, t) when x <> y -> Lam (y, subst x s t)
| App (f, a) -> App (subst x s f, subst x s a)
| Pair (t1, t2) -> Pair (subst x s t1, subst x s t2)
| Fst t -> Fst (subst x s t)
| Snd t -> Snd (subst x s t)
| Unit -> Unit
| t -> tРівність
let rec equal t1 t2 =
match t1, t2 with
| Var x, Var y -> x = y
| Lam (x, b), Lam (y, b') -> equal b (subst y (Var x) b')
| Lam (x, b), t -> equal b (App (t, Var x))
| t, Lam (x, b) -> equal (App (t, Var x)) b
| App (f1, a1), App (f2, a2) -> equal f1 f2 && equal a1 a2
| Pair (t1, t2), Pair (t1', t2') -> equal t1 t1' && equal t2 t2'
| Fst t, Fst t' -> equal t t'
| Snd t, Snd t' -> equal t t'
| Unit, Unit -> true
| _ -> falseРедукція
let rec reduce = function
| App (Lam (x, b), a) -> subst x a b
| App (f, a) -> App (reduce f, reduce a)
| Pair (t1, t2) -> Pair (reduce t1, reduce t2)
| Fst (Pair (t1, t2)) -> t1
| Fst t -> Fst (reduce t)
| Snd (Pair (t1, t2)) -> t2
| Snd t -> Snd (reduce t)
| Unit -> Unit
| t -> tНормалізація
let rec normalize t =
let t' = reduce t in
if equal t t' then t else normalize t'Внутрішня мова ДЗК
Мова
Бібліографія
[1]. Alonzo Church. A Set of Postulates for the Foundation of Logic. 1933
[2]. Alonzo Church. An Unsolvable Problem of Elementary Number Theory. 1941
[3]. Haskell Curry, Robert Fey. Combinatory Logic, Volume I. 1951
[4]. Dana Scott. A Type-Free Theory of Lambda Calculus. 1970
[5]. John Reynolds. Towards a Theory of Type Structure. 1974
[6]. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. 1984
[7]. G.Cousineau, P.-L.Curien, M.Mauny. The Categorical Abstract Machine. 1985