lambdaway :: lambdacode5

2 | list | login |load

| |

{require lib_lambdacode}

_h1 lambdacode {sup ( [[1|?view=lambdacode]] | [[2|?view=lambdacode2]] | [[3|?view=lambdacode3]] | [[4|?view=lambdacode4]] | 5) }

{{block}
_h1 introduction

_p The innumerable introductions to lambda-calculus do not shine by their simplicity, one immediately penetrates into what some call "The roaring forties" of computer programming and, suddenly, finds oneself struggling with condensed notations, various modes of reduction, free or bound variables, Church's numbers and on to top of it the strange Y-combinator, final barrier to cross before accessing the divine recursion. See for instance [[wikipedia|http://en.wikipedia.org/wiki/Lambda_calculus]].

_p In this page, merely inspired by [[Collected Lambdas|http://jwodder.freeshell.org/lambda.html]], we compare two dialects of λ-calculus, lambdatalk and lambdacode, giving freely editable {b active codes}.

_p 1) [[{b λ-calculus}|?view=lambda_calculus]]  is a formal language created in the 30s by Alonzo Church and is considered as the father of, at least, functional programming languages like LISP, SCHEME, ... Numerous presentations have been done - see section references - using a rather terse notation and without any details about implementation, making understanding difficult. Moreover algorithms can't be tested in real time, everything must be done by hand.

_p 2) [[{b lambdacode}|?view=lambdacode]] is a dialect of λ-calculus built on a standard implementation where lambdas can have {b free variables} getting their values from the lexical context, as LISP and SCHEME do. Moreover algorithms can be tested in the very wiki page.

_p 3) [[{b lambdatalk}|?view=fromroots2canopy]] is a dialect of λ-calculus built on a non standard implementation, using an inverted evaluator where lambdas are pure functions independant of any context, let alone the global one where are defined global constants and primitives. As a consequence, lambdas can't have {b free variables} getting their value from the lexical context, the {b closure} property. The lack of closure can be compensated using {b IIFE}s, Immediately Invoked Function Expressions, and thanks to the fact that lambdas can natively be partially applied. The current wiki page is coded using lambdatalk and obviously all algorithms can be tested in it.

_p In the following we build the bricks from scratch, booleans, pairs, lists, loops and some arithmetic.

_p As a quick introduction to the lambdatalk syntax, this is how can be defined some {b smart_add} function:

{pre
'{def smart_add
 {lambda {:a :b}
  The sum of :a and :b is equal to {+ :a :b}}}
-> {def smart_add
 {lambda {:a :b}
  The sum of :a and :b is equal to {+ :a :b}}}

'{smart_add 3 4}
-> {smart_add 3 4}
}

_p and the equivalent using the lambdacode syntax

{pre {lc
(def smart_add
 (lambda (a b)
  (join 'The 'sum 'of a 'and b 'is 'equal 'to (+ a b))))
-> _(def smart_add
 (lambda (a b)
  (join 'The 'sum 'of a 'and b 'is 'equal 'to (+ a b))))_

(smart_add 3 4)
-> _(smart_add 3 4)_
}}

_p Note how in lambdatalk words are not protected and function's arguments are prefixed with a colon "{b :}" and how in lambdacode words must be protected by a quote "{b '}" and function's arguments are free of any protection. Lambdatalk is intended for easy text writing with small portions of code. Lambdacode is intended for easy coding with full protected strings of texts. A matter of choice.

_p {i alain marty | 2021/10/21}
 
}  ;; end block

{{block}
_h1 lambdatalk version
_h2 booleans

{pre
TRUE := λxy. x 
FALSE := λxy. y 
AND := λpq. p q p
OR := λpq. p p q
XOR := λpq. p (NOT q) q
NOT := λpab. p b a ≡ λp. p FALSE TRUE
}

{pre
'{def TRUE {lambda {:a :b} :a}} 
-> {def TRUE {lambda {:a :b} :a}}
'{def FALSE {lambda {:a :b} :b}}
-> {def FALSE {lambda {:a :b} :b}}
'{def IF {lambda {:c :a :b}  {:c :a :b}}}
-> {def IF {lambda {:c :a :b}  {:c :a :b}}}

'{def AND {lambda {:a :b} {IF :a :b FALSE}}}
-> {def AND {lambda {:a :b} {IF :a :b FALSE}}}
'{def OR {lambda {:a :b} {IF :a TRUE :b}}}
-> {def OR {lambda {:a :b} {IF :a TRUE :b}}}
'{def NOT {lambda {:a} {IF :a FALSE TRUE}}}
-> {def NOT {lambda {:a} {IF :a FALSE TRUE}}}

'{def XOR
 {lambda {:a :b} 
  {OR {AND :a {NOT :b}}
      {AND :b {NOT :a}}}}}
-> {def XOR
 {lambda {:a :b} 
  {OR {AND :a {NOT :b}}
      {AND :b {NOT :a}}}}}
}

_h2 pairs & lists

{pre
PAIR := λxyf. f x y
CAR := λp. p TRUE
CDR := λp. p FALSE
NIL := λx. TRUE
NULL := λp. p (λxy. FALSE)
}

{pre
'{def PAIR {lambda {:a :b :c} {:c :a :b}}}
-> {def PAIR {lambda {:a :b :c} {:c :a :b}}}
'{def LEFT {lambda {:p} {:p TRUE}}}
-> {def LEFT {lambda {:p} {:p TRUE}}}
'{def RIGHT {lambda {:p} {:p FALSE}}}
-> {def RIGHT {lambda {:p} {:p FALSE}}}

'{def NIL {lambda {:a} TRUE}}
-> {def NIL {lambda {:a} TRUE}}  
'{def ISNIL {lambda {:p} {:p {lambda {:a :b} FALSE}}}}
-> {def ISNIL {lambda {:p} {:p {lambda {:a :b} FALSE}}}}

'{def DISP
 {lambda {:l}
  {{IF {ISNIL :l}
     {lambda {:l} }
     {lambda {:l} {LEFT :l} {DISP {RIGHT :l}}}}
              :l}}}
-> {def DISP
 {lambda {:l}
  {{IF {ISNIL :l}
       {lambda {:l} }
       {lambda {:l} {LEFT :l} {DISP {RIGHT :l}}}} :l}}}
 
'{def FRUITS
 {PAIR apple
  {PAIR banana
   {PAIR lemon
    {PAIR grapes
     {PAIR orange NIL}}}}}}
-> {def FRUITS
 {PAIR apple
  {PAIR banana
   {PAIR lemon
    {PAIR grapes
     {PAIR orange NIL}}}}}}

'{DISP {FRUITS}}
-> {DISP {FRUITS}}
}

_h2 hanoï

{pre
'{def HANOI          
 {lambda {:n :from :to :via}
  {{IF {ISNIL :n}
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
           {HANOI {RIGHT :n} :from :via :to}
           {br} move {LEFT :n} from tower :from to tower :to 
           {HANOI {RIGHT :n} :via :to :from} }}
            :n :from :to :via}}}
-> {def HANOI          
 {lambda {:n :from :to :via}
  {{IF {ISNIL :n}
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {HANOI {RIGHT :n} :from :via :to}
      {div} move {LEFT :n} from tower :from to tower :to 
    {HANOI {RIGHT :n} :via :to :from} }}
   :n :from :to :via}}}

