Théorie

Ce jeu représente le lambda calcul (non typé).

Un alligator de couleur est une lambda abstraction
Un (vieil) alligator blanc représente des parenthèses
Un oeuf est une variables
La règle numero un, "règle de je-te-mange", correspond à une beta-reduction.
La règle numero deux, "règle de la couleur", correspond à une alpha-conversion.
La règle du vieil alligator dit que si une paire de parenthèses contient un seul terme, les parenthèses peuvent être enlevées

λ-Calcul en CoffeeScript

                                 Id = (x) -> x
    TRUE  = (x) -> (y) -> x # λx.λy.x
    FALSE = (x) -> (y) -> y # λx.λy.y
    JSbool = (f) -> f(true)(false)
    AND = (p) -> (q) -> p(q)(p)               # λp.λq.p q p
    OR  = (p) -> (q) -> p(p)(q)               # λp.λq.p p q
    NOT = (p) -> (a) -> (b) -> p(b)(a)        # λp.λa.λb.p b a  

    $0 = ZERO  = (f) -> (x) -> x            # λf.λx.x
    $1 = ONE   = (f) -> (x) -> f x          # λf.λx.f x
    $2 = TWO   = (f) -> (x) -> f f x        # λf.λx.f (f x)
    $3 = THREE = (f) -> (x) -> f f f x      # λf.λx.f (f (f x))
    $4 = FOUR  = (f) -> (x) -> f f f f x    # λf.λx.f (f (f (f x)))
    $5 = FIVE  = (f) -> (x) -> f f f f f x  # λf.λx.f (f (f (f (f x))))

    ISZERO = (n) -> n( (x) -> FALSE )(TRUE) # λn.n (λx.FALSE) TRUE
    IF = (p) -> (a) -> (b) -> p(a)(b) # λp.λa.λb.p a b

    int   = (n) -> n((x) -> ++x)(0)
    toInt = (n) -> (n ((x) -> x + 1)) 0
               
    #Predecesseur & Successeur SUCC 
    # λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
    PRED = (n) -> (f) -> (x) -> n((g) -> (h) -> h g f)((u) -> x)((u) -> u)
    SUCC = (n) -> (f) -> (x) -> f (n(f)(x)) # λn.λf.λx.f (n f x)

    #addition PLUS
    PLUS = (m) -> (n) -> (f) -> (x) -> m(f)(n(f)(x)) # λm.λn.λf.λx.m f (n f x)
    PLUS = (m) -> (n) -> m(SUCC)(n) # λm.λn.m SUCC n

    #soustraction SUB
    SUB = (m) -> (n) -> n(PRED)(m) # λm.λn.n PRED m

    #multiplication MULT
    MULT = (m) -> (n) -> (f) -> m n f # λm.λn.λf.m (n f)

    #power POW
    POW  = (b) -> (e) -> e b  # λb.λe.e b     

    #Récursivité
    I = (x) -> x # λx.x

    #La Factorielle 
    # λr.λn.(1, if n = 0; else n × (r (n−1)))
    YP = (f) -> (g) -> (x) -> (f g g) x
    Y = (f) ->  (YP f) (YP f)
    FACT = Y (r) -> (n) -> (((ISZERO n) (x) -> ONE) (x) -> (MULT n) (r (PRED n))) I
    REPEAT = Y (r) -> (n) -> (c) -> (((ISZERO n) (x) -> NIL) (x) -> (PAIR c) ((r PRED n) c)) I
    alert int FACT FOUR

Fonctions Haskell-iennes

Une lambda abstraction s'écrit λx.x ⇔ f(x) = x ⇔ (x) -> x
L'application (λx.x)(2) ⇔ f(x) = x & x=2 ⇔ ((x) -> x)(2)
le λ-calculus encode données, logique des prédicats & recursivité
λ-calcul compute saklé computable !

                                  f = (x) -> x
                                                    
                                  alert ((x) -> x)(2)
                                  alert f
                                  alert f(2)
                                  alert "Sa ti giny, sati geign pas !"

Logique des prédicats

Church à les bools : true & false

                                TRUE  = (x) -> (y) -> x # λx.λy.x
                                FALSE = (x) -> (y) -> y # λx.λy.y
                                
                                booleanJavaScript = (f) -> f(true)(false)
                               
                                alert booleanJavaScript(TRUE)
                                alert booleanJavaScript(FALSE)
                                alert "sa mèm !"

(AND / OR) & (NOT / IFTHENELSE)

AND(TRUE)(TRUE) ⇔ lambda abstraction ⇔ function ⇔ η-conversion ⇔ TRUE

                                booleanJavaScript = (f) -> f(true)(false)
                                TRUE = (x) -> (y) -> x # λx.λy.x 
                                FALSE = (x) -> (y) -> y # λx.λy.y
                                
                                # λp.λq.p q p
                                AND = (p) -> (q) -> p(q)(p)
                                # λp.λq.p p q
                                OR  = (p) -> (q) -> p(p)(q)
                                # λp.λa.λb.p b a        
                                NOT = (p) -> (a) -> (b) -> p(b)(a)
                                
                                alert "oté fépètè !"
                                alert booleanJavaScript AND(TRUE)(TRUE) # --> true
                                alert booleanJavaScript AND(TRUE)(FALSE) # --> false
                                alert AND(FALSE)(TRUE)  # --> false
                                alert AND(FALSE)(FALSE) # --> false

Church à les Numéros

