2.6. Six schémas de métathéorie🔗

Six énoncés reviennent dans ce document sous des habillages différents, et chacun est démontré ici une fois pour toutes. Ce ne sont pas des théorèmes sur K7PL mais sur la forme de ses démonstrations : les chapitres qui suivent les instancient plutôt qu'ils ne les refont. RMQ 30. Écrire le schéma avant ses instances évite d'écrire trois fois la même récurrence, et rend visible ce qu'elles partagent.

Le premier gouverne toute transformation qui traverse une substitution. L'expansion d'une macro, le désucrage d'une forme de surface, la traduction vers le métalangage et l'abaissement vers la représentation intermédiaire ont ceci de commun qu'ils sont définis par récurrence sur la structure des termes et qu'ils doivent commuter avec la substitution — faute de quoi le sens dépendrait de l'ordre dans lequel on transforme et on substitue.

Le deuxième gouverne les traductions d'un système de règles vers un autre. Il dit ce qu'il faut établir, et rien de plus : non pas que la traduction préserve le jugement, mais que chaque règle de la source a une dérivation pour image.

Le troisième est un fait de théorie des graphes, employé deux fois par ce document et qu'il serait vain de démontrer deux fois.

Un quatrième schéma gouverne tout ce qui, dans ce document, retire. Cinq constructions l'instancient sans qu'aucune ne le nomme, et leur parenté n'est aujourd'hui qu'une ressemblance de forme.

Cinq constructions en sont des instances, et les reconnaître comme telles dispense de vérifier cinq fois la même chose. La projection conservatrice retire les opérations d'une sorte et garde le temps ; la projection observationnelle retire ce qui excède un niveau, temps compris ; l'effacement indexé retire ce qui est gradué au-dessus d'un niveau ; la restriction d'un espace de noms retire les arêtes hors d'une dimension ; et la purge de spécification de la dernière phase de compilation retire les blocs qui n'ont servi qu'à vérifier. RMQ 31. Cinq retraits, une condition. Ce qui change d'une instance à l'autre est le critère, jamais l'argument.

Ce que le schéma apporte n'est pas l'économie de cinq preuves, c'est la condition qu'elles partagent et qu'aucune n'énonçait : une restriction n'est un morphisme que si son critère est stable. Les deux projections du chapitre suivant diffèrent précisément par leur critère, et c'est pourquoi les confondre ouvrirait le canal que l'une d'elles prétend fermer — ce n'est pas une coïncidence malheureuse mais une conséquence du schéma.

Un cinquième schéma gouverne tout ce qui, dans ce document, répète. Cinq mécanismes font la même chose sous cinq noms, et aucun ne renvoie aux autres.

Cinq constructions en sont des instances. La traduction d'un grade fini ré-invoque n fois la traduction du contexte. Le parcours d'un vecteur compose n effets et met le contexte à l'échelle. L'opération à portée applique \varphi_n à l'effet de son bloc. L'expansion d'une macro applique \varphi_{r_i} à chaque argument. Et l'image du point fixe déductif borne son dépliage de la même façon. RMQ 32. Cinq noms pour une opération. Le schéma ne les rend pas interchangeables : il dit ce qu'ils partagent, et leurs différences deviennent lisibles.

Ce que le schéma apporte est que la restriction du théorème 2 se propage d'un coup aux cinq. Un grade infini traversant un effet à coût non nul est interdit partout où la ré-invocation apparaît, et il n'y a pas cinq conditions de bord à écrire mais une, portée par le schéma.

Un sixième schéma est le plus général des six, et il absorbe une part des précédents. Tout ce qui, dans ce document, traduit une représentation riche vers une représentation plus pauvre — l'élaboration de la syntaxe de surface, l'effacement de la dernière phase, l'abaissement vers la représentation intermédiaire, la traduction vers le métalangage — obéit au même énoncé.

Quatre constructions en sont des instances, et la quatrième est celle qui coûtait le plus cher : la fidélité de l'interpréteur de référence. Elle cesse d'être une propriété à établir construction par construction pour devenir la vérification de trois conditions sur une transformation. RMQ 33. Ce qui demandait une induction par construction demande désormais trois conditions par transformation. C'est le même travail divisé par le nombre de constructions.

Ce schéma dit en outre ce qu'il ne faut pas confondre, et c'est son second usage. Préserver le typage, simuler l'exécution et être correct vis-à-vis de la machine sont trois énoncés distincts~; le schéma établit le premier, et les deux autres demeurent. Les glissements entre eux sont la classe d'erreur que ce document a le plus de mal à éviter, parce que les trois s'énoncent avec les mêmes mots.

Un septième énoncé mérite le même traitement, et il porte sur les capacités plutôt que sur les termes. Le chapitre 4 l'emploie deux fois — pour la mémoire partagée et pour la frontière étrangère — et l'argument y est le même à un mot près.