Semántica algebraica (informática)

En informática , la semántica algebraica es una forma de semántica axiomática basada en leyes algebraicas para describir y razonar sobre especificaciones de programas de manera formal . ^{[1] [2] [3] [4]}

Sintaxis

La sintaxis de una especificación algebraica se formula en dos pasos: (1) definir una firma formal de tipos de datos y símbolos de operación, y (2) interpretar la firma a través de conjuntos y funciones.

Definición de firma

La signatura de una especificación algebraica define su sintaxis formal. La palabra "signatura" se utiliza como el concepto de " armadura de clave " en notación musical .

Una firma consta de un conjunto de tipos de datos , conocidos como tipos , junto con una familia de conjuntos, cada uno de los cuales contiene símbolos de operación (o simplemente símbolos) que relacionan los tipos. Usamos para denotar el conjunto de símbolos de operación que relacionan los tipos con el tipo . ${\displaystyle S}$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ ${\displaystyle s_{1},~s_{2},~...,~s_{n}\in S}$ ${\displaystyle s\in S}$

Por ejemplo, para la firma de pilas de enteros , definimos dos tipos, a saber, y , y la siguiente familia de símbolos de operación: ${\displaystyle int}$ ${\displaystyle stack}$

${\displaystyle {\begin{aligned}\Sigma _{\Lambda ,~stack}&=\{{\rm {new}}\}\\\Sigma _{int~stack,~stack}&=\{{\rm {push}}\}\\\Sigma _{stack,~stack}&=\{{\rm {pop}}\}\\\Sigma _{stack,~int}&=\{{\rm {depth}},{\rm {top}}\}\\\end{aligned}}}$

donde denota la cadena vacía . ${\displaystyle \Lambda }$

Interpretación de la firma desde la teoría de conjuntos

Un álgebra interpreta los símbolos de ordenamiento y operación como conjuntos y funciones . Cada ordenamiento se interpreta como un conjunto , que se denomina portador de ordenamiento , y cada símbolo de se asigna a una función , que se denomina operación de . ${\displaystyle A}$ ${\displaystyle s}$ ${\displaystyle A_{s}}$ ${\displaystyle A}$ ${\displaystyle s}$ ${\displaystyle \sigma }$ ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ ${\displaystyle \sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}}$ ${\displaystyle A}$

Con respecto a la firma de las pilas de números enteros, interpretamos la clasificación como el conjunto de números enteros y la clasificación como el conjunto de pilas de números enteros. Además, interpretamos la familia de símbolos de operaciones como las siguientes funciones: ${\displaystyle int}$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle stack}$ ${\displaystyle Stack}$

${\displaystyle {\begin{aligned}{\rm {new}}&:~\to Stack\\{\rm {push}}&:~\mathbb {Z} \times Stack\to Stack\\{\rm {pop}}&:~Stack\to Stack\\{\rm {depth}}&:~Stack\to \mathbb {Z} \\{\rm {top}}&:~Stack\to \mathbb {Z} \\\end{aligned}}}$

Semántica

La semántica se refiere al significado o comportamiento . Una especificación algebraica proporciona tanto el significado como el comportamiento del objeto en cuestión.

Axiomas ecuacionales

La semántica de una especificación algebraica se define mediante axiomas en forma de ecuaciones condicionales . ^[1]

Con respecto a la firma de las pilas de enteros, tenemos los siguientes axiomas:

Para cualquier y , ${\displaystyle z\in \mathbb {Z} }$ ${\displaystyle s\in Stack}$

${\displaystyle {\begin{aligned}&A1:~~{\rm {pop}}({\rm {push}}(z,s))=s\\&A2:~~{\rm {depth}}({\rm {push}}(z,s))={\rm {depth}}(s)+1\\&A3:~~{\rm {top}}({\rm {push}}(z,s))=z\\&A4:~~{\rm {pop}}({\rm {new}})={\rm {new}}\\&A5:~~{\rm {depth}}({\rm {new}})=0\\&A6:~~{\rm {top}}(s)=-404~{\rm {if~depth}}(s)=0\\\end{aligned}}}$

donde " " indica "no encontrado". ${\displaystyle -404}$

Semántica matemática

La semántica matemática (también conocida como semántica denotacional ) ^[5] de una especificación se refiere a su significado matemático.

