lambdascript 0.2.1

Educational tool illustrating beta reduction of typed and 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

// typed terms

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

// Booleans and if-else
define TRUE = lambda x.lambda y.x;     // K A B = A
define FALSE = lambda x.lambda y.y;  // (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;

// Arithmetic
define ZERO = lambda f.lambda x.x;
define ISZERO = lambda n.n (lambda z.FALSE) TRUE;
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 PRED = lambda n.lambda f.lambda x.n (lambda g.lambda h.h (g f)) (lambda u.x) (lambda u.u);
define SUBTRACT = lambda m.lambda n. n PRED m;
define LEQ = lambda m.lambda n. ISZERO (SUBTRACT m n);  // <=
define EQUALS = lambda m.lambda n.AND (LEQ m n) (LEQ n m);
LEQ ONE (PLUS ONE ONE);   //true
LEQ (PLUS ONE ONE) ONE;  // false
EQUALS ONE (TIMES ONE ONE); // true

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

*/