Intégralité totale vs Abstraction complète d'une traduction de programme

Les efforts de vérification du compilateur se résument souvent à prouver que le compilateur est complètement abstrait: qu'il préserve et reflète les équivalences (contextuelles).

Au lieu de fournir des preuves d'abstraction complètes, certains travaux récents de vérification du compilateur (basés sur des catégories) par Hasegawa [ 1 , 2 ] et Egger et. Al. [ 3 ] prouvent l'intégralité des différentes traductions CPS.

Question: Quelle est la différence entre une complétude complète et une abstraction complète?

Pour moi, l'exhaustivité ressemble à une réflexion d'équivalence pour une traduction et la plénitude semble être une conséquence de la préservation de l'équivalence.

Remarque : Curien [ 7 ] et Abramsky [ 8 ] explorent tous deux la relation entre la définissabilité, l'abstraction complète et, dans une certaine mesure, l'intégralité complète. Je soupçonne que ces ressources peuvent avoir la réponse à ma question, mais après une lecture en surface, je n'ai pas encore confirmé cela.

Contexte : Le terme «complétude complète» a été inventé par Abramsky et Jagadeesan [ 4 ] pour caractériser l'exactitude d'un modèle sémantique de jeu de la logique linéaire multiplicative.

Blute [ 5 ] fournit la définition suivante:

Soit $\mathcal{F}$ une catégorie libre. Nous disons qu'un modèle catégorique $\mathcal{M}$ est entièrement complet pour $\mathcal{F}$ ou que nous avons l' intégralité de $\mathcal{F}$ par rapport à $\mathcal{M}$ si, en ce qui concerne une certaine interprétation des générateurs, l'unique foncteur libre $[\![ - ]\!] : \mathcal{F} \rightarrow \mathcal{M}$ est plein.

Pour autant que je sache, Hasegawa dans [ 6 ] est le premier à adapter l'intégralité complète pour décrire une traduction de programme au lieu d'un modèle sémantique catégorique. Dans ce cas, la traduction de Girard du calcul lambda simplement tapé au calcul lambda linéaire. Plus tard, dans [ 1 ], il définit la complétude complète de la traduction CPS $(\cdot)^\circ$ comme:

Γ ⊢ M : σ Γ ∘ ; ∅ ⊢ M ∘ = N : ( σ ∘ → o ) ⊸ $\Gamma^{\circ};\emptyset \vdash N : (\sigma^\circ \rightarrow o) \multimap o$$\Gamma \vdash M : \sigma$$\Gamma^{\circ};\emptyset \vdash M^\circ = N : (\sigma^\circ \rightarrow o) \multimap o$

(où est un type de base dans le calcul lambda linéaire (langue cible), mais pas dans le calcul lambda informatique (langue source).)$o$

Pour moi, la définition de Hasegawa semble être une plénitude et devrait vraiment être combinée avec la complétude pour obtenir la pleine complétude.

Egger et. Al. [ 3 ] définissent l'intégralité complète d'une traduction CPS comme une combinaison de (1) exhaustivité et (2) plénitude:$(\cdot)^v$

(1): Si et puisΘ v | - ⊢ M v = la ß r | N v : ! τ v Θ ⊢ M = λ c N : $\Theta \vdash M,N : \tau$$\Theta^v | - \vdash M^v =_{\beta\eta} N^v : !\tau^v$$\Theta \vdash M =_{\lambda_c} N : \tau$

(2): Si alors il existe un terme tel que Θ ⊢ M : τ Θ v | - ⊢ M v = ß r | t : ! τ $\Theta^v | - \vdash t : !\tau^v$$\Theta \vdash M : \tau$$\Theta^v | - \vdash M^v =_{\beta\eta} t : !\tau^v$

(où est la théorie équationnelle de calcul de Moggi)$=_{\lambda_c}$

---

[1] " Effets linéairement utilisés: transformations monadiques et CPS en calcul lambda linéaire ", Hasegawa 2002

[2] " Sémantique de la poursuite-transmission linéaire en appel par nom ", Hasegawa 2004

[3] " Traductions CPS à usage linéaire dans le calcul de l'effet enrichi ", Egger et. Al. 2012

[4] " Jeux et complétude complète pour la logique linéaire multiplicative ", Abramsky et Jagadeesan 1992

[5] " Théorie des catégories pour les logiciens linéaires ", Blute 2003

[6] " Girard Translation and Logical Predicates ", Hasegawa 2000

[7] " Définissabilité et abstraction totale ", Curien 2007

[8] " Axiomes pour la définissabilité et la complétude complète ", Abramsky 1999

Malheureusement, il se passe trop de choses ici. Il est donc facile de mélanger les choses. L'utilisation de «complet» dans «pleine complétude» et «pleine abstraction» fait référence à des idées complètement différentes de plénitude. Mais, il y a aussi un lien vague entre eux. Donc, cela va être une réponse compliquée.

