4.6. Calcul de processus sous-jacent🔗

Les trois échelles qui précèdent ont été décrites l'une après l'autre, chacune avec sa structure propre. Reste à dire ce qu'elles sont ensemble, et le chapitre 1 (§1.4) l'a annoncé sous la forme d'une équation : la couche 2 relève d'un \pi-calcul enrichi de motifs de jonction. Cette section fait de cette équation une construction. Ce qu'elle apporte est une lecture, dans laquelle acteurs, sessions, jonctions et effets cessent d'être quatre mécanismes voisins pour devenir les constructeurs d'un même calcul — et le §3.6.4.5 en écrit depuis peu les règles, de sorte que cette lecture a désormais un appareil sous elle plutôt qu'au-dessus d'elle. RMQ 53. La lecture précédait les règles, ce qui est l'ordre de la découverte et non celui de la justification. Les règles étant écrites, les deux coïncident.

Ce métalangage n'est pas une invention de ce document, et le dire évite un malentendu que l'équation du chapitre 1 pourrait entretenir. Écrire « \pi-calcul augmenté de motifs de jonction » suggère une extension, dont il faudrait justifier ce qu'elle ajoute ; il s'agit en réalité d'une présentation alternative du même pouvoir expressif. Le calcul obtenu en ajoutant la réflexion à la machine chimique abstraite [60] est prouvé équivalent au \pi-calcul, à congruence barbelée faible près, et sa métathéorie est établie [61]. Ce document emprunte donc un calcul, il n'en propose pas un.

Une seconde parenté rend vérifiable ce qui serait resté une ressemblance. Il existe une extension des psi-calculi par motifs abstraits et filtrage, munie de sortes sur le langage des termes de données, qui représente directement plusieurs calculs de processus existants [62]. Le métalangage de ce document en est plausiblement une instance, et les conditions qui le décideraient sont énumérables plutôt qu'appréciables : une fonction de sorte équivariante sur les noms, les termes et les motifs~; quatre prédicats de compatibilité, un par rôle — émettre, recevoir, être substitué par, être lié par restriction de nom~; et un préordre de sous-sorte. La question de savoir si les sortes de ce document satisfont ces conditions n'est donc pas ouverte au sens où l'on ne saurait par où commencer : elle est ouverte au sens où le calcul reste à faire.

Ce qu'il en emprunte comprend la théorie équationnelle dont il a besoin. Raisonner sur une traduction suppose de savoir quand deux processus sont le même, et cette relation est disponible. Une équivalence observationnelle y est définie puis établie pleinement abstraite vis-à-vis de la congruence barbelée faible, les techniques employées étant celles de la bisimulation faible [61]. C'est elle qui donnera son sens à l'énoncé de fidélité du chapitre 6.

Le métalangage a pour types les propositions de la logique linéaire intuitionniste — celles-là mêmes que le chapitre 3 emploie comme types de session — et pour termes les processus suivants :

où J ::= x_1(y_1) \,\&\, \cdots \,\&\, x_n(y_n) est un motif de jonction, consommant n messages d'un seul tenant. Les quatre premières formes sont l'émission et la réception, la sélection et l'offre de branchement ; la cinquième est la coupure, seule forme de composition, qui lie deux processus sur un canal privé de type S ; la septième est le service répliqué ; la huitième le point fixe introduit au §2.4.

Chacune traduit un mécanisme déjà construit, et l'intérêt de la lecture est que cette correspondance est exhaustive : il n'y a rien dans la couche 2 qui n'y figure, et rien qui y figure sans emploi.

