Prolog 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 Prolog, les formules peuvent contenir des implications et des quantifications universelles en des positions qui sont interdites en Prolog. Les formules de Prolog sont en fait une extension stricte de celles de Prolog. Par exemple, dans les formules suivantes,
toute la partie soulignée est spécifique de Prolog.
À 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 , , , , et sont des identificateurs de variables, car ils sont introduits par des quantifications, et les , , , , , , et 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 () que contient () un récipient sont mortes (), ce récipient est stérile ()» et «Les grands-pères () qui se déduisent de ce que les pères présumés () sont considérés comme des pères () sont des grands-pères présumés ()». Leur présentation dans la syntaxe concrète de Prolog est la suivante :
s R :- pi B( (b B , c B R) => m B ) .
gpp GP PF :- (pi P(pi F(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 ( dans la première formule et 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 , alors que la seconde commence par . 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 Prolog 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 () ou une formule atomique* après une implication (). 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 Prolog, 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 Prolog 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,
le domaine de la variable est nécessairement constitué de fonctions puisque est appliquée à un .
Cette formule contient des termes plus complexes que les formules précédentes. Le terme est formé de l'application de la variable à la variable , et le terme est formé de l'application de la constante à la variable . Le rôle de est discuté à la section «Manipuler les expressions dans leur contexte»* --, mais nous pouvons déjà dire qu'il sert à construire une -abstraction* de niveau objet qui doit être distinguée d'une -abstraction du programme. Cette formule se paraphrase en «Si pour tout de type , est de type , alors est de type ». En d'autre termes, la constante représente la flèche des types de niveau objet, et la constante représente la relation de typage. La présentation de cette formule dans la syntaxe concrète de Prolog est la suivante :
ty (abs E) (fl A B) :- pi x( ty x A => ty (E x) B ) .
On peut aussi utiliser la notation du -calcul* pour désigner des fonctions particulières. Par exemple, dans la formule suivante
les expressions , et désignent respectivement la fonction identité, la fonction constante dont l'image est , et les fonctions qui ont la forme d'une somme. Il faut noter que si 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 dépendent ou non de selon les valeurs prises par ou .
On l'aura compris, la relation est un fragment de la relation de dérivation ; la formule est vrai si et seulement si est la dérivée de . Sa présentation dans la syntaxe concrète de Prolog est
d xx x1 .
d x( (A x) + (B x) ) x( (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 Prolog. La première est démontrable et l'autre non.
Introduire la seconde en tant que clause rendrait inconsistant n'importe quel programme Prolog. En revanche, considérée comme un but, elle échoue dans tous les programmes Prolog. 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 Prolog est la suivante :
pi p(p => p)
pi pp
Jusqu'à ce point les formules acceptées en Prolog constituent un sur-ensemble strict de celles que Prolog accepte. Cependant, les termes de Prolog sont aussi typés, ce qui n'est pas le cas des termes de Prolog. On pourrait typer les termes de Prolog de manière que tout terme de Prolog soit aussi un terme de Prolog, mais c'est précisément ce qu'on ne veut pas faire. Au contraire, les types de Prolog 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 Prolog car le type choisi pour les listes impose que tous les éléments d'une même liste aient le même type. Prolog 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 Prolog.
On présente pourtant souvent Prolog comme une extension de Prolog : on ajoute -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 Prolog*» de Prolog 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 à Prolog.