Lambda Reducer

Enter a lambda term, press "Enter Term" and then click a redex binding site (or click "Normalize") to contract redexes. See the documentation for more information.

// This is a demo lambda term which checks if parentheses are properly nested

// These are booleans and pairing operators
let true = \x\y x :		let false = \x\y y : 
let pair = \x\y\z.z x y:
let fst = \p. p true: 		let snd = \p. p false:

// This is one encoding of numbers
let zero = \x x :		let succ = \n\x . x false n : 
let pred = \n.n false :		
let IsZero(n) = n true :

/****************************************
//This is another (Church Numerals): 
let zero = \f\x x :		let succ = \n\f\x . f(n f x): 
let pred = \n.  snd . n ( \x. pair (succ . fst x) (fst x) )(pair zero zero)  :		
let IsZero(n) = n (\k.false) true : 
let + = \n1\n2. \f\x. n1 f (n2 f x) :
let * = \n1\n2. \f\x. n1 (n2 f) x:
let - = \n1\n2. n2 (\x. pred x) n1:
let ^ = \n1\n2. n2 n1:
****************************************/

// This is the Y combinator.
let fixedpoint = \f. (\x.f(x x))(\x.f(x x)) :

// These are some encodings for our application
let [ = succ zero :		let ] = succ . succ zero : 
let ; = zero :			let throw = fixedpoint . \b\x.IsZero(x) false b :

let h = 
	fixedpoint . \h\n\p . 
		(IsZero(p))(		
			(IsZero(n)) (
				true
			). 
				false 
		).
			(IsZero(pred p)) ( 
				h(succ n)
			). 
				(IsZero(n)) (
					throw 
				).
					h (pred n)
	:
let checkBalancedParens = h zero :

// This is where the actual term begins.
// The above statements are all let statements

checkBalancedParens [ [ ] ] [ ] ; yes no