THEORIE DES COMBINATEURS
   

Chapitre 1

Introduction

Chapitre 2

Fonction processus Curryfication

Chapitre 3

Théorie des combinateurs (Présentation non formelle)
H.B. CURRY

Chapitre 4

Théorie des combinateurs (Présentation formelle)
L’INDUCTION

Chapitre 5

Modélisation
Logico-Combinatoire
des réalités informatiques

Chapitre 6

La machine SK de
D. TURNER

V

MODELISATION
LOGICO-COMBINATOIRE
DES
REALITES INFORMATIQUES

Les booléens λ+++x.M
Les entiers λ++++x.M
La substitution Les vecteurs
λ+x.M Théorème de CRAIG
λ++x.M  

 

  • Dans cette section, nous montrons comment réaliser les entités informatiques classiques :

      • les booléens, leurs opérations et la conditionnelles ;

      • les entiers naturels et leurs opérations;

      • les listes.

  • Nous voyons aussi comment transformer une définition implicite (équation récursive) ou
    une définition explicite de fonction en un terme calculant la fonction.

Les booléens (G. Boole, 1849)

  • En logique, on utilise deux marques, t et f, pour représenter la vérité et la fausseté des propositions.

  • On choisit de modéliser les deux valeurs de vérité par :           

    t ≡def K

    f ≡def K I

  • t et f sont les modèles de t et f.

Les booléens : expression conditionnelle

  • On a :
      • t X Y ≡ K X Y := X
      f X Y ≡ K I X Y := I Y := Y
  • On peut donc modéliser l’expression conditionnelle :

    if  P  then  F  else G

    par :
    P F G

Les booléens : la conjonction

  • On a (vieux Lispien) : x ∧ y = if  x  then  y  else  f

  • Donc on cherche ∧ tel que x y = x y f

  • A faire en exercice

Les booléens : la disjonction

  • On a (vieux Lispien) : x ∨ y = if x then t else y

  • Donc on cherche ∨ tel que ∨ x y = x t y

  • A faire en exercice

Les booléens : la négation

  • On a : ¬ x = if x then f else t

  • Donc on cherche ¬ tel que ¬ x = x f t

  • A faire en exercice

 Les entiers naturels

  • Nous allons développer un modèle des entiers naturels appelé entiers ou itérateurs de CHURCH.

  • Nous introduisons la notation :

fn x ≡def
 f(f...(f x)..)
   
 

n x f

  

 

   définie par:

f0 x ≡def x

fn+1 x ≡def f (fn x)

 

  • On a bien entendu :   fp+q x ≡ fp (fq x). Exercice…

Les entiers naturels de CHURCH

  • On pose:

    0 ≡def K I (zéro)

    s ≡def S B (successeur)
     

  • Le modèle de l’entier naturel n est n ≡def sn 0

  • De tels modèles d’entiers sont appelés des numéraux.

Les itérateurs de CHURCH

  • Théorème. Soit n un entier de CHURCH, alors, on a :

n f x  :=  fn x

  • Démonstration: A faire en exercice
  • L’entier de CHURCH n permet donc d’itérer une fonction f sur un argument x.

Les entiers naturels : test d’égalité à zéro

  • On recherche z tel que :
            

z 0 = t

z n+1 = f

  • Dans un cas comme cela, on cherche à examiner l’argument de la fonction. Il n’existe pas de
    terme permettant d’examiner le « contenu » d’un autre terme, par exemple savoir si c’est
    une application ou pas. On sait même que c’est IMPOSSIBLE…

  • Le seul moyen d’« examiner » un terme est de l’appliquer à des arguments et de regarder ce que cela donne.

  • On cherchera donc z sous la forme z n = n U en recherchant U pour obtenir le résultat voulu. Ca ne marchera pas, on cherchera z sous la forme z n = n U V en recherchant U et V.

  • On cherche z sous la forme z n = n U V, il faut donc trouver U et V tels que:

0 U V = t

n+1 U V = f

  • 0 U V ≡ K I U V = I V = V , il faut donc V ≡ t

  • n+1 U V ≡ s n U V ≡ S B n U V = B U (n U) V = U (n U V) = f
    on peut obtenir ce résultat en prenant U ≡ K f

  • On veut donc : z n = n (K f) t = C* (K f) n t = C (C* (K f)) t n

  • On prend donc :     z ≡def C (C* (K f)) t

Les entiers naturels : l’addition

  • On cherche + tel que + m n = m+n

  • A faire en exercice

Les entiers naturels :la multiplication

  • On cherche * tel que * m n = m*n

  • A faire en exercice

Les entiers naturels

