Best viewed in 24pt and full-screen

H

type horn formule -> (A->A->A) o .
horn (A / B) Pol :- horn A Pol , horn B Pol .
horn (qqsoit F) MOINS :- pi x( horn (F x) MOINS ) .
horn (A => B) MOINS :- horn A PLUS , horn B MOINS .
horn (A / B) PLUS :- horn A PLUS , horn B PLUS .
horn (existe F) PLUS :- pi x( horn (F x) PLUS ) .

Spécification des formules de Horn en termes de polarités*.

Harrop, Ronald (1926) [Harrop 56, Harrop 60]. Après avoir montré que des énoncés de la forme (ou ) ne sont démontrables que si soit  soit  l'est (ou l'est pour un terme ), Harrop a recherché des résultats similaires pour des énoncés de la forme (ou ). La question est donc de savoir si on peut se contenter de preuves constructives* pour démontrer ces énoncés. Harrop a montré que pour que la démontrabilité de ces formules puisse se réduire à la démontrabilité constructive, il fallait que les occurrences de  et  dans la formule  soient contraintes. Cette contrainte aboutit à la notion de formule de Harrop, et à celle de formule héréditaire de Harrop* si on veut que toutes les étapes de la démonstration de  ou  (ou ) soit constructives.

C'est cette propriété de constructivité qui permet de conserver en Prolog la notion de réponse qui existe en Prolog (voir la section «Prolog -- clauses de Horn et programmation logique»*).

Ronald Harrop est actuellement (1998) professeur émérite à l'université Simon Fraser de Vancouver, où il étudie les applications médicales de l'informatique (radiothérapie, tomographie).

Harrop (formules héréditaires de). n.f. Formule engendrée par le non-terminal de la grammaire suivante :

Les non-terminaux , et engendrent respectivement les clauses, les buts et les formules atomiques* (ou atomes). Par convention, ces dernières sont des -termes simplement typés* de type o* ().

Les catégories et sont souvent notées  et  pour goal (but*) et definite clause (clause définie*). Malheureusement, ce  et ce  deviennent perturbants quand on considère l'habitude, venant de la théorie des preuves en calcul des séquents, d'appeler les formules analogues à celles de  des formules de droite, et formules analogues à celles de  des formules de gauche.

On peut spécifier en Prolog la structure des formules héréditaires de Harrop de la façon suivante. Plutôt que d'utiliser deux règles pour les clauses et les buts, on n'utilise qu'une règle munie d'une polarité*.

type harrop formule -> (A->A->A) -> o .

harrop (A / B) Pol :- harrop A Pol , harrop B Pol .

harrop (qqsoit F) Pol :- pi x( harrop (F x) Pol ) .

harrop (A => B) Pol :- harrop A (INV Pol) , harrop B Pol .

harrop (A / B) PLUS :- harrop A PLUS , harrop B PLUS .

harrop (existe F) PLUS :- pi x( harrop (F x) PLUS ) .

On peut aussi proposer la définition suivante qui véhicule mieux l'intuition que les formules de Harrop sont des formules de Horn «augmentées».

harrop F Pol :-
         (     pi F( horn (qqsoit F) PLUS :- pi x( horn (F x) PLUS ) )
         => pi A(pi B( horn (A => B) PLUS :- horn A MOINS , horn B PLUS ))
         => horn F Pol ) .

Hauptsatz. n.m. (rel. Gentzen*, calcul des séquents* et coupure*) (allemand pour «théorème fondamental»). La règle de coupure est redondante et peut être éliminée. Dans le cas où des axiomes sont ajoutés au calcul des séquents pour représenter une théorie par rapport à laquelle se font les preuves, les applications de la règle de coupure qui concernent ces axiomes ne peuvent être éliminées.

La redondance concerne les théorèmes, mais pas les preuves. Les mêmes théorèmes peuvent être prouvés avec ou sans règles de coupure, mais pas nécessairement avec les mêmes preuves.

Il est heureux que la règle de coupure soit redondante car c'est la seule du calcul des séquents qui n'a pas la propriété de la sous-formule. En effet, la formule  qui est partagée par les prémisses ne figure pas dans la conclusion. Cela pose problème pour une procédure de recherche de preuve qui utilise les règles de déduction de bas en haut.