Deux réglages restent à fixer sur cette grammaire, et tous deux retirent du non-déterminisme plutôt qu'ils n'en ajoutent. Le premier porte sur les motifs de jonction. Les règles de réaction d'une définition de jonction décrivent des comportements en concurrence, et leur déclenchement admet en général un choix non déterministe — source que le chapitre 1 ne compte pas parmi les siennes. Deux politiques existent : celle du premier motif rendrait l'ordre d'écriture des clauses sémantiquement significatif, de sorte que la mise en page déciderait quel couple de messages est consommé. La partition en ensembles disjoints rend le choix forcé, et donc inexistant [63]. K7PL retient la seconde, et le coût en est nul : le compilateur vérifie déjà statiquement l'exhaustivité des motifs, de sorte que la disjonction est une vérification du même ordre, faite au même endroit.

Le second porte sur le point fixe. La grammaire ci-dessus en donne un opérateur arbitraire, et c'est la seule exception à la règle que ce document applique partout ailleurs — la couche 3 interdit la récursion générale et exprime toute itération comme un pli sur le plus petit point fixe. Aucune raison n'est donnée à cette exception, et il n'y en a pas de bonne : ajouter à un lambda-calcul linéaire concurrent les types récursifs et les catamorphismes, en suivant la sémantique des algèbres initiales, y fait naître les types de session récursifs au lieu de les postuler [64]. Le point fixe du métalangage devrait donc être un catamorphisme, comme celui de la couche 3, et l'exception disparaître.

• Un acteur est un point fixe gardé par une réception. La coalgèbre terminale du §2.3 — un état S, une transition S \to (\text{Msg} \Rightarrow S \times \text{Out}) — s'écrit \mathbf{fix}\,X\langle s\rangle.\, a(m).\, \llbracket H \rrbracket(s,m), où le gestionnaire produit l'état suivant qu'il repasse à X. Le point fixe est la finalité de la coalgèbre, lue sur les termes plutôt que sur les objets.

• Un canal de session est un canal du calcul, et son type est le protocole. La dualité, dérivée au chapitre 3 du retournement des arguments de \multimap, est ici celle des deux extrémités d'une coupure : le processus qui offre S et celui qui l'emploie sont les deux prémisses d'une même règle.

• Un motif de jonction est la construction J \triangleright P, et son atomicité est celle de la règle. Les n messages sont consommés en une seule transition, ce que le théorème 42 énonce et ce que le §4.2 rapproche d'une transition de réseau de Petri.

• Le séquencement des effets est le préfixage : \overline{x}\langle v\rangle.P ordonne l'émission avant P, et cet ordre ne commute pas. C'est ce que la quantale d'effets du chapitre 3 dénote par son produit non commutatif ; le préfixe du calcul en est la forme syntaxique.

• Une capacité de couche 1 est un canal linéaire, et une capacité de lecture un service répliqué — la distinction entre l'usage unique et l'usage libre y devient celle entre x(y).P et !x(y).P, c'est-à-dire le grade. Le service répliqué se déplie toutefois à sens unique, et ce n'est pas un arrangement de présentation. La loi de réplication — l'équivalence entre l'exponentielle et sa décomposition en une copie et l'exponentielle — n'est pas dérivable en logique linéaire, seul un sens l'est [65]. La conséquence relevée par cette littérature est qu'un encodage qui supposerait l'équivalence ne capture pas fidèlement l'exécution du calcul de processus telle qu'elle est traditionnellement définie. La correction ne coûte rien ici : on garde la moitié qui se dérive, sous forme d'un dépliage à sens unique, et l'énoncé de fidélité du chapitre 6 s'énonce sur cette moitié.

• La composition d'un système est un emboîtement de coupures. C'est ce qui explique l'acyclicité du §4.5 sans qu'elle ait à être postulée : un terme est un arbre de coupures, et un arbre n'a pas de cycle.

Un second principe d'architecture y trouve son fondement, et ce document le posait jusqu'ici sans appui. La localité — un acteur n'accède qu'à son propre état, aucune mémoire n'est partagée entre machines, et le modèle mémoire du §4.5 a pour portée une machine — n'est pas une discipline que K7PL s'imposerait par prudence. C'est l'une des deux modifications qui définissent le calcul dans lequel il se traduit : on l'obtient de la machine chimique générique en imposant la localité et en ajoutant la réflexion, et c'est cela qui rend le modèle consistant avec la distribution [61]. Ce que le chapitre 4 décrit comme un choix d'architecture est donc une propriété du calcul sous-jacent, et l'ordre des raisons s'en trouve inversé. La localité n'est pas imposée à un modèle qui pourrait s'en passer, elle est ce qui rend ce modèle distribuable.

