Interpret a program written in the untyped λ-calculus. The interpreter project can be found here. This is for the simple untyped Lambda Calculus. If you have any errors to report, do so by commenting on the project page.
// Logic
let id = \ v . v;
// operators
let true = \ t . \ f . t;
let false = \ t . \ f . f;
let and = \ b . \ c . b c false;
let or = \ b . \ c . b true c;
let not = \ b . b false true;
let imp = \ b . \ c . or (not b) c;
// conditional
let test = \ l . \ m . \ n . l m n;
// testing
//test (not true) if else
test (imp false true) if else
// Pairs
let id = \ v . v;
// operators
let true = \ t . \ f . t;
let false = \ t . \ f . f;
let and = \ b . \ c . b c false;
let or = \ b . \ c . b true c;
let not = \ b . b false true;
let imp = \ b . \ c . or (not b) c;
// conditional
let test = \ l . \ m . \ n . l m n;
// pairs
let pair = \ f . \ s . \ b . b f s;
let fst = \ p . p true;
let snd = \ p . p false;
// testing
//snd (pair v w)
test (imp (snd (pair false true)) (fst (pair true false))) if else
// Church Numerals
// stack overflow is reached quickly when using minus
let id = \ v . v;
// bools
let true = \ t . \ f . t;
let false = \ t . \ f . f;
let test = \ l . \ m . \ n . l m n;
// pairs
let pair = \ f . \ s . \ b . b f s;
let fst = \ p . p true;
let snd = \ p . p false;
// church numerals
let 0 = (\ s . \ z . z);
let 1 = (\ s . \ z . s z);
let 2 = (\ s . \ z . s (s z));
let 3 = \ s . \ z . s (s (s z));
// num operators
let isZero = \ m . m (\ x . false) true;
let scc = \ n . \ s . \ z . s (n s z);
let plus = \ m . \ n . \ s . \ z . m s (n s z);
// num operators decs
let zz = pair 0 0;
let ss = \ p . pair (snd p) (plus 1 (snd p));
let prd = \ m . fst (m ss zz);
let minus = \ m . \ n . n prd m;
let times = \ m . \ n . m (plus n) 0;
// testing
//test (isZero 0) yes no
//isZero (prd 1)
//isZero (plus 3 1)
//isZero (minus 3 1)
//isZero (times 3 0)
//test (isZero (minus 2 1)) yes no
times 3 3
Share