# Untyped Lambda Calculus ### Basics **What is the Grammar of Lambda Calculus?** ``` t ::= terms x variable λx.t abstraction t t application ``` **How are things grouped together?** - application associates to the left: s t u = (s t) u - bodies of abstractions are taken to extend as far to the right as possible. λx. λy. x y x = λx. (λy. ((x y) x)) **What is [x ↦ t_2]t_12 in (λx.t_12)t_2 ⟶ [x ↦ t_2]t_12?** The term obtained by replacing all free occurrences of x in t_12 t_2. **What is a *free variable*?** An occurrence of x is *free* if it appears in a position where it is not bound by an enclosing straction on x. **What is a *redex*?** A term of the form (λx.t_12) t2 **What is a *closed* term?** A term with no free variables **What is a *beta reducion*?** Applying (λx.t_12)t_2 ⟶ [x ↦ t_2]t_12 on a *redex* **What are the various evaluation strategies?** - *full beta-reduction*: any redex can be reduced at any time - *normal order strategy*: leftmost, outermost redex is reduced first - *call by name*: normal order + no reductions inside abstractions. optimized version: *call by need* - *call by value*: normal order + redex is reduced only when its rhs is reduced to a value ### Programming in the Lambda Calculus **How to get multiple arguments?** f = λ(x, y).s can be rewritten as f = λx.λy.s. Instead of f v w, we apply like: ((f v) w). **How to implement Booleans?** ``` tru = λt. λf. t; fls = λt. λf. f; ``` **How to implement boolean operators?** ``` and = λb. λc. b c fls; or = λb. λc. b tru c; not = λb. b fls tru; ``` **How to implement Pairs?** ``` pair = λf. λs. λb b f s; fst = λp. p tru; snd = λp. p fls; ``` **How to implement Numbers?** c_0 = λs. λz. z; c_1 = λs. λz. s z; c_2 = λs. λz. s (s z); c_3 = λs. λz. s (s (s z)); etc. takes in a succ (s) and 0 and applies succ to n times to 0. scc = λn λs. λz. s (n s z) scc takes in a church numeral and applies the successor to it Another successor func: scc = λn λs. λz. n (s (s z)) plus = λm. λn. λs λz. m s (n s z) times = λm. λn. m (plus n) c_0 Is it possible to define times w/o using plus?