lambdascript 0.1.56

Educational tool illustrating beta reduction of untyped lambda terms, parser generation
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

// Sample Solutions to Lambda Calculus Homework in Lambdascript.

// 2.
2;  // 2 is evaluated into 2, which is already a normal form
(lambda x.lambda y. (y x)) u (lambda x.x);


// 3. Basic combinators:
3;
define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.x z (y z);

K I I;
S I K;
S K (K I);
S (K I);

// note that the lambdascript program does call-by-name by default.
weak (S (K I));  // this does "weak head reduction using call-by-value"

// 4. Arithmetic
4;
define ZERO = K I;
define ONE = lambda f.lambda x.f x;
define PLUS = lambda m.lambda n.lambda f.lambda x.m f (n f x);
define TIMES = lambda m.lambda n.lambda f.lambda x.m (n f) x;
define TWO = PLUS ONE ONE;

PLUS TWO ONE;
TIMES ZERO TWO;

// 4b.
4 b;  // a space is needed otherwise there's parser error
define EXPT = lambda m.lambda n.n m;
define TREE = PLUS ONE TWO;

EXPT TREE TWO;


// 5. Booleans and if-else
5;
define TRUE = K;     // K A B = A
define FALSE = K I;  // (K I) A B = B
define IF = lambda b.lambda x.lambda y.b x y;
define NOT = lambda b.IF b FALSE TRUE;
define OR = lambda a.lambda b.IF a TRUE b;
define AND = lambda a.lambda b.IF a b FALSE;
OR;
OR FALSE FALSE;
OR FALSE TRUE;
OR TRUE FALSE;
OR TRUE TRUE;


6;
define NOT = lambda n.n FALSE TRUE;
NOT;
NOT FALSE;
NOT TRUE;
NOT (NOT TRUE);  // "no, no it can't be true!"  but it is.

7;
IF TRUE 1 2;
IF FALSE 1 2;


// Data structure (pairs, linked-list = nested pairs)
define PAIR = lambda a.lambda b.lambda c.IF c a b; // called "CONS"
define FST = lambda c.c TRUE;  // first element of cons pair, "CAR"
define SND = lambda c.c FALSE; // second element of cons pair, "CDR"
define NIL = FALSE;   // represents empty list
define ISNIL = lambda p.p (lambda a.lambda b.lambda z.FALSE) TRUE;

8;
define M = PAIR a (PAIR b c);
M;
FST M;
SND M;
SND (SND M);

9;
define ISZERO = lambda n.n (lambda z.FALSE) TRUE;
ISZERO;
ISZERO (TIMES ONE ZERO);
ISZERO (PLUS ONE ZERO);

10;
still working on it;
define lazy INFINITY = (lambda x.x x) (lambda x.x x);
// without "lazy" it will go into an infinite loop

//  weak (INFINITY);   // uncomment at your own risk...