La soustraction
et
la division
seront vues plus tard.

Les définitions explicites
  • Nous avons eu affaire à des définitions explicites du style f x = S (x (+ x 0)), à charge pour nous de déterminer f .
     
     f x  = S (x (+ x 0))                   f x  = S (x (+ x 0))

    •  =S (x (C + 0 x))                      = B S x (+ x 0)

     =S (I x (C + 0 x))                    = B S x (C + 0 x)

     =S (S I (C + 0 ) x)                   = S (B S) (C + 0 ) x

     =B S (S I (C + 0 )) x

 

  • En agissant ainsi, on réalise l’ABSTRACTION de la variable x dans le terme S (x (+ x 0)).

  • Il existe en général plusieurs manières de réaliser une abstraction. Il n’y a AUCUNE pour que les résultats soient égaux…

  • Si je trouve f, B f I convient aussi…

  • Convenons de NOTER (λ x.M) tout terme résultat d’une abstraction de x dans M. C’est-à-dire un terme tel que :

                   (λ x.M) x := M et  x ∉ (λ*x.M)

    et plus exactement tel que :

                   (λ*x.M) N := [N / x] M et  x ∉ (λ*x.M)

     où [N / x] M DESIGNE le résultat de la substitution de N à toutes les occurrences de x.

  • Le processus de calcul d’un (λ*x.M) peut-il être automatisé ? La réponse est OUI !

La substitution

  • Si M et N sont des termes et x une variable, la substitution de N à x dans M, notée [N / x]M se définit par induction :

      • [N / x] c ≡def c si c est une constante; (BASE)

      • [N / x] x ≡def N; (BASE)

      • [N / x] y ≡def y si y est une variable et y ≠ x; (BASE)

      • [N / x] (P Q) ≡def ([N / x]P [N  / x]Q); (PAS)

  • [N / x]M désigne simplement le remplacement de TOUTES les occurrences de x dans M par N.
    Cela ne pose aucun problème car il n’y a pas de quantificateurs.

  • Pourquoi définir la substitution ? Pour pouvoir faire des démonstrations par induction concernant la substitution.

  • [N / x] M sera lu :

      • substitution de N à x dans M;

      • ou remplacement de x par N dans M;

      • ou N à la place de x dans M;

      • ou M dans lequel on remplace x par N;

      • etc.

Exemple de substitution rigoureuse

[A / x] (S (x (+ x 0)))

          ≡ [A / x]S [A / x](x (+ x 0))

          ≡S ([A / x]x [A / x](+ x 0))

          ≡S (A ([A / x](+ x) [A /x]0))

          ≡S (A ([A / x]+ [A /x]x 0))

          ≡S (A (+ A 0))

Un algorithme d’abstraction (λ+x.M)

  • Soit x une variable et M un terme, on définit (λ+x.M) par induction sur M :

      • (λ+x.c) ≡def K c si c est une constante; (BASE)

      • (λ+x.x) ≡def I; (BASE)

      • (λ+x.y) ≡def K y si y est une variable et y ≠ x; (BASE)

      • (λ+x.PQ) ≡def S (λ+x.P) (λ+x.Q)
  • Theorème. On a :

(λ+x.M) N := [N / x] M et x ∉(λ+x.M)

et :           

(λ+x.M) est une forme normale.

  • Démonstration : A faire en exercice

Exemple d’abstraction

    λ+x . S (x (+ x 0))

      ≡ S (λ+x . S) (λ+x . (x (+ x 0)))

      ≡ S (K S) (S (λ+x . x) (λ+x . (+ x 0)))

      ≡ S (K S) (S I (S (λ+x . + x) (λ+x . 0)))

      ≡ S (K S) (S I (S (S (λ+x . +) (λ+x . x)) (K 0)))

      ≡ S (K S) (S I (S (S (K +) I) (K 0)))

  • On a pris (λ+x . +) ≡ K + et (λ+x . 0) ≡ K 0 comme si + et 0 étaient atomiques…

Définition explicite

  • L’algorithme d’abstraction λ+ permet à partir d’une toute définition explicite f x = E(x)
    d’une fonction f d’obtenir un terme (λ+x . E(x)) qui est un algorithme pour la fonction f.

  • La notation (λ+x . M) désigne le terme obtenu comme résultat de l’abstraction de x
    dans M par l’algorithme λ+.

  • On voit donc que deux combinateurs suffisent à transformer toute définition explicite
    en un terme de la théorie des combinateurs.

