3.4. Grammaire des types
Les sections qui suivent écrivent ce que le corps décrit sans le poser : la grammaire des types et des termes, puis le jeu des règles de typage. Elles sont la fondation des preuves — la préservation du typage par la traduction, la non-interférence graduée, la divulgation délimitée, les règles de la loi distributive et celles de la gradation indexée sont des inductions ou des relations logiques, et se définissent par récurrence sur une grammaire ou sur un jeu de règles. Les deux grammaires sont écrites, la somme et la conjonction additive sous leur forme indexée ; le jeu de règles est complet pour les constructeurs du noyau, à une exception déclarée — l'arène, dont l'élimination relève du modèle mémoire et non du système de types. La sémantique opérationnelle et ses théorèmes suivent au chapitre 4 (§4.7).
Les types se rangent en trois strates, conformément au chapitre 1 (§1.4) : les types de valeur, les types de calcul, et les modalités graduées qui les relient. La séparation des deux premières est celle qu'impose l'appel par poussée de valeur, et la grammaire ci-dessous la porte.
\begin{align*}
\text{(valeurs)}\quad V &::= b \mid @_n V \mid \mathbf{1} \mid V \otimes V \mid \textstyle\bigoplus_{i \in I} V_i \mid \mathsf{Vec}\;n\;V \mid \mathsf{Arena}\;V \mid \mathsf{Cap}\;\rho \mid !_{r} V \mid U_{\varepsilon}\,C \mid \exists \alpha. V \mid \mu\alpha. V\\
\text{(calculs)}\quad C &::= F_{\varepsilon}\,V \mid V \multimap C \mid \textstyle\mathop{\&}_{i \in I} C_i \mid \forall \alpha. C \mid \nu\alpha. C\\
\text{(sessions)}\quad S &::= \mathbf{End} \mid V \otimes S \mid V \multimap S \mid \oplus\{\ell_i : S_i\} \mid \&\{\ell_i : S_i\} \mid {\bigcirc} S \mid {\Box} S \mid {\Diamond} S\\
\text{(grades)}\quad r &::= \langle u, m, \ell, \beta \rangle \in \mathcal{R} = \mathbb{N}_\infty \times \{\mathrm{d} \preceq \mathrm{m}\} \times \mathcal{L} \times \mathcal{B}\\
\text{(effets)}\quad \varepsilon &::= \langle \varphi, \kappa \rangle \in \mathcal{E} = \mathcal{E}_0 \times (\mathbb{N}_\infty \times \mathbb{N}_\infty)^{\mathcal{L}}
\end{align*}
Grammaire des types : trois strates, le grade comme quadruplet, l'effet comme produit d'une quantale et d'une famille temporelle indexée par les niveaux
Cette grammaire est complète au sens précis où elle est croisée avec le jeu de règles, et le compte n'est plus une opinion : cinquante règles de typage, dont quatre ne gouvernent aucun constructeur de terme ; quarante-six constructeurs de termes, dont neuf valeurs et trente-sept calculs. Le croisement est vérifié mécaniquement à chaque construction du document, et il fait échouer celle-ci dès qu'un constructeur apparaît dans une règle sans figurer à la grammaire, ou l'inverse. Les quatre règles sans constructeur ne sont pas une anomalie : ce sont les deux règles de sous-typage, qui s'appliquent à tout terme sans en former, et les deux règles structurelles de formation de contexte. Une grammaire qui ne serait pas croisée avec ses règles ne serait pas incomplète — elle serait invérifiable, ce qui est pire, puisque rien ne signalerait l'écart.
Trois points appellent un commentaire, car ils fixent des choix que le corps a pris sans les écrire
sous cette forme. Le premier est que !_r est une modalité et non quatre : son indice est un
quadruplet, dont les composantes sont l'usage, la marque de monotonie, le niveau de confidentialité
et le budget, et le §2.4 établit que cette structure
produit est licite. Le deuxième est que les types de session portent les trois modalités temporelles
du §4.5, ce qui est la manière dont le débit s'exprime. Le troisième
est que \mathsf{Trellis}_{\text{fin}}, condition de l'opérateur de point fixe, se lit sur cette
grammaire. Le dire en prose ne suffit pas à une induction, qui a besoin d'un prédicat ; on le pose
donc par les quatre clauses qui l'engendrent, et par rien d'autre.
\begin{gather*}
\frac{\;b \text{ de porteur fini, égalité décidable}\;}{\;\mathsf{Trellis}_{\text{fin}}(b)\;}
\qquad
\frac{\;}{\;\mathsf{Trellis}_{\text{fin}}(\mathbf{1})\;}
\\[8pt]
\frac{\;\mathsf{Trellis}_{\text{fin}}(V_1) \quad \mathsf{Trellis}_{\text{fin}}(V_2)\;}{\;\mathsf{Trellis}_{\text{fin}}(V_1 \otimes V_2)\;}
\qquad
\frac{\;\mathsf{Trellis}_{\text{fin}}(V) \quad n < \omega\;}{\;\mathsf{Trellis}_{\text{fin}}(\mathsf{Vec}\;n\;V)\;}
\\[8pt]
\frac{\;\mathsf{Trellis}_{\text{fin}}(V_i)\;(\forall i \in I) \quad I \text{ fini}\;}{\;\mathsf{Trellis}_{\text{fin}}(\textstyle\bigoplus_{i \in I} V_i)\;}
\end{gather*}
Le prédicat de treillis fini, défini par induction sur la grammaire des types de valeur
Aucune autre clause. En particulier !_r, U_{\varepsilon}\,C, l'existentiel et le point fixe \mu n'y
entrent pas, et ce n'est pas un oubli : un porteur qui les admettrait cesserait d'être fini, et
l'itération de l'opérateur de point fixe cesserait de terminer.
Le quatrième porte sur le facteur temporel de l'effet, et il rectifie ce que ce texte écrivait.
Le chapitre 1 (§1.4) pose que le niveau étiquette l'effet, et
sur ses deux composantes ; il signale en outre que la cellule appariant le niveau et le temps est
celle qui rend le canal temporel énonçable. Un facteur temporel réduit à un \mathbb{N}_\infty nu
ne peut pas porter cela : il compte des pas sans dire à quel niveau ils ont été faits. C'est donc
une famille \kappa \in \mathbb{N}_\infty^{\mathcal{L}}, un \mathbf{tick} étant compté au
niveau du calcul qui le produit. L'ordre reste celui du produit, point par point ; le séquencement
additionne les familles composante par composante ; l'unité est la famille nulle ; et l'itération
\varphi_n multiplie chaque composante par n.
Cette forme n'alourdit que là où les niveaux varient, ce que la suite démontre.
Si tous les \mathbf{tick} d'un calcul sont produits à un même niveau \ell, la famille
\kappa est concentrée en \ell, et la restriction de \mathcal{E} aux tels effets est
isomorphe, comme quantale ordonnée, à \mathcal{E}_0 \times \mathbb{N}_\infty.
L'application \kappa \mapsto \kappa(\ell) est une bijection entre les familles concentrées en
\ell et \mathbb{N}_\infty, d'inverse k \mapsto k\,\delta_\ell. Elle préserve l'addition et
l'ordre, qui sont définis point par point, ainsi que la multiplication scalaire de \varphi_n.
Elle est donc un isomorphisme de quantales ordonnées sur ce sous-ensemble, lequel est clos par
produit et par borne supérieure puisque la concentration en \ell l'est.
La lecture qu'il faut en faire est celle que le chapitre 1 a déjà pratiquée sur les contextes. Une
zone non restreinte n'était pas une seconde zone mais la partie de grade \omega de la première ;
un compteur de pas nu n'est pas une seconde notion mais la famille concentrée en un niveau. Là où le
langage n'emploie qu'un niveau — la couche 1 dans son usage ordinaire, tout programme qui ne mêle
pas les confidentialités —, la généralisation est invisible.