Best viewed in 24pt and full-screen
next up previous contents
Next: La métaprogrammation Up: Prolog Previous: Prolog - clauses de

Une extension de Prolog ?

tex2html_wrap_inline56836Prolog est un langage de programmation logique. Cela signifie que les programmes sont des formules logiques et que les exécuter consiste à les prouver. Dans le cas de tex2html_wrap_inline56836Prolog, les formules peuvent contenir des implications et des quantifications universelles en des positions qui sont interdites en Prolog. Les formules de tex2html_wrap_inline56836Prolog sont en fait une extension stricte de celles de Prolog. Par exemple, dans les formules suivantes,

displaymath51444

toute la partie soulignée est spécifique de tex2html_wrap_inline56836Prolog.

À ce point de la discussion, seule la structure de ces formules nous intéresse. Cependant, ce sont les premières formules de ce mémoire. Nous en commentons donc aussi la syntaxe et la sémantique. Dans ces formules, les tex2html_wrap_inline55298, tex2html_wrap_inline56450, tex2html_wrap_inline51464, tex2html_wrap_inline51466, tex2html_wrap_inline53470 et tex2html_wrap_inline53950 sont des identificateurs de variables, car ils sont introduits par des quantifications, et les tex2html_wrap_inline56418, tex2html_wrap_inline55794, tex2html_wrap_inline51492, tex2html_wrap_inline51494, tex2html_wrap_inline51498, tex2html_wrap_inline54574, tex2html_wrap_inline51496 et tex2html_wrap_inline51502 sont des identificateurs de prédicats. Rien ne distingue les identificateurs de prédicats des constructeurs de termes si ce n'est qu'ils sont utilisés pour former des formules. En syntaxe concrète, ils seront distingués par leurs types. Ces formules se paraphrasent en «Si toutes les bactéries (tex2html_wrap_inline56418) que contient (tex2html_wrap_inline55794) un récipient sont mortes (tex2html_wrap_inline51492), ce récipient est stérile (tex2html_wrap_inline51494)» et «Les grands-pères (tex2html_wrap_inline51496) qui se déduisent de ce que les pères présumés (tex2html_wrap_inline51498) sont considérés comme des pères (tex2html_wrap_inline54574) sont des grands-pères présumés (tex2html_wrap_inline51502)». Leur présentation dans la syntaxe concrète de tex2html_wrap_inline56836Prolog est la suivante :

s R :- pi Btex2html_wrap_inline56812( (b B , c B R) => m B ) .

gpp GP PF :- (pi Ptex2html_wrap_inline56812(pi Ftex2html_wrap_inline56812(p P F :- pp P F))) => gp GP PF .

Il faut noter que les structures d'imbrication de ces deux formules sont différentes et que les deux quantifications universelles soulignées (tex2html_wrap_inline51512 dans la première formule et tex2html_wrap_inline51514 dans la seconde) ne sont pas exactement de même nature. On peut s'en rendre compte assez facilement en considérant les premiers signes de la notation préfixe de ces formules. La première commence par tex2html_wrap_inline51516, alors que la seconde commence par tex2html_wrap_inline51518. En termes plus généraux, la quantification universelle soulignée dans la première expression est dans la prémisse d'un nombre impair d'implications, alors que celle qui est soulignée dans la seconde est dans la prémisse d'un nombre pair.

Une des caractéristiques de tex2html_wrap_inline56836Prolog est que le langage de ses formules est suffisamment riche pour que certains connecteurs y soient utilisés sous tous les points de vue qu'autorise le calcul des prédicats : hypothèse ou conclusion. En Prolog, le préfixe ne pourrait contenir qu'une conjonction (tex2html_wrap_inline51356) ou une formule atomique* après une implication (tex2html_wrap_inline55358). Quantification universelle et implication n'y sont utilisées qu'en position d'hypothèse (clause*), alors que la conjonction y est aussi utilisée en position de conclusion (but*). En tex2html_wrap_inline56836Prolog, quantification universelle, implication et conjonction peuvent être utilisées en position d'hypothèse et de conclusion.

Les idées de parité du nombre d'implications, et de position d'hypothèse ou de conclusion peuvent-être complètement formalisées par la notion de polarité*.

Les quantifications de tex2html_wrap_inline56836Prolog portent sur des termes d'ordre supérieur. Que les termes soient d'ordre supérieur signifie que certains d'entre eux peuvent être interprétés comme des fonctions et qu'ils généralisent strictement les termes de premier ordre de Prolog. Par exemple, dans la formule suivante,

displaymath51445

le domaine de la variable tex2html_wrap_inline51794 est nécessairement constitué de fonctions puisque tex2html_wrap_inline51794 est appliquée à un tex2html_wrap_inline53952.