On peut alors se demander pourquoi la règle de coupure figure dans le système déductif initial. D'une part, elle a un contenu intuitif évident, celui de démontrer des lemmes séparément et de les utiliser dans une preuve. Elle a donc sa place à côté des autres règles qui elles aussi ont un contenu intuitif évident. D'autre part, elle résume des propriétés métalogiques du calcul des séquents : beaucoup de métathéorèmes se démontrent avec son aide. En fait, elle résume tellement bien le calcul des séquents qu'elle possède une variante qui est complète pour une présentation appropriée du calcul des prédicats : la règle de résolution*. Dans ce cas, la théorie est entièrement représentée par des axiomes, les clauses*, et la règle de coupure ne peut pas du tout être éliminée.

Herbrand, Jacques (Paris, 1908-La Bérarde, 1931) [Herbrand 68]. En étudiant l'Entscheidungsproblem (le problème de reconnaître si une proposition est vraie ou non dans une théorie du calcul des prédicats), Herbrand a montré qu'il n'était pas nécessaire de considérer un univers arbitraire d'interprétation des formules, mais qu'il suffisait de considérer une suite croissante d'interprétations par des termes construits à l'aide des symboles de la théorie et de symboles représentant l'imbrication des quantificateurs. Une formule est valide si et seulement si elle est validée par l'une de ces interprétations. L'argument de croissance de la suite est la taille des termes des interprétations.

Le théorème de Herbrand conduit à une syntaxisation de la sémantique. On peut y voir aussi un passage du calcul des prédicats au calcul propositionnel puisque l'interprétation des formules donne des formules sans variables ; Herbrand propose donc une technique d'élimination des quantificateurs.

L'application la plus connue du théorème de Herbrand est le principe de résolution* de Robinson. Ce principe permet de calculer le modèle de Herbrand qui invalide la théorie augmentée de la négation du théorème (preuve par réfutation) à l'aide d'une combinaison de l'opération d´unification* et de la règle de coupure*. Une spécialisation de la résolution est au cur de la sémantique opérationnelle de Prolog.

Un trait important des travaux de Herbrand est l'approche constructive : les définitions sont conçues comme des algorithmes qui construisent des objets et les propriétés sont décrites avec les algorithmes qui permettent de les vérifier. C'est ainsi que, ayant à résoudre des systèmes d'équations sur les termes de ses interprétations, Herbrand décrit ce qui passe pour être la première expression de la procédure d'unification.

1. Si une des égalités à satisfaire égale une variable restreinte [essentiellement existentielle*] à un autre individu, ou bien cet individu contient , et on ne peut y satisfaire [test d´occurrence*], ou bien il ne contient pas  ; cette égalité sera alors une des égalités associées cherchées [une substitution solution*] et on remplacera  par cette fonction dans les autres égalités à satisfaire.
2. Si une des égalités à satisfaire égale une variable générale [essentiellement universelle*] à un autre individu, qui ne soit pas une variable restreinte, il est impossible d'y satisfaire.
3. Si une des égalités à satisfaire égale à , ou bien les fonctions élémentaires et sont différentes, auquel cas il est impossible d'y satisfaire, ou bien les fonctions et sont les mêmes, auquel cas on remplace l'égalité par celles obtenues en égalant à .

En proposant des définitions constructives de fonctions de plus en plus complexes, Jacques Herbrand a aussi contribué à l'émergence de la notion de fonction récursive générale [Herbrand 68, Kleene 71, Chabert et al. 94].

Herbrand (base de). n.f. (rel. Herbrand*) Ensemble des formules atomiques* finies qui peuvent être construites avec les symboles de prédicat et les constructeurs de termes d'un programme. La sémantique déclarative de Prolog* fait correspondre à tout programme une partie de sa base de Herbrand, qui est un modèle du programme.

Herbrand (univers de). n.m. (rel. Herbrand*) Ensemble des termes finis qui peuvent être formés avec les constructeurs de termes d'un programme.

En Prolog, on étend cette notion en considérant l'ensemble des combinateurs -normaux qui peuvent être formés avec les constructeurs de termes d'un programme.

. n.f. Higher-order Hereditary Harrop Grammar ou grammaire en formules héréditaires de Harrop* d'ordre supérieur [Le Huitouze et al. 93a]. Résulte de la transposition à Prolog* du principe des * (voir section «Prolog et grammaires logiques»*).