Cette dernière remarque suggère l'énoncé que cette section doit à la lecture qu'elle propose.

Une seconde voie existe pour les cas de la couche 3, plus directe, et elle rejoint un choix déjà fait. Le fragment séquentiel déterministe du calcul cible est essentiellement le \lambda-calcul en style à passage de continuations, de sorte que toute transformée CPS y plonge le \lambda-calcul [61] — et K7PL a retenu l'appel par poussée de valeur, cadre où cette transformée se lit sans détour. L'inclusion qu'affirme l'équation du chapitre 1 cesse ainsi d'être une affirmation pour devenir un plongement nommé.

L'esquisse ne conduit pas l'induction cas par cas, et deux points y résisteraient. RMQ 54. L'obstacle est de conduire la traduction, non de trouver une cible. Celle-ci existe et porte ce qu'il faut. Les types dépendants pragmatiques du §3.2 demandent des quantificateurs du second ordre que le métalangage doit posséder — fragment disponible avec sa propre théorie de l'équivalence comportementale [66]. Et le point fixe du §2.4 suppose que le semi-treillis d'arrivée soit lui-même interprété. Une machine abstraite pour sessions linéaires correspondant à la logique linéaire classique, étendue de quantificateurs du second ordre et de types inductifs, fournit l'un et l'autre, avec une stratégie d'évaluation séquentielle déterministe dérivée de la focalisation et une adéquation établie dans les deux sens [67]. C'est elle que ce document désigne comme interprétation du métalangage, sans conduire ici la vérification.

S'il tient, correction et adéquation se raisonnent une fois au niveau du métalangage et non construction par construction de K7PL — c'est l'économie que ce chapitre revendique. S'il tombe, chaque construction du langage redemande son propre argument de correction, et la dette de fidélité du chapitre 6 redevient aussi large qu'elle en avait l'air.

Les trois conséquences qui précèdent supposent une induction que ce document doit maintenant conduire, au moins dans son plan. Elle porte sur la dérivation, et se range en quatre groupes selon ce que chaque règle engage.

Le premier groupe est celui des règles structurelles, et il ne demande rien. L'affaiblissement envoie sur l'affaiblissement du séquent, la contraction sur la duplication d'un service répliqué — laquelle est licite exactement quand le grade vaut \omega, ce qui est l'hypothèse de la règle source. L'échange n'a pas d'image, les contextes du métalangage étant des ensembles.

Le deuxième est celui des connecteurs, et il suit la traduction usuelle des propositions comme sessions. L'abstraction devient une réception, l'application une coupure sur canal frais, le couple une émission suivie de la continuation, la projection une sélection, le branchement une offre. Chaque règle envoie sur une règle, et la préservation du typage y est immédiate puisque les types sont les mêmes objets de part et d'autre.

Le troisième est celui des règles propres à K7PL, et c'est là que l'induction fait un travail. Un acteur envoie sur un point fixe gardé par une réception, sa coalgèbre terminale devenant la finalité de ce point fixe. Un motif de jonction envoie sur la construction homonyme, dont l'atomicité est celle de la règle. Le séquencement d'effets envoie sur le préfixage, et c'est ici que la marque de non-commutativité du produit de la quantale trouve son image~: préfixer n'est pas commutatif non plus. Un effet devient une émission sur le canal distingué de sa sorte, et l'opération \mathbf{tick} une émission sur celui du temps. Une capacité linéaire devient un canal linéaire, une capacité de lecture un service répliqué — le choix étant dicté par le grade, ce qui est licite puisque le grade \omega est l'image du fragment cartésien.

