Codificación semántica

Este artículo no cita ninguna fuente . Por favor, ayude a mejorar este artículo añadiendo citas de fuentes fiables . El material sin fuentes puede ser cuestionado y eliminado . Buscar fuentes:  «Codificación semántica» – noticias  · periódicos  · libros  · académico  · JSTOR ( marzo de 2017 ) ( Aprenda cómo y cuándo eliminar este mensaje )

Una codificación semántica es una traducción entre lenguajes formales . Para los programadores, la forma más familiar de codificación es la compilación de un lenguaje de programación en código de máquina o código de bytes. La conversión entre formatos de documentos también son formas de codificación. La compilación de documentos TeX o LaTeX en PostScript también son procesos de codificación comunes. Algunos preprocesadores de alto nivel, como Camlp4 de OCaml , también implican la codificación de un lenguaje de programación en otro.

Formalmente, una codificación de un lenguaje A en un lenguaje B es una conversión de todos los términos de A en B. Si hay una codificación satisfactoria de A en B, B se considera al menos tan poderoso (o al menos tan expresivo ) como A.

Una noción informal de traducción no es suficiente para ayudar a determinar la expresividad de los idiomas, ya que permite codificaciones triviales como la asignación de todos los elementos de A al mismo elemento de B. Por lo tanto, es necesario determinar la definición de una codificación "suficientemente buena". Esta noción varía según la aplicación.

Comúnmente, se espera que una codificación preserve una serie de propiedades.${\displaystyle [\cdot ]:A\longrightarrow B}$

solvencia

Para cada operador n-ario de A, existe un operador n-ario de B tal 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}])}$

lo completo

Para cada operador n-ario de A, existe un operador n-ario de B tal 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})]}$

(Nota: hasta donde el autor tiene conocimiento, este criterio de completitud nunca se utiliza).

La conservación de las composiciones es útil en la medida en que garantiza que los componentes puedan examinarse por separado o en conjunto sin "romper" ninguna propiedad interesante. En particular, en el caso de las compilaciones, esta solidez garantiza la posibilidad de proceder a la compilación por separado de los componentes, mientras que la integridad garantiza la posibilidad de descompilarlos.

Esto supone 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 para un paso de reducción y para cualquier número de pasos de reducción.${\displaystyle \longrightarrow }$${\displaystyle \longrightarrow ^{*}}$

solvencia

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

lo completo

Para cada término del lenguaje A y cada término del lenguaje B, si entonces existe alguno tal que .${\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}]}$

Esta conservació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 no se añada ningún comportamiento mediante la codificación. En particular, en el caso de la compilación de un lenguaje de programación, la solidez y la completitud juntas significan que el programa compilado se comporta de acuerdo con la semántica de alto nivel del lenguaje de programación.

Esto también supone la existencia de una noción de reducción tanto en la lengua A como en la lengua B.

solvencia

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

lo completo

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

En el caso de la compilación de un lenguaje de programación, la solidez garantiza que la compilación no introduzca no terminaciones como bucles o recursiones sin fin. La propiedad de completitud es ú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 supone 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, por oposició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 una página.

solvencia

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

lo completo

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

Esto supone la existencia de la noción 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 otras. Las simulaciones se utilizan normalmente para describir optimizaciones en tiempo de compilación.

solvencia

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

lo completo

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

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

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

solvencia

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

lo completo

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

Esto supone 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 distribución de procesos y datos entre varias computadoras o CPU.

solvencia

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

lo completo

Si un término es la composición de dos agentes entonces debe ser la composición de dos agentes tales que y .${\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}}$

• Bisimulación
• Compilador
• Semántica
• Codificación de diccionario semántico (SDE)

• El wiki de transformación del programa