Best viewed in 24pt and full-screen

V-W

% v_i : vanilla interpreter
type v_i o -> o .
v_i true .
v_i (B1 , B2) :- v_i B1 , v_i B2 .              %
v_i B :- clause B C , v_i C .                    % et

Écriture en Prolog du méta-interpréteur de Prolog en Prolog. La
recherche en profondeur et l´unification sont complètement sous-
traitées au métalangage.

Vanilla interpreter. n.m. (anglo-américain pour interpréteur de base, par analogie avec la crème glacée de base qui serait toujours à la vanille) Le méta-interpréteur de Prolog écrit en Prolog qui sert de base à de nombreux autres développements en métaprogrammation ( prédicat v_i*).

On peut ajouter à l'interpréteur de Prolog les règles suivantes pour en faire un interpréteur de Prolog :

v_i (sigma B) :- v_i (B _) .                                %

v_i (pi B) :- pi c( v_i (B c) ) .                          %

v_i (H => B) :-                                                 %
         ( pi B(pi C( clause B C :- instance B H C )) => v_i B ) .

type instance o -> o -> o -> o .

instance B (pi H) E :- instance B (H _) E .       %

instance B (B :- C) C .                                      %

On peut ajouter à cet interpréteur des paramètres et des opérations de contrôle pour construire une trace des calculs, instrumenter la démonstration, ou bien la rendre complète. Ce ne serait plus un vanilla interpreter ( un méta-interpréteur complet*).

-Variable. n.f. Désigne une variable introduite par une -abstraction*. Les -variables* acquièrent une valeur par le biais de la -réduction*. On peut les interpréter comme les paramètres formels d'une fonction.

Variable logique. n.f. Désigne une variable qui résulte de l'élimination d'une quantification essentiellement existentielle*. Elle désigne un terme inconnu qui pourrait satisfaire la formule quantifiée. Leur valeur se précise par le biais des substitutions* calculées par l´unification*.

Variable objet. n.f. (rel. métaprogrammation*) Variable des structures manipulées par un métaprogramme. Un enjeu de la métaprogrammation est de préserver à la fois la substituabilité et la portée des variables objet. Les solutions traditionnelles de Prolog (représentations close* et non close*) sacrifient l'une ou l'autre de ces propriétés. La solution Prolog (représentation par abstraction*) les préserve toutes les deux.

Variable de type. n.f. Variable apparaissant en position de type. Une variable dans un type assigné à une expression, est généralement considérée comme étant universellement quantifiée. Ainsi, la déclaration

type cons A -> (list A) -> (list A) .

se lit «pour tout type , cons est de type ». C'est le point de vue du polymorphisme générique à la . C'est aussi le point de vu explicité dans certains articles sur Prolog [Miller et Nadathur 86b]. Cependant, ce point de vue n'explique pas bien le rôle des types lors de l'exécution. Il est significatif que le théorème de correction sémantique du typage à la permet justement de ne plus avoir de types lors de l'exécution [Milner 78].

Un autre point de vue est de considérer une variable de type comme signifiant un paramètre de type [Louvet et Ridoux 96, Louvet 96]. Dans ce cas, la déclaration précédente se lit «pour tout type , (cons ) est de type ». Ici, est passé en paramètre de cons. C'est le point de vue du polymorphisme paramétrique*.

Vrai. n.m. (rel. faux*) En Prolog, on peut coder le vrai (la tautologie) et le faux (l'absurdité) sans faire référence à un domaine de calcul, ni à une signature particulière. Par exemple,

... :- sigma X(pi y( X = y )) .

et

... :- pi x( sigma Y(x = Y) ) .

ne dépendent pas d'un domaine de calcul, mais un peu de la signature. En effet, il faut que la relation = corresponde bien à l'égalité. On peut s'affranchir de tout contexte avec les formules suivantes.

... :- pi pp .

et

... :- pi p( p => p ) .