CODEWITHSUNDEEP
functional-programminglambdalambda-calculus
Srikrishnan Suresh
Srikrishnan Suresh

Reputation: 729

Add4 Using Lambda Expression

I know that using lambda expressions, we can write succ = λnfx • f (n f x ) and twice = λfn • f f(n ). My aim now is to write add4 using these two which adds 4 to the church numerals.

How do I write the beta-reduction steps for this?

Thanks for the help in advance...

Upvotes: 0

Views: 89

Answers (1)

Jack
Jack

Reputation: 2273

Well, twice succ is a function that applies succ twice, so twice (twice succ) is a function that applies twice succ twice, thereby applying succ four times. So it should just be add4 = twice (twice succ).

twice = λf.λn.(f (f n))
twice (twice succ)
=> twice (λf.λn.(f (f n)) succ)
=> twice λn.(succ (succ n))
=> λf.λn.(f (f n)) λn.(succ (succ n))
=> λf.λn.(f (f n)) λx.(succ (succ x))
=> λn.(λx.(succ (succ x)) (λx.(succ (succ x)) n))
=> λn.(λx.(succ (succ x)) (succ (succ n)))
=> λn.(succ (succ (succ (succ n))))
=> λn.(succ (succ (succ (succ n))))

Upvotes: 3

Related Questions