Introduction to λ-calculus

Uladzimir Abramchuk

Introduction
to λ-calculus

Uladzimir Abramchuk

Introduction to lambda-calculus

λ-calculus

Alonzo Church

λ-expressions

t ::= terms:
v ::= values:

Simple λ functions - Identity

Name Definition JS equivalent
id 
λx.x
 
						function(x) { 
	return x;
}

Simple λ functions - Application

Name Definition JS equivalent
apply 
λf.λx.f x
 
						function(f) { 
	return function(x) { 
		return f(x); 
	}; 
}

Simple λ functions - Self application

Name Definition JS equivalent
self_apply 
λs.s s
 
						function(s) { 
	return s(s); 
}

Scope - Bound variables

x is bound when it occurs in the body t of an abstraction 
λx.t
λ-expression JS equivalent 
λx.x
 
function(x) { return x; }
 
λz.λx.x z
 
function(z) {
	return function(x) {
		return x(z);
	};
}

Scope - Free variables

x is free if it is not bound by any enclosing abstraction on x
λ-expression JS equivalent 
x y
 
x(y)
 
λy.x y
 
function(y) {
	return x(y);
}

Scope

A term with no free variables is said to be closed; closed terms are also called combinators

λ-expression JS equivalent 
(λx.x) x
 
(function(x) { 
	return x; 
})(x)

β reduction

				(λx.t) t2 -> [x := t2]t
			
[x := t2]t
means "the term obtained by replacing all free occurences of x in t by t2"
A term of form 
(λx.t) t2
is called a redex ("reducible expression")

β reduction

λ-expression JS equivalent 
(λx.x) y => y
 
(function(x) { 
	return x; 
})(y) => y

Normal order β reduction

The leftmost, outermost redex is always reduced first
Works similar to if-clause in JS

			id (id (λz.id z)) =>
			id (λz.id z) =>
			λz.id z =>
			λz.z

Applicative order β reduction

Only outermost redexes are reduced and a redex is reduced only when its right-hand side has already been reduced to a value
Works similar to function call in JS

			id (id (λz.id z)) ->
			id (λz.id z) ->
			λz.id z
Evaluation termination

Evaluation termination

There is no way of telling whether or not the evaluation of an expression will ever terminate!

(λs.s s) (λs.s s) //Won't terminate!

A term is in normal form if no β reduction is possible

1st Church-Rosser theorem

If there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions

A term in the λ-calculus has at most one normal form

2nd Church-Rosser theorem

If an expression has a normal form, then it may be reached by normal order evaluation

α conversion

λx.λy.(x y) y => λy.y y //Wrong!
			λx.λy.(x y) y == //α-rename bound variable y into z
			λx.λz.(x z) y =>
			λz.y z

η conversion

Two functions are the same if and only if they give the same result for all arguments

λ-expression JS equivalent 
λx.expr x
 
function(x) { 
	return expr(x); 
}
 
expr
 
expr

Currying (schönfinkeling)

λx.λy.x y
Original Curried 
function(x, y) {
	return x(y);
}
 
function(x) {
	return function(y) {
		return x(y);
	};
}

Partial application

Partial function application says "if you fix the first arguments of the function, you get a function of the remaining arguments"

Original Partially applied 
λf.λx.f x
 
λx.id x
 
function(f, x) {
	return f(x);
}
 
function(x) {
	return id(x);
}

Notation

def name = function
def id = λx.x
def self_apply = λs.s s
def apply = λfunc.λarg.func arg
//This works only as textual replacement!

Notation

== defined replacement notation
=> normal order β reduction
=> ... => multiple normal order β reduction
-> applicative order β reduction
-> ... -> multiple applicative order β reduction

Selecting one of two arguments

def fst = λf.λs.f
def snd = λf.λs.s
			(fst arg1) arg2 == 
			((λf.λs.f) arg1) arg2 => 
			(λs.arg1) arg2 => 
			arg1

Making pairs from two arguments

def pair = λf.λs.λfunc.(func f) s
			(pair arg1) arg2 == 
			((λf.λs.λfunc.(func f) s) arg1) arg2 => 
			(λs.λfunc.(func arg1) s) arg2 => 
			λfunc.(func arg1) arg2

Selecting second argument from pair

			(λfunc.(func arg1) arg2) snd =>
			(snd arg1) arg2 => ... =>
			arg2

Booleans and conditions

Booleans

condition ? expression : expression

			def cond = λe1.λe2.λc.(c e1) e2
def true = fst
def false = snd

Booleans

			def not = λx.((cond false) true) x
def and = λx.λy.(x y) false
def or = λx.λy.(x true) y

