Lambda Calculus

Lambda calculus is a simple and powerful notation for defining functions. Among its uses are

• foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala
• basis of higher order logic

In lambda calculus, functions have no side effects

• they are mathematical functions from arguments to results
• lambda calculus also supports higher-order functions
• this model is appropriate for studying type checking
• directly applicable to purely functional languages (like Haskell)
• applies to other languages if we ensure that assignments do not change types

Anonymous Functions in Lambda Calculus

A function which takes its argument and increments it by 2 is given by lambda expression . The operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition, writing instead of . Here are some example expressions and their values: Concrete syntax for :

• Isabelle theorem prover: '(% x.x+2)5' or '(\<lambda> x.x+2)5'
• ocaml: '(function x → x+2)5'
• Haskell: '(\ x → x+2)5'
• Scala ((x:int) => x+2)(5)

Lambda Expressions

Abstract syntax of untyped lambda expressions: That is, an expression is 1) a variable, 2) a lambda expression defining a function, or 3) an application of one expression to another.

Certain predefined variables are called constants (e.g. 7, 42, 13, but also operations +, *).

Types are given by the following grammar: There can be additional primitive types .

Currying we have Therefore is a function that increments its argument by • expression is just a shorthand for This is called currying in the honor of Haskell Curry

In general, instead of function we can use function Beta Reduction

The main rule of lambda calculus is beta reduction, which formalizes function application: Here we assume capture-avoiding substitution

• we do renaming to avoid name clashes

Example: Rules for Constants

For each constant we have appropriate rule, for example we have and so on, for each pair of integer constants. Similarly, we can introduce conditional constant , writing , with rules and so on.

If we get something like this is a run-time type error

• program would crash at run-time or produce bad result
• we introduce a type system to avoid this