'{def DISKS
 {PAIR DISK_1
 {PAIR DISK_2
 {PAIR DISK_3
 {PAIR DISK_4
 {PAIR DISK_5 NIL}}}}}}
-> {def DISKS
 {PAIR DISK_1
 {PAIR DISK_2
 {PAIR DISK_3
 {PAIR DISK_4
 {PAIR DISK_5 NIL}}}}}}

'{HANOI {DISKS} A B C}
->
{HANOI {DISKS} A B C}
}

_h2 more on lists

{pre
'{def REV
 {def REV.r
  {lambda {:a :b}
   {{IF {ISNIL :a}
    {lambda {:a :b} :b}
    {lambda {:a :b} {REV.r {RIGHT :a}
                           {PAIR {LEFT :a} :b} }}}
             :a :b}}}
 {lambda {:a}
  {REV.r :a NIL}}}
-> {def REV
 {def REV.r
  {lambda {:a :b}
   {{IF {ISNIL :a}
    {lambda {:a :b} :b}
    {lambda {:a :b} {REV.r {RIGHT :a} {PAIR {LEFT :a} :b} }}}
             :a :b}}}
 {lambda {:a}
  {REV.r :a NIL}}}

'{DISP {REV {FRUITS}}}
-> {DISP {REV {FRUITS}}}

'{def LENGTH
 {lambda {:l}
  {{IF {ISNIL :l}
   {lambda {:l} ZERO}
   {lambda {:l} {SUCC {LENGTH {RIGHT :l}}}}}
            :l}}}
-> {def LENGTH
 {lambda {:l}
  {{IF {ISNIL :l}
       {lambda {:l} ZERO}
       {lambda {:l} {SUCC {LENGTH {RIGHT :l}}}}} :l}}}

'{church {LENGTH {FRUITS}}}
-> {church {LENGTH {FRUITS}}}

'{def APPEND
 {def APPEND.r
  {lambda {:a :b}
   {{IF {ISNIL :b}
    {lambda {:a :b} :a}
    {lambda {:a :b} {APPEND.r {PAIR {LEFT :b} :a}
                              {RIGHT :b}}}}
             :a :b}}}
 {lambda {:a :b}
  {APPEND.r :b {REV :a} }}}
-> {def APPEND
 {def APPEND.r
  {lambda {:a :b}
   {{IF {ISNIL :b}
    {lambda {:a :b} :a}
    {lambda {:a :b} {APPEND.r {PAIR {LEFT :b} :a} {RIGHT :b}}}} :a :b}}}
 {lambda {:a :b}
  {APPEND.r :b {REV :a} }}}

'{DISP {APPEND {FRUITS} {DISKS}}}
-> {DISP {APPEND {FRUITS} {DISKS}}}

INDEX := λxi. CAR (i CDR x)

'{def INDEX
 {lambda {:x :i}
  {{IF {ISZERO :i}
   {lambda {:x :i} {LEFT :x}}
   {lambda {:x :i} {INDEX {RIGHT :x} {PRED :i}}}}
            :x :i}}}
-> {def INDEX
 {lambda {:x :i}
  {{IF {ISZERO :i}
   {lambda {:x :i} {LEFT :x}}
   {lambda {:x :i} {INDEX {RIGHT :x} {PRED :i}}}}
            :x :i}}}

'{INDEX {FRUITS} ZERO}  
-> {INDEX {FRUITS} ZERO}
'{INDEX {FRUITS} ONE}
-> {INDEX {FRUITS} ONE}
'{INDEX {FRUITS} TWO}
-> {INDEX {FRUITS} TWO}
'{INDEX {FRUITS} THREE}
-> {INDEX {FRUITS} THREE}

'{def LAST {lambda {:l} {LEFT {REV :l}}}}
-> {def LAST {lambda {:l} {LEFT {REV :l}}}}

'{LAST {FRUITS}}
-> {LAST {FRUITS}}

'{def BUTLAST {lambda {:l} {REV {RIGHT {REV :l}}}}}
-> {def BUTLAST {lambda {:l} {REV {RIGHT {REV :l}}}}}

'{DISP {BUTLAST {FRUITS}}}
-> {DISP {BUTLAST {FRUITS}}}

