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 noeuds sont des applications
    et dont les feuilles sont les atomes.

  • On peut mesurer la taille d'un arbre comme étant le nombre de noeuds 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))
  • etc
  

La fonction factorielle

  • Définition :
    f(x) = if x=0 then 1 else x * f(x-1)

  • 1ère étape : curryfication, écriture préfixée
    f x = z x 1 (* x (f (p x)))

  • 2ème étape : abstraction de l'argument
    f = (λ+x . z x 1 (* x (f (p x))))

  • 3ème étape : équation de point-fixe
    f = (λ+f . (λ+x . z x 1 (* x (f (p x))))) f

  • 4ème étape : extraction du point-fixe
              f = Y (λ+f . (λ+x . z x 1 (* x (f (p x)))))

Définitions multiples

  • Un programme (fonctionnel) n'est pas simplement fait de définitions explicites ou
    de définitions implicites simples. En général c'est un ensemble de définitions de
    fonctions s'appelant les unes les autres.

  • Exemple:
            pair(x) = si x=0 alors true sinon impair(x-1)
            impair(x) = si x=0 alors false sinon pair(x-1) 
    On appelle cela des récursivités croisées.

  • La forme générale d'un programme est :

f1 x1 ... xn = E1(f1,…,fk,x1,…,xn)
f2 x1 ... xn = E2(f1,…,fk,x1,…,xn)
…
fk x1 ... xn = Ek(f1,…,fk,x1,…,xn)

  • Il n'est pas nécessaire que les fonctions aient la même arité mais j'en ai marre de cliquer
    dans cet éditeur pour obtenir des indices d'indices... Bref...

  • On commence par réaliser l'abstraction des variables dans les corps des fonctions :
f1 = λ+ x1 ... xn . E1(f1,…,fk,x1,…,xn)
f2 = λ+ x1 ... xn . E2(f1,…,fk,x1,…,xn)
…
fk = λ+ x1 ... xn . Ek(f1,…,fk,x1,…,xn)
Puis on écrit :  
f1 = (λ+ f1 ... fk . (λ+ x1 ... xn . E1(f1,…,fk,x1,…,xn)) f1 ... fk
f2 = (λ+ f1 ... fk . (λ+ x1 ... xn . E2(f1,…,fk,x1,…,xn)) f1 ... fk
…
fk = (λ+ f1 ... fk . (λ+ x1 ... xn . Ek(f1,…,fk,x1,…,xn)) f1 ... fk

Soit :

f1 = U1 f1 ... fk, U1 ≡def (λ+ f1 ... fk . (λ+ x1 ... xn . E1(f1,…,fk,x1,…,xn))
f2 = U2 f1 ... fk, U2 ≡def (λ+ f1 ... fk . (λ+ x1 ... xn . E2(f1,…,fk,x1,…,xn))
…
fk = Uk f1 ... fk, U1k ≡def (λ+ f1 ... fk . (λ+ x1 ... xn . Ek(f1,…,fk,x1,…,xn))

Puis on s'intéresse à :

F = [f1, f2, ..., fk]

= Vn f1 f2 ... fk

= Vn (U1 f1 f2 ... fk) (U2 f1 f2 ... fk) ... (Uk f1 f2 ... fk)

= Vn (U1 (P1 F) (P2 F) ... (Pk F)) ... (Uk (P1 F) (P2 F) ... (Pk F))

Là, on dispose d'une équation simple en F que l'on résoud comme déjà vu :
F = Y (λ+ F. Vn (U1 (P1 F) (P2 F) ... (Pk F)) ... (Uk (P1 F) (P2 F) ... (Pk0 F)))
Puis :     fi ≡def Pi F     pour i de 1 à k

Base de combinateurs

  • Un ensemble {C1,..,Cn} de combinateurs est appelé une base si pour toute variable x et
    tout terme M il existe un terme F construit avec les combinateurs de la base uniquement et tel que :
F N = [N / x] M

  • Exemple : {S,K} est une base (algorithme λ+).

  • Exemple : {B,C,K,W} est une base.
    A démontrer en exercice.

Un autre pour le bestiaire…

  • On pose Q = (λ+x . X K S K)

  • Q Q = Q K S K = K K S K S K = K K S K = K K

  • Q Q Q = K K Q = K

  • Q (Q Q) = Q (K K) = K K K S K = K S K = S

  • On peut exprimer S et K en fonction de Q donc :
    { Q } est une base !

  • Un seul combinateur suffit-il ? Non ! Où est la faille ?

Combinateur propre

  • Un combinateur C est dit propre s'il existe n tel que C x1,..,xn := E où E est une combinaison pure
    de x1,..,xn, c'est-à-dire un terme construit à partir de x1,..,xn uniquement par l'opération d'application.

  • Exemple : S est propre (n=3).

  • Exemple : K est propre (n=2).

  • Exemple : Q est impropre.

  • Un combinateur impropre ne peut être défini par une règle de réduction. Il a " besoin "
    d'autres combinateurs propes et pour être définis.

Théorème de CRAIG (1958, grande année !)

  • Une base de combinateurs propres doit contenir au moins deux éléments.

  • La démonstration est basée sur les effets des combinateurs (quelques pages) :

      • effet d'effacement : K

      • effet associatif : S, B

      • effet permutatif : S, C

      • effet duplicatif : S, W

  • Une base de combinateurs doit proposer ces 4 effets.

  • Un seul combinateur ne peut avoir ces 4 effets. 

Combinateurs et calculabilité

Il est clair que les fonctions partielles récursives peuvent être implémentées par S et K
donc (thèse de CHURCH) :

Tout ce qui est

effectivement calculable

peut être calculé par des combinateurs.

Combinateurs et implémentation

  • Le travail de cette section montre que l'on peut implémenter un langage de programmation
    avec S et K.

  • Une fois que la possibilité de modéliser quelque chose est démontrer, on peut l'incorporer
    sans risque dans la théorie. Exemple : on introduit des constantes pour les booléens et
    leurs opérations et des règles appropriées. Ces règles qui ont une portée sémantique
    sont appelées des d-règles.

  • Langage implémenté par des combinateurs :

  • HASKELL, MIRANDA, etc.

  • CAML mais avec des combinateurs bien plus puissants.

Combinateurs et programmation

  • Penser en termes combinateurs signifie penser en termes de combinaisons d'opérateurs,
    d'opérateurs sur les opérateurs, etc.

  • Des langages : FP, GRAAL, ...

  • Un style de programmation : composer des opérations...

  • Une maîtrise des processus récursifs : programmer la fonction de Fibonacci avec un langage
    de macro-expansion comme M4.

  • Une culture... Formalisme. Opérateurs. Abstraction.
 
Avez-vous des questions?
 
 
Suivant  
 
Précédent  
 
Table des matières