Notations - Généralités

1. Généralités

Les expressions

On se place sur un ensemble S* construit comme suit :

On a un ensemble S de symboles, S = {a,b,c,···,x,y,z,···}.
On a deux symboles spéciaux : λ et apply.
λ est le symbole d'abstraction du λ-calcul : il permet de construire des λ-expressions. apply est le symbole d'application d'une λ-expression sur un terme. L'usage n'ayant pas précisément fixé de notation, une application se représente par : λx.E a ou (λx.E a) ou (λx.E) a. Ici, on explicite l'application en la nommant : (apply λx.E a).
Un terme de S* est de la forme :
1. u : c'est un symbole (u∈S) ;
2. λx.E, où E∈S* : c'est une λ-expression ;
3. (f x1···xn), où f∈S : c'est l'appel d'une fonction primitive (c'est-à-dire un symbole qui admet une interprétation fonctionnelle implicite – ou au moins intuitive) ;
4. (apply f x1···xn), où f,x1,···,xn sont dans S* : c'est l'application du terme f sur les termes x1,···,xn ;
5. on utilise aussi des symboles primitifs, c'est-à-dire des symboles qui ont encore une interprétation intuitive.
Par exemple :
1. a,b,c,···,x,y,z,···
2. λx.(+ x 3) : c'est la fonction x:→(+ x 3)
3. (+ x y) : intuitivement c'est l'addition de x et de y
4. (apply λx.x a) : c'est l'application de la fonction x:→x sur le symbole a
5. 1,2,3,··· : intuitivement ce sont les nombres

L'interprétation

On définit une interprétation sur S* par les données suivantes :

On a un ensemble S de valeurs, S = {a,b,c,···,x,y,z,···}.
On a une application :

I : [S → S]×S* → S

(env,E) :→ I[env E]

où [S → S] est l'ensemble des fonctions :
- partiellement définies sur un sous-ensemble fini de S à valeur dans S,
- qui ont une valeur conventionnelle sur les symboles primitifs.
Dans la suite, on appelle ces fonctions des contextes d'évaluation ou encore des environnements.

Remarques

Intuitivement, on n'a qu'un nombre restreint de variables qui ont une valeur dans un environnement donné : c'est pourquoi on considère des fonctions partielles sur S. Inversement si on utilise dans un terme t une variable indéfinie dans un environnement env (un symbole qui n'a pas d'image par env), on interprète le terme t par une valeur constante o de S, qui représente l'indéfini. C'est-à-dire qu'on pose :

I[env t] = o

Savoir dans quels cas on considère qu'on utilise un symbole est l'objet de ce qui suit.

Les symboles primitifs s'interprètent de façon "naturelle" :

Si l'on a I[env x] = x et I[env y] = y, alors par exemple :

I[env (+ x y)] = (I[env +] I[env x] I[env y]) = (+ x y) I[env 1] = 1 I[env 2] = 2

et d'une façon générale, on note de la même manière un symbole primitif et sa valeur dans un environnement.

`I :`	`[S → S]×S*`	`→`	`S`
	`(env,E)`	`:→`	`I[env E]`