2.3. Curryfication et uplets
Formalisation des opérations et relations
Formaliser en théorie des ensembles chaque notion d'opération (resp. relation) d'arité fixe
n > 1, agissant comme structures n-aire entre n ensembles, requiert les
symboles suivants (généralisant le cas n = 1 des fonctions, accepté comme primitif):
- Une liste de n foncteurs de domaines (parfois non disponibles mais pas
nécessaires car les domaines sont généralement fixés par le contexte);
- Son évaluateur est un opérateur (resp. prédicat) d'arité n+1,
noté sous forme remplie comme f(x0,…,xn−1),
d'arguments une opération (resp. relation) n-aire f et ses n
arguments x0,…,xn−1;
- Son définisseur lie n variables à leurs
domaines respectifs sur un terme (resp. une formule)..
Donnons aux définisseurs d'opérations la notation suivante qui sera plus
tard (2.7) justifiée comme reflétant leurs définitions: dans le cas binaire (n = 2) les opérations
définies par un opérateur binaire A de domaines E et F seront notées
E×F ∋ (x,y) ↦ A(x,y)
Ayant vu ce que sont les opérations et relations (leurs rôles), discutons comment elles sont réductibles
à autre chose.
Un aspect est que les relations sont réductibles aux opérations, et vice-versa:
-
La notion de relation n-aire peut être construite comme une classe d'opérations
n-aires, en prenant la paire booléenne comme ensemble d'arrivée, comme on a
fait en 1.4 (pour les prédicats) et on formalisera en 2.4.
- Inversement, la notion d'opération
n-aire peut être construite comme une classe de relations d'arité n+1 (2.7).
Ces constructions sont utiles malgré la circularité (elles ne réduisent pas l'arité). Mais pour des
motifs fondateurs on a besoin d'une construction réduisant à des cas d'arité inférieure,
jusqu'aux ensembles et aux fonctions. Il y a en fait 2 telles constructions.
Curryfication
Les plus simples constructions des notions d'opérations n-aire à partir de nos outils primitifs pour
les fonctions, sont leurs représentations curryfiées, définies comme classes de fonctions en exprimant le
définisseur d'opération comme n usages successifs du définisseur de
fonction (un pour chaque variable liée); et donc l'évaluateur comme
n usages de l'évaluateur de fonctions. Pour n = 2, cela signifie qu'une
opération binaire sous forme curryfiée b de domaines E et F se définit par
un opérateur binaire B, et s'évalue en retour comme B, par les formules
b = (E ∋ x ↦
(F ∋ y ↦ B(x,y)))
Dom b = E ∧ ∀x∈E, Dom b(x) = F
∧ ∀y∈F, B(x,y) = b(x)(y)
dont l'équivalence, similaire à l'axiome 1. des fonctions, s'en déduit.
Le premier foncteur de domaine vient par Dom b = E, mais le second,
donné comme valeur commune de tous les Dom b(x), n'est défini que pour
E ≠ ∅. La fonction intermédiaire b(x) = (F ∋ y
↦ B(x,y)) représente le foncteur défini par B de paramètre
x (libre) et d'argument y (lié).
Cela fait en gros fonctionner chaque opération binaire comme un évaluateur de
fonction, en donnant à x un rôle de fonction d'argument y;
l'évaluateur de fonction curryfié rend simplement chaque fonction qu'il prend:
f ↦ ((Dom f) ∋ y ↦ f(y)).
De même, la notion de relation n-aire se définit sous forme curryfiée comme une classe,
donnant le rôle de définisseur à une succession de n−1 usages du
définisseur de fonction et 1 usage du symbole de compréhension.
Ainsi la forme curryfiée r d'une relation binaire de domaines E et F, se définit à
partir d'un prédicat binaire R, et s'évalue en retour comme R,
par les formules équivalentes
r = (E ∋ x ↦
{y ∈ F | R(x,y)})
Dom r = E ∧ (∀x∈E, r(x) ⊂ F
∧ ∀y∈F, R(x,y) ⇔ y ∈ r(x))
Cela ne laisse aucun moyen de définir le second foncteur de domaine
(F ne peut pas être restauré à partir de r).
Ces constructions ont le défaut de rompre la symétrie des rôles entre les arguments.
La méthode de construction suivante, par les uplets, conservera cette symétrie, et sera
généralement préférée pour cette raison.
Uplets
Pour toute théorie et tout nombre naturel n, une notion de n-uplet est une notion
construite comme domaine de variables servant à abréger une liste de n symboles de
variables appartenant à des notions données précédemment acceptées. Un 2-uplet s'appelle
un couple, un 3-uplet est un triplet, un 4-uplet est un quadruplet et ainsi
de suite. Ainsi, chaque uplet x (objet ainsi construit) représente une méta-fonction
d'«interprétation» de cette liste (méta-ensemble) de n variables, vers le modèle.
Les symboles définisseurs et évaluateurs des uplets ont une forme spéciale car, bien qu'étant
des méta-fonctions, les uplets jouent dans la théorie un rôle autre que ceux de foncteurs ou fonctions.
Un définisseur de n-uplets n'est pas un symbole liant mais un opérateur n-aire, qui
rassemble ses n variables en une en les prenant comme arguments
dans une parenthèse et séparées par des virgules: ( ,…, ).
Ainsi, chaque structure (resp. opération, relation) peut être re-formalisée comme
une structure unaire (resp. une fonction, une relation unaire) de domaine un type (resp. une classe qui
est en fait un ensemble) d'uplets, à utiliser avec le définisseur d'uplets qui convient.
Cela peut être implicitement fait en réinterprétant la notation: S(x,y)
peut être lu en voyant S soit comme une structure binaire (resp. opération, relation),
soit comme une structure unaire prenant comme argument le couple donné
par le terme (x,y) formé par le définisseur de couples d'arguments
x et y.
Le rôle de l'évaluateur de n-uplets est joué par une liste de n foncteurs
appelés projections qui extraient chaque variable de la liste donnée (en
donne la valeur). Cette liste
joue le rôle de l'évaluateur de fonctions curryfié dans le sens inverse, en fixant son
méta-argument dont le domaine (le domaine des uplets en tant que méta-fonctions)
n'est pas vu par la théorie comme un ensemble d'objets mais comme une liste de
n symboles à prendre séparément.
Les détails formels de cette construction varient selon que nous prenons une théorie générique ou une théorie des ensembles.
Axiome des uplets
Dans les théories génériques, ce doit être un type construit distinct pour non seulement
chaque n mais aussi chaque choix du type de chacune de ces n variables
(si on part d'une théorie avec plusieurs types - ce choix d'une liste de variables avec
leurs types revient au choix d'un type
de symbole de prédicat), mais cela forme directement une construction légitime (4.11).
Pour n=2 (les autres cas sont similaires), et pour un type P de couples
(x,y) où x,y ont les types E et F, les projections
π0 et π1 sont liées au définisseur de couples, par l'axiome
∀E x, ∀F y,
∀P z, (x = π0(z) ∧ y =
π1(z)) ⇔ (x,y) = z
qui implique
∀P z, (π0(z),
π1(z)) = z
∀E x,
∀F y, π0(x,y) = x
∀E x, ∀F y,
π1(x,y) = y
∀E x,x', ∀F y,y',
(x,y) = (x',y') ⇔ (x = x' ∧ y = y')
Uplets en théorie des ensembles
La théorie des ensembles n'ayant pas de types n'a besoin que d'une notion de n-uplet
pour chaque n. Mais il y a une difficulté: pour justifier rigoureusement que tous les
outils de la théorie des ensembles restent applicables aux uplets de la même manière
qu'au reste des éléments, les uplets doivent être intégrés parmi les éléments. À savoir,
la théorie des ensembles doit développer ses notions d'uplets en les définissant comme
des classes d'éléments déjà existants, au lieu de simplement les accepter par les
constructions ci-dessus, qui les laissaient comme des types séparés.
Pour cela, les uplets étant des méta-fonctions, ils sont naturellement représentés par des fonctions.
Cela suppose de copier leur méta-domaine, qui est une liste de symboles, en un ensemble
(d'éléments). À savoir, représentons le domaine des n-uplets considérés par
l'ensemble Vn des n nombres de 0 à n−1 tous désignés par des symboles
de constantes que nous concevrons simplement comme des chiffres. Pour justifier cela comme
un développement de la théorie des ensembles, ces chiffres peuvent être définis par des termes
clos de valeurs distinctes, tels que ∅, {∅}, {∅, {∅}} et autant qu'on voudra d'autres
ensembles et fonctions exprimables à partir de là. La notion de n-uplet est alors définie
comme la classe de toutes les fonctions de domaine Vn.
Puis les projections sont définies par l'évaluateur de fonction appliqué aux chiffres respectifs,
ce qui peut être lu comme déguisé dans leurs notations: pour tous n-uplets x,
∀i∈Vn, πi(x) =
x(i).
Cette notation indicielle, jouant sur l'équivalence entre lire l'indice i comme un
argument ou un méta-argument visant à prendre le i-ème
symbole d'une liste (ici πi est la i-ème projection donnant
valeur de la i-ième variable), est également couramment utilisée pour les uplets:
xi peut être lu comme la i-ème variable dans l'uplet x =
(x0,…,xn−1), ou comme une troisième
notation pour le même évaluateur après x(i) et πi(x).
D'autres d'outils doivent être introduits avant de définir en théorie des ensembles
les définisseurs d'uplet (2.4) et les définisseurs d'opération utilisant les uplets (2.6).
Other languages:
EN : 2.3. Tuples