ud (arbre2 A) -> (arbre2 A) -> (arbre2 A) . ud G D) F :- aplatir G Gf , aplatir D Df , conc Gf Df F . ud G D) --> aplatir_g G 
aplatir_g D .
-Abstraction.
n.f.
(rel. -calcul*)
(
ex.progr. déclaration de abs*)
Construction de la syntaxe du -calcul
qui lie une -variable* dans un -terme*.
Si 
est une -variable
et si 
est un -terme,
alors 
est une -abstraction.
On peut interpréter la -abstraction comme une fonction qui
à tout fait correspondre .
Les -abstractions sont engendrées par la règle de grammaire suivante :
où les 
sont les identificateurs de variables.
L'abstraction introduit les notions d'en-tête, de tête
et de corps.
Dans le terme 
,
l'en-tête est 
,
la tête est 
et le corps est 
.
On dit qu'une abstraction lie les variables de son en-tête.
On distingue ainsi entre occurrences de variable liées et libres.
Dans le terme 
,
n'a que des occurrences libres,
la seule occurrence de 
est liée,
et a une occurrence libre et une autre liée
(respectivement sa première et sa seconde).
Dans le sous-terme souligné,
et n'ont que des occurrences libres
et la seule occurrence de est liée.
Plus généralement,
une occurrence de variable est liée dans un terme de référence
si elle est sous-terme
d'une abstraction qui lie la variable et qui est sous-terme
du terme de référence.
Une occurrence de variable est dite libre si elle n'est pas liée.
On appelle variables libres d'un terme
les variables qui ont une occurrence libre dans le terme,
variables liées celles qui ont une occurrence liée dans le terme.
Un terme sans variables libres est appelé combinateur*.
Antécédent.
n.m.
( séquent*)
Antiskolémisation.
n.m.
( skolémisation*)
Application.
n.f.
( ex.progr. déclaration de app*)
Construction de la syntaxe du -calcul*
qui combine deux -termes*.
Si et 
sont des -termes, alors
est une application.
On peut interpréter l'application du
-calcul comme l'application d'une
fonction à un argument .
Les applications sont engendrées par la règle suivante :
On admet que l'application est associative à gauche,
ce qui rend certaines parenthèses inutiles :
par exemple,
dénote la même chose que 
.
1) En Prolog, désigne le nombre d'arguments que doit prendre un symbole fonctionnel pour produire un terme du premier ordre bien formé. C'est le minimum qu'on puisse faire en matière de typage.
En Standard Prolog*, plusieurs symboles fonctionnels d'arités différentes peuvent avoir le même nom et cela peut laisser penser que ce minimum n'est même pas vérifié. Il n'en est rien car, il s'agit là des noms externes des symboles fonctionnels, que les concepteurs ont jugé bon de pouvoir surcharger. Les noms internes sont distingués par un suffixe qui dénote l'arité. Par exemple, f/1 est distingué de f/2.
2)
En Prolog,
l'arité d'un constructeur de type est notée par une expression de la forme
.
L'arité est alors le nombre de
«
» dans l'expression.
Par exemple,
liste : 
est d'arité 1,
et
paire : 
est d'arité 2.
3)
En -calcul typé, désigne souvent la sorte des constructeurs
de type.
L'arité n'est alors pas toujours assimilable à un entier
(par exemple, le -calcul typé
d'ordre 
[Barendregt 91]).