Cette formule contient des termes plus complexes que les formules précédentes. Le terme tex2html_wrap_inline51558 est formé de l'application de la variable tex2html_wrap_inline51794 à la variable tex2html_wrap_inline53952, et le terme tex2html_wrap_inline51542 est formé de l'application de la constante tex2html_wrap_inline51548 à la variable tex2html_wrap_inline51794. Le rôle de tex2html_wrap_inline51548 est discuté à la section «Manipuler les expressions dans leur contexte»* --, mais nous pouvons déjà dire qu'il sert à construire une tex2html_wrap_inline56836-abstraction* de niveau objet qui doit être distinguée d'une tex2html_wrap_inline56836-abstraction du programme. Cette formule se paraphrase en «Si pour tout tex2html_wrap_inline53952 de type tex2html_wrap_inline56448, tex2html_wrap_inline51558 est de type tex2html_wrap_inline56450, alors tex2html_wrap_inline51794 est de type tex2html_wrap_inline51564». En d'autre termes, la constante tex2html_wrap_inline51566 représente la flèche des types de niveau objet, et la constante tex2html_wrap_inline51568 représente la relation de typage. La présentation de cette formule dans la syntaxe concrète de tex2html_wrap_inline56836Prolog est la suivante :

ty (abs E) (fl A B) :- pi xtex2html_wrap_inline56812( ty x A => ty (E x) B ) .

On peut aussi utiliser la notation du tex2html_wrap_inline56836-calcul* pour désigner des fonctions particulières. Par exemple, dans la formule suivante

displaymath51446

les expressions tex2html_wrap_inline54234, tex2html_wrap_inline51578 et tex2html_wrap_inline51586 désignent respectivement la fonction identité, la fonction constante dont l'image est tex2html_wrap_inline55186, et les fonctions qui ont la forme d'une somme. Il faut noter que si tex2html_wrap_inline51584 représente aussi des fonctions qui ont la forme d'une somme, elle ne représente que celles qui ne dépendent pas de leur argument. Les fonctions désignées par tex2html_wrap_inline51586 dépendent ou non de tex2html_wrap_inline53952 selon les valeurs prises par tex2html_wrap_inline56448 ou tex2html_wrap_inline56450.

On l'aura compris, la relation tex2html_wrap_inline51594 est un fragment de la relation de dérivation ; la formule tex2html_wrap_inline51596 est vrai si et seulement si tex2html_wrap_inline54124 est la dérivée de tex2html_wrap_inline55216. Sa présentation dans la syntaxe concrète de tex2html_wrap_inline56836Prolog est

d xtex2html_wrap_inline56812x xtex2html_wrap_inline568121 .

d xtex2html_wrap_inline56812( (A x) + (B x) ) xtex2html_wrap_inline56812( (DA x) + (DB x) ) :- d A DA , d B DB .

Être d'ordre supérieur peut aussi signifier contenir des variables propositionnelles ou prédicatives. Par exemple, les formules suivantes sont légales en tex2html_wrap_inline56836Prolog. La première est démontrable et l'autre non.

displaymath51447

Introduire la seconde en tant que clause rendrait inconsistant n'importe quel programme tex2html_wrap_inline56836Prolog. En revanche, considérée comme un but, elle échoue dans tous les programmes tex2html_wrap_inline56836Prolog. Elle constitue donc une définition de l'absurdité qui reste valable dans tous les contextes.

Leur présentation dans la syntaxe concrète de tex2html_wrap_inline56836Prolog est la suivante :

pi ptex2html_wrap_inline56812(p => p)

pi ptex2html_wrap_inline56812p

Jusqu'à ce point les formules acceptées en tex2html_wrap_inline56836Prolog constituent un sur-ensemble strict de celles que Prolog accepte. Cependant, les termes de tex2html_wrap_inline56836Prolog sont aussi typés, ce qui n'est pas le cas des termes de Prolog. On pourrait typer les termes de tex2html_wrap_inline56836Prolog de manière que tout terme de Prolog soit aussi un terme de tex2html_wrap_inline56836Prolog, mais c'est précisément ce qu'on ne veut pas faire. Au contraire, les types de tex2html_wrap_inline56836Prolog doivent imposer des régularités là où Prolog n'en impose pas. Par exemple, le terme [1, 3.14, []] est légal en Prolog. Il désigne une liste dont les éléments sont, dans l'ordre, l'entier 1, le rationnel 3.14 et la liste vide []. Ce terme n'est pas légal en tex2html_wrap_inline56836Prolog car le type choisi pour les listes impose que tous les éléments d'une même liste aient le même type. tex2html_wrap_inline56836Prolog n'est donc pas une extension stricte de Prolog car des notations de Prolog sont réutilisées avec un sens restreint. La section «Typage»* -- contient un développement de cette idée et un exemple de programme Prolog qui n'est pas typable en tex2html_wrap_inline56836Prolog.

On présente pourtant souvent tex2html_wrap_inline56836Prolog comme une extension de Prolog : on ajoute tex2html_wrap_inline56836-termes* simplement typés, implications dans les buts et quantifications explicites, et le tour est joué. Nous sommes aussi passé par là et avons proposé une «reconstruction pragmatique de tex2html_wrap_inline56836Prolog*» de tex2html_wrap_inline56836Prolog fondée explicitement sur cette idée [Belleannée et al. 95]. Une autre idée sous-tendait ce travail, mais était laissée implicite, quoique bien visible pour le lecteur attentif. Cette idée est le rôle que peut avoir la métaprogrammation*, considérée comme une technique de programmation généraliste, pour la conception d'un langage de programmation. C'est la seconde idée que nous allons explorer dans cette introduction à tex2html_wrap_inline56836Prolog.


next up previous contents
Next: La métaprogrammation Up: Prolog Previous: Prolog - clauses de

Olivier Ridoux
Mon Apr 27 11:10:23 MET DST 1998