lambdaway :: lambda_calculus

5 | list | login |load

| |

_h1 [[lambda_calculus]] {sup {sup (iteration only)}}

_p In this paper we explore the iterative nature of church numerals.

_h2 church numerals

_p In pure λ-calculus natural numbers don't exist. Alonzo Church defined [0,1,2,3,...,n] as successive functions waiting for 2 values. The set of Church numerals, [{b C0, C1, C2, ..., CN}] is built using a {b C0} starting function and the {b successor} function, defined this way in the lambdatalk syntax:

{pre
1) '{def C0 {lambda {:f :x} :x}}
-> {def C0 {lambda {:f :x} :x}}

2) '{def succ {lambda {:n :f :x} {:f {:n :f :x}}}}
-> {def succ {lambda {:n :f :x} {:f {:n :f :x}}}}
}

_p Here are the first ones following {b C0}

{pre
'{def C1 {succ {C0}}} -> {def C1 {succ {C0}}}
'{def C2 {succ {C1}}} -> {def C2 {succ {C1}}}
'{def C3 {succ {C2}}} -> {def C3 {succ {C2}}}
}

_p A church numbers {b CN} can be generaly defined this way

{pre
'{def CN {lambda {:f :x} {:f {:f {:f ... N times ... {:f :x}}}}}}
}

_p highlighting its true nature of {b iterator} applying N times a function to a value. This is a powerful property which will be used in the followings to build some arithmetical operators working on church numerals.

_p And first to build a useful function displaying church numerals as natural numbers :

{pre
'{def church
 {lambda {:n}
  {:n                         // apply n times
      {lambda {:x} {+ :x 1}}  // the increment function
      0                       // to the initial value 0
}}}
-> {def church {lambda {:n} {:n {lambda {:x} {+ :x 1}} 0} }}

'{church {C0}} -> {church {C0}}
'{church {C1}} -> {church {C1}}
'{church {C2}} -> {church {C2}}
'{church {C3}} -> {church {C3}}
}

_p For the {b add(n,m)} function we iterate n times {b succ} on {b m}

{pre 
add=λ n.λ m.nsucm ;; {def add {lambda {:n :m :f :x} {{:n :f} {:m :f :x}}}}

'{def add {lambda {:n :m} {:n succ :m}}}  
-> {def add {lambda {:n :m} {:n succ :m}}}

'{church {add {C2} {C3}}}
-> {church {add {C2} {C3}}}
}

_p For the {b mul(n,m)} function we iterate n times {b '{add :m}} on {b C0}

{pre
mult=λ n.λ m.n(addm)0 ;; {def mul {lambda {:n :m :f :x} {:n {:m :f} :x}}}

'{def mul {lambda {:n :m} {:n {add :m} {C0}}}}
-> {def mul {lambda {:n :m} {:n {add :m} {C0}}}}

'{church {mul {C2} {C3}}}
-> {church {mul {C2} {C3}}}
}

_p Here is the {b exp(n,m)} function

{pre
exp=λ n.λ m.mn

'{def pow {lambda {:n :m :f :x} {{:m :n :f} :x}}}
-> {def pow {lambda {:n :m :f :x} {{:m :n :f} :x}}}

'{church {pow {C2} {C3}}}
-> {church {pow {C2} {C3}}}
}

_h2 the predecessor

_p Geting the predecessor of a church numeral is tricky. The idea is in this iterative algorithm:

{pre
pair = [0,0]
repeat 6 times
    pair = [pair[1],pair[1]+1]
return pair[0]
}

_p Let's trace the successive states of {b pair}

{pre
0: [1 , 0]             
1: [0 , 0+1]           = [0,1]
2: [1 , 1+1]           = [1,2]
3: [2 , 2+1]           = [2,3]
4: [3 , 3+1]           = [3,4]
5: [4 , 4+1]           = [4,5]
6: [5 , 5+1]           = [5,6] -> precedent of 6 is 5
}

_p So we build a tool to aggregate two terms, the {b pair}

{pre
'{def pair {lambda {:a :b :m} {:m :a :b}}} 
-> {def pair {lambda {:a :b :m} {:m :a :b}}}   
'{def left {lambda {:p} {:p {lambda {:x :y} :x}}}} 
-> {def left {lambda {:p} {:p {lambda {:x :y} :x}}}}
'{def right {lambda {:p} {:p {lambda {:x :y} :y}}}} 
-> {def right {lambda {:p} {:p {lambda {:x :y} :y}}}}

'{def 56 {pair 5 6}}
-> {def 56 {pair 5 6}}
'{left {56}}
-> {left {56}}
'{right {56}}
-> {right {56}}
}

_p We define the function {b pred.fun} to be iterated

{pre
'{def pred.fun
 {lambda {:p}
  {pair {right :p} {succ {right :p}}}}}
-> {def pred.fun {lambda {:p} {pair {right :p} {succ {right :p}}}} }
}

