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