Horn, Alfred [Horn 51]. En étudiant les relations entre des structures , ..., et vis-à-vis de la satisfaction d'une axiomatisation , Horn a montré les deux théorèmes suivants (entre autres) : (a) si  a une forme conjonctive prénexe* dont les facteurs de la matrice* contiennent au plus un littéral* positif* (en termes modernes, une théorie de Horn), et si  est vraie de chacune des , alors  est vraie de , (b) si les sont les mêmes pour chaque , si  a une forme prénexe sans quantificateur existentiel, et si  est vraie de , alors  est vraie de .

Une conséquence importante est que si deux structures et satisfont une théorie de Horn, alors leur intersection la satisfait aussi. Par (a), la satisfait, et puisque il n'y a pas de quantification existentielle, la restriction de à la satisfait, et enfin, par (b), la satisfait.

Les exemples suivants montrent le rôle des hypothèses des théorèmes (a) et (b). Les structures et satisfont l'axiome , mais la structure

ne la satisfait pas. Inversement, la structure satisfait l'axiome , alors qu'aucune des structures  ou  ne le satisfait.

En terme de modèle, les théorèmes de Horn permettent d'isoler un unique plus petit modèle de Herbrand* pour les théories de Horn, et donc de donner la sémantique des programmes Prolog*. Par définition, la sémantique d'un programme Prolog est son unique plus petit modèle de Herbrand*.

Horn (clause de). n.f. (rel. Horn*) Clause* qui ne contient pas plus d'un littéral* positif*. On appelle tête l'éventuel littéral positif et corps les littéraux négatifs*. En général, on note la clause comme une implication .

On appelle clause définie une clause de Horn qui a exactement un littéral positif. On appelle clause unitaire ou fait* une clause définie dont le corps est vide.

Un programme Prolog* est un ensemble fini de clauses de Horn. Les modèles des théories décrites par des clauses de Horn ont la propriété de constituer une collection fermée par intersections : l'intersection de deux modèles est encore un modèle.

Huet (semi-algorithme de). n.m. Procédure qui calcule les préunificateurs* d'un problème d´unification d´ordre supérieur*. La procédure parcourt un arbre de recherche dont les nuds sont étiquetés par des problèmes d'unification d'ordre supérieur et les arcs sont étiquetés par des substitutions*. Un invariant est que tout préunificateur du problème d'unification d'ordre supérieur qui étiquette la racine de l'arbre est la composition des substitutions trouvées sur l'arête de l'arbre qui mène à un nud et d'un préunificateur du problème d'unification qui étiquette ce nud. Les nuds feuilles peuvent être soit en échec si on a détecté une contradiction dans le problème associé, soit en succès si on a détecté que le problème associé a une solution triviale, soit ouverts dans les autres cas. L'objectif du développement de l'arbre est de n'avoir plus que des nuds en échec ou en succès.

Le développement de l'arbre se fait à l'aide de plusieurs opérations élémentaires qui terminent toujours. Que l'unification ne termine pas se traduit donc exclusivement par le développement d'un arbre infini.

 

Huet présente une version de l'algorithme qui résoud les problèmes d'unification modulo -équivalence et des commentaires qui explique comment cet algorithme se spécialise pour la -équivalence. C'est cette dernière version qui est utilisée en Prolog et c'est la seule que nous décrivons.

L'opération élémentaire de simplification * permet de détecter les contradictions dans un nud ouvert ou, en leur absence, de ramener tout problème à des sous-problèmes de la forme où  est flexible. Elle vérifie aussi que les constantes ou variables essentiellement universelles qui apparaissent en tête des termes d'une même paire sont compatibles. Quand ce n'est pas le cas, le nud est déclaré en échec.

L'opération élémentaire * s'applique à des paires flexibles* et permet de détecter les problèmes résolus. Elle reconnaît des formes particulières de problème qui peuvent être résolues sans utiliser la procédure générale. Elle a un rôle heuristique important et il faut que les formes reconnues couvrent effectivement les cas «triviaux».

L'opération élémentaire * s'applique à des paires flexible-rigide* non-résolues et dérive de nouveaux nuds fils du nud ouvert en inventant de nouvelles substitutions dont le domaine est la variable en tête* de .