_p and the function {b pred} which applies {b pred.fun} to the initial value {b '{pair {C1} {C0}}}

{pre
'{def pred
 {lambda {:n} 
  {left {:n pred.fun {pair {C0} {C0}}}}}}  
-> {def pred {lambda {:n} {left {:n pred.fun {pair {C1} {C0}}}}}}
}

_p and finally returns the left term of the pair.

{pre
'{church {pred {mul {C2} {C3}}}}    // pred(2*3) = pred(6)
-> {church {pred {mul {C2} {C3}}}}
}

_p We can now subtract two numbers

{pre
'{def subtract {lambda {:m :n} {{:n pred} :m}}}
-> {def subtract {lambda {:m :n} {{:n pred} :m}}}

'{church {subtract {C3} {C2}}} 
-> {church {subtract {C3} {C2}}}

}

_h2 fibonacci

_p Defined using this. iterative algorithm:

{pre
p = [0,1]
repeat 6 times
    p = [p[1],p[0]+p[1]]
return p[0]
}

_p Let's trace {b fib(6)}:

{pre
0: [0 , 1]             
1: [1 , 0+1]           = [1,1]
2: [1 , 1+1]           = [1,2]
3: [2 , 1+2]           = [2,3]
4: [3 , 2+3]           = [3,5]
5: [5 , 3+5]           = [5,8]
6: [8 , 5+8]           = [8,13] -> fib(6) = 8
}

_p We define the function fib.fun to be iterated

{pre
'{def fib.fun
 {lambda {:p}
  {pair {right :p} {add {left :p} {right :p}}}}}
-> {def fib.fun {lambda {:p} {pair {right :p} {add {left :p} {right :p}}}}}
}

_p and the function {b fib} applying {b fib.fun} to the initial value {b '{pair {C0} {C1}}}
{pre
'{def fib
 {lambda {:n}
  {left {:n fib.fun {pair C0 C1}}}}}    
-> {def fib {lambda {:n} {left {:n fib.fun {pair {C0} {C1}}}}}}
}

_p and finally returns the left term of the pair.

{pre
fib(6) = '{church {fib {mul {C2} {C3}}}} 
-> {church {fib {mul {C2} {C3}}}}
}

_h2 factorial

_p The iterative algorithm:

{pre
p = [1,1]
repeat 6 times
    p = [p[0]+1,p[0]*p[1]]
return p[1]
}

_p Let's trace {b fac(6)}:

{pre
1: [1 , 1]             
2: [2 , 1*2]           = [1,2]
3: [3 , 1*2*3]         = [1,6]
4: [4 , 1*2*3*4]       = [1,24]
5: [5 , 1*2*3*4*5]     = [1,120]
6: [6 , 1*2*3*4*5*6]   = [1,720] -> fac(6) = 720
}

_p We define the function fac.fun to be iterated

{pre
'{def fac.fun
 {lambda {:p}
  {pair {succ {left :p}} {mul {left :p} {right :p}}}}}
-> {def fac.fun {lambda {:p} {pair {succ {left :p}} {mul {left :p} {right :p}}}}}
}

_p and the function {b fac} applying {b fac.fun} to the initial value {b '{pair {C1} {C1}}}

{pre
'{def fac
 {lambda {:n}
  {right {:n fac.fun {pair {C1} {C1}}}}}}
-> {def fac {lambda {:n} {right {:n fac.fun {pair {C1} {C1}}}}}}
}

_p and finally returns the right term of the pair.

{pre
'{church {fac {add {C2} {C3}}}} 
-> {church {fac {add {C2} {C3}}}} 
}

_p Note that for [[Parigot|https://homepage.divms.uiowa.edu/~astump/talks/colloq-10-24-2014.pdf]] numbers are {b recursors}... For me the answer is in [[λ-calculus using binary numbers of variable length|?view=oops6]].

_p {i alain marty | 2022/02/19}

{style 
pre {box-shadow:0 0 8px; padding:10px;} 
}