Best viewed in 24pt and full-screen

Les formules héréditaires de Harrop

Il se trouve qu'il existe un fragment du calcul des prédicats intuitionniste qui a de bonnes propriétés calculatoires et qui permet justement de combiner librement les implications et les quantifications universelles. Ce fragment est celui où on n'admet que les occurrences positives* du connecteur «ou» () et du quantificateur «il existe» (), et où on admet les connecteurs «et» et «implique» ( et ), et le quantificateur «quel que soit» () sans restriction. Intuitivement, on dit qu'une occurrence de connecteur est de polarité* positive si elle est imbriquée à gauche d'un nombre pair ou nul d'implications. Si ce nombre est impair, l'occurrence est négative. Par exemple, dans les formules et , les occurrences de sont négatives, alors qu'elles sont positives dans et . On convient que la polarité d'une occurrence de connecteur ou de quantificateur est celle du non-terminal qui l'engendre. On notera une occurrence d'un objet  de polarité  (par exemple, et )

Les formules de ce fragment sont les formules héréditaires de Harrop*, et elles ont la propriété que la prouvabilité uniforme* est complète par rapport à la logique intuitionniste pour ces formules. En d'autres termes, les théorèmes intuitionnistes des formules héréditaires de Harrop ont tous une preuve constructive* qui peut être atteinte par une stratégie simple et dirigée par la formule à prouver. Cela ne signifie pas que ce fragment est décidable ; il ne l'est pas. Dans la suite, nous ne considérerons plus que le calcul des prédicats intuitionniste.

La polarité rend partiellement compte de la distinction habituelle en programmation logique entre programme (ensemble de clauses) et but. Les buts sont des formules positives et les clauses des formules négatives. La forme des clauses peut être encore restreinte pour leur donner l'apparence de règles de déduction avec une conséquence (la tête*) bien distinguée des prémisses (le corps*). La grammaire suivante décrit des formules héréditaires de Harrop où les occurrences négatives de l'implication (c'est-à-dire dans les clauses) ne peuvent avoir comme conclusion que des formules atomiques.

Cependant, cette dissymétrie n'est pas fondamentale, et n'est qu'une présentation d'une logique totalement symétrique. Nous allons retrouver une présentation totalement symétrique en appliquant progressivement des identités logiques.

La première chose est d'observer que les peuvent être remplacés par un  bien choisi et construit avec un nouveau symbole de prédicat, à condition que la formule soit ajoutée au programme. De même, les peuvent être remplacés par un bien choisi et construit avec un nouveau symbole de prédicat, à condition que la formule soit ajoutée au programme. Dans les deux cas, le programme original et le programme résultat ne sont pas équivalents, à cause des nouveaux symboles de prédicats, mais ils fournissent les mêmes réponses si on n'utilise que la signature originale. On peut ainsi éliminer les occurrences positives de la disjonction et de la quantification existentielle, et donc toutes leurs occurrences. On obtient alors le langage décrit par la grammaire suivante :

L'identité suivante

est une identité intuitionniste pour les deux polarités. Elle permet d'introduire des conclusions d'occurrences négatives de l'implication qui sont elles-mêmes des implications. De la même manière, on observe que les identités suivantes

sont des identités intuitionnistes pour les deux polarités. Elles permettent d'introduire des conjonctions et des quantifications universelles comme conclusions d'occurrences négatives de l'implication.

À ce stade, le langage des formules positives est le même que celui des formules négatives. On peut donc les confondre. Le langage logique obtenu n'utilise que les connecteurs «et» et «implique» ( et ), et le quantificateur «quel que soit» (), et il les utilise sans restriction.

Prolog est la présentation dissymétrique de cette logique. La présentation symétrique montre que cette logique est relativement simple, mais la présentation dissymétrique est nécessaire pour donner une sémantique opérationnelle au langage. C'est elle qui oriente les formules et permet de les décomposer en tête* et corps* analogues à l'en-tête et au corps d'une procédure d'un langage impératif.

Il faut bien noter qu'ici la forme clausale ne résulte pas d'une mise sous forme normale conjonctive* avec skolémisation* (chose qui n'a pas de correspondant intuitionniste), mais seulement d'une présentation dissymétrique d'une logique parfaitement symétrique. On peut observer que si on interdit les occurrences positives de l'implication et de la quantification universelle, ce qui reste constitue les clauses de Horn*. De plus, les conséquences intuitionnistes d'une théorie de Horn sont les mêmes que les conséquences classiques. On en conclut donc que l'interprétation intuitionniste des formules héréditaires de Harrop (le noyau de Prolog) contient strictement l'interprétation classique des formules de Horn (le noyau de Prolog).

Comme en Prolog, l'unification est une opération importante du schéma d'exécution, et pour qu'elle soit bien définie on restreint le domaine des -termes à un domaine fortement normalisable* et où le problème d'unification n'est pas trop difficile. Pour cela, on choisit le domaine des -termes simplement typés* [Church 40], mais d'autres domaines fortement normalisables conviendraient. Il faut noter que les -termes simplement typés constituent un bon compromis entre un problème d'unification qui n'est pas trop difficile en pratique, même si certains le jugent déjà trop difficile parce que seulement semi-décidable* et infinitaire*, et la valeur ajoutée d'une discipline de type à la . Rappelons cependant que Prolog n'est pas typé, et que c'est pour cela que Prolog n'est pas un sur-ensemble strict de Prolog.

La motivation de la métaprogrammation nous a donc conduit à un langage de programmation logique dont la structure logique est plus riche que celle de Prolog et dont le domaine de calcul est celui des -termes simplement typés. L'enchaînement des motivations peut être résumé comme suit :

1. Les structures objet introduisant des noms munis d'une notion de portée sont commodément représentées par des -termes et les calculs sur ces structures utilisent la -équivalence*.
2. Pour parcourir les -termes représentant les structures objet sans introduire de -variables libres il faut les appliquer à des constantes universelles, celles-ci sont introduites par les quantifications universelles dans les buts.
3. Cette opération n'est valide qu'en présence de l'axiome de -équivalence.
4. Ces constantes universelles doivent être dotées de propriétés que l'on peut introduire par l'effet de l'implication dans les buts.
5. Pour que le problème d'unification soit mieux défini, il faut restreindre le domaine des -termes. Le typage simple convient assez bien : il délimite un domaine qui est encore utile, le problème d'unification associé est résoluble en pratique et il offre en prime une discipline de type communément admise dans d'autres langages.