Introduction

Expression

expression ::= name | function | application

! Body expression can be any kind of expression, including another function

function ::= λname.body where body ::= expression

λx.x ^ x here is a functions bounded value the dot "." separate name from the expression.

This expression is called function's body

application ::= (function_expression argument_expression) where function_expression ::= expressionargument_expression ::= expression

(λx.x λa.λb.b) A function application specializes an abstraction by providing a value for the name. In a function application, also known as a bound pair, the function expression is said to be applied to the argument expression.

1: the function expression is evaluated to return an expression

2: the value of the argument expression - call by value (applicative order reduction - the actual parameter expression is evaluated before being passed to the formal parameter) or the unevaluated argument expression - call by name (normal order - the actual parameter is not being evaluated before being passed to the formal parameter )

3: functional body expression is evaluates

Simple λ function

Identity

λx.x ~ (x) => x

(λx.x λx.x) = ... = λx.x

(x => x)(x => x)

Self application function

λs(s s) - applies its argument to its argument bounded variable s body expression (s s) function expression and argument expression is s

Function application function

λfunc.λarg(func arg) bound variable - func body is functional expression - λarg(func arg) which has bounded variable arg and functional application (func arg) as body expression

this has the name func as function expression and name as argument expression

func => arg => func(arg)

((λfunc.λarg(func arg) λx.x) λs.(s s))

(((func) => (arg) => func(arg))(x => x))(s => s(s))

((λfunc.λarg(func arg) λx.x) - function expression is an application. Must be evaluated first.

bounded value func is replaced by argument λx.x in the body: λarg(func arg) giving: λarg(λx.x arg)

The orginal expression is now (λarg(λx.x arg) λs.(s s)) So the bouned variable arg is replaced by λs.(s s) in body: (λx.x arg) giving: (λx.x λs.(s s))

The bounded variable x is replaced by argument λs.(s s) in body x giving λs.(s s)

Basic function

def identity = λx.x let identity = x => x def self_apply = λs.(s . ) let self_apply = s => s(s) def apply = λfunc.λarg(func arg) let apply = func => arg => func(arg)

(name argument) == (function argument)

β reduction (function argument) => expression to mean that the expression results from the application of the function the unevaluated argument

def identity2 = λx.((apply identity) x)

(identity2 identity) == (λx.((apply identity) x) identity) => ((apply identity) identity) == ((λfunc.λarg(func arg) identity) identity) => λarg(identity arg) identity) => (identity identity) => ... => identity

(identity2 argument) == (λx.((apply identity) x) argument) => ((apply identity) argument) ...=> (identity argument) => ... => argument

identity2 and identity has the same effect

function application function

we can use the function application function to define a function with the same effect as the function application function itself. Suppose: function is any function. Then: (apply function) == ( λfunc.λarg(func arg) function) => λarg.(function arg)

Apply this to any argument we get: (λarg.(function arg) argument) => (function argument)

def self_apply_2 = λs.((apply s) s)

(self_apply_2 identity) == ( λs.((apply s) s) identity) => ((apply identity) identity) => ... { using (apply function) } => (identity identity) => .. => identity

(self_apply_2 argument) == ( λs.((apply s) s) argument) => ((apply argument) argument) => ... => (argument argument)

Selecting arguments

def select_first = λfirst.λsecond.first first => second => first

((select_first identity) apply) == ((λfirst.λsecond.first identity) apply) => (λsecond.identity apply) => identity

((select_first argument1) argument2) == ((λfirst.λsecond.first argument1) argument2) => (λsecond.argument1 argument2) => argument1

argument2 is never used since body of λsecond not contain a reference to it

def select_second = λfirst.λsecond.second

Make pairs

def make_pair = λfirst.λsecond.λfunc.((func first) second)

((make_pair identity) apply) == ((λfirst.λsecond.λfunc.((func first) second) identity) apply) => (λsecond.λfunc.((func identity) second) apply) => λfunc.((func identity) apply)

If this applied to select_first (λfunc.((func identity) apply) select_first) == ((select_first identity) apply) == ((λfirst.λsecond.))

General rule ((make_pair argument1) argument2) == ((λfirst.λsecond.λfunc.((func first) argument1) second) argument2) => (λsecond.λfunc.((func argument1) second) argument2) => λfunc.((func argument1) argument2)

(((make_pair argument1) argument2) select_first) == (λfunc.((func argument1) argument2) select_first) => ((select_first argument1) argument2) == ((λfirst.λsecond.first argument1) argument2) => (λsecond.argument1 argument2) => argument1

(((make_pair argument1) argument2) select_second) => ... => (λsecond.argument2 argument2) => argument2

Simplification though η reduction

λname.(expression name) == expression (λname.(expression name) argument) => (expression argument)

Exercises 1

A

λa.(a λb.(a b))

