Encodage sémantique - Semantics encoding

Un encodage sémantique est une traduction entre des langages formels . Pour les programmeurs, la forme d'encodage la plus connue est la compilation d'un langage de programmation en code machine ou en byte-code. La conversion entre les formats de document est également une forme de codage. La compilation de documents TeX ou LaTeX vers PostScript sont également des processus d'encodage couramment rencontrés. Certains préprocesseur de haut niveau tels que OCaml de Camlp4 impliquent également encodage d'un langage de programmation dans un autre.

Formellement, un codage d'une langue A dans la langue B est une mise en correspondance de tous les termes de A dans B.S'il y a un codage satisfaisant de A dans B, B est considéré au moins aussi puissant (ou au moins aussi expressif ) que A.

Propriétés

Une notion informelle de traduction n'est pas suffisante pour aider à déterminer l'expressivité des langues, car elle permet des encodages triviaux tels que le mappage de tous les éléments de A sur le même élément de B. Par conséquent, il est nécessaire de déterminer la définition d'un encodage "assez bon" . Cette notion varie selon l'application.

Généralement, un codage est censé conserver un certain nombre de propriétés. ${\ displaystyle [\ cdot]: A \ longrightarrow B}$

Conservation des compositions

solidité: Pour tout opérateur n-aire de A, il existe un opérateur n-aire de B tel que ${\ displaystyle op_ {A}}$ ${\ displaystyle op_ {B}}$; ${\ displaystyle \ forall T_ {A} ^ {1}, T_ {A} ^ {2}, \ dots, T_ {A} ^ {n}, [op_ {A} (T_ {A} ^ {1}, T_ {A} ^ {2}, \ cdots, T_ {A} ^ {n})] = op_ {B} ([T_ {A} ^ {1}], [T_ {A} ^ {2}], \ cdots, [T_ {A} ^ {n}])}$
exhaustivité: Pour tout opérateur n-aire de A, il existe un opérateur n-aire de B tel que ${\ displaystyle op_ {A}}$ ${\ displaystyle op_ {B}}$; ${\ displaystyle \ forall T_ {B} ^ {1}, T_ {B} ^ {2}, \ dots, T_ {B} ^ {n}, \ exists T_ {A} ^ {1}, \ dots, T_ {A} ^ {n}, op_ {B} (T_ {B} ^ {1}, \ cdots, T_ {B} ^ {N}) = [op_ {A} (T_ {A} ^ {1}, T_ {A} ^ {2}, \ cdots, T_ {A} ^ {n})]}$

(Remarque: à la connaissance de l'auteur, ce critère d'exhaustivité n'est jamais utilisé.)

La conservation des compositions est utile dans la mesure où elle garantit que les composants peuvent être examinés séparément ou ensemble sans "casser" aucune propriété intéressante. En particulier, dans le cas des compilations, cette solidité garantit la possibilité de procéder à une compilation séparée des composants, tandis que l'exhaustivité garantit la possibilité de décompilation.

Préservation des réductions

Ceci suppose l'existence d'une notion de réduction à la fois sur le langage A et sur le langage B. Typiquement, dans le cas d'un langage de programmation, la réduction est la relation qui modélise l'exécution d'un programme.

Nous écrivons pour une étape de réduction et pour un nombre quelconque d'étapes de réduction. ${\ displaystyle \ longrightarrow}$ ${\ displaystyle \ longrightarrow ^ {*}}$

solidité: Pour tous les termes de la langue A, si alors . ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1} \ longrightarrow ^ {*} T_ {A} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} [T_ {A} ^ {2}]}$
exhaustivité: Pour chaque terme de la langue A et tous les termes de la langue B, s'il en existe alors . ${\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {B} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} T_ {B} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {B} ^ {2} = [T_ {A} ^ {2}]}$

Cette préservation garantit que les deux langues se comportent de la même manière. La solidité garantit que tous les comportements possibles sont préservés tandis que l'exhaustivité garantit qu'aucun comportement n'est ajouté par l'encodage. En particulier, dans le cas de la compilation d'un langage de programmation, la solidité et l'exhaustivité signifient ensemble que le programme compilé se comporte en fonction de la sémantique de haut niveau du langage de programmation.

Préservation de la résiliation

Cela suppose également l'existence d'une notion de réduction tant sur la langue A que sur la langue B.

