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

define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.x z (y z);

define SKI = S K I

// 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;