# 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

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