CODEWITHSUNDEEP
lambda-calculus
Ofek Ron
Ofek Ron

Reputation: 8580

How to interpret a lambda calculus expression?

say I am given the expression (i will refer to l as lambda):

lx.f1 f2 x

where f1 and f2 are functions and x suppose to some number.

how do you interpret this expression? is lx.(f1 f2) x the same as lx.f1 (f2 x)?

as an exemple, what will be the diffrence in the result of lx.(not eq0) x and lx.not (eq0 x)? (eq0 is a function that return true if the parm equals 0 and not is the well known not function)

more formally T=lx.ly.x ,F=lx.ly.y ,not = lx.xFT and eq0 = lx.x(ly.F)T

Upvotes: 1

Views: 241

Answers (1)

sepp2k
sepp2k

Reputation: 370142

f1 f2 x is the same as (f1 f2) x. Function application is left-associative.

is ln.(f1 f2) x the same as ln.f1 (f2 x)?

No, not at all. (f1 f2) x calls f1 with f2 as its argument and then calls the resulting function with x as its argument. f1 (f2 x) calls f2 with x as its argument and then calls f1 with the result of f2 x as its argument.

ln.(not eq0) x and ln.not (eq0 x)?

If we're talking about a typed lambda calculus and not expects a boolean as an argument, the former will simply cause a type error (because eq0 is a function and not a boolean). If we're talking about the untyped lambda calculus and true and false are represented as functions, it depends on how not is defined and how true and false are represented.

If true and false are Church booleans, i.e. true is a two-argument function that returns its first argument and false is a two-argument function that returns its second argument, then not is equivalent to the flip function, i.e. it takes a two-argument function and returns a two-argument function whose arguments have been reversed. So (not eq0) x will return a function that, when applied to two other arguments y and z, will evaluate to ((eq0 y) x) z. So if y is 0, it will return x, otherwise z.

Upvotes: 2

Related Questions