Complétude complète : "Sound and complete" est une propriété que vous souhaitez avoir pour une logique traditionnelle par rapport à sa sémantique. La solidité signifie que tout ce que vous pouvez prouver dans la logique est vrai dans le modèle sémantique. L'exhaustivité signifie que tout ce qui est vrai dans le modèle sémantique est prouvable dans la logique. Nous disons qu'une logique est saine et complète pour un modèle sémantique particulier. Quand nous arrivons à une logique constructive, comme la théorie de type Martin-Lof ou la logique linéaire, nous nous soucions non seulement de savoir si les formules sont prouvables, mais aussi de leurs preuves. Une formule prouvable peut avoir de nombreuses preuves et une logique constructive veut les séparer. Ainsi, une sémantique pour une logique constructive implique de spécifier non seulement si une formule est vraie, mais aussi une notion sémantique abstraite de "preuve" ("preuve") pour sa vérité. Abramsky et ses collègues ont inventé le terme «pleine complétude» pour signifier que les preuves dans la logique peuvent exprimer toutes les preuves sémantiques dans le modèle. Donc, "complet" fait référence aux preuves ici. Une logique «complète» peut prouver tout ce dont elle a besoin. Une logique "entièrement complète" a toutes les preuves dont elle a besoin. Ainsi, "complétude complète" signifie "complétude constructive" ou "complétude de preuve". Cela n'a rien à voir avec une abstraction complète.

Abstraction complète : "Adéquate et entièrement abstraite" est une propriété que vous souhaitez pour le modèle sémantique d'un langage de programmation. (Notez la première différence: nous avons maintenant affaire aux propriétés du modèle sémantique, pas les propriétés du langage!) L'adéquation signifie que, chaque fois que deux termes ont la même signification dans le modèle sémantique, ils sont équivalents du point de vue observationnel dans le langage de programmation (par rapport à une certaine notion d'exécution). L'abstraction complète signifie que, si deux termes sont équivalents sur le plan de l'observation, ils ont la même signification dans le modèle sémantique. Ces idées peuvent être liées à la solidité et à l'exhaustivité, mais d'une manière quelque peu artificielle. Si nous considérons le modèle sémantique d'un langage de programmation comme une "logique" ou une "méthode de preuve" pour parler d'équivalence d'observation, alors l'adéquation signifie que cette méthode de preuve est solide; l'abstraction complète signifie que cette méthode de preuve est terminée. Il n'y a aucune notion de «pleine complétude»méthode de preuve. (Mais, une telle chose est théoriquement possible, et un de ces jours, quelqu'un pourrait le faire.)

Dans votre cas, vous vous intéressez aux traductions plutôt qu'aux modèles sémantiques. Les propriétés d'adéquation et d'abstraction complète peuvent être étendues pour traiter les traductions comme suit. Vous pensez que la langue cible est votre "modèle sémantique", c'est-à-dire un formalisme que vous comprenez parfaitement d'une manière ou d'une autre. Si oui, vous avez une notion d'équivalence pour cela. Ensuite, nous disons que la traduction est adéquate si, chaque fois que les traductions de deux programmes sources sont équivalentes dans la langue cible, elles sont équivalentes du point de vue observationnel dans la langue source. Nous disons qu'il est totalement abstrait si, chaque fois que deux programmes sources sont équivalents du point de vue observationnel dans la langue source, leurs traductions sont équivalentes dans la langue cible.

En réalité, je ne connais pas de langues cibles que nous comprenons vraiment parfaitement. Tout ce que nous savons, c'est une autre notion d'équivalence observationnelle pour la langue cible. Dans ce cas, la traduction est adéquate si l'équivalence observationnelle des traductions dans la langue cible implique l'équivalence observationnelle dans la langue source. La traduction est entièrement abstraite si l'équivalence observationnelle des termes dans la langue source implique l'équivalence observationnelle des traductions dans la langue cible. Certains auteurs considèrent que la «traduction entièrement abstraite» signifie la combinaison de ces deux propriétés:

$$\tau(M) \cong \tau(N) \Longrightarrow M \cong N$$ $$M \cong N \Longrightarrow \tau(M) \cong \tau(N)$$ $$M \cong N \iff \tau(M) \cong \tau(N)$$

Egger et al semblent étendre de manière similaire l'idée de complétude complète aux traductions. Dans leur configuration, les formules sont des types et les preuves sont des termes. Leur traduction traduit aussi bien les types que les termes. Ils appellent leur traduction complète entièrement si la traduction d'un type n'a que les termes qui sont obtenus en traduisant les conditions initiales de type . $A$$A$

$$\forall N : \tau(A).\; \exists M : A.\, \tau(M) = N$$

