05 - The Untyped Lambda-Calculus

Lambda grammer:

t ::==    # terms
	x       # variable
  λx.t    # abstraction
  t t     # application

Church Booleans

tru = λt. λf. t;
fls = λt. λf. f;

test = λl. λm. λn. l m n;

image-20240503163917192

and = λb. λc. b c fls;

Ex 5.2.1: Define logical or and not functions