'{def RANGE
 {def RANGE.r
  {lambda {:a :b :c}
   {{IF {GT :a :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {RANGE.r {SUCC :a} :b {PAIR :a :c}}}} 
             :a :b :c}}}
 {lambda {:a :b}
  {REV {RANGE.r :a :b NIL}}}}
-> {def RANGE
 {def RANGE.r
  {lambda {:a :b :c}
   {{IF {GT :a :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {RANGE.r {SUCC :a} :b {PAIR :a :c}}}} :a :b :c}}}
 {lambda {:a :b}
  {REV {RANGE.r :a :b NIL}}}}

'{def MAP
 {lambda {:f :x}
  {{IF {ISNIL :x}
   {lambda {:f :x} }
   {lambda {:f :x} {:f {LEFT :x}} {MAP :f {RIGHT :x}}}} 
            :f :x}}}
-> {def MAP
 {lambda {:f :x}
  {{IF {ISNIL :x}
   {lambda {:f :x} }
   {lambda {:f :x} {:f {LEFT :x}} {MAP :f {RIGHT :x}}}} :f :x}}}

'{MAP church {RANGE TWO {MUL THREE THREE}}}
-> {MAP church {RANGE TWO {MUL THREE THREE}}}

'{MAP {lambda {:i} {church {POW TWO :i}}}
     {RANGE ONE {MUL THREE THREE}}} 
-> {MAP {lambda {:i} {church {POW TWO :i}}} {RANGE ONE {MUL THREE THREE}}}

'{def REDUCE
 {lambda {:f :z :x}
  {{IF {ISNIL :x}
   {lambda {:f :z :x} :z}
   {lambda {:f :z :x} {REDUCE :f {:f {LEFT :x} :z} {RIGHT :x}}}}
            :f :z :x}}}
-> {def REDUCE
 {lambda {:f :z :x}
  {{IF {ISNIL :x}
   {lambda {:f :z :x} :z}
   {lambda {:f :z :x} {REDUCE :f {:f {LEFT :x} :z} {RIGHT :x}}}} :f :z :x}}}

'{church {REDUCE ADD ZERO {RANGE ONE {MUL THREE THREE}}}}
-> {church {REDUCE ADD ZERO {RANGE ONE {MUL THREE THREE}}}}
}

} ;; end block

{{block}
_h1 lambdacode version

_h2 booleans

{pre
TRUE := λxy. x 
FALSE := λxy. y 
AND := λpq. p q p
OR := λpq. p p q
XOR := λpq. p (NOT q) q
NOT := λpab. p b a ≡ λp. p FALSE TRUE
}

{pre {lc 
(def TRUE (lambda (a b) a))
-> _(def TRUE (lambda (a b) a))_
(def FALSE (lambda (a b) b))
-> _(def FALSE (lambda (x y) y))_
(def IF (lambda (a b c) (a b c)))
-> _(def IF (lambda (x y z) (x y z)))_

(def AND (lambda (a b) (IF a b FALSE)))
-> _(def AND (lambda (a b) (IF a b FALSE)))_
(def OR (lambda (a b) (IF a TRUE b)))
-> _(def OR (lambda (a b) (IF a TRUE b)))_
(def NOT (lambda (a b) (IF a FALSE TRUE)))
-> _(def NOT (lambda (a b) (IF a FALSE TRUE)))_

(def XOR
 (lambda (a b)
  (OR (AND a (NOT b))
      (AND b (NOT a)))))
-> _(def XOR
 (lambda (a b)
  (OR (AND a (NOT b))
      (AND b (NOT a)))))_
}}

_h2 pairs & lists

{pre
PAIR := λxyf. f x y
CAR := λp. p TRUE
CDR := λp. p FALSE
NIL := λx. TRUE
NULL := λp. p (λxy. FALSE)
}

{pre {lc

(def PAIR (lambda (a b) (lambda (c) (c a b))))
-> _(def PAIR (lambda (x y) (lambda (z) (z x y))))_
(def LEFT (lambda (p) (p TRUE)))
-> _(def LEFT (lambda (z) (z TRUE)))_
(def RIGHT (lambda (p) (p FALSE)))
-> _(def RIGHT (lambda (z) (z FALSE)))_

(def NIL (lambda (x) TRUE)) 
-> _(def NIL (lambda (x) TRUE))_
(def ISNIL (lambda (p) (p (lambda (x y) FALSE))))
-> _(def ISNIL (lambda (p) (p (lambda (x y) FALSE))))_

(def DISP
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join (LEFT list) (DISP (RIGHT l))))) 
             l)))
-> _(def DISP
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join (LEFT l) (DISP (RIGHT l))))) l)))_