solidité: pour n'importe quel terme , si toutes les réductions de convergent, alors toutes les réductions de convergent. ${\ displaystyle T_ {A}}$ ${\ displaystyle T_ {A}}$ ${\ displaystyle [T_ {A}]}$
exhaustivité: pour n'importe quel terme , si toutes les réductions de convergent, alors toutes les réductions de convergent. ${\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ ${\ displaystyle T_ {A}}$

Dans le cas de la compilation d'un langage de programmation, la solidité garantit que la compilation n'introduit pas de non-terminaison comme des boucles sans fin ou des récursions sans fin. La propriété d'exhaustivité est utile lorsque le langage B est utilisé pour étudier ou tester un programme écrit en langage A, éventuellement en extrayant des parties clés du code: si cette étude ou ce test prouve que le programme se termine en B, alors il se termine également en A.

Conservation des observations

Cela suppose l'existence d'une notion d'observation à la fois sur le langage A et sur le langage B. Dans les langages de programmation, les observables typiques sont des résultats d'entrées et de sorties, par opposition au calcul pur. Dans un langage de description tel que HTML , un observable typique est le résultat du rendu de page.

solidité: pour chaque observable en termes de A, il existe un observable de termes de B tel que pour tout terme avec observable , a observable . ${\ displaystyle obs_ {A}}$ ${\ displaystyle obs_ {B}}$ ${\ displaystyle T_ {A}}$ ${\ displaystyle obs_ {A}}$ ${\ displaystyle [T_ {A}]}$ ${\ displaystyle obs_ {B}}$
exhaustivité: pour tout observable en termes de A, il existe un observable en termes de B tel que pour tout terme avec observable , a observable . ${\ displaystyle obs_ {A}}$ ${\ displaystyle obs_ {B}}$ ${\ displaystyle [T_ {A}]}$ ${\ displaystyle obs_ {B}}$ ${\ displaystyle T_ {A}}$ ${\ displaystyle obs_ {A}}$

Préservation des simulations

Ceci suppose l'existence d'une notion de simulation à la fois sur le langage A et sur le langage B. Dans un langage de programmation, un programme en simule un autre s'il peut effectuer toutes les mêmes tâches (observables) et éventuellement quelques autres. Les simulations sont généralement utilisées pour décrire les optimisations au moment de la compilation.

solidité: pour tous les termes , si simule puis simule . ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$
exhaustivité: pour tous les termes , si simule puis simule . ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1}}$

La préservation des simulations est une propriété beaucoup plus forte que la préservation des observations, qu'elle implique. À son tour, il est plus faible qu'une propriété de conservation des bisimulations . Comme dans les cas précédents, la solidité est importante pour la compilation, tandis que l'exhaustivité est utile pour tester ou prouver les propriétés.

Préservation des équivalences

Cela suppose l'existence d'une notion d'équivalence à la fois sur le langage A et sur le langage B.En règle générale, cela peut être une notion d'égalité de données structurées ou une notion de programmes syntaxiquement différents mais sémantiquement identiques, tels que la congruence structurelle ou l'équivalence structurelle.

solidité: si deux termes et sont équivalents en A, alors et sont équivalents en B. ${\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$
exhaustivité: si deux termes et sont équivalents en B, alors et sont équivalents en A. ${\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {2}}$

Préservation de la distribution

Ceci suppose l'existence d'une notion de distribution à la fois sur le langage A et sur le langage B. Typiquement, pour la compilation de programmes distribués écrits en Acute , JoCaml ou E, cela signifie la distribution des processus et des données entre plusieurs ordinateurs ou CPU.

solidité: si un terme est la composition de deux agents, alors doit être la composition de deux agents . ${\ displaystyle T_ {A}}$ ${\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A} ^ {1}] ~ | ~ [T_ {A} ^ {2}]}$
exhaustivité: si un terme est la composition de deux agents, alors doit être la composition de deux agents tels que et . ${\ displaystyle [T_ {A}]}$ ${\ displaystyle T_ {B} ^ {1} ~ | ~ T_ {B} ^ {2}}$ ${\ displaystyle T_ {B}}$ ${\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {1}] = T_ {B} ^ {1}}$ ${\ displaystyle [T_ {A} ^ {2}] = T_ {B} ^ {2}}$