docs/fype.txt


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

Lambda Rules:

(1) x ϵ V => x ϵ Λ
(2) M,N ϵ Λ => (M N) ϵ Λ (Application)
(3) M ϵ Λ and x ϵ V => (λx.M) ϵ Λ (Abstraction)
(4) No further Terms in Λ existent

Examples:

(λx.(λy.x)) ≡ λx.λy.x ≡ λx y.x ≡ false
(λx.(λy.y)) ≡ λx.λy.y ≡ λx y.y ≡ true
λx.λy.((x y) false) ≡ λx y.((x y) false) ≡ and

Syntax:

(λx . (λy.x)) ≡ λx.λy.x ≡ λx y . x ≡ false
true: x y = x;

(λx.(λy.y)) ≡ λx.λy.y ≡ λx y . y ≡ true
false: x y = y;

λx.λy.((x y) false) ≡ λx y.((x y) false) ≡ and
and: x y = (x y) false;

id: x = x;

greet: x = say (~ "Hello " x);