Encodage sémantique
Un encodage sémantique est une traduction entre deux langages formels.
Dans le domaine de l'informatique, les encodages les plus courants sont la compilation d'un langage de programmation en langage machine ou en langage intermédiaire et la conversion d'un document depuis un format de données vers un autre. La compilation d'un langage de mise en forme tel que TeX, LaTeX ou TEI vers PostScript ou PDF est aussi une forme d'encodage. De même, certains préprocesseurs de haut-niveau tels qu'Apple WorldScript ou Camlp4 pour Objective Caml, procèdent à des encodages entre divers langages de programmation.
Définition
modifierFormellement, un encodage d'un langage formel A dans un langage formel B est une fonction qui, à chaque terme de A, associe un terme de B.
![{\displaystyle [\cdot ]:A\longrightarrow B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/19aca89d1b15088ab5ddecd85ec90ab13edac688)
S'il existe un encodage 'satisfaisant' de A vers B, on considère que le langage B est 'au moins aussi puissant' (ou 'expressif') que le langage A.
Propriétés des encodages
modifierLa notion informelle de « traduction » entre deux langages, ou même l'existence d'une fonction de A vers B, est insuffisante pour comparer l'expressivité de deux langages. En effet, pour peu que le langage B ne soit pas vide, il est toujours possible de trouver une fonction qui à tous les termes de A associe le même terme de B. Il est donc nécessaire de définir dans quelles circonstances un encodage est suffisant.
Cette notion dépend de l'application. Nous présentons ici quelques propriétés classiques considérées comme importantes.
Préservation des compositions
modifier- Pour tout opérateur d'arité n dans A, il existe un opérateur d'arité n dans B tel que
- Interprétation
- Si l'encodage dispose de cette propriété, il est possible de travailler sur des composants séparés, que ce soit pour les compiler ou pour les étudier. Cette propriété est généralement considérée comme indispensable.
- Pour tout opérateur d'arité n dans A, il existe un opérateur d'arité n dans B tel que
- Interprétation
- Cette propriété garantit la possibilité de désencoder les termes encodés.
![{\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}])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dde845e5d034bd6a375773b70e51b3c59c212dbe)
![{\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})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/74cef38c88f773bd4701bb12fe05cd449137b073)
