Lambda calculus predecessor function reduction steps

Page 1 of 1

1 Replies - 549 Views - Last Post: 09 January 2012 - 09:41 AM Rate Topic: -----

Topic Sponsor:

#1 rsutvs  Icon User is offline

  • New D.I.C Head

Reputation: 0
  • View blog
  • Posts: 1
  • Joined: 09-January 12

Lambda calculus predecessor function reduction steps

Posted 09 January 2012 - 07:53 AM

I am getting stuck with the Wikipedia description of the predecessor function in lambda calculus.

What Wikipedia says is the following:

PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)

Can someone explain reduction processes step-by-step?

Thanks.
Is This A Good Question/Topic? 0
  • +

Replies To: Lambda calculus predecessor function reduction steps

#2 sepp2k  Icon User is online

  • D.I.C Lover
  • member icon

Reputation: 620
  • View blog
  • Posts: 1,036
  • Joined: 21-June 11

Re: Lambda calculus predecessor function reduction steps

Posted 09 January 2012 - 09:41 AM

Quote

Can someone explain reduction processes step-by-step?


Which reduction process? Do you mean an example reduction of an actual application of PRED? Sure, here's the reduction for PRED 1:

PRED 1
<=>
(λnfx.n (λgh.h (g f)) (λu.x) (λu.u)) (λhy. h y)
<=>
λfx. (λhy. h y) (λgh.h (g f)) (λu.x) (λu.u)
<=>
λfx. (λgh.h (g f)) (λu.x) (λu.u)
<=>
λfx. (λu.u) ((λu.x) f)
<=>
λfx. (λu.u) x
<=>
λfx. x
<=>
0

Was This Post Helpful? 0
  • +
  • -
Page 1 of 1