Maintenant, pour le lien vague entre la complétude complète et l'abstraction complète. Prouver qu'un modèle sémantique ou une traduction est complètement abstrait implique souvent une certaine définissabilité. En effet, nos langues sont généralement d'ordre supérieur. Donc, si le modèle sémantique ou la langue cible a trop de «contextes», alors il pourra piquer nos termes ou significations sémantiques de manière indésirable et gâcher leur équivalence. "Voies indésirables" signifie que le langage de programmation lui-même ne peut pas les pousser. Donc, pour obtenir une abstraction complète, nous devons nous assurer que les «contextes» disponibles dans le modèle sémantique ou la langue cible proviennent de ceux de la langue source sous une forme ou une autre. Notez que cela concerne la propriété d'exhaustivité complète.

Pourquoi voulons-nous de telles propriétés? Ça n'a rienà voir avec les compilateurs! Nous voulons ces propriétés afin de prétendre que la langue source s'intègre dans la langue cible. Si nous sommes satisfaits d'une langue cible particulière (comme étant claire, compréhensible, fondamentale ou donnée par Dieu), alors, si la langue source y est intégrée, nous pouvons affirmer qu'il n'y a rien de nouveau dans la langue source. Ce n'est qu'un fragment de la langue cible que nous connaissons et aimons. C'est juste du sucre syntaxique. Ainsi, des traductions entièrement abstraites sont fournies par des personnes pour établir que des langues cibles particulières sont excellentes. Ils sont aussi parfois donnés par des personnes qui ont une langue grosse ou compliquée à gérer. Ainsi, au lieu de définir directement une sémantique pour eux, ils la traduisent dans un langage de base puis donnent une sémantique au langage de base. Par exemple, le rapport Haskell fait cela. Mais l'abstraction complète de ces traductions est rarement prouvée car les langues source sont grandes et compliquées. Les gens croient que la traduction est bonne.

Encore une fois, cela n'a rien à voir avec les compilateurs. Les compilateurs sont rarement adéquats ou totalement abstraits. Et ils n'ont pas besoin de l'être! Tout ce qu'un compilateur doit faire est de conserver le comportement d'exécution de programmes complets. Le langage cible d'un compilateur est généralement énorme, ce qui signifie qu'il a beaucoup de contextes qui peuvent gâcher l'équivalence. Ainsi, les programmes équivalents dans la langue source ne sont presque jamais équivalents au contexte lorsqu'ils sont compilés.

Résumé: la complétude complète signifie que la fonction d'interprétation n'est pas seulement complète, mais aussi surjective sur les programmes. L'abstraction complète n'a pas besoin de surjectivité. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$

Détails: La signification détaillée de l'abstraction complète et de l'exhaustivité complète dépend de la nature de ce / où / comment vous interprétez. Voici un rendu pour l'interprétation d'un langage de programmation typé dans un autre. Vous avez une fonction d'interprétation mappe trois choses.$\semb{.}$

• Types de la langue source à types dans la langue cible.$A$$\semb{A}$

• Contextes dans la langue source aux contextes dans la langue cible.$\Gamma$$\semb{\Gamma}$

• Programmes dans le contexte vers les programmes dans le contexte .$\Gamma \vdash P : \alpha$$\semb{\Gamma} \vdash \semb{P} : \semb{\alpha}$

Dans une interprétation catégorique, les deux premières cartes s'effondrent en une seule. La fonction d'interprétation peut avoir diverses propriétés, par exemple elle peut être compositionnelle, ou conserver la terminaison ou ... L'abstraction complète est une de ces propriétés. Rappelons que l'abstraction complète de que$\semb{.}$

$$P \cong^S Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T \semb{Q}$$

pour tout . Ici est la notion choisie d'équivalence de programme typé pour la langue source tandis que joue ce rôle pour la langue cible. Plus précisément, parce que nous sommes dans un cadre tapé,≅ S ≅ $P, Q$$\cong^S$$\cong^T$

Γ , α , P ,

$$P \cong^S_{\Gamma, \alpha} Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T_{\semb{\Gamma}, \semb{\alpha}} \semb{Q}$$ pour tous les appropriés . L'abstraction complète implique que Est sain et raison pour laquelle nous parlons d'abstraction complète et pas seulement de solidité et d'exhaustivité est que nous voulons également que la langue cible soit `` en quelque sorte '' non triviale, par exemple, pas un modèle de terme. Mais formaliser cette non-trivialité est difficile, et nous faisons simplement allusion à la non-trivialité par terminologie.$\Gamma, \alpha, P, Q$$\semb{.}$

Maintenant, une abstraction complète n'implique pas que Est surjectif sur les types, les contextes ou les programmes en contexte.$\semb{.}$

L'exhaustivité complète signifie que la carte Est (complète et) surjective sur les programmes en contexte pour tous les contextes et types définissables, c'est-à-dire tout programme dans le la langue cible est la dénotation de certains dans la langue source, c'est-à-dire . Notez que cela ne nécessite pas que surjectif sur les types et les contextes, car cette propriété tient rarement dans les interprétations qui nous intéressent généralement.$\semb{.}$Γ ⊢ P : α Q $\semb{\Gamma} \vdash Q : \semb{\alpha}$$\Gamma \vdash P : \alpha$$Q = \semb{P}$$\semb{.}$