510 Lambda Calculi

• Lambda Calculi

  • untyped lambda calculus, λ

  • typed lambda calculi

    • simply typed lambda calculi, λ→

• Lambda Calculus

  • untyped lambda calculus

  • definition

    • function abstraction

    • function application

      • variable binding

      • variable substitution

  • reductions

    • α-conversion

      • α-conversion

    • β-reduction

      • redex

      • normal form

      • weak head normal form

      • β-normal form

    • η-conversion

  • concepts

    • bound vars

    • free vars

  • evaluation

    • normal

    • applicative

  • encoding schemes

• Typed lambda calculi

  • Simply typed lambda calculi, λ→