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 firma de una especificación algebraica define su sintaxis formal. La palabra "firma" se utiliza como el concepto de " firma clave " en notación musical .

Una firma consta de un conjunto de tipos de datos , conocidos como géneros , junto con una familia de conjuntos, cada uno de los cuales contiene símbolos de operación (o simplemente símbolos) que relacionan los géneros. Usamos para denotar el conjunto de símbolos de operación que relacionan los géneros con el género . ${\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 teórica de conjuntos de la firma.

Un álgebra interpreta los símbolos de géneros y operaciones como conjuntos y funciones . Cada tipo se interpreta como un conjunto , que se denomina portador de tipo , y cada símbolo 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 pilas de enteros, interpretamos la clasificación como el conjunto de números enteros e interpretamos la clasificación como el conjunto de pilas de enteros. Además interpretamos la familia de símbolos de operación 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 está definida por axiomas en forma de ecuaciones condicionales . ^[1]

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

Para cualquiera 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 hasta el isomorfismo ) como el modelo "más representativo" de la especificación algebraica.

Semántica operativa

La semántica operativa ^[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 operativa 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 reescribir.

Considere los axiomas de las pilas de números enteros. Sea " " el que indique "reescritura en". ${\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 fundamental conduce a la misma forma normal. Se dice que termina si la reescritura de cualquier término fundamental conduce 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 a la vez confluente y terminante. En otras palabras, es canónico si la reescritura de cualquier término fundamental 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 cuestiones de corrección de programas. Por ejemplo, numerosos investigadores han aplicado tales especificaciones para probar la equivalencia observacional de objetos en la programación orientada a objetos . Véase Chen y Tse ^[8] como fuente secundaria que proporciona una revisión histórica de investigaciones destacadas realizadas entre 1981 y 2013.

Ver también

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

Referencias

1. JA Goguen; JW Thatcher; EG Wagner; JB Wright (1977). "Semántica de á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 de álgebra 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 conferencias sobre informática. vol. 308. Saltador . 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. Prensa del MIT . ISBN  9780262071727.
5. David A. Schmidt (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . Editores William C. Brown. ISBN 9780205104505.
6. Gordon D. Plotkin (1981). “Un enfoque estructural de la semántica operativa” (Informe Técnico DAIMI FN-19). Departamento de Informática, Universidad de Aarhus .
7. S. Lucas; J. Meseguer (2014). "Terminación operativa 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 conferencias sobre 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 con 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". Transacciones IEEE sobre ingeniería de software . 39 (11): 1549-1563. doi :10.1109/TSE.2013.33. hdl : 10722/187124 . S2CID  8694513.