Best viewed in 24pt and full-screen

S

type (s, scission) (list A) -> (list A) -> (list A) -> o .
dynamic s .
s [X|Xs] [_ , _|Cs] [X|Ls] :- s Xs Cs Ls .
scission List Left Right :- s Right [] [] => s List List Left .

Scission d'une liste de longueur paire en deux moitiés.

S. (rel. logique combinatoire*) Combinateur de la logique combinatoire régi par l'axiome suivant.

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

type comb_S ((A->B->C)->(A->B)->A->C) -> o

comb_S S :- pi x(pi y(pi z( (S x y z) = (x z (y z)) ))) .

Semi-décidable. adj. (rel. décidable*) Se dit d'un problème de décision pour lequel il n'existe au mieux que des procédures qui terminent toujours dans les cas de succès et peuvent ne pas terminer dans les cas d'échec. On appelle ces procédures des semi-algorithmes.

Séquent. n.m. (rel. calcul des séquents*) Assemblage de formules qui énonce que la disjonction des est une conséquence de la conjonction des . Un cas particulier intéressant est celui des séquents intuitionnistes. Ce sont les séquents où .

Un autre cas particulier est celui des séquents de type. Un séquent de type énonce que  a le type dans le contexte . La forme exacte du contexte dépend du système de type et de sa présentation, mais il s'agit généralement d'une collection d'assertion de typage, . Par exemple, dans le cas des types simples*, les sont des -variables*.

Dans tous les cas, on appelle conséquent la partie droite d'un séquent et antécédent, la partie gauche.

sigma. synt.progr. (rel. pi*) Notation concrète du quantificateur existentiel, , en Prolog.

Ce connecteur est définissable en Prolog de la manière suivante :

type sigma (_->o) -> o .

sigma B :- (B _) .

Signature. n.f. Ensemble de constantes typées. La signature d'un programme est l'ensemble des constantes qui y figurent. Dans la pratique, elles et leurs types sont déclarés. La signature d'un séquent* dans une preuve consiste en la signature du programme plus toutes les constantes universelles* «inventées» par la règle d'introduction de la quantification universelle à droite dans des séquents situés plus près de la racine de la preuve.

Simplification. n.f. (abr. ) Une des opérations élémentaires du semi-algorithme de Huet*.

La simplification décompose un problème d'unification d'ordre supérieur en des problèmes où  est flexible.

La simplification s'apparente à l'unification de premier ordre mais doit prendre en compte les -abstractions*. Dans la pratique, on la fait précéder de la procédure d'unification au premier ordre qui pourra traiter le problème efficacement si aucune -abstraction n'est rencontrée. On peut ainsi compiler la partie premier ordre de l'unification en réutilisant les techniques connues pour Prolog* [Brisset et Ridoux 92b, Brisset et Ridoux 94].

Skolem, Albert Thoralf (Norvège, 1887-1963). Skolem établit la version définitive du théorème de Löwenheim-Skolem : tout ensemble satisfaisable d'expressions du premier ordre admet un modèle dénombrable. Il a introduit une forme d'élimination de quantificateur qui constitue un premier pas vers la théorie de Herbrand* ( skolémisation*).

Skolémisation. n.f. Opération qui consiste à éliminer des quantificateurs existentiels en remplaçant les variables qu'ils introduisent par des termes constitués de constructeurs nouveaux appliqués aux variables universelles dont dépendent les variables existentielles éliminées.

C'est la forme de skolémisation utilisée dans le cadre de la résolution* pour mettre la formule à réfuter en forme normale conjonctive*. On peut aussi la présenter sous une forme duale à utiliser pour la recherche d'une preuve.

Dans les deux cas, l'objectif est de n'avoir plus qu'une sorte de quantificateur dans des formules prénexes*. La forme sans quantifications existentielles (forme normale de Skolem pour la réfutation) est utilisée pour la résolution*. Dans ce cas, c'est le test d´occurrence* de l´unification* qui va rétablir l'effet des quantifications éliminées.

Au lieu d'inventer une constante, on peut la laisser introduire par une quantification universelle. La skolémisation devient alors permutation de quantificateurs.

Dans ces trois cas, il faut bien noter que la formule skolémisée n'est pas équivalente à la formule originale. C'est le cas même pour la troisième version, car le type de  qui pouvait être vide dans l'original a le constructeur  dans le résultat.

On peut aussi définir une forme d'antiskolémisation qui a pour effet la permutation inverse.

Il faut noter que cette transformation préserve l'équivalence. Elle a été étudiée par Miller [Miller 92], et elle ou son inverse peuvent être employées par l'interpréteur Prolog ( partage de représentation*), ou par le programmeur.

Les relations et peuvent être définies en Prolog de la manière suivantes :

skolem (existe Y(qqsoit x(F Y x))) (qqsoit f(existe Y(F Y (f Y)))) .

askolem (qqsoit x(existe Y(F x Y))) (existe f(qqsoit x(F x (f x)))) .

Standard Prolog. Forme normalisée de Prolog*.

Substitution. n.f. (rel. unification*) Opération qui consiste à remplacer dans un terme toutes les occurrences libres* d'une variable par un autre terme. On la note ( est remplacée par ). L'opération s'étend au remplacement simultané de plusieurs variables. On appelle domaine de la substitution les variables remplacées, et codomaine les termes qui les remplacent.

Une substitution peut être spécifiée par des paires <variable,terme>, ou bien par un problème d'unification dont elle est la solution la plus générale, ou par une requête* à un programme logique* dont elle est la substitution solution*.

Substitution explicite. n.f. Dans la présentation classique du -calcul*, l'expression de la -équivalence* utilise la notion de substitution du métalangage. Il en résulte que la substitution, qui n'est pas une opération triviale, échappe à la formalisation du -calcul. D'où l'idée d'une présentation du -calcul dans laquelle les substitutions sont des objets du langage, et leurs lois sont décrites dans la formalisation du -calcul.

Les points de vue implicite et explicite ont aussi un impact sur l'implémentation du -calcul. Selon le point de vue implicite, la substitution est implémentée par une procédure qui est appelée à chaque -réduction*. Avec le point de vue explicite, la substitution est implémentée par une structure de donnée et des règles de réécriture spécifiques ont la charge de la propager.

Les substitutions explicites peuvent faire l'objet d'une étude de principe sous la forme de -calculs avec substitutions explicites [Abadi et al. 91] ou d'une étude plus technologique qui montre comment appliquer cette technique à un -calcul implicite [Revesz 88]. Nous avons suivi la seconde voie ( *), mais il faut noter qu'il est possible de présenter l´unification des termes d´ordre supérieur* dans un -calcul avec substitutions explicites [Dowek et al. 95].

Substitution solution. n.f. Le point de vue classique de la programmation logique sur la notion de résultat est que le résultat d'un calcul (donc de la recherche d'une preuve) est une substitution qui appliquée à la requête, la rend tautologique. Un interpréteur calcule les plus générales d'entre elles qu'on appelle substitutions solutions.