Lambda Calculus: Basic concepts

• Introduction

  • functions in mathematics

  • functions in programming languages

  • lambda calculus as a formalization of functions

  • lambda calculus as a programming language

• Lambda Calculi

  • introduction

  • elements

    • lambda expression

    • lambda term

      • parameters (variables)

      • lambda abstraction

      • lambda application

  • variants

    • untyped lambda calculus

    • simply typed lambda calculus

    • typed lambda calculi

  • untyped lambda calculus

    • informal introduction

    • formal definition

  • binding

    • binder

    • binding scope

    • formal parameter

    • parameter (variable) occurrence

      • binding occurrence

      • application occurrence

  • conversions

    • alpha-conversion

      • alpha-equvalence

      • renaming

    • beta-conversion

      • beta-reduction

      • substitution

      • name capture

    • eta-conversion

      • eta-reduction

      • eta-expansion

    • delta-conversion

      • let-binding

  • interpretation

    • evaluation

    • inference rules

    • call-by-value

    • call-by-name

    • call-by-sharing

    • strictness

    • laziness