Numero Zéro à Church ⇔ 0 ⇔ Fonction IDentité ⇔ (x) -> x

                              booleanJavaScript = (f) -> f(true)(false)
                              TRUE = (x) -> (y) -> x # λx.λy.x
                              FALSE = (x) -> (y) -> y # λx.λy.y
                              
                              $0 = ZERO  = (f) -> (x) -> x            # λf.λx.x
                              $1 = ONE   = (f) -> (x) -> f x          # λf.λx.f x
                              $2 = TWO   = (f) -> (x) -> f f x        # λf.λx.f (f x)
                              $3 = THREE = (f) -> (x) -> f f f x      # λf.λx.f (f (f x))
                              $4 = FOUR  = (f) -> (x) -> f f f f x    # λf.λx.f (f (f (f x)))
                              $5 = FIVE  = (f) -> (x) -> f f f f f x  # λf.λx.f (f (f (f (f x))))

                              ISZERO = (n) -> n( (x) -> FALSE )(TRUE) # λn.n (λx.FALSE) TRUE
                              IFTHENELSE = (p) -> (a) -> (b) -> p(a)(b) # λp.λa.λb.p a b

                              alert "Nawar mounwar saklé vrè !"
                              alert IFTHENELSE(TRUE)(THREE)(FOUR)  # --> THREE
                              alert IFTHENELSE(FALSE)(THREE)(FOUR) # --> FOUR
                              alert IFTHENELSE(ISZERO(ZERO))(THREE)(FOUR) # --> THREE
                              alert IFTHENELSE(ISZERO(ONE))(THREE)(FOUR)  # --> FOUR

Churchons les Numéros Javascript

int ⇔ integerJavaScript ⇔ Church Numeral

                              int   = (n) -> n((x) -> ++x)(0)
                              
                              $0 = ZERO = (f) -> (x) -> x # λf.λx.x
                              $1 = ONE = (f) -> (x) -> f x # λf.λx.f x
                              $2 = TWO = (f) -> (x) -> f f x # λf.λx.f (f x)
                              $3 = THREE = (f) -> (x) -> f f f x # λf.λx.f (f (f x))
                              $4 = FOUR = (f) -> (x) -> f f f f x # λf.λx.f (f (f (f x)))
                              $5 = FIVE = (f) -> (x) -> f f f f f x # λf.λx.f (f (f (f (f x))))
                              
                              #Predecesseur & Successeur SUCC 
                              # λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
                              PRED = (n) -> (f) -> (x) -> n((g) -> (h) -> h g f)((u) -> x)((u) -> u)
                              SUCC = (n) -> (f) -> (x) -> f (n(f)(x)) # λn.λf.λx.f (n f x)

                              #addition PLUS
                              PLUS = (m) -> (n) -> (f) -> (x) -> m(f)(n(f)(x)) # λm.λn.λf.λx.m f (n f x)
                              PLUS = (m) -> (n) -> m(SUCC)(n) # λm.λn.m SUCC n

                              #soustraction SUB
                              SUB = (m) -> (n) -> n(PRED)(m) # λm.λn.n PRED m

                              #multiplication MULT
                              MULT = (m) -> (n) -> (f) -> m n f # λm.λn.λf.m (n f)

                              #power POW
                              POW  = (b) -> (e) -> e b  # λb.λe.e b     

                              alert   PLUS(ONE)(TWO) # --> THREE
                              alert int PLUS(ONE)(TWO)  # --> 3
                              alert int SUCC(ONE)       # --> 2
                              alert int MULT(TWO)(FIVE) # --> 10
                              alert int POW(TWO)(FIVE)  # --> 32
                              alert int PRED(TWO)       # --> 1
                              alert int SUB(THREE)(TWO) # --> 1
                              alert int SUB(TWO)(THREE) # --> 0
                              alert "Perkutè kwé ?!"

Combinateurs

combinateurs ⇔ lambda expressions sans constante
En λ-calcul les abstractions sont anonymous !
Pas de nom de fonction dans le corps de la fonction
Heureusement : le combinateurwaï Y

                              int = (n) -> n((x) -> ++x)(0)
                              
                              #Le plus simple : le combinateur Identité
                              I = (x) -> x # λx.x
                              
                              TRUE  = (x) -> (y) -> x # λx.λy.x
                              FALSE = (x) -> (y) -> y # λx.λy.y
                              
                              $0 = ZERO  = (f) -> (x) -> x            # λf.λx.x
                              $1 = ONE   = (f) -> (x) -> f x          # λf.λx.f x
                              $2 = TWO   = (f) -> (x) -> f f x        # λf.λx.f (f x)
                              $3 = THREE = (f) -> (x) -> f f f x      # λf.λx.f (f (f x))
                              $4 = FOUR  = (f) -> (x) -> f f f f x    # λf.λx.f (f (f (f x)))
                              $5 = FIVE  = (f) -> (x) -> f f f f f x  # λf.λx.f (f (f (f (f x))))

                              ISZERO = (n) -> n( (x) -> FALSE )(TRUE) # λn.n (λx.FALSE) TRUE
                              #Predecesseur & Successeur SUCC 
                              # λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
                              PRED = (n) -> (f) -> (x) -> n((g) -> (h) -> h g f)((u) -> x)((u) -> u)
                              SUCC = (n) -> (f) -> (x) -> f (n(f)(x)) # λn.λf.λx.f (n f x)

                              #multiplication MULT
                              MULT = (m) -> (n) -> (f) -> m n f # λm.λn.λf.m (n f)

                              #Récursivité
                              U = (f) -> f(f)
                              Y = (g) -> ((x) -> g (x x))((x) -> g (x x)) # λg.(λx.g (x x)) (λx.g (x x))
      
                              #La Factorielle 
                              # λr.λn.(1, if n = 0; else n × (r (n−1)))
                              YP = (f) -> (g) -> (x) -> (f g g) x
                              Y = (f) ->  (YP f) (YP f)
                              FACT = Y (r) -> (n) -> (((ISZERO n) (x) -> ONE) (x) -> (MULT n) (r (PRED n))) I

                              alert int FACT FOUR