Le quatrième groupe est celui des cas résistants, au nombre de quatre, et ils se nomment. Les types dépendants pragmatiques demandent un fragment du second ordre, disponible avec sa théorie de l'équivalence [66]~; la traduction y envoie un indice sur une variable de type quantifiée, et la préservation demande que la quantification du métalangage soit assez riche pour porter les contraintes que le solveur décharge — ce que ce document n'établit pas. L'opérateur de point fixe déductif demande que le semi-treillis d'arrivée soit lui-même interprété, faute de quoi son image n'a pas de type~; la machine à sessions linéaires possède les types inductifs nécessaires [67], mais l'interprétation du treillis y reste à donner. Et les canaux distingués demandent que la traduction ne produise que des termes bien sortés, une sorte étant réservée aux effets et interdite au programme traduit~; c'est une propriété de la traduction elle-même, vérifiable par une induction parallèle sur la même dérivation, et non une hypothèse supplémentaire. Le quatrième ne résiste pas aujourd'hui mais résisterait demain, et c'est le seul dont ce document sache qu'il ne pourra pas le lever. Si la discipline d'échange restreint envisagée au chapitre 3 (§3.1) était adoptée, une zone de contexte porterait un ordre~; or la composition parallèle du métalangage est commutative, et un ordre ne survit pas à une image commutative. La traduction resterait correcte — l'extrusion de portée qu'elle emploie repose sur une propriété de grade que l'ordre ne touche pas —. Mais elle cesserait de transporter l'ordre, de sorte qu'une propriété établie sur la zone ordonnée ne se lirait plus sur l'image. C'est une perte et non un échec, et la nommer maintenant coûte moins que de la découvrir en adoptant la discipline : elle est l'un des prix de cette adoption, et il n'était pas compté.

Reste à dire ce qu'on fait du métalangage une fois la traduction établie, car c'est là que l'économie se réalise. On ne l'interprète qu'une fois. Une machine abstraite pour les sessions linéaires, dont la stratégie d'évaluation est séquentielle et déterministe et dont l'adéquation est prouvée dans les deux sens, en fournit l'interprétation [67]~; l'équivalence observationnelle du calcul, pleinement abstraite vis-à-vis de la congruence barbelée faible, en fournit la théorie des programmes [61]. Correction et adéquation se raisonnent donc à ce niveau, une fois pour toutes, et non construction par construction de K7PL. C'est ce que signifiait, au chapitre 6 (§6.3), l'affirmation que la dette de fidélité est plus étroite qu'elle n'y paraissait~: elle se réduit à la préservation du typage par \llbracket \cdot \rrbracket, dont le plan qui précède donne l'induction sans la mener à son terme.

Trois conséquences se lisent sur cette traduction, et c'est en cela qu'elle vaut mieux qu'une reformulation.

La première concerne l'effacement. Le chapitre 2 (§2.4) signale que l'architecture de K7PL est un système de raffinement de types, soit un foncteur des dérivations vers les termes sous-jacents, sans exhiber ce foncteur. C'est \llbracket \cdot \rrbracket : une dérivation de K7PL porte \mathcal{G} et \mathcal{E} ; son image ne les porte pas. L'effacement de la Phase 8 n'est donc pas une opération de compilation qu'il faudrait justifier séparément — c'est l'action de ce foncteur sur les objets, et la non-interférence du chapitre 1 est l'énoncé que le métalangage ne voit pas la dérivation.

La deuxième concerne l'échelle du système. Le §4.5 pose que l'orchestrateur est une coalgèbre sans exhiber le foncteur qui l'engendre. Sous la traduction, un système est un terme — composition parallèle d'acteurs sous restriction des canaux privés —, et le foncteur cherché est celui dont la coalgèbre finale interprète ce terme. Le produit des foncteurs de comportement individuels, restreint aux transitions que la topologie de coupures autorise. Ce n'est pas une nouvelle construction, c'est la lecture de la composition parallèle comme opération sur les coalgèbres.