Définition implicite

  • On avait appelé définition implicite une équation récursive de la forme  f x = E(f,x).

  • On commence par écrire f = (λ+x . E(f,x)). C’est une équation en f où la variable x n’apparaît plus.

  • Puis on écrit f = (λ+f . (λ+x . E(f,x))) f. En effet,
    (λ+f.(λ+x.E(f,x))) f := [f/f ](λ+x.E(f,x)) ≡(λ+x.E(f,x)).

  • De plus, (λ+f . (λ+x . E(f,x))) est un terme ne contenant que des S et des K. Il est appelé la
    fonctionnelle associée à la définition récursive    . L’équation dit que f est un point-fixe de cette fonctionnelle. 

  • De la définition implicite f x = E(f,x), on est arrivé à l’équation f = (λ+f . (λ+x . E(f,x))) f
    qui est une équation de point-fixe.

  • Une solution de cette équation nous est donnée par le combinateur de point-fixe Y :

f= Y (λ+f . (λ+x . E(f,x)))

  • Les combinateurs S et K nous permettent donc de trouver un algorithme pour calculer
    l’une des solutions de toute équation récursive.

  • Y permet de calculer le plus petit point-fixe, c’est-à-dire
    la fonction la moins définie solution de l’équation récursive.

Substitution simultanée

  • La notation [X/x,Y/y,…,Z/z]M désigne le résultat de la substitution simultanée de X à x, Y à y, … et Z à z dans M.

  • Exemple. [y / x, z / y] (+ x y) ≡ (+ y z)

  • Exercice. Donner une définition par induction de la substitution simultanée.

Abstraction multiple

On pose
(λ+x, y, …, z . M) ≡def (λ+x . (λ+y . (… (λ+z . M)..)))
  • Théorème. On a les propriétés suivantes :
      • (λ+x, y, …, z . M) est une forme normale
      • x ∉ (λ+x, y, …, z . M)
      • y ∉ (λ+x, y, …, z . M)
      • …
      • z ∉ (λ+x, y, …, z . M)
      • (λ+x, y, …, z . M) X Y … Z := [X/x, Y/y, …, Z/z]M
  • Démonstration. A faire en exercice.

Un peu de complexité (un tout petit peu… faut pas pousser !)

  • On peut représenter un terme sous la forme d’un arbre binaire dont les nœuds sont des applications
    et dont les feuilles sont les atomes.

  • On peut mesurer la taille d’un arbre comme étant le nombre de nœuds de cet arbre.

  • L’équation (λ+x.PQ) ≡def S (λ+x.P) (λ+x.Q) nous dit que la taille de l’arbre résultat est au moins
    le double de la taille de M.

  • Si on effectue n abstractions consécutives, la taille de l’arbre est multipliée par 2n. Peut-on optimiser ?

Une première amélioration

  • Soit F tel que x ∉ F on remarque que (λ+x . F x) ≠ F mais est un terme plus compliqué.

  • Exemple :
          (λ+x . I x) ≡ S (λ+x . I) (λ+x . X) ≡ S (K I) I

  • Or F pourrait convenir puisque l’on demande à (λ+x . F x) de ne pas contenir x et d’être tel que
    (λ+x . F x) N := [N / x](F x) ≡ F N

  • On aurait alors :
          (λ+x . I x) ≡ I

Un algorithme d’abstraction (λ++x.M)

  • Soit x une variable et M un terme, on définit (λ++x.M) par induction sur M :

    • (λ++x.F x) ≡def F si x ∉ F; (PRIORITAIRE)

    • (λ++x.c) ≡def K c si c est une constante; (BASE)

    • (λ++x.x) ≡def I; (BASE)

    • (λ++x.y) ≡def K y si y est une variable et y ≠ x; (BASE)

    • (λ++x.PQ) ≡def S (λ++x.P) (λ++x.Q)

  • Théorème. On a :                       
(λ++x.M) N := [N / x] M et x ∉ λ++x.M)
  • On perd la propriété de la forme normale.

Une deuxième amélioration

  • Soit F non atomique tel que x ∉ F on remarque que (λ +x . F) ≠ K F mais est un terme plus compliqué.

  • Exemple :
                (λ+ x . I I) ≡ S (λ+ x . I) (λ+ x . I) ≡ S (K I) (K I)

  • Or K F pourrait convenir puisque l’on demande à (λ+ x . F) de ne pas contenir x et d’être tel que
    (λ+ x . F) N := [N / x]F ≡ F =: K F N

  • On aurait alors :
                (λ+x . I I) ≡ K (I I)

