Les 
-termes du métalangage fournissent une notation convenable pour des
objets structurés qui introduisent une notion de portée.
Cependant,
ils font se poser un peu plus les problèmes de nommage.
En effet,
l'axiome de
-équivalence*,
qui dit comment on peut changer les noms en toute sécurité,
ne s'applique qu'aux noms liés par une
-abstraction* ;
il ne s'applique pas aux noms libres.
Or,
les occurrences libres de noms apparaissent naturellement quand
on parcourt une structure.
Nous allons utiliser comme exemple la règle de déduction qui décrit à quelle
condition une -abstraction 
a le type 
.
Dans ce qui suit,
tous les -termes appartiennent au niveau objet,
mais comme nous n'avons pas encore fait de choix de représentation a priori,
nous commençons par utiliser la notation habituelle.
Un des objectifs de l'analyse qui suit est précisément de motiver la
représentation à adopter.
La règle se lit de haut en bas pour la déduction,
«si le fait que 
est de type 
permet de montrer
que 
est de type 
,
alors est de type »,
et elle se lit de bas en haut pour l'inférence de type,
« doit être d'un type ,
tel que si est de type
alors est de type ».
La variable est liée par un dans la conclusion de la règle ;
il semble donc que l'on puisse la renommer
en utilisant la -équivalence.
Il n'en est rien car elle apparaît aussi libre dans la prémisse et là
la -équivalence n'y peut rien.
Donc une telle règle ne se lit pas seulement selon les lois du -calcul.
En général,
cette règle est assortie d'une condition de renommage des
-variables ou d'une structure du contexte 
qui permet qu'une
-variable masque les -variables homonymes
de portées plus grandes.
Dans la variante suivante,
la variable n'a plus à la fois des occurrences libres et des
occurrences liées.
Ici,
le nom qu'a la
-variable liée n'a plus d'importance.
La raison pour laquelle la -abstraction doit être appliquée
à une constante nouvelle est que des -abstractions imbriquées
peuvent utiliser le même nom de variable, , sous des types différents.
Par exemple,
dans 
le du sous-terme souligné est de type 
,
tandis que l'autre
est de type .
Chaque constante nouvelle correspond à la traversée d'une
-abstraction.
Elle est associée à un type dans le contexte,
,
et est «diffusée» dans le terme par application,
.
La condition que 
n'apparaît
ni dans ni dans en rappelle une autre.
En effet,
dans le calcul des séquents*,
la quantification universelle dans les conséquences est
décrite de la manière suivante :
On appelle ces constantes qui remplacent les variables universelles
des constantes universelles
(eigen-values en anglais).
On voit que la quantification universelle implémente naturellement la
condition de la seconde version de la règle de typage des
-abstractions.
L'observation que nous venons de faire sur les occurrences libres de noms
se généralise à d'autres relation que la relation de typage.
Il faut un moyen de parcourir une structure, tout en construisant un
contexte pour tous les noms dont on a déjà rencontré
la déclaration.
Pour ne pas introduire de -variables libres,
le seul moyen d'entrer dans une structure qui introduit un nom,
et qui donc est représentée par une -abstraction,
est d'appliquer la représentation de la structure à un
terme qui prendra la place du nom en toutes ces occurrences.
On ne peut pas choisir n'importe quel terme.
Par exemple,
les termes choisis pour remplacer deux noms qui pourraient
apparaître dans le même contexte doivent être différents.
Ils doivent aussi être différents des termes qui sont déjà
là dans la représentation de la structure.
En fait, si l'axiome d´extensionnalité des fonctions* est admis,
la seule solution est d'appliquer la représentation de la structure à
une constante universelle nouvelle.
À chaque traversée d'une structure qui augmente le contexte
correspond une quantification universelle.
L'axiome d'extensionnalité des fonctions
est nécessaire pour assurer que les conclusions
tirées des applications sont valides pour les abstractions.
En effet,
l'exploration d'une
-abstraction par application à des
constantes universelles revient à comparer des fonctions d'après leurs
comportements plutôt que d'après leurs définitions.
Cela ne peut se faire qu'avec l'hypothèse d'extensionnalité des fonctions,
qui est une conséquence de la 
-équivalence*.
Nous décidons donc de parcourir les -abstractions qui représentent des
structures qui introduisent des noms en les appliquant à des constantes
universelles de telle manière qu'il y ait une constante universelle par
-abstraction traversée.
Par définition, les constantes universelles sont nouvelles et ne font donc pas partie de la signature* du programme. Elles posent donc un problème nouveau lorsque l'exploration progressive d'une structure finit par les atteindre : aucune définition ne les concerne. Il faudrait pouvoir donner les propriétés des constantes universelles au moment où on les introduit et pour leur durée de vie seulement. C'est ce que permettent les quantifications qualifiées par un prédicat : par exemple,
Il faut se souvenir qu'une forme plus explicite de cette formule est
La conjonction existe naturellement dans les langages de programmation
logique comme Prolog, mais pas l'implication.
Plus exactement,
elle existe,
mais uniquement pour définir des clauses,
et pas pour construire des formules à démontrer.
Il faut donc l'ajouter.
En suivant cette idée,
le codage de la règle de typage des -abstractions
en une règle de déduction pour le calcul des prédicats serait le suivant :
Il reste à déterminer comment on reconnaît que 
est une
-abstraction.
Cela se fait simplement par marquage.
Une -abstraction objet ne se reconnaît pas par le fait qu'elle
est représentée par une -abstraction du métalangage,
mais simplement par le fait d'une marque.
D'ailleurs,
si on y réfléchit un peu,
on voit qu'il est impossible de tester qu'un terme du métalangage
est une -abstraction.
En effet, toute -abstraction est 
-équivalente
à une infinité d'applications :
par exemple,
Si on convient que la marque des -abstractions est abs,
on peut traduire la règle de typage des -abstractions
en la formule logique suivante où toutes les implications et quantifications
sont explicitées :
