( eta_exp (app E x) Type2 (F x) ) . 
-Expansion de termes du niveau objet.
Élimination des coupures.
n.f.
(
calcul des séquents*, Gentzen* et Hauptsatz*)
Élimination des quantificateurs.
n.f.
Technique qui permet de ramener des preuves dans le
calcul des prédicats à des preuves dans le calcul propositionnel.
Le théorème de Herbrand*,
le principe de résolution* de Robinson,
et les règles d'introduction du
calcul des séquents*
(quand elles sont interprétées «de bas en haut»)
décrivent des techniques d'élimination des quantificateurs.
Le théorème de Herbrand permet de se ramener à chercher une
formule prouvable parmi une suite de formules sans quantificateur ni variable.
Le principe de résolution permet de se ramener à l'application d'un
modus ponens généralisé.
Les règles du calcul des séquents permettent
de se ramener à des formules sans quantificateur.
.
[Elliott et Pfenning 91]
Le système
est la première implémentation complète de 
Prolog.
C'est un interpréteur écrit en Common Lisp par Frank Pfenning de
l'université de Carnegie Mellon et Amy Felty du laboratoire
Bell Labs de 
( à l'époque de ce développement -- 1991 --,
Lucent Technologies maintenant).
Cette équivalence formalise le renommage des variables.
Par exemple,
mais
car
.
La 
-équivalence est automatiquement prise en compte par la
représentation des -termes de niveau objet proposée.
Il n'y a donc pas d'expression explicite de la
-équivalence.
Cette équivalence formalise l'évaluation d'une application par substitution d'un
terme, 
, à un paramètre formel, 
.
Par exemple,
mais
car 
est libre dans elle-même et liée dans
.
Cependant,
.
Il est possible de satisfaire la précondition de
la 
-équivalence pour tout terme de la forme 
en utilisant la -équivalence pour renommer les variables
liées de 
.
On peut représenter cette relation en Prolog pour des
-termes de niveau objet
de la façon suivante :
type beta l_terme -> l_terme -> o .
beta (app (abs E) F) (E F) .
En fait,
on a utilisé la -équivalence du métalangage, Prolog.
Cette équivalence
est une forme faible de la -équivalence qui s'applique
seulement lorsque le membre gauche du -rédex est lui-même un
-rédex.
C'est une circonstance très fréquente en
Prolog
et qui permet de représenter les termes sous leur forme -longue*
sans encourir de surcoût.
En effet,
l'implémentation de cette équivalence ne nécessite ni renommage ni recopie.
On peut représenter cette relation en Prolog pour des
-termes de niveau objet
de la façon suivante :
type beta_eta l_terme -> _terme -> o .
beta_eta (app (abs (app E)) F) (app E F) .
Cette équivalence est une forme faible de la -équivalence qui s'applique
seulement lorsque le paramètre effectif est une variable
qui n'apparaît pas libre dans la fonction.
Si est une variable,
la -conversion de en 
rend la condition vraie
(car 
)
et trivialise le calcul de 
.
La 
-réduction revient donc à un renommage de variable.
La 
-équivalence est à la base de la définition d'un fragment de
Prolog,
appelé 
*
pour lequel l´unification*
est décidable* et unitaire*.
Cette équivalence
formalise le principe d´extensionnalité des fonctions* :
deux fonctions qui rendent partout le même résultat sont les mêmes.
Il permet de montrer
.
Par exemple,
mais 
car 
.
Contrairement à ce qui se passe pour la -équivalence*,
la -équivalence* ne peut jamais rien
pour satisfaire la précondition de la -équivalence*.
On peut représenter cette relation en Prolog pour des
-termes de niveau objet
de la façon suivante :
type eta l_terme -> l_terme -> o .
eta (abs (app E)) E .
-Équivalence.
n.f.
Plus petite relation d'équivalence définie par congruence
sur la syntaxe des -termes*
et contenant la -équivalence*,
la -équivalence*,
et optionnellement la -équivalence*.
Les équivalences et sont toujours adoptées
dans le -calcul,
mais l'équivalence est optionnelle.
Ce qui ne signifie pas qu'elle est sans effet.
Seulement,
elle n'intervient pas dans la puissance de calcul du
-calcul.
-Expansion.
n.f.
Action de réécrire un terme 
en 
,
où a un type de la forme 
et où
n'a pas d'occurrence libre dans
.
Combinée avec la -réduction*, cette opération
produit la forme normale -longue*.
Extensionnel.
adj.
(ant. intentionnel*)
Se dit d'un procédé point par point pour définir des ensembles
ou des fonctions, ou pour prouver des propositions.
La définition d'un ensemble par ses éléments est extensionnelle,
ainsi que la définition d'une fonction par son graphe.
Une démonstration extensionnelle d'une quantification universelle peut
procéder par cas.
Extensionnalité fonctionnelle.
n.f.
Voir aussi extensionnalité en Prolog*.
Principe selon lequel deux fonctions qui rendent partout les mêmes
résultats sont égales :
Cette propriété n'est pas démontrable à l'aide des seules
équivalences * et *.
Il faut ajouter la -équivalence*
pour satisfaire ce principe.
Un point important à noter est que la -équivalence ne satisfait
complètement le principe d'extensionnalité que pour le
-calcul* pur (c'est-à-dire non-typé).
Dans le cas du -calcul simplement typé*,
des fonctions décrites par des -termes qui ne sont pas
-équivalents*
peuvent être extensionnellement égales sur les termes de leur type argument.
Cela est déjà vrai en dehors de tout typage lorsque l'on considère
pour arguments des ensembles particuliers de -termes.
Par exemple,
l'incrémentation des
entiers de Church* peut être
réalisée par deux -termes qui ne sont pas -équivalents,
mais qui pourtant donnent les mêmes résultats sur tous les entiers de Church.
Prouver l'équivalence
de ces deux -termes pour un domaine de termes
donné nécessite un principe de déduction plus fort :
l'induction sur la structure des termes.
,
si
.
,
si
.
-Équivalence.
,
si
.
,
si
.
,
si