Testing

I have included the following tests. They can be run by clicking on eval. You can modify them as you see fit. They are borrowed from TaPL.

Logical Operators

// 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 //fst (pair v w) test (imp (snd (pair false true)) (snd (pair true false))) if else //test (and (snd (pair false true)) (snd (pair true false))) if else

Numerals

~~Note that for now these are quite slow due to closure copies.~~

// Numerals let id = \ v . v; // bools let true = \ t . \ f . t; let false = \ t . \ f . f; // pairs let pair = \ f . \ s . \ b . b f s; let fst = \ p . p true; let snd = \ p . p false; // 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); // 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))); let 4 = scc 3; let 5 = scc 4; // num operators decs let zz = pair 0 0; let ss = \ p . pair (snd p) (plus 1 (snd p)); let prd = \ m0 . fst (m0 ss zz); let minus = \ m . \ n . n prd m; let times = \ m . \ n . m (plus n) 0; let test = \ l . \ m . \ n . l m n; let equal = \ m . \ n . isZero (minus m n); // testing //test (isZero 0) yes no //isZero (prd 1) //isZero (plus 3 1) //isZero (minus 3 1) //isZero (times 3 3) test (isZero (prd (prd (prd 3)))) yes no

Closures #1

let id = \ v . v; let closure = (\ a . \ b . \ c . b c) ctest1 ctest2; // testing closure a

Closures #2

let id = \ v . v; let f1 = \ a . a; let closure = (\ a . \ b . \ c . b c) cls1 (\ a . f1); closure a

Closures #3

let id = \ v . v; let f1 = \ a . a; let closure = (\ a . \ b . \ c . b c a) cls1 (\ a . (\ b . b) f1); closure a

Write you own test

let id = \ v . v; id

ρ is again used to describe the scope environment. If you find any errors, please report those as a comment below.