💾 Archived View for soviet.circumlunar.space › ayb › notes › lambda.gmi captured on 2022-06-03 at 23:36:47. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Lambda Calculus

Plan

Definition
Beta reduction
Alpha conversion
Eta conversion
De Bruijn indices
Church encoding
Scott encoding
Boehm-Berarducci encoding
Parigot encoding
Stump-Fu encoding

Definition

Lambda calculus is a formal mathematical system allowing expression of functions in a simple form. It has three types of expressions which, formulated in BNF are:

e ::= v      (variable)
      (e e') (application)
      \v.e   (lambda abstraction)

where e and e' are expressions and v is a variable.

Syntactic sugar is often added:

\ab->e  <=> \a->(\b.e)    where you can have an aribtrary number of variables
f x y z <=> (((f x) y) z) where f can have an aribtrary number of arguments

Bound and free variables

In the expression "\x.E", the variable x is bound, meaning that it is definied in the expression, whereas in the expression "\x.x", the variable y is free, meaning that it has not been definied.

Beta reduction

Beta reduction is lambda calculus' function application, i.e. the expression "(\x.E1)E2", will be reduced to E1 where all the free occurences of x in E1 will be replaced by E2. Sometimes, these reductions can lead to name clashes, thus alpha conversion is requiered if De Bruijn indices are not used.

Alpha conversion

Alpha conversion is useful when different lambda abstractions use the same variable name, which calling may result in name clashes. To solve that problem, alpha conversion renames bound variable, stating that variable are anonymous, i.e. "\y.y" and "\x.x" are equivalent terms. Such terms will have the same representation with De Bruijn indices.

Eta conversion

Eta conversion is a simple conversion allowing simplification of expression of the form "\x.(fx)", converting it to "f". This means that taking an argument and calling f with it is calling

De Bruijn indices

De Bruijn indices are an alternative representation of lambda expressions, variable names are eliminated because they are meaningless. Instead, indices are used, they refer to the number of outer lambdas before before the one binding the variable, i.e. the expression "\x.x" will be "\0" and the expression "\xy.x" will become "\\1". Thus this system removes the necessity of alpha conversion and simplifies beta reduction.

Church encoding

Since lambda calculus only contains functions, to use usual data types - such as integers, booleans or lists - one needs a way to represent these only using function. One of the first way to do that has been found by Church.

Booleans

Booleans are defined like that:

True  = \x y -> x
False = \x y -> y

You can implement basic logic operations:

not a = a False True
or a b  = a True b
and a b = a b False

You can implement conditionals:

if c t f = c t f

Integers

Pairs

Lists

Scott encoding

Scott-Morgenssen encoding provides a simple way to translate ADTs in lambda expressions and easily do pattern matching on them. The i'th constructor with j arguments of an ADT with n constructors is encoded as follows:

c_i a_1 a_2 ... a_j = \p_1 p_2 ... p_i ... p_n -> (p_i a_1 a_2 ... a_j)

Pattern-matching is can be translated easily, i.e:

case e of
  C1 a_1 ... a_i -> e_1
  C2 a_1 ... a_j -> e_2
  ...
  Cn a_1 ... a_k -> e_n

becomes:

e (\a_1 ... a_i -> e_1 a_1 ... a_i) 
  (\a_1 ... a_j -> e_2 a_1 ... a_j) 
  ... 
  (\a_1 ... a_k -> e_n a_1 ... a_k)

We can, now, implement basic ADTs.

data Bool = True | False

True  = \x y -> x
False = \x y -> y

data Peano = Zero | Succ Peano

Zero   = \x y -> x
Succ n = \x y -> y n

data List a = Nil | Cons a (List a)

Nil      = \x y -> x
Cons h t = \x y -> y h t