(def FRUITS
 (PAIR 'apple
  (PAIR 'banana
   (PAIR 'lemon
    (PAIR 'grapes
     (PAIR 'orange NIL))))))
-> _(def FRUITS
 (PAIR 'apple
  (PAIR 'banana
   (PAIR 'lemon
    (PAIR 'grapes
     (PAIR 'orange NIL))))))_

(DISP FRUITS)   
-> _(DISP FRUITS)_
}}

_h2 hanoï

{pre {lc

(def HANOI          
 (lambda (n from to via)
  ((IF (ISNIL n)
   (lambda (n from to via) ')
   (lambda (n from to via) (join
    (HANOI (RIGHT n) from via to)
      '< br>move (LEFT n) 'from 'tower from 'to 'tower to 
    (HANOI (RIGHT n) via to from))))
   n from to via)))
-> _(def HANOI          
 (lambda (n from to via)
  ((IF (ISNIL n)
   (lambda (n from to via) ')
   (lambda (n from to via)
    (join
    (HANOI (RIGHT n) from via to)
      '<br>move (LEFT n) 'from 'tower from 'to 'tower to 
    (HANOI (RIGHT n) via to from))))
   n from to via)))_

(def DISKS 
 (PAIR 'DISK_1
 (PAIR 'DISK_2
 (PAIR 'DISK_3
 (PAIR 'DISK_4
 (PAIR 'DISK_5 NIL))))))
-> _(def DISKS 
 (PAIR 'DISK_1
 (PAIR 'DISK_2
 (PAIR 'DISK_3
 (PAIR 'DISK_4
 (PAIR 'DISK_5 NIL))))))_

(HANOI DISKS 'A 'B 'C)
->
_(HANOI DISKS 'A 'B 'C)_

}}

_h2 more on lists

{pre
equivalent code left to the reader :)
}

} ;; end block

{{block}
_h1 lambdatalk version

_h2 Church numbers

{pre
0 := λfx. x
1 := λfx. f x
2 := λfx. f (f x)
3 := λfx. f (f (f x))
4 := λfx. f (f (f (f x)))
5 := λfx. f (f (f (f (f x))))
}

{pre
'{def ZERO {lambda {:s :z} :z}}
-> {def ZERO {lambda {:s :z} :z}}
'{def ONE {lambda {:s :z} {:s :z}}}
-> {def ONE {lambda {:s :z} {:s :z}}}
'{def TWO {lambda {:s :z} {:s {:s :z}}}}
-> {def TWO {lambda {:s :z} {:s {:s :z}}}}
'{def THREE {lambda {:s :z} {:s {:s {:s :z}}}}}
-> {def THREE {lambda {:s :z} {:s {:s {:s :z}}}}}

'{def church {lambda {:n} {:n {lambda {:x} {+ :x 1}} 0}}}
-> {def church {lambda {:n} {:n {lambda {:x} {+ :x 1}} 0}}}

'{church {ZERO}}
-> {church {ZERO}}
'{church {ONE}}
-> {church {ONE}}
'{church {TWO}}
-> {church {TWO}}
'{church {THREE}}
-> {church {THREE}}
}

_h2 comparison operators

{pre
Test whether a number is zero:
ISZERO := λn. n (λx. FALSE) TRUE
'{def ISZERO {lambda {:n} {:n {lambda {:x} FALSE} TRUE}}}
-> {def ISZERO {lambda {:n} {:n {lambda {:x} FALSE} TRUE}}}

Less than:
LT := λab. NOT (LEQ b a)
'{def LT {lambda {:a :b} {NOT {LEQ :b :a}}}}
-> {def LT {lambda {:a :b} {NOT {LEQ :b :a}}}}

Less than or equal to:
LEQ := λmn. ISZERO (SUB m n)
'{def LEQ {lambda {:m :n} {ISZERO {SUB :m :n}}}}
-> {def LEQ {lambda {:m :n} {ISZERO {SUB :m :n}}}}

Equal to:
EQ := λmn. AND (LEQ m n) (LEQ n m)
'{def EQ {lambda {:a :b} {AND {LEQ :a :b} {LEQ :b :a}}}}
-> {def EQ {lambda {:a :b} {AND {LEQ :a :b} {LEQ :b :a}}}}

Not equal to:
NEQ := λab. OR (NOT (LEQ a b)) (NOT (LEQ b a))
'{def NEQ {lambda {:a :b} {OR {NOT {LEQ :a :b}} {NOT {LEQ :b :a}}}}}
-> {def NEQ {lambda {:a :b} {OR {NOT {LEQ :a :b}} {NOT {LEQ :b :a}}}}}

Greater than or equal to:
GEQ := λab. LEQ b a
'{def GEQ {lambda {:a :b} {LEQ :b :a}}}
-> {def GEQ {lambda {:a :b} {LEQ :b :a}}}

Greater than:
GT := λab. NOT (LEQ a b)
'{def GT {lambda {:a :b} {NOT {LEQ :a :b}}}}
-> {def GT {lambda {:a :b} {NOT {LEQ :a :b}}}}

}

_h2 mathematical operators

{pre
'{def SUCC
 {lambda {:n}
  {{lambda {:n :x :y} {:x {:n :x :y}}} :n}}} 
-> {def SUCC {lambda {:n} {{lambda {:n :x :y} {:x {:n :x :y}}} :n}}}

'{def PRED
 {lambda {:n}
  {LEFT {:n {lambda {:p}
   {PAIR {RIGHT :p} {SUCC {RIGHT :p}}}} 
   {PAIR ZERO ZERO}}}}}
-> {def PRED
 {lambda {:n}
  {LEFT {:n {lambda {:p}
   {PAIR {RIGHT :p} {SUCC {RIGHT :p}}}}
   {PAIR ZERO ZERO}}}}}

'{def ADD
 {lambda {:n :m}
  {:n SUCC :m }}}   
-> {def ADD
 {lambda {:n :m}
  {:n SUCC :m }}}

'{def SUB
 {lambda {:m :n}
  {{:n PRED} :m}}} 
-> {def SUB
 {lambda {:m :n}
  {{:n PRED} :m}}}

'{def MUL
 {lambda {:m :n} 
  {:m {{lambda {:n :s} {ADD :n :s}} :n} ZERO}}}  
-> {def MUL
 {lambda {:m :n}
  {:m {{lambda {:n :s} {ADD :n :s}} :n} ZERO}}}

'{def POW
 {lambda {:m :n}
  {:n {{lambda {:m :s} {MUL :m :s}} :m} ONE}}}   
-> {def POW
 {lambda {:m :n}
  {:n {{lambda {:m :s} {MUL :m :s}} :m} ONE}}}

'{def DIV                            
 {lambda {:a :b}
  {{IF {ISZERO {SUB :b :a}}
       {lambda {:a :b} {SUCC {DIV {SUB :a :b} :b}}}
       {lambda {:a :b} ZERO}}
               :a :b}}}
-> {def DIV                            
 {lambda {:a :b}
  {{IF {ISZERO {SUB :b :a}}
       {lambda {:a :b} {SUCC {DIV {SUB :a :b} :b}}}
       {lambda {:a :b} ZERO}}
               :a :b}}}

'{def MOD
 {lambda {:a :b}
  {SUB :a {MUL {DIV :a :b} :b}}}}
-> {def MOD
 {lambda {:a :b}
  {SUB :a {MUL {DIV :a :b} :b}}}}

'{def GCD
 {lambda {:a :b}
  {{IF {ISZERO :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {GCD :b {MOD :a :b}}}} :a :b}}}
-> {def GCD
 {lambda {:a :b}
  {{IF {ISZERO :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {GCD :b {MOD :a :b}}}} :a :b}}}

'{church {SUCC THREE}}
-> {church {SUCC THREE}}
'{church {PRED THREE}}
-> {church {PRED THREE}}
'{church {ADD TWO THREE}}
-> {church {ADD TWO THREE}}
'{church {SUB THREE TWO}}
-> {church {SUB THREE TWO}}
'{church {MUL TWO THREE}}
-> {church {MUL TWO THREE}}
'{church {POW TWO THREE}}
-> {church {POW TWO THREE}}
'{church {DIV {ADD TWO THREE} TWO}}
-> {church {DIV {ADD TWO THREE} TWO}}
'{church {MOD {ADD TWO THREE} TWO}}
-> {church {MOD {ADD TWO THREE} TWO}}
'{church {GCD {MUL TWO THREE} TWO}}
-> {church {GCD {MUL TWO THREE} TWO}}
}

_h2 factorial

{pre
FAC ≡ λn. n (λfax. f (MUL a x) (SUCC x)) K 1 1
FAC = λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)
}

{pre
'{def ifac
 {lambda {:n}
  {RIGHT {:n {lambda {:p}
   {PAIR {SUCC {LEFT :p}} {MUL {LEFT :p} {RIGHT :p}}}}
   {PAIR ONE ONE}}}}}
-> {def ifac
 {lambda {:n}
  {RIGHT {:n {lambda {:p}
   {PAIR {SUCC {LEFT :p}} {MUL {LEFT :p} {RIGHT :p}}}}
   {PAIR ONE ONE}}}}}

'{church {ifac {ADD TWO THREE}}}
-> {church {ifac {ADD TWO THREE}}}

'{def rfac
 {lambda {:n}
  {{IF {ISZERO :n}
   {lambda {:n} ONE}
   {lambda {:n} {MUL :n {rfac {PRED :n}}}}} :n}}}
-> {def rfac
 {lambda {:n}
  {{IF {ISZERO :n}
   {lambda {:n} ONE}
   {lambda {:n} {MUL :n {rfac {PRED :n}}}}} :n}}}

'{church {rfac {ADD TWO THREE}}}
-> {church {rfac {ADD TWO THREE}}}
}

_h2 fibonacci

{pre
FIBONACCI := λn. n (λfab. f b (PLUS a b)) K 0 1
}

{pre
'{def ifib
 {lambda {:n}
  {RIGHT {{PRED :n} {lambda {:p}
   {PAIR {RIGHT :p} {ADD {LEFT :p} {RIGHT :p}} }} 
   {PAIR ZERO ONE}} }}}
-> {def ifib
 {lambda {:n}
  {RIGHT {{PRED :n} {lambda {:p}
   {PAIR {RIGHT :p} {ADD {LEFT :p} {RIGHT :p}} }} 
   {PAIR ZERO ONE}} }}}

'{church {ifib {MUL THREE THREE}}}       
-> {church {ifib {MUL THREE THREE}}}

'{def rfib
 {lambda {:n}
  {{IF {ISZERO {PRED {PRED :n}}}
   {lambda {:n} ONE}
   {lambda {:n} {ADD {rfib {PRED :n}} {rfib {PRED {PRED :n}}}}}} :n}}}
-> {def rfib
 {lambda {:n}
  {{IF {ISZERO {PRED {PRED :n}}}
   {lambda {:n} ONE}
   {lambda {:n} {ADD {rfib {PRED :n}} {rfib {PRED {PRED :n}}}}}} :n}}}

'{church {rfib {MUL THREE THREE}}}
-> {church {rfib {MUL THREE THREE}}}

'{def trfib
 {lambda {:a :b :n}
  {{IF {ISZERO :n}
   {lambda {:a :b :n} :a}
   {lambda {:a :b :n} {trfib {ADD :a :b} :a {PRED :n}}}} :a :b :n}}} 
-> {def trfib
 {lambda {:a :b :n}
  {{IF {ISZERO :n}
   {lambda {:a :b :n} :a}
   {lambda {:a :b :n} {trfib {ADD :a :b} :a {PRED :n}}}} :a :b :n}}}

'{church {trfib ZERO ONE {MUL THREE THREE}}}
-> {church {trfib ZERO ONE {MUL THREE THREE}}}

}

_h2 Y-combinator

{pre
FACTORIAL := Y (λgx. ISZERO x 1 (MULT x (g (PRED x))))
}

{pre
'{def Y {lambda {:g} {:g :g}}}
-> {def Y {lambda {:g} {:g :g}}}

'{def yfac
 {lambda {:g :x}
  {{IF {ISZERO :x}
       {lambda {:g :x} ONE}
       {lambda {:g :x} {MUL :x {:g :g {PRED :x}}}}} :g :x}}}
-> {def yfac
 {lambda {:g :x}
  {{IF {ISZERO :x}
       {lambda {:g :x} ONE}
       {lambda {:g :x} {MUL :x {:g :g {PRED :x}}}}} :g :x}}}

'{church {{Y yfac} {ADD TWO THREE}}}
-> {church {{Y yfac} {ADD TWO THREE}}}
}

_h2 2{sup 3} lambda expression

{pre
2{sup 3} = 
'{church 
{{lambda {m n}
 {n {{lambda {m s} {{lambda {m n} 
 {m {{lambda {n s} {{lambda {n m}
 {n {lambda {n}
 {{lambda {n x y} {x {n x y}}} n}} m }} n s}} n} 
 {lambda {s z} z}}} m s}} m} {lambda {s z} {s z}}}} 
 {lambda {s z} {s {s z}}} 
 {lambda {s z} {s {s {s z}}}}
}
}
= {church 
{{lambda {m n}
 {n {{lambda {m s} {{lambda {m n} 
 {m {{lambda {n s} {{lambda {n m}
 {n {lambda {n}
 {{lambda {n x y} {x {n x y}}} n}} m }} n s}} n} 
 {lambda {s z} z}}} m s}} m} {lambda {s z} {s z}}}} 
 {lambda {s z} {s {s z}}} 
 {lambda {s z} {s {s {s z}}}}
}}
}

_h2 sandbox

{pre
EXP := λab. b a
'{def pow2 {lambda {:a :b} {:b :a}}}
'{church {pow2 TWO THREE}}   // doesn't work

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

'{church {pow3 TWO THREE}} 
-> {church {pow3 TWO THREE}}
}

°°°
_h2 trampoline

{pre
{def SUM
 {def SUM.r
  {lambda {:a :b :c}
   {{IF {GT :a :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {SUM.r {SUCC :a} :b {ADD :c :a} }}} :a :b :c}}}
 {lambda {:a :b}
  {SUM.r :a :b ZERO} }}

{def trampoline
 {def trampoline.r
  {lambda {:op :func :end :step :acc :i}
   {if {> :i :end}
    then :acc
    else {trampoline.r :op :func :end  :step
                       {:op {:func :i {+ :i {- :step 1}}} :acc} 
                       {+ :i :step} }}}}
 {lambda {:op :func :start :end :step}
  {trampoline.r :op :func :end :step 0 :start} }}
 
{def TRAMPOLINE
 {def TRAMPOLINE.r
  {lambda {:op :func :end :step :acc :i}
   {{IF {GT :i :end}
    {lambda {:op :func :end :step :acc :i} :acc}
    {lambda {:op :func :end :step :acc :i}
     {TRAMPOLINE.r :op :func :end  :step
      {:op {:func :i {ADD :i {PRED :step}}} :acc} {ADD :i :step} }}} 
             :op :func :end :step :acc :i}}}
 {lambda {:op :func :start :end :step}
  {TRAMPOLINE.r :op :func :end :step ZERO :start} }}

{def STEP {MUL THREE {ADD TWO THREE}}} -> {church {STEP}}
{def END {MUL {STEP} {MUL TWO THREE}}}  -> {church {END}}

'{church {SUM ZERO {END}}} 
'{church {TRAMPOLINE ADD SUM ONE {END} {STEP}}}

}
°°°
} ;; end block

{{block}
_h1 lambdacode version

_h2 Church numbers

{pre
0 := λfx. x
1 := λfx. f x
2 := λfx. f (f x)
3 := λfx. f (f (f x))
4 := λfx. f (f (f (f x)))
5 := λfx. f (f (f (f (f x))))
}

{pre {lc
(def ZERO  (lambda (s z) z))
-> _(def ZERO  (lambda (s z) z))_
(def ONE   (lambda (s z) (s z)))
-> _(def ONE   (lambda (s z) (s z)))_
(def TWO   (lambda (s z) (s (s z))))
-> _(def TWO   (lambda (s z) (s (s z))))_
(def THREE (lambda (s z) (s (s (s z)))))
-> _(def THREE (lambda (s z) (s (s (s z)))))_

(def church (lambda (n) (n (lambda (x) (+ x 1)) 0)))
-> _(def church (lambda (n) (n (lambda (x) (+ x 1)) 0)))_

(church ZERO)
-> _(church ZERO)_
(church ONE)
-> _(church ONE)_
(church TWO)
-> _(church TWO)_
(church THREE)
-> _(church THREE)_
}}

_h2 comparison operators

{pre {lc
Test whether a number is zero:
ISZERO := λn. n (λx. FALSE) TRUE
(def ISZERO (lambda (n) (n (lambda (x) FALSE) TRUE)))
-> _(def ISZERO (lambda (n) (n (lambda (x) FALSE) TRUE)))_

Less than:
LT := λab. NOT (LEQ b a)
(def LT (lambda (a b) (NOT (LEQ b a))))
-> _(def LT (lambda (a b) (NOT (LEQ b a))))_

Less than or equal to:
LEQ := λmn. ISZERO (SUB m n)
(def LEQ (lambda (m n) (ISZERO (SUB m n))))
-> _(def LEQ (lambda (m n) (ISZERO (SUB m n))))_

Equal to:
EQ := λmn. AND (LEQ m n) (LEQ n m)
(def EQ (lambda (a b) (AND (LEQ a b) (LEQ b a))))
-> _(def EQ (lambda (a b) (AND (LEQ a b) (LEQ b a))))_

Not equal to:
NEQ := λab. OR (NOT (LEQ a b)) (NOT (LEQ b a))
(def NEQ (lambda (a b) (OR (NOT (LEQ a b)) (NOT (LEQ b a)))))
-> _(def NEQ (lambda (a b) (OR (NOT (LEQ a b)) (NOT (LEQ b a)))))_

Greater than or equal to:
GEQ := λab. LEQ b a
(def GEQ (lambda (a b) (LEQ b a)))
-> _(def GEQ (lambda (a b) (LEQ b a)))_

Greater than:
GT := λab. NOT (LEQ a b)
(def GT (lambda (a b) (NOT (LEQ a b))))
-> _(def GT (lambda (a b) (NOT (LEQ a b))))_
}}

_h2 mathematical operators

{pre {lc
(def SUCC
 (lambda (n)
  (lambda (x y) (x (n x y)))))
-> _(def SUCC
 (lambda (n)
  (lambda (x y) (x (n x y)))))_

(def PRED
 (lambda (n) 
  (LEFT (n (lambda (p)
   (PAIR (RIGHT p) (SUCC (RIGHT p)) ))
   (PAIR ZERO ZERO)))))
-> _(def PRED
 (lambda (n) 
  (LEFT (n (lambda (p)
   (PAIR (RIGHT p) (SUCC (RIGHT p)) ))
   (PAIR ZERO ZERO)))))_

(def ADD 
 (lambda (m n)
  (m SUCC n)))
-> _(def ADD
 (lambda (m n)
  (m SUCC n)))_

(def SUB
 (lambda (m n)
  (n PRED m)))
-> _(def SUB
 (lambda (m n)
  (n PRED m)))_

(def MUL
 (lambda (m n)
  (m (lambda (s) (ADD n s)) ZERO) ))
-> _(def MUL
 (lambda (m n)
  (m (lambda (s) (ADD n s)) ZERO) ))_

(def POW
 (lambda (m n)
  (n (lambda (s) (MUL m s)) ONE) ))
-> _(def POW
 (lambda (m n)
  (n (lambda (s) (MUL m s)) ONE) ))_

(def DIV                            
 (lambda (a b)
  ((IF (ISZERO (SUB b a))
       (lambda (a b) (SUCC (DIV (SUB a b) b)))
       (lambda (a b) ZERO))
                a b)))
-> _(def DIV                            
 (lambda (a b)
  ((IF (ISZERO (SUB b a))
       (lambda (a b) (SUCC (DIV (SUB a b) b)))
       (lambda (a b) ZERO))
                a b)))_

(def MOD
 (lambda (a b)
  (SUB a (MUL (DIV a b) b))))
-> _(def MOD
 (lambda (a b)
  (SUB a (MUL (DIV a b) b))))_

(def GCD
 (lambda (a b)
  ((IF (ISZERO b)
   (lambda (a b) a)
   (lambda (a b) (GCD b (MOD a b)))) a b)))
-> _(def GCD
 (lambda (a b)
  ((IF (ISZERO b)
   (lambda (a b) a)
   (lambda (a b) (GCD b (MOD a b)))) a b)))_

(church (SUCC THREE))
-> _(church (SUCC THREE))_
(church (PRED THREE))
-> _(church (PRED THREE))_
(church (ADD TWO THREE)) 
-> _(church (ADD TWO THREE))_
(church (SUB THREE TWO)) 
-> _(church (SUB THREE TWO))_
(church (MUL TWO THREE))
-> _(church (MUL TWO THREE))_
(church (POW TWO THREE))
-> _(church (POW TWO THREE))_  
(church (DIV (ADD TWO THREE) TWO))
-> _(church (DIV (ADD TWO THREE) TWO))_  
(church (MOD (ADD TWO THREE) TWO))
-> _(church (MOD (ADD TWO THREE) TWO))_ 
(church (GCD (MUL TWO THREE) TWO)) 
-> _(church (GCD (MUL TWO THREE) TWO))_
}}

_h2 factorial

{pre
FAC ≡ λn. n (λfax. f (MUL a x) (SUCC x)) K 1 1
FAC = λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)
}

{pre {lc
(def ifac
 (lambda (n) 
  (RIGHT (n (lambda (p)
   (PAIR (SUCC (LEFT p)) (MUL (LEFT p) (RIGHT p))))
   (PAIR ONE ONE)))))
-> _(def ifac
 (lambda (n) 
  (RIGHT (n (lambda (p)
   (PAIR (SUCC (LEFT p)) (MUL (LEFT p) (RIGHT p))))
   (PAIR ONE ONE)))))_

(church (ifac (MUL TWO THREE))) 
-> _(church (ifac (MUL TWO THREE)))_

(def rfac
 (lambda (n)
  ((IF (ISZERO n)
   (lambda (n) ONE)
   (lambda (n) (MUL n (rfac (PRED n))))) n)))
-> _(def rfac
 (lambda (n)
  ((IF (ISZERO n)
   (lambda (n) ONE)
   (lambda (n) (MUL n (rfac (PRED n))))) n)))_

(church (rfac (MUL TWO THREE)))
-> _(church (rfac (MUL TWO THREE)))_  
}}

_h2 fibonacci

{pre
FIBONACCI := λn. n (λfab. f b (PLUS a b)) K 0 1
}

{pre {lc
(def ifib
 (lambda (n)
  (RIGHT ((PRED n) (lambda (p)
   (PAIR (RIGHT p) (ADD (LEFT p) (RIGHT p)))) 
   (PAIR ZERO ONE)) )))
-> _(def ifib
 (lambda (n)
  (RIGHT ((PRED n) (lambda (p)
   (PAIR (RIGHT p) (ADD (LEFT p) (RIGHT p)))) 
   (PAIR ZERO ONE)) )))_

(church (ifib (MUL THREE THREE)))
-> _(church (ifib (MUL THREE THREE)))_

(def rfib
 (lambda (n)
  ((IF (ISZERO (PRED (PRED n)))
   (lambda (n) ONE)
   (lambda (n) (ADD (rfib (PRED n)) (rfib (PRED (PRED n)))))) n)))
-> _(def rfib
 (lambda (n)
  ((IF (ISZERO (PRED (PRED n)))
   (lambda (n) ONE)
   (lambda (n) (ADD (rfib (PRED n)) (rfib (PRED (PRED n)))))) n)))_

(church (rfib (MUL THREE THREE)))
-> _(church (rfib (MUL THREE THREE)))_

(def trfib
 (lambda (a b n)
  ((IF (ISZERO n)
   (lambda (a b n) a)
   (lambda (a b n) (trfib (ADD a b) a (PRED n)))) a b n)))
-> _(def trfib
 (lambda (a b n)
  ((IF (ISZERO n)
   (lambda (a b n) a)
   (lambda (a b n) (trfib (ADD a b) a (PRED n)))) a b n)))_

(church (trfib ZERO ONE (MUL THREE THREE)))
-> _(church (trfib ZERO ONE (MUL THREE THREE)))_

}}

_h2 Y-combinator

{pre
FACTORIAL := Y (λgx. ISZERO x 1 (MULT x (g (PRED x))))
}

{pre {lc
(def Y
 (lambda (h)
  ((lambda (x) (h (lambda (a) ((x x) a))))
   (lambda (x) (h (lambda (a) ((x x) a))))))) 
-> _(def Y
 (lambda (h)
  ((lambda (x) (h (lambda (a) ((x x) a))))
   (lambda (x) (h (lambda (a) ((x x) a)))))))_

(def yfac
 (lambda (g)
   (lambda (x)
    ((IF (ISZERO x)
     (lambda (x) ONE)
     (lambda (x) (MUL x (g (PRED x))))) x)))) 
-> _(def yfac
 (lambda (g)
   (lambda (x)
    ((IF (ISZERO x)
     (lambda (x) ONE)
     (lambda (x) (MUL x (g (PRED x))))) x))))_

(church ((Y yfac) (ADD TWO THREE)))
-> _(church ((Y yfac) (ADD TWO THREE)))_

}}

_h2 2{sup 3} lambda expression

{pre {lc
2{sup 3} =
(church 
 ((lambda (m n)
  (n (lambda (s) ((lambda (m n)
  (m (lambda (s) ((lambda (m n)
  (m (lambda (n)
  (lambda (x y) (x (n x y)))) n)) n s)) 
  (lambda (s z) z)) ) m s)) (lambda (s z) (s z))) ) 
  (lambda (s z) (s (s z))) 
  (lambda (s z) (s (s (s z))))
 )
)
= _(church 
((lambda (m n)
  (n (lambda (s) 
((lambda (m n)
  (m (lambda (s) ((lambda (m n)
  (m (lambda (n)
  (lambda (x y) (x (n x y)))) n)) n s)) 
(lambda (s z) z)) ) m s)) (lambda (s z) (s z))) ) 
(lambda (s z) (s (s z))) 
(lambda (s z) (s (s (s z))))
))_

}}
  
} ;; end block

{{block}

_h1 conclusion

_p Obviously lambdatalk and lambdacode are not reduced to the λ-calculus level and get benefit from the powerful technologies given for free by web browsers. But it's an other story, detailed for instance in [[coding]] and [[oops]].

_p {i alain marty | 2021/10/21 updated on 2022/10/31}

_h2 references

_ul [[A Tutorial Introduction to the Lambda Calculus (Raul Rojas)|http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf]]
_ul [[The Lambda Calculus (Don Blaheta)|http://cs.brown.edu/courses/cs173/2001/Lectures/2001-10-25.pdf]]
_ul  [[λ-calculus (wikipedia)|http://en.wikipedia.org/wiki/Lambda_calculus]], 
_ul [[Church_encoding|https://en.wikipedia.org/wiki/Church_encoding]],
_ul [[the-y-combinator-no-not-that-one|https://medium.com/@ayanonagon/the-y-combinator-no-not-that-one-7268d8d9c46]], 
_ul [[lambda-calculus-for-absolute-dummies|http://palmstroem.blogspot.fr/2012/05/lambda-calculus-for-absolute-dummies.html]], 
_ul [[lambda calcul|http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/index.html]], (André van Meulebrouck)
_ul [[simonpj|http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/V.HTM]]
_ul [[Y|http://mvanier.livejournal.com/2897.html]]
_ul [[Collected Lambda Calculus Functions|http://jwodder.freeshell.org/lambda.html]]  ;; jwodder@sdf.org
_ul [[epigrams|http://pu.inf.uni-tuebingen.de/users/klaeren/epigrams.html]]
_ul [[VIGRE|http://www.math.uchicago.edu/~may/VIGRE/VIGRE2006/PAPERS/Chariker.pdf]]
_ul [[palmstroem|http://palmstroem.blogspot.fr/2012/05/lambda-calculus-for-absolute-dummies.html]] 
_ul [[what-is-lambda-calculus-and-why-should-you-care|https://zeroturnaround.com/rebellabs/what-is-lambda-calculus-and-why-should-you-care/]]
_ul [[Show HN: λ-calculus revisited|https://news.ycombinator.com/item?id=22222682]]
_ul [[SHEN|http://www.schoolofinternalalchemy.com/]]
_ul [[pablo rauzy|https://www.irif.fr/~carton/Enseignement/Complexite/ENS/Redaction/2009-2010/pablo.rauzy.pdf]]
_ul [[lambda-calculus-in-javascript|https://medium.com/openmindonline/lambda-calculus-in-javascript-1ee947cadb21]]

_ul ... and some others on the web! 
_ul [[HN|https://news.ycombinator.com/item?id=33401612]] | [[HN|https://news.ycombinator.com/item?id=33417491]]

} ;; end block

{{hide}
{def block 
  div {@ style="display:inline-block; 
                width:500px; vertical-align:top; margin:10px; padding:5px;
               "}}
}

{style 
body { background:#444; } 
#page_frame { border:0; background:#444; color:#000; width:600px; margin-left:0; }
#page_content { background:#444; color:#fff; border:0; width:3400px; box-shadow:0 0 0; font-family:papyrus, optima; }
.page_menu { background:transparent; color:#fff; }
a { color:#f80; }
pre { box-shadow:0 0 8px #000; padding:5px; background:#444; color:#fff; font:normal 1.0em courier; }
b { color:cyan; }
h1 { font-size:4.0em; margin-left:0; color:#fff}
h2 { font-size:3.0em; }
h3 { font-size:2.0em; }
}