Un algorithme d’abstraction (λ+++x.M)

  • Soit x une variable et M un terme, on définit ( λ+++x.M) par induction sur M :

      • (λ+++x.F) ≡def K F si x ∉ F; (PRIORITAIRE)

      • (λ+++x.F x) ≡def F si x ∉ F; (PRIORITAIRE)

      • (λ+++x.c) ≡def K c si c est une constante; (BASE)

      • (λ++++x.x) ≡def I; (BASE)

      • (λ+++x.y) ≡def K y si y est une variable et y ≠ x; (BASE)

      • (λ+++x.PQ) ≡def S (λ+++x.P) (λ+++x.Q)

  • Théorème. On a :

      •                         (λ+++x.M) N := [N / x] M et  x ∉ (λ+++x.M)

Un algorithme d’abstraction (λ++++x.M)

  • Soit x une variable et M un terme, on définit (λ++++x.M) par induction sur M :

      • (λ++++x. F (G x)) ≡def B F G si x ∉(F G); (PRIORITAIRE)

      • (λ++++x. F x (G x)) ≡def S F G si x ∉ (F G); (PRIORITAIRE)

      • (λ+++++x. F x G) ≡def C F G si x ∉ (F G); (PRIORITAIRE)

      • (λ++++x.F) ≡def K F si x ∉ F; (PRIORITAIRE)

      • (λ++++x.F x) ≡def F si x ∉ F; (PRIORITAIRE)

      • etc.

  • Théorème. On a :

                        (λ++++x.M) N := [N / x] M et x ∉ (λ++++M)

Une autre manière d’améliorer (λ+x.M)

  • La méthode : simplifier le résultat de (λ+x.M) :

      • S (K F) (K G) → K (F G)  si x ∉(F G)

      • S (K F) G → B F G si x ∉(F G)

      • S F (K G) → C F G si x ∉(F G)

      • etc.

  • Ces règles de simplifications ne font pas mieux que les algorithmes améliorés (elles en sont extraites)
    mais elles sont plus délicates à manier…

Modéliser les structures de données

  • On sait que l’on peut modéliser toutes les structures de données à partir de la paire que nous noterons <a,b>.

  • Une modélisation de la paire est un triplet de fonctions π, π1, π2 tel que :

      • π a b est le modèle de la paire ;

      • π1est la première projection, i.e. π1(π a b) := a

      • π2 est la deuxième projection, i.e. π2(π a b) := b

La paire de CHURCH

  • La paire de CHURCH est une modélisation de la paire.

  • On pose π ≡def (λ+a. (λ+b. (λ+x. x a b)))

  • π a b est égal à une valeur qui ne nous importe pas et π a b x := x a b

  • Si je veux extraire a de la paire (π a b), il me suffit de l’appliquer à K car
    π a b K := K a b := a.
    On posera donc π1 ≡def (λ+c. c K)

  • Si je veux extraire b de la paire (π a b), il me suffit de l’appliquer à K I
    car π a b (K I) := K I a b := I b.
    On posera donc :
    π 2 ≡def (λ+c. c (K I))

Les vecteurs

  • Un vecteur de longueur n, [a1,..,an], peut être modélisé à l’aide des paires par :
             <a1 , <a2, < … , <an-1,<an, K I>>..>>
Exercice
1.On cherche Vn tel que Vn a1 … an soit le modèle du vecteur [a1,..,an] de longueur n :
    1. Trouver V0.
    2. Exprimer Vn+1 en fonction de Vn.
    3. Trouver une formule pour Vn en fonction de l’entier de Church n.
2.On veut les projections Pi telles que Pi(Vn a1 … an) := ai.
Utiliser le même genre de technique que pour déterminer Vn.

La fonction prédécesseur

• On cherche p tel que p 0 := 0 et p n+1 := n.

• L’opération <x , y> → <y , y+1> est réalisée par le terme (λ+c. π (π2 c) (s (π2 c))).

• On itère n fois cette opération sur la paire <0 , 0> :

– <0 , 0>, itération 0
– <0 , 1>, itération 1
– <1 , 2>, itération 2
– …
– <k-1 , k>, itération k


• p ≡def (λ+n. (π1 (n (λ+c. π(π1 c) (s (π2 c))) (π 0 0))))

En vrac…

  • -  = (λ+x,y . y p x)
  • < = (λ+x,y . ¬ (≥ x y))
  • ≤ (λ+x,y . z (- x y))    
  • = = (λ+x,y . ∧ (≤ x y) (≥ x y))
  • ≥ = (λ+x,y . z (- y x))
  • /  = (λ+x,y . < x y 0 (s (/ (- x y) y)))
    donc     : / = Y (    λ+f . (λ+x,y . < x y 0 (s (f (- x y) y))))
  • > = (λ+x,y . ¬ (≤ x y))