a - bound value (a λb.(a b)) - expression body. Application where a - function_expression and λb.(a b) - argument expression. Function b - bounded. (a b) - application

B

λx.λy.λz((z x) (z y))

λx - function λy.λz((z x) (z y)) - body λy - function λz((z x) (z y)) - body λz - function ((z x) (z y)) - body: application (z x) - function expression (z y) - expression body

Exercises 2

A

((λx.λy.(y x) λp.λq.p) λi.i) => (λy.(y λi.i) λp.λq.p) => (λp.λq.p λi.i) => λq.λi.i == select_second

((λx.λy.(y x) λp.λq.p) λi.i) => (λy.(y λp.λq.p) λi.i) => (λy.(y λp.λq.p) λi.i) => (λi.i λp.λq.p) => λp.λq.p == select_first

B

((((λx.λy.λz.((x y) z) λf.λa.(f a)) λi.i) λj.j) => ((((λy.λz.(λf.λa.(f a) y) z) λi.i) λj.j) => (((λz.(λf.λa.(f a) λj.j) z) λi.i) => (((λf.λa.(f a) λj.j) λi.i) => ((λa.(λi.i a) λj.j) => (λi.i λj.j) => λj.j

C

(λh.( ( λa.λf.(f a) h) h) λf.(f f)) => ( ( λa.λf.(f a) λf.(f f)) λf.(f f) ) => ( λf.(f λf1.(f1 f1)) λf.(f f)) => (λf.(f f) λf.(f f))

D

( ( λp.λq.(p q) (λx.x λa.λb.a) ) λk.k) => ( ( λq.((λx.x λa.λb.a) q) ) λk.k) => ( λq.((λx.x λa.λb.a) q) λk.k) => ((λx.x λa.λb.a) λk.k) => (λa.λb.a λk.k) => λb.λk.k

E

( ( (λf.λg.λx.(f (g x) ) λs.(s s) ) λa.b.b) λx.y.x) => ( ( λg.λx.(λs.(s s) (g x) ) λa.b.b) λx.y.x) => (λx.(λs.(s s) (λa.b.b λx.y.x)) λa.b.b) => (λs.(s s) (λa.b.b λx.y.x)) => (λs.(s s) λb.b) => (λb.b λb.b) => λb.b ((λa.b.b λx.y.x) (λa.b.b λx.y.x)) => (λb.b (λa.b.b λx.y.x)) => (λa.b.b λx.y.x) => λb.b

Exercises 3

A

(identity argument) => ... => argument

( ( apply ( apply identity ) ) argument) => .. =>
( ( apply identity ) argument) => .. => ( identity argument) => .. => argument

B

((apply function) argument)=> ... => (function argument)

((λx.λy.(((make_pair x) y) identity) function) arguemnt) => (λy.(((make_pair function) y) identity) arguemnt) => (((make_pair function) arguemnt) identity) => .. => (λfunc.((func function) arguemnt) identity ) => ((identity function) arguemnt) => ((identity function) arguemnt) => (function arguemnt)

((make_pair argument1) argument2) == λfunc.((func argument1) argument2)

C

identity arg => arg ((self_apply (self_apply select_second)) arg) => (((self_apply select_second) (self_apply select_second)) arg) => .. => (((select_second select_second) (self_apply select_second)) arg) => .. => ((select_second select_second) arg) => .. => arg

Exercises 4

def make_triplet = λfirst.λsecond.λthird.λfunc(((func first) second) third)

Excrete 5 & 6

a) λx.λy.(λx.y λy.x) ~ λx.λy.(λx1.y λy1.x) b) λx.(x (λy.(λx.x y) x)) ~ λx.(x (λy.(λx1.x1 y) x)) c) λa.(λb.a λb.(λa.a b)) ~ λa.(λb.a λb.(λa1.a1 b)) d) (λfree.bound λbound.(λfree1.free1 bound))

Truth values and conditions

def cond = λe1.λe2.λc((c e1) e2)

( (cond exp1) exp2) == ( ( λe1.λe2.λc((c e1) e2) exp1 ) exp2 ) => ( ( λe2.λc((c exp1) e2) exp2 ) => ( λc((c exp1) exp2)

If function is applied to select first

( ( λc((c exp1) exp2) select_first ) => ((select_first)) => ( ( select_first exp1 ) exp2 ) => .. => exp1

If function is applied to select_second

( ( λc((c exp1) exp2) select_second ) => ( ( select_second exp1 ) exp2 ) => .. => exp2

def true = select_first def false = select_second

def not

def not = λx.((x false) true)

simplifying inner body

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

((λe2.λc((c false) e2) true) x) => (λc((c false) true) x) => ((x false) true)

Not true

(not true) == (λx.((x false) true) true) => ((true false) true) => ((λfirst.λsecond.first false) true) => (λsecond.false true) => false

(not false) == (λx.((x false) true) false) => ((false false) true) => ((λfirst.λsecond.second false) true) => (λsecond.second true) => true

and

Using the selectors, if the left operand is TRUE, then select the right operand and if the left operand is FALSE, then select FALSE, so we will define AND as: def and = λx.λy.((x y) false)

Simplifying the inner body gives: (((cond y) false) true) => .. => ((x y) false)

sample TRUE AND FALSE

((and true) false) == (( λx.λy.((x y) false) true) false) => (λy.((true y) false) false) => ((true false) false) => ((λfirst.λsecond.first false) false) == (λsecond.false false) => false

OR

def or = λx.λy.(((cond true) y) x) = λx.λy.((x true) y)

Natural numbers

Explicitly define natural numbers as successors of zero

1 = successor of 0 2 = successor of 1 successor of successor of 0 3 = successor of 2 successor of successor of 1 successor of successor of successor of 0

etc

def one = (succ zero) def two = (succ one) def three = (succ two)

two == (succ (succ zero)) three == (succ (succ (succ zero)))

def zero = identity def succ = λn.λs((s false) n)

so each time succ is applied to a number n it builds a pair function with false first and the original number second. For example:

one == (succ zero) == (λn.λs.((s false) n) zero) => λs.((s false) zero)

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

three == (succ two) == (λn.λs.((s false) n) two) => (λs.((s false) two) == (λs.((s false) λs.((s false) λs.((s false) zero)))

def iszero

def iszero = λn.(n select_first)

def pred

def pred = λn.(((iszero n) zero) (n select_second))

Simplification notaton

function argument1 argument2 argument3 instead of ( ... ((function argument1) argument2) argument3)

rewrite pred with simplificaton

def pred = λn.((iszero n) n (n select second))

simplify function definition

def names = λname.expression becomes def names name = expression

def identity x = x def self_apply s = s s

def apply func = λarg.(func arg) ~ def apply func arg = func arg

def select_first first = λsecond.first ~ def select_first first second = first

def select_second frist = λsecond.second ~ def select_second frist second = second

def make_pair e1 = λe2.λc(c e1 e2) ~ def make_pair e1 e2 = λс(с e1 e2) ~ def make_pair e1 e2 c = c e1 e2

def cond e1 e2 c = c e1 e2 def true first second = first def false first second = second def not x = x false true def and x y = x y false def or x y = x true y

conditions

if condition then true choise else false choise

def pred n = if iszero n then zero else n select_second

def not = if x then false else true

def and = if x then y else false

def or = if x then true else y

Recursion

ADD

rec add x y = if iszero y then x else add (succ x) (pred y)

MULT

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

POWER

rec power x y = if iszero y then one else mult x (power x (pred y))

Example

powe two three => ... => mult two (pow two (pred three)) -> ... -> mult two (mult two (power two (pred (pred three)))) -> ... -> mult two (mult two (mult two (power two (pred (pred(pred three)))))) -> .. -> mult two (mult two (mult two one)) -> ... -> mult two (mult two two) -> ... -> mult two four => ... => eight

SUB

rec sub x y = if iszero y then x else sub (pred x) (pred y)

Example 1

sub four two => ... => sub (pred four) (pred two) => ... => sub (pred (pred four)) (pred (pred two) ) => ... => (pred (pred four)) => ... => two

Example 2

sub one two => ... => sub (pred one) (pred two) => ... => sub (pred (pred one)) (pred (pred two)) => ... => pred (pred one) => ... => pred zero => ... => zero

ABS_DIFF

def abs_diff x y = add (sub x y) (sub y x)

EQUAL

def equal x y = iszero (abs_diff x y)

Example

equal two three => ... => iszero (abs_diff two three) -> ... -> iszero (add (sub two three) (sub three two)) -> ... -> iszero (add zero one) -> ... -> iszero one => ... => false

EQUAL (rec)

req equal x y = if and (iszero x) (iszero y) then true else if or (iszero x) (iszero y) then false else equal (pred x) (pred y)

Example

equal two two => ... => equal (pred two) (pred two) -> ... -> equal one one => ... => equal (pred one) (pred one) -> ... -> equal zero zero => ... => true

GREATER

def greater x y = not (iszero (sub x y))

GREATER_OR_EQUAL

def greater_or_equal x y = iszero (sub y x)

DIV

req div1 x y = if greater y x then zero else succ (div1 (sub x y) y)

def div x y = if iszero y then zero else div1 x y

Example

div nine four => ... => div1 nine four => ... => succ (div1 (sub nine four) four) -> ... -> succ (div1 five four) -> ... -> succ (succ (div1 (sub five four) four)) -> ... -> succ (succ (div1 one four)) -> ... -> succ (succ zero) -> ... -> two