La semántica matemática de una especificación algebraica es la clase de todas las álgebras que satisfacen la especificación. En particular, el enfoque clásico de Goguen et al. ^{[1] [2]} toma el álgebra inicial ( única salvo isomorfismo ) como el modelo "más representativo" de la especificación algebraica.

Semántica operacional

La semántica operacional ^[6] de una especificación significa cómo interpretarla como una secuencia de pasos computacionales.

Definimos un término fundamental como una expresión algebraica sin variables . La semántica operacional de una especificación algebraica se refiere a cómo se pueden transformar los términos fundamentales utilizando los axiomas ecuacionales dados como reglas de reescritura de izquierda a derecha , hasta que dichos términos alcancen sus formas normales , donde ya no es posible reescribirlos.

Consideremos los axiomas para pilas de números enteros. Sea " " el que denota "reescribe a". ${\displaystyle \Rrightarrow }$

${\displaystyle {\begin{aligned}&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {pop}}({\rm {new}})))))))&\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))))&({\rm {by~Axiom~}}A4)\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&{\rm {top}}({\rm {push}}(3,~{\rm {new}}))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&3&({\rm {by~Axiom~}}A3)\\\end{aligned}}}$

Propiedad canónica

Se dice que una especificación algebraica es confluente (también conocida como Church-Rosser ) si la reescritura de cualquier término básico conduce a la misma forma normal. Se dice que es terminal si la reescritura de cualquier término básico conducirá a una forma normal después de un número finito de pasos. Se dice que la especificación algebraica es canónica (también conocida como convergente ) si es confluente y terminal. En otras palabras, es canónica si la reescritura de cualquier término básico conduce a una forma normal única después de un número finito de pasos.

Dada cualquier especificación algebraica canónica, la semántica matemática concuerda con la semántica operacional. ^[7]

Como resultado, las especificaciones algebraicas canónicas se han aplicado ampliamente para abordar problemas de corrección de programas. Por ejemplo, numerosos investigadores han aplicado dichas especificaciones a la prueba de equivalencia observacional de objetos en programación orientada a objetos . Véase Chen y Tse ^[8] como una fuente secundaria que proporciona una revisión histórica de investigaciones destacadas desde 1981 hasta 2013.

Véase también

• Semántica algebraica (lógica matemática)
• OBJ (lenguaje de programación)
• José Goguen

Referencias

1. JA Goguen; JW Thatcher; EG Wagner; JB Wright (1977). "Semántica del álgebra inicial y álgebras continuas". Revista de la ACM . 24 (1): 68–95. doi : 10.1145/321992.321997 . S2CID  11060837.
2. JA Goguen ; JW Thatcher; EG Wagner (1978). "Un enfoque algebraico inicial para la especificación, corrección e implementación de tipos de datos abstractos". En RT Yeh (ed.). Tendencias actuales en metodología de programación, vol. IV: Estructuración de datos . Prentice Hall . págs. 80–149.
3. JA Goguen ; C. Kirchner; H. Kirchner; A. Megrelis; J. Meseguer (1988). "Una introducción a OBJ3". Actas del Primer Taller sobre Sistemas de Reescritura de Términos Condicionales . Apuntes de clase en Ciencias de la Computación. Vol. 308. Springer . págs. 258–263. doi :10.1007/3-540-19242-5_22. ISBN 978-3-540-19242-8.
4. JA Goguen ; G. Malcolm (1996). Semántica algebraica de programas imperativos. MIT Press . ISBN  9780262071727.
5. David A. Schmidt (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . William C. Brown Publishers. ISBN 9780205104505.
6. Gordon D. Plotkin (1981). "Un enfoque estructural de la semántica operacional" (Informe técnico DAIMI FN-19). Departamento de Ciencias Informáticas, Universidad de Aarhus .
7. S. Lucas; J. Meseguer (2014). "Terminación operacional fuerte y débil de teorías de reescritura ordenadas por orden". En S. Escobar (ed.). Reescritura de la lógica y sus aplicaciones. Apuntes de clase en informática. Vol. 8663. Cham: Springer . págs. 178–194. doi :10.1007/978-3-319-12904-4_10. ISBN . 978-3-319-12903-7.
8. HY Chen; TH Tse (2013). "Igualdad entre iguales y desiguales: una revisión de los criterios de equivalencia y no equivalencia en las pruebas a nivel de clase de software orientado a objetos". IEEE Transactions on Software Engineering . 39 (11): 1549–1563. doi :10.1109/TSE.2013.33. hdl : 10722/187124 . S2CID  8694513.