# Lambda Calculus: OUTLINE

* Syntax of lambda calculus
  * variables
  * lambda abstraction
  * lambda application
* Introduction to lambda calculus
  * Lambda calculus
  * Lambda terms
  * Alonzo Church
* Definition
  * function abstraction
  * function application
    * Substitution
    * α-conversion
    * β-reduction
    * η-conversion
    * δ-reduction
    * ξ-equality
    * de Bruijn indexing
  * Forms of lambda terms
    * Redex
    * Beta normal form
    * Normal form
    * WHNF

## Category:Lambda\_calculus

https://en.wikipedia.org/wiki/Category:Lambda\_calculus

Lambda calculus Anonymous function Applicative computing systems Apply B, C, K, W system Beta normal form Böhm tree Calculus of constructions Call-by-push-value Cartesian closed category Church encoding Church-Rosser theorem Combinatory logic Currying De Bruijn index De Bruijn notation Deductive lambda calculus Director string Divergence (computer science) Explicit substitution Fixed-point combinator Higher-order function Hindley-Milner type system Intersection type discipline Kleene-Rosser paradox Knights of the Lambda Calculus Krivine machine Lambda calculus definition Lambda cube Lambda lifting Lambda-mu calculus Let expression Mogensen-Scott encoding Montague grammar Normalisation by evaluation Normalization property (abstract rewriting) Pattern calculus Pure type system Reduction strategy Rho calculus Scott-Curry theorem Simply typed lambda calculus SKI combinator calculus Supercombinator System F System F-sub System U Type inhabitation Typed lambda calculus Untyped lambda calculus Η-conversion

https://en.wikipedia.org/wiki/Lambda\_calculus https://en.wikipedia.org/wiki/Anonymous\_function https://en.wikipedia.org/wiki/Applicative\_computing\_systems https://en.wikipedia.org/wiki/Apply https://en.wikipedia.org/wiki/B,\_C,\_K,\_W\_system https://en.wikipedia.org/wiki/Beta\_normal\_form

https://en.wikipedia.org/wiki/Bohm\_tree

https://en.wikipedia.org/wiki/Calculus\_of\_constructions https://en.wikipedia.org/wiki/Call-by-push-value https://en.wikipedia.org/wiki/Cartesian\_closed\_category https://en.wikipedia.org/wiki/Church\_encoding https://en.wikipedia.org/wiki/Church-Rosser\_theorem https://en.wikipedia.org/wiki/Combinatory\_logic https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/De\_Bruijn\_index https://en.wikipedia.org/wiki/De\_Bruijn\_notation https://en.wikipedia.org/wiki/Deductive\_lambda\_calculus https://en.wikipedia.org/wiki/Director\_string https://en.wikipedia.org/wiki/Divergence\_(computer\_science) https://en.wikipedia.org/wiki/Explicit\_substitution https://en.wikipedia.org/wiki/Fixed-point\_combinator https://en.wikipedia.org/wiki/Higher-order\_function https://en.wikipedia.org/wiki/Hindley-Milner\_type\_system https://en.wikipedia.org/wiki/Intersection\_type\_discipline https://en.wikipedia.org/wiki/Kleene-Rosser\_paradox https://en.wikipedia.org/wiki/Knights\_of\_the\_Lambda\_Calculus https://en.wikipedia.org/wiki/Krivine\_machine https://en.wikipedia.org/wiki/Lambda\_calculus\_definition https://en.wikipedia.org/wiki/Lambda\_cube https://en.wikipedia.org/wiki/Lambda\_lifting https://en.wikipedia.org/wiki/Lambda-mu\_calculus https://en.wikipedia.org/wiki/Let\_expression https://en.wikipedia.org/wiki/Mogensen-Scott\_encoding https://en.wikipedia.org/wiki/Montague\_grammar https://en.wikipedia.org/wiki/Normalisation\_by\_evaluation https://en.wikipedia.org/wiki/Normalization\_property\_(abstract\_rewriting) https://en.wikipedia.org/wiki/Pattern\_calculus https://en.wikipedia.org/wiki/Pure\_type\_system https://en.wikipedia.org/wiki/Reduction\_strategy https://en.wikipedia.org/wiki/Rho\_calculus https://en.wikipedia.org/wiki/Scott-Curry\_theorem https://en.wikipedia.org/wiki/Simply\_typed\_lambda\_calculus https://en.wikipedia.org/wiki/SKI\_combinator\_calculus https://en.wikipedia.org/wiki/Supercombinator https://en.wikipedia.org/wiki/System\_F https://en.wikipedia.org/wiki/System\_F-sub https://en.wikipedia.org/wiki/System\_U https://en.wikipedia.org/wiki/Type\_inhabitation https://en.wikipedia.org/wiki/Typed\_lambda\_calculus https://en.wikipedia.org/wiki/Untyped\_lambda\_calculus https://en.wikipedia.org/wiki/%CE%97-conversion
