Codificación semántica

solvencia

Para cada operador n-ario${\displaystyle op_{A}}$de A, existe un operador n-ario${\displaystyle op_{B}}$de B tal que

${\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}])}$

lo completo

Para cada operador n-ario${\displaystyle op_{A}}$de A, existe un operador n-ario${\displaystyle op_{B}}$de B tal que

${\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})]}$

(Nota: hasta donde el autor sabe, este criterio de exhaustividad nunca se utiliza).

La preservación de las composiciones resulta útil en la medida en que garantiza que los componentes puedan examinarse por separado o en conjunto sin alterar ninguna propiedad de interés. En particular, en el caso de las compilaciones, esta integridad garantiza la posibilidad de proceder con la compilación individual de los componentes, mientras que la completitud garantiza la posibilidad de la descompilación.

Esto presupone la existencia de una noción de reducción tanto en el lenguaje A como en el lenguaje B. Normalmente, en el caso de un lenguaje de programación, la reducción es la relación que modela la ejecución de un programa.

Escribimos${\displaystyle \longrightarrow }$para un paso de reducción y${\displaystyle \longrightarrow ^{*}}$para cualquier número de pasos de reducción.

solvencia

Para cada término${\displaystyle T_{A}^{1},T_{A}^{2}}$del idioma A, si${\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}$entonces${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}$.

lo completo

Para cada término${\displaystyle T_{A}^{1}}$del idioma A y todos los términos${\displaystyle T_{B}^{2}}$del idioma B, si${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}$entonces existe algo${\displaystyle T_{A}^{2}}$de tal manera que${\displaystyle T_{B}^{2}=[T_{A}^{2}]}$.

Esta preservación garantiza que ambos lenguajes se comporten de la misma manera. La solidez garantiza que se conserven todos los comportamientos posibles, mientras que la completitud garantiza que la codificación no añada ningún comportamiento. En particular, en el caso de la compilación de un lenguaje de programación, la solidez y la completitud implican que el programa compilado se comporta de acuerdo con la semántica de alto nivel del lenguaje de programación.

Esto también presupone la existencia de una noción de reducción tanto en el lenguaje A como en el lenguaje B.

solvencia

para cualquier término${\displaystyle T_{A}}$, si todas las reducciones de${\displaystyle T_{A}}$convergen, entonces todas las reducciones de${\displaystyle [T_{A}]}$converger.

lo completo

para cualquier término${\displaystyle [T_{A}]}$, si todas las reducciones de${\displaystyle [T_{A}]}$convergen, entonces todas las reducciones de${\displaystyle T_{A}}$converger.

En el caso de la compilación de un lenguaje de programación, la solidez garantiza que la compilación no introduzca errores de terminación, como bucles infinitos o recursiones infinitas. La propiedad de completitud resulta útil cuando se utiliza el lenguaje B para estudiar o probar un programa escrito en el lenguaje A, posiblemente extrayendo partes clave del código: si este estudio o prueba demuestra que el programa termina en B, entonces también termina en A.

Esto presupone la existencia de una noción de observación tanto en el lenguaje A como en el lenguaje B. En los lenguajes de programación, los observables típicos son resultados de entradas y salidas, en contraposición a la computación pura. En un lenguaje de descripción como HTML , un observable típico es el resultado de la representación de la página.

solvencia

para cada observable${\displaystyle obs_{A}}$en términos de A, existe un observable${\displaystyle obs_{B}}$de términos de B tales que para cualquier término${\displaystyle T_{A}}$con observable${\displaystyle obs_{A}}$,${\displaystyle [T_{A}]}$tiene observable${\displaystyle obs_{B}}$.

lo completo

para cada observable${\displaystyle obs_{A}}$en términos de A, existe un observable${\displaystyle obs_{B}}$en términos de B tales que para cualquier término${\displaystyle [T_{A}]}$con observable${\displaystyle obs_{B}}$,${\displaystyle T_{A}}$tiene observable${\displaystyle obs_{A}}$.

Esto presupone la existencia del concepto de simulación tanto en el lenguaje A como en el lenguaje B. En un lenguaje de programación, un programa simula a otro si puede realizar las mismas tareas (observables) y posiblemente algunas más. Las simulaciones se utilizan normalmente para describir optimizaciones en tiempo de compilación.

solvencia

para cada término${\displaystyle T_{A}^{1},T_{A}^{2}}$, si${\displaystyle T_{A}^{2}}$simula${\displaystyle T_{A}^{1}}$entonces${\displaystyle [T_{A}^{2}]}$simula${\displaystyle [T_{A}^{1}]}$.

lo completo

para cada término${\displaystyle T_{A}^{1},T_{A}^{2}}$, si${\displaystyle [T_{A}^{2}]}$simula${\displaystyle [T_{A}^{1}]}$entonces${\displaystyle T_{A}^{2}}$simula${\displaystyle T_{A}^{1}}$.

La preservación de simulaciones es una propiedad mucho más fuerte que la preservación de observaciones, que implica. A su vez, es más débil que la propiedad de preservación de bisimulaciones . Como en casos anteriores, la solidez es importante para la compilación, mientras que la completitud es útil para probar o demostrar propiedades.

Esto presupone la existencia de una noción de equivalencia tanto en el lenguaje A como en el lenguaje B. Normalmente, esta noción puede ser la de igualdad de datos estructurados o la de programas sintácticamente diferentes pero semánticamente idénticos, como la congruencia estructural o la equivalencia estructural.

solvencia

si dos términos${\displaystyle T_{A}^{1}}$y${\displaystyle T_{A}^{2}}$son equivalentes en A, entonces${\displaystyle [T_{A}^{1}]}$y${\displaystyle [T_{A}^{2}]}$son equivalentes en B.

lo completo

si dos términos${\displaystyle [T_{A}^{1}]}$y${\displaystyle [T_{A}^{2}]}$son equivalentes en B, entonces${\displaystyle T_{A}^{1}}$y${\displaystyle T_{A}^{2}}$son equivalentes en A.

Esto presupone la existencia de una noción de distribución tanto en el lenguaje A como en el lenguaje B. Normalmente, para la compilación de programas distribuidos escritos en Acute , JoCaml o E, esto significa la distribución de procesos y datos entre varios ordenadores o CPU.

solvencia

si un término${\displaystyle T_{A}}$es la composición de dos agentes${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$entonces${\displaystyle [T_{A}]}$debe ser la composición de dos agentes${\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}$.

lo completo

si un término${\displaystyle [T_{A}]}$es la composición de dos agentes${\displaystyle T_{B}^{1}~|~T_{B}^{2}}$entonces${\displaystyle T_{B}}$debe ser la composición de dos agentes${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$de tal manera que${\displaystyle [T_{A}^{1}]=T_{B}^{1}}$y${\displaystyle [T_{A}^{2}]=T_{B}^{2}}$.