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

III

THEORIE DES COMBINATEURS
(Présentation non formelle)

H.B. CURRY

Théorie des combinateurs L'arbre de réduction
Naissance des combinateurs Le lemme de Churche-Rosser
Définition des combinateurs Combinateurs Ω & ω
S & K Unicité de la forme normale
Combinateur B Définition implicite vs. explicite
Combinateur W Théorème de normalisation
Combinateur C Théorème de standardisation
Combinateur C*  

 

Convention adoptée

  • Nous adoptons définitivement  les conventions suivantes:

  • Les fonctions sont curryfiées.

  • Déparenthésage de l'argument.

  • Associativité à gauche de l'application.

    Donc :

  • (x + 1) * (2 + 6) devient * (+ x 1) (+ 2 6)

  • f(g(x,y)z) devient f (g x y) z

  • + 1 est la fonction « successeur «.

La théorie des combinateurs

  • La théorie des combinateurs est née des travaux des logiciens M. SCHOENFINKEL (1905) et H.B. CURRY (1930).

  • L'idée était de faire de la logique un calcul comme les autres, comme l'arithmétique par exemple. En arithmétique, on écrit (1064 * 2043 + 12) et on calcule la valeur de l'expression. Pourquoi ne pourrait-on pas calculer la valeur d'une formule pour savoir si elle « vraie « ?

  • H.B. CURRY voulait donc mécaniser le raisonnement (c'était très tendance à son époque...).

  • A présent, nous savons que ce n'est pas possible car vouloir mécaniser le raisonnement introduit le paradoxe de CURRY...

  • L'aspect logique de cette théorie est maintenant bien éloigné et l'on préfère parler de Théorie des Combinateurs plutôt que de Logique Combinatoire.

Naissance des combinateurs

  • Le langage mathématique (logique) utilise des variables.
  • Exemple. La commutativité de l'addition s'écrit :
∀x . ∀y . x + y = y + x
  • Mais les variables et leurs quantificateurs sont des outils particulièrement complexes.
 

  • La logique « doit « posséder une règle qui dit que de ∀x.A(x) on doit pouvoir déduire A(t) pour n'importe quel t.

  • A(t) est la formule A(x) où l'on a remplacé x par t, ce que l'on note [t/x]A(x) et qui se lit substitution de t à x dans A(x).

  • Cela peut sembler simple a priori mais de grands noms se sont littéralement « cassé les dents « sur la définition de la substitution.

  • La question se pose alors de l'utilité absolue des variables. Certes, ce sont de plaisantes amies qui permettent d'exprimer simplement des propriétés mais n'existe-t-il pas d'autres moyens pour faire de même.

  • La réponse surprenante est positive et nous est donnée par le logicien H.B. CURRY.

  • Reprenons la commutativité de l'addition:

∀x . ∀y . x + y = y + x

  • En mode curryfié :
∀x . ∀y .+ x y = + y x
  • Introduisons un processus de calcul C admettant trois arguments a, b et c et calculant son résultat comme suit : appliquer a à c, puis appliquer le résultat éventuel de (a c) à b. Ce que l'on peut résumer par :
C a b c := a c b
  • On a :  C + x y = + y x
 
  • La formule

∀x . ∀y . + x y = + y x

peut donc se réécrire

∀x . ∀y . + x y = C + x y

Avec C tel que C a b c := a c b

Cette formule est vraie si :

∀x . + x = C + x

qui elle-même est vraie si :

+ = C +

 
  • Ainsi, en introduisant la fonction-processus C tel que C a b c := a c b, on peut exprimer la commutativité de l'addition par :

C + = +

  • Nous avons remplacer l'utilisation d'un outil complexe, la variable quantifiée, par celle d'un outil trivial: LE COMBINATEUR C.

  • Le combinateur C est une fonction processus définie en donnant le processus de calcul qui permet d'obtenir le résultat en fonction de ses trois arguments. Ce processus est décrit ou résumé par la formule :

C a b c := a c b

  • Maintenant un problème se pose : faut-il introduire un combinateur spécifique chaque fois que l'on désire exprimer une propriété ?

  • Si tel était le cas, l'intérêt des combinateurs serait limité aux systèmes finis.

  • H.B. CURRY nous donne la réponse : il suffit de deux combinateurs pour tout exprimer, c'est le théorème de complétude fonctionnelle.

Définition des combinateurs

  • La théorie des combinateurs ne connait comme opération que l'application d'une fonction à un argument notée (f x).

  • Un combinateur comme C est défini par une règle de la forme   C a b c := a c b qui définit implicitement un processus de calcul.

  • La symbole := est dit symbole de réduction. Il est orienté. Par analogie, on pourrait dire que 5+2 := 7 car un calcul a été fait pour passer de 5+2 à 7.

La combinateur d'effacement K

  • Le combinateur K est défini par la règle :
K X Y := X

 

  • Il prend deux arguments et rend son premier argument en résultat. C'est une fonction-processus.

  • K (Konstant) permet de fabriquer une fonction constante car (K x) appliqué à n'importe quoi fournit toujours x comme résultat.

Le combinateur de composition S

  • Le combinateur S est défini par la règle :

    • S X Y Z := X Z (Y Z)

  • S réalise une composition (Substitution) des fonctions X (binaire) et Y (unaire).

S et K

  • Si l'application de K est toujours définie, il n'en est pas de même pour celle de S. Pour que S X Y Z soit défini, il faut que :

      • l'application de X à Z, i.e. X Z,  soit définie ;

      • l'application de Y à Z, i.e. Y Z, soit définie ;

      • l'application de (X Z) à (Y Z), i.e. X Z (Y Z), soit définie.

  • Mais que se passe-t-il lorsque l'une de ces applications n'est pas définie ?

S et K, le point de vue formaliste

  • Une réponse originale soutenue par H.B. CURRY est de considérer la règle (S) comme purement symbolique en disant que S suivie de trois « choses « X, Y et Z se réécrit en X Z ( Y Z), c'est-à-dire que l'on écrit la première chose, puis la troisième, puis une parenthèse ouvrante, puis la deuxième, puis à nouveau de la troisième, puis une parenthèse fermante.

  • C'est le point de vue FORMALISTE qui considère la syntaxe comme étant l'objet des mathématiques, l'apport de sens étant uniquement le travail des « applicateurs « des mathématiques.

S et K, le point de vue formaliste

  • Donc CURRY considère que S X Y Z a toujours un sens : celui de la manipulation symbolique qu'elle entraîne.
  • Le point de vue formaliste nous vient de loin et peut sembler étrange mais...

S et K, le point de vue formaliste (Tartahlia et Cardano, 15e siècle)

  • Une équation de la forme  X3 + pX + q = 0 peut se mettre sous la forme (X – a) (bX2 + cX + d)=0 où a, b, c et d s'exprime facilement en fonction de p et q.

  • On a alors les solutions:

X = a, X = (-c + (c2 – 4bd)1/2) / 2b, X = (-c - (c2 – 4bd)1/2) / 2b

  • On a une méthode de résolution qui appliquée à X3 – X = 0 fournit les solutions 0, 1 et –1.

  • Un calcul purement symbolique nous a donné les solutions de l'équation mais nous avons manipulé des expressions qui n'avaient pas de sens au 15e siècle : des racines carrées de nombres négatifs...

S et K

  • S et K sont donc définis par les règles :
          (S)  S X Y Z := X Z (Y Z)          (K) K X Y := X

  • Dans ces règles, X, Y et Z peuvent être remplacées par n'importe quoi. Ce sont des méta-variables.

  • Techniquement, chacune de ces règles traduit une infinité d'axiomes : un axiome pour chacune des valeurs possibles (au plus dénombrables) des méta-variables qu'elle utilise.

Exercice

Calculer

S K K X
en utilisant les règles :

(S) S X Y Z := X Z (Y Z)
(K) K X Y := X

 

  • Donc si je définis I comme étant S K K alors I est tel que  I X := X.

  • I est la fonction IDENTITE.

Notation : la réduction et l'expansion

  • On a déjà vu le symbole de réduction X := Y

  • Intuitivement, il signifie que l'on passe de X à Y en réalisant des calculs, c'est-à-dire en appliquant des opérateurs.

  • On a 5 + 2 := 7 mais pas 7 := 5 + 2

  • L'opération inverse de la réduction s'appelle l'expansion et est notée =:. On a 7 =: 5+2

Notation : l'égalité

  • L'égalité notée X = Y est la fermeture symétrique et transitive de la réduction.

  • Plus simplement, X = Y si l'on passe de X à Y par une suite finie d'expansions et de réductions.

  • Exemple : 5 + (3*3) := 5+9 := 14 =: 7+7, donc on a : 5 + (3*3) = 7+7

 

Notation : l'égalité par définition

  • L'égalité par définition notée X ≡def Y signifie que Y est la définition de X.

  • Ainsi, on peut poser : I ≡def S K K

  • Si l'on a une égalité par définition X ≡def Y, cela signifie que l'on peut à tout moment remplacer X par Y et réciproquement.
  • En terme de langage informatique, il s'agit d'une macro-définition : X et Y sont indiscernables.

Notation : l'égalité par définition

  • On connaît tous le vieux bug :

#define N 3+4

x = 6 * N ;

qui une fois la macro-définition expansée se traduit par :

x = 6 * 3 + 4 ;

qui est bien différent de l'effet attendu :
x = 6 * (3 + 4);
  • On connaît tous la solution :

#define N (3+4)

  • Le même gag peut se produire avec les combinateurs. On pose : I ≡def S K K

  • Si l'on remplace I naïvement par sa définition dans S I K, on obtient S S K K K qui est incorrect car c'est (((S S) K) K) K

  • Il faut donc parenthéser et obtenir S (S K K) K

Notation : l'égalité syntaxique

  • On écrit X ≡ Y pour signifier que X et Y sont deux notations pour exactement la même chose.

  • Cela signifie que l'on passe de X à Y par :

      • Des remplacements corrects basés sur des égalités par définition ;

      • Des applications de règles d'associativité ou de tout autre règle purement syntaxique.

      • Exemple : S I K ≡ S (S K K) K ≡ (S (S K K))K

      • L'égalité syntaxique ne fait pas du tout appel à la notion de calcul.

Le combinateur B

Exercice
Posons B ≡def S (K S) K
Calculer :

B F G X
en utilisant les règles :
(S) S X Y Z := X Z (Y Z)
(K) K X Y := X
(I) I X := X , I ≡def S K K

 

  • Donc si l'on pose B ≡def S (K S) K, on a :

B F G X := F (G X)

  • B F G se comporte comme la composition usuelle de deux fonctions notée F o G et telle que
    F o G (x) = F (G (x))    . B est appelé le COMPOSEUR.

Le combinateur W

Exercice
Posons W ≡def S S (K I)
Calculer :

W F X
en utilisant les règles :
(S) S X Y Z := X Z (Y Z)
(K) K X Y := X
(I) I X := X , I ≡def S K K
(B) B F G X := F (G X), B ≡def S (K S) K

 

  • Donc si l’on pose W ≡def S S (K I), on a :

W F X := F X X

  • W est appelé le DUPLICATEUR.

Remarque

  • Dans le calcul qui a mené de W F X à F X X, on a utilisé I comme s'il été défini par la règle

    I X := X

alors que I est simplement défini par :

     I ≡def S K K
  • Cela ne pose aucun problème car il s'agit simplement d'abréger plusieurs étapes de réduction en une seule.
  • Toujours durant le calcul de W F X à F X X, nous avons fait un choix lors de la réduction de
    • S F (K I F) X
  • Il y a deux manières de réduire.
  • Le théorème de CHURCH-ROSSER nous confirmera que ce choix a peu d'importance.

 

Le combinateur C

Exercice
Posons C ≡def S (B B S) (K K)
Calculer :

C F X Y
en utilisant les règles :
(S) S X Y Z := X Z (Y Z)
(W) W F X := F X X, W ≡def S S (K I)
(K) K X Y := X
(I) I X := X , I ≡ def S K K
(B) B F G X := F (G X), B ≡ def S (K S) K

  • Donc si l’on pose C ≡def S (B B S) (K K), on a :

C F X Y := F Y X

  • C'est appelé le PERMUTATEUR

  • C'est aussi le combinateur permettant d’exprimer la commutativité d’une opération.

Le combinateur C*

 

Exercice
Posons C* ≡def CI

Calculer

C* X Y
en utilisant les règles :
(S) S X Y Z := X Z (Y Z)
(W) W F X := F X X, W ≡def S S (K I)
(K) K X Y := X
(I) I X := X , I ≡ def S K K
(B) B F G X := F (G X), B ≡ def S (K S) K

  • Nous le rajoutons à notre bestiaire...

(S) S X Y Z := X Z (Y Z) (W) W F X := F X X, W ≡defS S (K I)
(K) K X Y := X (C) C F X Y := F Y X, C ≡def S (B B S) (K K)
(I) I X := X , I ≡def S K K (C*) C* X Y := Y X, C* ≡def C I
(B) B F G X := F (G X), B ≡def S (K S) K  
 

Terminologie

  • Un terme de la forme K X Y ou S X Y Z est appelé un redex.

  • Le résultat après réduction est appelé le contractum.

  • On étend cette terminologie aux termes de la forme I X, B F G X, etc.

L'arbre de réduction

Comme un terme peut contenir plusieurs redexes, il peut subir plusieurs réductions différentes conduisant à des termes différents. On construit l'arbre de réduction. Exemple :

  • Les rédexes sont ordonnés de gauche à droite en fonction de la position de leur première lettre dans le terme. Les fils d'un noeud de l'arbre sont ordonnés de gauche à droite suivant l'ordre des rédexes.

  • Des arbres de réduction comme celui de K I (S I I (S I I)) peuvent être infinis.

  • Des arbres de réduction comme celui de S I I (S I I) peuvent être infinis et sans feuilles.

  • Des arbres comme celui de S S (K I) I I peuvent être finis.

  • Les feuilles de l'arbre sont des termes sans rédexes.

Terminologie

  • Un terme qui ne contient pas de rédex est dit irréductible. On dit aussi que c'est une forme normale.

  • Si un terme se réduit à une forme normale, on dit qu'il est normalisable.

Le lemme de CHURCH-ROSSER

Si des termes M, P et Q sont tels que M := P et M := Q alors il existe un terme Z tel que :
P := Z et Q := Z.

Parfois appelé Lemme Diamant ou Lemme de confluence.

  • La démonstration du lemme est longue et fastidieuse. Elle a été généralisée par J.W. KLOP, un élève de H. BARENDREGT, depuis à tout système dont les combinateurs sont « bien définis «.

  • Le principe est d'étudier d'abord le cas où les réductions M := P et M := Q ne concerne chacune qu'une seule étape de réduction:

On examine ce qui reste du rédex R de M lorsque l'on réduit le rédex T de M. Cela s'appelle le résiduel de R.

1er cas : R et T disjoints  
... (R) ... (T) ... := ... (C) ... (T) ...
Puis on examine ce qu'il faut faire à P et Q pour retomber sur ses pieds.
2ème cas : R inclus dans T
... (K (... R ...) Y) ... := ... (K (... C ...) Y) ...
... (K X (... R ...)) ... := ... (K X (... C ...)) ...
... (S (... R ...) Y Z) ... := ... (S (... C ...) Y Z) ...    
... (S X (... R ...) Z) ... := ... (S X (... C ...) Z) ...  
... (S X Y (... R ...)) ... := ... (S X Y (... C ...)) ...

Enfin, et c'est le plus difficile, on généralise au cas où la réduction
M := Q est une suite de plusieurs réductions élementaires.
3ème cas : T inclus dans R
... (K (... T ...) Y) ... := ... (... T ...) ...
... (K X (... T ...)) ... := ... X ...
... (S (... T ...) Y Z) ... := ... ((... T ...) Z (Y Z))...
... (S X (... T ...) Z) ... := ... (X Z ((... T ...) Z))...
... (S X Y (... T ...)) ... := ... (X (... T ...) (Y (... T ...)))...

Unicité de la forme normale

  • Soient P et Q deux formes normales telles que M := P et M := Q, alors il existe Z
    tel que P := Z et Q := Z. Mais P et Q étant irréductibles, la seule solution est que
    P     ≡ Z ≡ Q. D'où :

  • Théorème de l'unicité de la forme normale : la forme normale d'un terme, lorsqu'elle existe, est unique.

  • Conséquence : les feuilles d'un arbre de réduction, lorsqu'elles existent, sont identiques.

  • Ce que nous dit le théorème de l'unicité de la forme normale, c'est que s'il existe plusieurs moyens de réduire un terme à une forme normale (par le choix des rédexes) alors on retrouvera toujours une forme normale qui est unique.

  • Ainsi la forme normale de K I (S I I (S I I)) est I.

  • Cependant un mauvais choix des rédexes peut ne pas permettre d'obtenir une forme normale même lorsque celle-ci existe.

  • Si l'on réduit K I (S I I (S I I)) en choisissant uniquement des rédexes dans le sous-terme
    (S I I (S I I)), on n'obtient pas la forme normale.

Les combinateurs Ω et ω

    Exercice
    Posons ω ≡def S I I
    Calculer :

    ω X
    en utilisant les règles :
    (S) S X Y Z := X Z (Y Z)
    (I) I X := X , I     ≡ def S K K

     

  • On pose Ω ≡def ωω, on a :

                   Ω ≡ ωω := ωω := ...

Récapitulatif

(S) S X Y Z := X Z (Y Z) (W) W F X := F X X, W ≡deb S S (K I)
(K) K X Y := X (C) C F X Y := F Y X, C ≡deb S (B B S) (K K)  
(I) I X := X , I ≡deb S K K (C*) C* X Y := Y X, C* ≡deb C I
(B) B F G X := F (G X), B ≡deb S (K S) K (Ω) Ω ≡deb ω ω, ω ≡deb S I I, ω X := X X

Stratégie de réductions

  • Puisque selon le choix des rédexes que l'on opère, on peut ou pas obtenir la forme normale d'un terme normalisable, on introduit la notion de stratégie de réduction.

  • Une stratégie de réduction est une méthode permettant de choisir un rédex dans un terme pour le réduire.

  • Une stratégie de réduction est dite normalisatrice si elle conduit à la forme normale d'un terme lorsque ce terme est normalisable.

Appel par valeur, référence et nom

  • En informatique, la plupart des langages pratique l'appel par valeur, c'est-à-dire qu'ils évaluent les arguments d'une fonction avant d'appeler la fonction.         
    int f(int x) { return x+2 ; }
    f(2+5) := f(7) := 9
  • L'appel par référence, qui exige que l'argument soit une variable et qui transmet une référence sur la variable n'a pas de sens dans un langage fonctionnel où la variable-case-mémoire n'a elle-même pas de sens.

    void incr(int& v) { v++ ; }
    int i = 3 ;
    incr(i) ;

  • L'appel par nom, réservé aux langages fonctionnels, transmet l'argument non évalué à la fonction.

          f(x) = x + x
          f(2 + 3) = (2+3) + (2+3) = 5 + (2+3) = 5 + 5 = 10

Les expressions ne sont évaluées que lorsque c'est nécessaire.

  • L'évaluation paresseuse consiste à faire de l'appel par nom mais en évaluant au plus une fois chaque expression par une implémentation appropriée :

Exemple

  • Soit la fonction binaire f définie par :
          f(x,y) ≡def if x=0 then x else f(x-1,f(x,y))
  • Appel par valeur :
          f(0,y) = if 0=0 then 0 else f(0-1,f(0,y)) = 0       
f(1,y) = if 1=0 then 1 else f(1-1,f(1,y))
                     = f(1-1,f(1,y))
                     = f(0,f(1,y))
                     = ...
La « définition « récursive  et l'appel par valeur nous fournissent la fonction g définie par :

g(0, y) = 0

g(n+1,y) indéfini

  • Appel par nom :

f(0,0) = if 0=0 then 0 else f(0-1,f(0,0)) = 0

f(1,0) = if 1=0 then 1 else f(1-1,f(1,0))

= f(1-1,f(1,0))

= if 1-1=0 then 1-1 else f((1-1)-1,f(1-1,0))

= if 0=0 then 1-1 else f((1-1)-1,f(1-1,0))

= 1-1

= 0

La « définition « récursive et l'appel par nom nous fournissent la fonction h définie par :
                h(x,y) = 0

Définition implicite vs. explicite

  • Une « définition « récursive n'est pas une définition, c'est une équation.

  • D'un point de vue mathématique, une définition récursive est une équation dont les solutions sont des fonctions. Exemples :

      • f(x) = f(x)+1 n'a aucune solution;

      • f(x) = if x=0 then 1 else x * f(x-1) a une seule solution;

      • notre exemple précédent a au moins deux solutions;

      • f(x) = f(x) a une infinité de solutions.

  • Une équation récursive sera appelée une définition implicite par opposition aux définitions explicites de la forme :  
                    f(x,y) = if x=0 then y else x + 2y.

Mode d'évaluation

  • f (1,0) a une valeur (une forme normale ?) si on utilise l'appel par nom et est indéfini si on utilise l'appel par valeur.

  • Appel par nom : choisir le rédex le plus à gauche, i.e. choisir un rédex qui n'est contenu dans aucun autre.

  • Appel par valeur : choisir le rédex le plus interne, i.e. ne pas réduire un rédex qui contient d'autre rédex.

Théorème de normalisation

  • On appelle stratégie normale (ou leftmost strategy) la stratégie qui consiste à choisir le rédex le plus à gauche.

  • THEOREME : LA STRATEGIE NORMALE EST NORMALISATRICE.

  • Dans l'arbre de réduction d'un terme normalisable, on trouvera la forme normale en suivant la branche la plus à gauche.

Théorème de standardisation

  • Une réduction est dite standard si le rédex Rk contracté lors du k-ième pas de réduction n'est le résiduel d'aucun rédex Ri, i ≥1 situé strictement à sa gauche.

  • THEOREME : SI X := Y
    ALORS IL EXISTE UNE REDUCTION STANDARD DE X VERS Y.
 
Avez-vous des questions?
 
 
Suivant  
 
Précédent  
 
Table des matières  
 
Solution des exercices