Booleans

			((cond y) false) x == 
			(((λe1.λe2.λc.(c e1) e2) y) false) x => 
			((λe2.λc.(c y) e2) false) x => 
			(λc.(c y) false) x => 
			(x y) false

Natural numbers and arithmetics

Natural numbers

			def zero = id
def succ = λn.λs.(s false) n
def one = succ zero
def two = succ one == succ (succ zero)
...

Natural numbers

			def iszero = λn.n fst
def pred = λn.((iszero n) zero) (n snd)

Natural numbers

			iszero zero => 
			(λn.n fst) zero => 
			zero fst == 
			id fst => 
			fst == 
			true

Natural numbers

			iszero (λs.(s false) num) == 
			(λn.n fst) (λs.(s false) num) => 
			(λs.(s false) num) fst => 
			(fst false) num => ... => 
			false

Notation

function arg1 arg2 ... argN

instead of 
(...((function arg1) arg2) ... argN)
def pred = λn.(iszero n) zero (n snd)

instead of 
def pred = λn.((iszero n) zero) (n snd)

Notation

def names name = expression

instead of 
def names = λname.expression
def id x = x
def self_apply s = s s
def fst f = λs.f

Notation

if ... then ... else ...

instead of 
cond true_choice false_choice condition
def pred n = if iszero n
				then zero
				else n snd

Addition

def add x y = if iszero y
				 then x
				 else add (succ x) (pred y)
//Doesn't work this way! 
//All names in expressions must be replaced by their 
//definitions before the expression is evaluated!
//Inner add will be substituted infinitely...

Recursion

def rec = λf.(λs.f (s s)) (λs.f (s s))//Y combinator
def add1 f x y = if iszero y
					then x
					else f (succ x) (pred y)
def add = rec add1

Notation

rec name = expression
rec add x y = if iszero y
				 then x
				 else add (succ x) (pred y)
rec mult x y = if iszero y
				  then zero
				  else add x (mult x (pred y))

Arithmetic operations

rec sub x y = if iszero y
				 then zero
				 else sub (pred x) (pred y)
def abs_diff = add (sub x y) (sub y x)
def equal x y = iszero (abs_diff x y)

Types

Representing typed objects

def make_obj type value = λs.s type value
def type obj = obj fst
def value obj = obj snd
def istype t obj = equal (type obj) t

Errors

def error_type = zero
def MAKE_ERROR = make_obj error_type
def ERROR = MAKE_ERROR error_type
def iserror = istype error_type

Booleans

def bool_type = one
def MAKE_BOOL = make_obj bool_type
def TRUE = MAKE_BOOL true
def FALSE = MAKE_BOOL false
def isbool = istype bool_type
def BOOL_ERROR = MAKE_ERROR bool_type

Booleans

def COND E1 E2 C = if isbool C 
					  then if value C 
					  		  then E1
							  else E2
					  else BOOL_ERROR

Notation

IF condition THEN expr1 else expr2

instead of 
COND expr1 expr2 condition
def NOT X = IF X
			THEN FALSE
			ELSE TRUE

Natural numbers

def numb_type = two
def MAKE_NUMB = make_obj numb_type
def NUMB_ERROR = MAKE_ERROR numb_type
def ISNUMB N = MAKE_BOOL (isnumb N)

Natural numbers

def SUCC N = if isnumb N
				then MAKE_NUMB (succ (value N))
			 	else NUMB_ERROR
def PRED N = if isnumb N
			 	then if iszero (value N)
				  		then NUMB_ERROR
				  		else MAKE_NUMB ((value N) select_second)
			 	else NUMB_ERROR

Lists

Lists

def list_type = three
def islist = istype list_type
def ISLIST L = MAKE_BOOL (islist L)
def MAKE_LIST = make_obj list_type

Lists

def CONS H T = if islist T
				  then MAKE_LIST λs.(s H T)
				  else LIST_ERROR
def NIL = MAKE_LIST λs.(s LIST_ERROR LIST_ERROR)

Lists

def HEAD L = if islist L
				then (value L) fst
				else LIST_ERROR
def TAIL L = if islist L
				then (value L) snd
				else LIST_ERROR

Lists

def ISNIL = if islist L
			   then MAKE_BOOL (iserror (HEAD L))
			   else LIST_ERROR

Q&A

Further reading

  1. Structure and Interpretation of Computer Programs
  2. An Introduction to Functional Programming Through Lambda Calculus
  3. Types and Programming Languages

Introduction to λ-calculus

Slides: http://bit.ly/NH99es

Email: u.abramchuk@gmail.com
Github: http://github.com/u-abramchuk

Uladzimir Abramchuk

Thank you!