Une restriction doit toutefois y être ajoutée à la main, et c'est la seule des trois conséquences qui en demande une. Cet argument remonte de la cible vers la source, quand les deux autres en descendent. Or la topologie de coupures ne porte pas les disciplines que la cible ne connaît pas — l'ordre d'une zone d'échange (chapitre 3, §3.1) en est une. Le foncteur ainsi obtenu admet donc des transitions que la source interdit : c'est une sur-approximation, dont la coalgèbre de l'orchestrateur est une sous-coalgèbre. Cela suffit à établir que le foncteur existe et quelle forme il a ; cela ne suffirait pas à en tirer une propriété de sûreté, une sur-approximation ne démontrant jamais une sûreté.

La troisième concerne la fidélité de l'interpréteur de référence (chapitre 6, §6.3). L'interpréteur est fidèle si ses transitions sont celles du métalangage. Comme celui-ci est interprété une fois pour toutes, correction et adéquation se raisonnent à son niveau et non sur chaque construction de K7PL. Cette remarque se laisse porter jusqu'à un énoncé, qui dit ce qu'un interpréteur de référence garantit et ce qu'il ne garantit pas.

La dette qu'il reste à acquitter n'est donc plus « prouver l'interpréteur correct » mais « établir que \llbracket \cdot \rrbracket préserve le typage », ce que le théorème 45 énonce, dont l'induction est planifiée et non conduite.

Une réserve doit fermer cette section, car la lecture a un coût que sa commodité pourrait masquer. La composante \mathcal{E} n'a pas d'image dans le métalangage : ce qui s'y raisonne est la structure de communication et de contrôle, non les effets — ni, par conséquent, le temps, que le chapitre 1 (§1.4) y a logé sous la forme d'une opération \mathbf{tick}. Un interpréteur prouvé fidèle au métalangage ne serait donc prouvé fidèle qu'à cette part-là, et les garanties de la Phase 3 comme celles de la Phase 7 resteraient à établir ailleurs. Il faut se garder d'en tirer que les effets échapperaient à tout traitement structurel : ils sont gradués comme le contexte l'est, et la correction conjointe des deux gradations est un résultat établi sur ce régime d'évaluation [68]. Ce qui échappe au métalangage échappe au métalangage, non au système de types.

Cette réserve n'a pas à être définitive, et ce document choisit de ne pas s'y tenir. Un effet peut se traduire dans un calcul de processus, et par un procédé classique : une opération à effet devient une communication sur un canal distingué, réservé à cet effet et non accessible au programme traduit. Émettre sur le canal du temps est ce que \mathbf{tick} devient ; un gestionnaire d'effet devient un processus qui offre une session sur ce canal. Le métalangage porte alors \mathcal{E} comme il porte déjà \Delta, la traduction devient totale sur les trois composantes, et la fidélité d'un interpréteur cesse d'être partielle.

Deux conséquences accompagnent ce choix, et la seconde est un coût. La première est que la non-interférence temporelle devient énonçable dans le métalangage : dire qu'une durée ne dépend pas d'un secret revient à dire que les communications sur le canal du temps sont indiscernables, ce qui est une propriété du calcul et non une propriété à établir en dehors de lui. La seconde est que le métalangage grossit — il faut une discipline pour les canaux distingués, qui garantisse qu'aucun programme traduit n'y accède directement. Cette discipline n'a pas à être inventée : le calcul cible emploie déjà un système de sortes sur les canaux, dont le traitement des motifs de jonction est le premier usage, et où l'on ne considère que les processus bien sortés [61]. Il suffit d'y réserver une sorte aux canaux d'effet et d'exiger qu'aucun terme issu de la traduction ne la mentionne. La charge se ramène donc à un cas de l'induction plutôt qu'elle ne s'y ajoute : établir que la traduction produit des termes bien sortés. Le chapitre 6 (§6.3) mesure ce que ce choix change pour la dette de fidélité.