Best viewed in 24pt and full-screen

I-J-K

type jointure (A->B) -> (B->C) -> (A->C) -> o .
jointure R1 R2 RJ :- pi x(pi y( RJ x y = sigma J( R1 x J, R2 J y ) )) .
ou
jointure R1 R2 xy(sigma J( R1 x J, R2 J y )) .

Jointure de deux relations. Version avec quantification universelle,
version avec -abstraction.

I. (rel. logique combinatoire*) Combinateur identité. Il est régi par l'axiome suivant :

Il est définissable en -calcul*, , en logique combinatoire, , et en Prolog :

type comb_I (A->A) -> o .

comb_I I :- pi x( I x = x ) .

Imitation. n.f. Une des opérations élémentaires du semi-algorithme de Huet*.

Pour chaque paire , où  est une tête flexible* (c'est-à-dire une variable logique*) et  est une tête rigide*, si  est une constante, la règle d'imitation produit la substitution* , où chaque représente une application , où  est une variable logique nouvelle et d'un type approprié.

Après application de la substitution, de la -réduction* et de la simplification*, le problème se ramène à résoudre les paires pour chaque  ().

Le principe de l'imitation est que puisque le terme rigide commence par un , on va tenter de substituer à . Cependant,  et ne sont pas nécessairement du même type et ne peuvent donc pas être substitués l'un pour l'autre. Par exemple,  attend  paramètres, alors que en attend . On va donc «habiller» de manière à obtenir un terme compatible avec  ; d'où les  abstractions pour les  paramètres de  et les qui dépendent des d'une manière laissée indéterminée.

L'introduction des fait qu'il n'est pas toujours possible de trouver un unificateur pertinent*.

Implication. n.f. (rel. implication classique* et implication intuitionniste*)

Implication classique. n.f. Connecteur logique formalisant la causalité et qui peut être décrit par la table de vérité suivante :

De cette table et de celles de la disjonction et de la négation il est facile de conclure que . Le fait que (ex falso quod libet sequitur) est la source d'un grand nombre de discussions et de contre-propositions.

Implication intuitionniste. n.f. Connecteur logique formalisant la causalité intuitionniste. Dans ce cadre, la preuve par l'absurde (reductio ad absurdum), le tiers-exclus (tertium non datur : ) et l'élimination de la double négation () sont invalides. L'implication intuitionniste ne peut pas être décrite par une table de vérité finie, mais elle peut l'être par des règles de déduction ( calcul des séquents*).

L'implication de Prolog doit être interprétée par la règle de déduction intuitionniste. En particulier, prouver que la prémisse est fausse n'est jamais utilisé pour prouver un but formé d'une implication.

Inconnue. n.f. ( variable logique*)

Indécidable. adj. (ant. décidable*)

Induction structurelle. n.f. ( induction structurelle en Prolog typé* et induction structurelle en Prolog*) Technique de programmation qui consiste à définir un calcul par récurrence sur la structure de ses entrées. Dans le cas de la programmation logique*, le calcul est défini par une relation et la notion d'entrée doit être relativisée ( réversibilité*), mais le concept s'applique aisément comme une discipline de programmation.

Dans le cas de langages de programmation typés, cette technique peut être formalisée plus précisément car les types fournissent une description formelle des structures attendues. Par exemple, dans un langage comme Prolog*, l'ensemble des termes qui ont un type donné est partiellement décrit par les constructeurs de terme* dont le type du résultat est le type en question. Une relation peut alors être définie au cas par cas en fonction des différents constructeurs du type de l'argument sur lequel est réalisée l'induction structurelle.

Le traitement de chaque cas est décrit par une règle associée à un constructeur et qui contient deux parties que l'on peut qualifier de syntaxique et de sémantique. La partie syntaxique consiste en des utilisations récursives de la relation à définir sur les arguments du constructeur qui ont le type considéré. La partie sémantique consiste dans l'application d'un prédicat à 1) tous les arguments du constructeur, 2) toutes les valeurs produites par les utilisations récursives de la relation et 3) la valeur associée au terme argument par la relation à définir.

Voir aussi la section «Transformations de grammaires en Prolog»* -- pour un autre exemple de séparation entre un composant syntaxique et un composant sémantique. Dans ce cas, le composant syntaxique représente une induction structurelle sur les règles d'une grammaire considérées comme les constructeurs d'un type d'arbre de dérivation.

Inférence de type. n.f. (rel. condition de tête*) Calcul de notations de type manquantes. La syntaxe abstraite d'un langage typé comprend souvent de nombreuses notations de type dont beaucoup sont redondantes et peuvent être reconstituées automatiquement. On souhaite donc que la syntaxe concrète les laisse implicites. Beaucoup d'auteurs associent d'une part le typage «à la Curry», la notation implicite des types et l'inférence de type, et d'autre part le typage «à la Church» et la notation explicite des types par des déclarations. Nous pensons qu'il s'agit d'une erreur d'interprétation et que l'inférence de type a à voir avec la différence entre syntaxe concrète et syntaxe abstraite. Les deux syntaxes obéissent à des économies différentes. L'économie de la syntaxe concrète est celle de l'écriture et de la lecture, alors que l'économie de la syntaxe abstraite est celle des manipulations formelles. Dans le premier cas, on privilégie la concision et pour cela on admet des notations contextuelles. Dans le second cas, on souhaite que les propriétés des composants d'une expression se voient facilement, et pour cela on préfère des notations moins contextuelles.

La théorie de l'inférence de type est très «fragile» au sens où elle dépend très brutalement des caractéristiques du langage. Par exemple, le problème d'inférence de type pour est décidable [Milner 78], et même relativement facile en pratique, et il devient indécidable si on autorise le polymorphisme dans les définitions récursives [Mycroft 84]. De la même manière, le problème d'inférence de type pour Prolog est décidable en l'absence de la condition de tête* [Hanus 89a, Hanus 89b] et indécidable en présence de cette condition (voir aussi section «Typage»*).

Intentionnel. adj. (ant. extensionnel*) Se dit d'un procédé générique pour définir des ensembles ou des fonctions, ou pour prouver des propositions. La définition d'un ensemble par la propriété qu'ont tous ses éléments et eux seuls est intentionnelle, ainsi que la définition d'une fonction par un procédé de calcul. Une démonstration intentionnelle d'une quantification universelle ne peut pas procéder par cas ; si une proposition universelle intentionnelle est vraie, non seulement il y a une preuve pour chaque point du domaine, mais elle est la même pour tous les points.

Prolog met en uvre le point de vue intentionnel. Les quantifications universelles permettent de spécifier qu'une relation doit vérifier certaines propriétés intentionnelles. Elles ne permettent pas de spécifier de propriétés extensionnelles. Par exemple, elles ne permettent pas de spécifier que deux relations ont le même graphe. Ainsi, n'est pas démontrable. En d'autres termes, la quantification universelle des formules de Harrop intuitionnistes n'a pas de caractère énumératif. Même si dans cet exemple on peut inférer que  est de type , la preuve du but universel ne se fera pas en remplaçant  par tous les individus possibles (, , ...). La variable  est simplement remplacée par une nouvelle constante, différente de tous les individus connus. Si une preuve est possible avec cette nouvelle constante, elle le sera avec n'importe quel individu. Donc, la formule ne signifie pas seulement que tout  (du bon type) a la propriété , mais aussi que la preuve est la même pour tous.

Itérateur. n.m. (rel. induction structurelle*) On peut déduire de tout type inductif* une fonction d'ordre supérieur qui remplace chaque constructeur d'un terme de ce type par des fonctions passées en paramètre [Böhm et Berarducci 85, Pierce et al. 89, Huet et al. 97]. On appelle cette fonction un itérateur. Cela formalise l'observation que beaucoup de programmes de calcul sur les listes (conc, longueur, etc.) se ressemblent et qu'il en est de même pour de nombreuses autres structures de données. En ce sens, choisir une structure de données c'est choisir une classe d'algorithmes, ceux qu'on peut définir avec l'itérateur de la structure de données. Il faut quand même remarquer que tout calcul sur un type n'est pas représentable par l'itérateur de ce type. Par exemple, le parcours dichotomique d'une liste n'est pas représentable de cette manière.

Les termes d'un type inductif peuvent être représentés par des -termes qui sont leurs propres itérateurs. Par exemple, la représentation des listes par les combinateurs suivants réalise cet effet :

NIL = cnn

CONS = gdcn(c g (d c n))

On peut aussi traduire chaque type inductif en un prédicat qui réalise son itérateur. Par exemple, le prédicat qui réalise l'itérateur des listes est le suivant :

type iter_liste R -> (A->R->R) -> (list A) -> R -> o .

iter_liste N C [] N .

iter_liste N C [E|Es] (C E T) :- iter_liste N C Es T.

Dans cette variante, le traitement appliqué à chaque cons est décrit par une fonction. On peut vouloir le décrire par un prédicat, surtout en Prolog où le langage des formules logiques est plus puissant que celui des termes. On obtiendrait ainsi la définition suivante :

type iter_liste R -> (A->R->R->o) -> (list A) -> R -> o .

iter_liste N C [] N .

iter_liste N C [E|Es] R :- iter_liste N C Es T , C E T R .

K. (rel. logique combinatoire*) Combinateur de projection. Il est régi par l'axiome suivant :

Il est définissable en -calcul* : et en Prolog :

type comb_K (A->B->A) -> o .

comb_K K :- pi x(pi y( (K x y) = x )) .