💾 Archived View for soviet.circumlunar.space › ayb › notes › lambda.gmi captured on 2023-07-10 at 13:47:58. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2021-12-03)
-=-=-=-=-=-=-
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
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 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 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 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 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.
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 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
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