¿Qué constituye la semántica denotacional?

En un hilo diferente , Andrej Bauer definió la semántica denotacional como:

El significado de un programa es una función de los significados de sus partes.

Lo que me molesta de esta definición es que no parece distinguir lo que comúnmente se considera semántica denotacional de lo que comúnmente se considera semántica no denotacional, es decir, semántica operacional estructural .

Más precisamente, el ingrediente clave aquí es la modularidad o composicionalidad de la semántica, o dicho de otra manera, el hecho de que se definen de acuerdo con la estructura abstracta del programa.

Como la mayoría (¿todas?) La semántica formal hoy en día tiende a ser estructural, ¿es esta la definición requerida?

Entonces, mi pregunta es: ¿Qué es la semántica denotacional?

La distinción que hago personalmente entre semántica operacional y denotacional es algo así:

• la semántica denotativa es matemática y equitativa. Los detalles de la reducción importan menos que el resultado final, que es un valor intemporal en algún espacio matemático.
• la semántica operacional es algorítmica. Se desarrolla en pasos individuales en el tiempo. El proceso es parte del significado, y el resultado final es solo un paso distinguido en ese proceso.

La diferencia a veces puede ser bastante sutil, y puede ser difícil saber si es solo una diferencia de estilo o de sustancia.

Sin embargo, podemos ver cómo la definición compositiva de Andrej se deriva más naturalmente de la definición denotacional, y también podemos imaginar fácilmente una semántica no confluente y no compositiva que aún cumple con la definición operativa.

Si tuviera que adivinar lo que diría Dana Scott, probablemente diría que la semántica denotacional es compositiva (como lo que afirmé) y que el significado de un programa debe ser un objeto matemático genuino, no una entidad sintáctica o formalista. Por supuesto, tal punto de vista requiere que uno diferencie entre la manipulación formal de la sintaxis y las matemáticas "verdaderas". Esto es necesariamente una distinción no matemática.

Como una ocurrencia tardía, uno presumiblemente querría que el significado sea adecuado en el sentido de que dos programas observacionalmente diferentes no reciben el mismo significado. Por supuesto, la adecuación de este tipo depende de lo que uno admite como "observación".

Bajo este punto de vista, se podría argumentar que la semántica operacional estructural no es semántica denotacional porque iguala el significado de una entidad sintáctica con otra entidad sintáctica (un valor o una secuencia de reducción).

Estoy de acuerdo en que la identificación de A. Bauer de la semántica denotacional con la composicionalidad (en Libros sobre semántica del lenguaje de programación ) realmente no caracteriza bien lo que tradicionalmente se entiende por semántica denotacional, ya que la semántica claramente operativa y la lógica de programa (semántica axiomática) son composicionales .

Sugeriría que el término se entiende mejor desde el punto de vista sociohistórico, ya que se refiere libremente a una cierta tradición teórica (comenzó en serio cuando Scott produjo un modelo teórico en celosía del cálculo lambda sin tipo) con ciertas herramientas preferidas (teoría del orden, teoremas de punto fijo , topología, teoría de categorías) y lenguajes de destino preferidos (puramente funcionales y secuenciales). Me imagino que, aparte del interés intelectual puro, la semántica denotacional se inventó principalmente porque:

1. Solía ​​ser difícil razonar sobre la semántica operativa.

2. Solía ​​ser difícil dar semántica axiomántica a lenguajes no triviales.

Yo diría que ambos problemas se han mejorado en gran medida, (1) por ejemplo, mediante técnicas basadas en bisimilación provenientes de la teoría de procesos (que puede verse como una forma específica de semántica operativa) o, por ejemplo, el trabajo de Pitts en semántica operativa y programa equivalencia, y (2) por los desarrollos de, por ejemplo, la lógica de separación o las lógicas de Hoare derivadas como versiones tipadas de las lógicas Hennessy-Milner a través de incrustaciones de lenguaje de programación en tipeado cálculo.$\pi$

Entonces, en resumen, argumentaría que el término "semántica denotacional" se ha vuelto menos preciso y, por lo tanto, menos útil. Puede ser útil para la comunidad semántica converger hacia una mejor terminología.

Estoy contento con la respuesta de Adrej, pero me gustaría profundizar más.

Para empezar, la semántica denotacional quiere decir algo como "el significado de esta notación es eso". Un verdadero semántico quiere imaginar que los significados son lo que existe en nuestra mente y que las anotaciones son solo una forma de expresar esos significados. El requisito de que la semántica denotacional debe ser compositiva se deduce de esto. Si los significados son primarios y las notaciones secundarias, entonces no tenemos más remedio que definir los significados de notaciones más grandes como funciones de los significados de sus constituyentes.

Si aceptamos este punto de vista, entonces una buena semántica denotacional necesita capturar los significados que presumimos que tenemos en mente. Cualquier semántica compositiva no necesariamente encajaría en la factura. Si se me ocurre una definición semántica compositiva y nadie está de acuerdo en que diga algún significado que tengan en su cabeza, entonces es de poca utilidad. La semántica de juegos en la actualidad se encuentra en esta situación. Es una definición compositiva y técnicamente bastante fuerte, pero muy pocas personas están de acuerdo en que tiene algo que ver con los significados que tienen en mente.

Dicho esto, cualquier definición de composición tiene varias ventajas técnicas. Podemos usarlo para verificar equivalencias u otras propiedades por inducción en la sintaxis de los términos. Podemos usarlo para verificar la solidez de los sistemas de prueba, nuevamente por inducción en la sintaxis de los términos. Podemos verificar la exactitud de los compiladores o las técnicas de análisis de programas (que, por su naturaleza, se definen por inducción en la sintaxis). Una definición semántica completamente abstracta tiene aún más ventajas técnicas. Puede usarlo para mostrar que dos programas no son equivalentes, que no puede hacer con ninguna semántica compositiva arbitraria. Una definición semántica totalmente definible es aún mejor. Aquí los dominios semánticos tienen exactamente lo que puede expresar en el lenguaje de programación (con algunas condiciones). Por lo tanto, puede enumerar los valores en los dominios para ver qué valores hay, lo que sería difícil de hacer con anotaciones sintácticas. Por todos estos motivos, la semántica de los juegos tiene puntajes brillantes.

Sin embargo, las definiciones semánticas compositivas han estado perdiendo su ventaja a lo largo de los años. Robin Milner y Andy Pitts han desarrollado una serie de técnicas de " razonamiento operativo ", que funcionan exclusivamente en la sintaxis, pero utilizando la semántica operativa donde sea necesario para hablar sobre el comportamiento. Estas técnicas de razonamiento operacional son de baja tecnología. Sin lujosas matemáticas. No hay objetos infinitos. Podemos enseñarles a estudiantes universitarios y cualquiera puede usarlos. Entonces, muchas personas se preguntan por qué necesitamos la semántica denotacional. (Martin Berger probablemente esté en este campamento).

Personalmente, no tengo ningún problema con tener muchas herramientas en mi caja de herramientas. Las técnicas de denominación pueden obtener mejores puntajes para algunos problemas y las técnicas operativas para otros. Los investigadores que desarrollan la teoría podrían estar mejor sintonizados con un enfoque u otro. Con bastante frecuencia, podemos desarrollar las ideas en un enfoque y transferir esas ideas al otro enfoque. (Gran parte del trabajo de Andy Pitts es de este tipo. La parametricidad relacional se desarrolló en el entorno denotacional, pero es capaz de descubrir cómo volver a expresarlo como razonamiento operativo. Cuando lo miro, digo "wow, nunca habría pensó que eso sería posible ". La lógica de separación también va por este camino. Steve Brookes dio una prueba de solidez de 60 páginas para la lógica de separación concurrente utilizando semántica denotacional.

Los enfoques operativos también obtienen una puntuación brillante cuando los lenguajes de programación se vuelven muy elegantes, con todo tipo de tipos de orden superior. Es posible que no tengamos idea de cómo modelar matemáticamente tales cosas. O bien, los modelos matemáticos estándar pueden resultar inconsistentes bajo el estrés de la locura. (Por ejemplo, vea "El polimorfismo no es una teoría de conjuntos" de Reynolds). Los enfoques operativos que funcionan exclusivamente en la sintaxis pueden dejar de lado todos estos problemas matemáticos.

Otro enfoque que es intermedio entre los enfoques operacionales y denotacionales es la realizabilidad . En lugar de trabajar con términos sintácticos como en los enfoques operacionales, vamos en parte a la denotación utilizando otra forma de representantes matemáticos. Es posible que estos representantes no califiquen como "significados" denotacionales reales, pero al menos serían un poco más abstractos que los términos sintácticos. Por ejemplo, para el cálculo lambda polimórfico, primero podemos dar significados a los términos sin tipo (en algún modelo del cálculo lambda sin tipo) y luego usarlos como representantes ('realizadores') para hacer alguna forma de "razonamiento operacional" a un poco Nivel más abstracto.

Por lo tanto, que haya una sana competencia entre los enfoques denotacional, operativo y de realizabilidad. No hay daño.

Por otro lado, también podría haber una competencia "poco saludable" entre los diferentes enfoques. Las personas que trabajan con un enfoque podrían estar tan estrechamente vinculadas con él que podrían no ver el punto de los otros enfoques. Idealmente, todos deberíamos ser conscientes de las fortalezas y debilidades de los diferentes enfoques y desarrollar una actitud científica hacia ellos, incluso si no son nuestros favoritos individuales.

[Una respuesta más. Probablemente no sea genial acumular varias respuestas. Pero, oye, este es un problema profundo.]

Dije que estaba de acuerdo con la respuesta de Andrej, pero parece que no estoy completamente de acuerdo. Hay una diferencia.

Dije que una semántica denotacional tiene que decir "el significado de esta notación es eso". Lo que quise decir es que a las notaciones se les debe asignar significados, que son alguna forma de entidades conceptuales , no otras notaciones. En contraste, Andrej también exigió, parafraseando a Scott, que los significados deben ser objetos "matemáticos". No creo que el bit matemático sea necesario.

Por ejemplo, estaría perfectamente bien, desde mi punto de vista, que los significados de las anotaciones sean procesos físicos. Después de que todos los programas de computadora frenen en su automóvil, vuelen aviones, arrojen bombas y demás. Estos son procesos físicos, no elementos en algún espacio matemático. No puedes soltar una bomba, ver si mata a alguien y recuperarla si no lo hace. Los programas de computadora no pueden hacer eso. Pero las funciones matemáticas sí pueden. (Se llaman operaciones "snapback"). Por lo tanto, no está nada claro que las funciones matemáticas tengan buenos significados para los programas de computadora.

Por otro lado, realmente todavía no sabemos cómo hablar de procesos físicos de manera abstracta. Por lo tanto, podríamos utilizar alguna descripción matemática de los procesos para articular nuestras ideas. Pero estas descripciones matemáticas serían solo eso, "descripciones". No son significados. Los significados reales serían solo los procesos físicos que imaginamos conceptualmente.

En su discurso de aceptación del premio SIGPLAN (que debería estar en YouTube pronto), Hoare dijo que ACP usó un "enfoque algebraico", CSP usó un "enfoque denotacional" y CCS usó un "enfoque operativo" para describir los procesos. Ohad y yo estábamos sentados juntos en la sesión, nos miramos y dijimos "eso es realmente interesante". Entonces, hay mucho espacio conceptual aquí que se está explorando. Creo que gran parte del trabajo posterior de Scott, sobre sistemas de vecindario y sistemas de información, etc., fue de hecho un esfuerzo por explicar las funciones como "procesos" de alguna forma. La geometría de interacción de Girard y la semántica de los juegos posteriores también son esfuerzos para explicar las funciones como procesos. Diría que desarrollar una teoría sólida de los procesos podría ser la gran contribución que la informática podría hacer a las matemáticas del siglo XXI. No aceptaría la creencia de que las matemáticas tienen todas las respuestas y deberíamos intentar reducir los fenómenos computacionales a conceptos matemáticos para comprenderlos.

Lo que me sorprende es lo bien que funciona la ocultación de información en los cálculos con estado (programación imperativa y cálculos de procesos), mientras que es torpe y complicado en formalismos matemáticos / funcionales. Sí, tenemos parametricidad relacional, y nos permite sortear muy bien las limitaciones de los formalismos matemáticos. Pero no coincide con la simplicidad y elegancia de la programación imperativa. Entonces, no creo que los formalismos matemáticos sean la respuesta correcta, aunque admitiría que son la mejor respuesta que tenemos en este momento. Pero deberíamos seguir buscando. Existe una buena teoría de los procesos que superará sin dudas las matemáticas tradicionales.

[¡Con suerte, esta es mi última respuesta a esta pregunta!]

La pregunta original de Ohad era sobre cómo la semántica denotacional difiere de la semántica operacional estructural. Pensó que ambos eran compositivos. En realidad, eso no es cierto. La semántica operacional estructural se da como secuencias de pasos. Cada paso se expresa de manera compositiva (¡y es notable que Plotkin descubra que esto es posible!), Pero todo el comportamiento no se define compositivamente. Esto es lo que dice Plotkin en su introducción al artículo de SOS [énfasis agregado]:

En la semántica denotacional, se sigue un ideal de composicionalidad, donde el significado de una frase compuesta se da en función del significado de sus partes. En el caso de la semántica operativa, se considera el comportamiento de una frase de programa, que es solo la recopilación de las transiciones que puede realizar. Sin embargo, este comportamiento no es compositivo cuando se considera como una función de las frases del programa. Sin embargo, las reglas lo dan estructuralmente, es decir, primitivo recursivamente, en la sintaxis; ...

El hecho de que cada paso se exprese composicionalmente no significa que todo el comportamiento se exprese composicionalmente.

Hay un buen artículo de Carl Gunter llamado Formas de especificación semántica , donde se comparan y contrastan los diferentes métodos para especificar la semántica. Gran parte de este material también se reproduce en el primer capítulo de su texto "Semántica de lenguajes de programación". Esperemos que esto aclare la imagen.

Otra palabra sobre "semántica operativa". En los primeros días, el término "operacional" se usaba para referirse a cualquier definición semántica que se refería a pasos detallados de evaluación. Tanto los semánticos denotacionales como los defensores axiomáticos menospreciaron la semántica "operativa", considerándola de bajo nivel y orientada a la máquina. Creo que esto realmente se basó en su creencia de que eran posibles descripciones de mayor nivel. Estas creencias se hicieron añicos tan pronto como consideraron la concurrencia. Los procesos y la semántica denotativa de concurrencia de de Bakker y Zucker tiene estos pasajes interesantes:

Utilizaremos la metodología de la semántica denotacional . "Denotacional" debe contrastarse aquí con "operacional": la idea clave del primer enfoque es que las expresiones en un lenguaje de programación denotan valores en dominios matemáticos equipados con una estructura apropiada, mientras que en el segundo las operaciones prescritas por las construcciones del lenguaje son modelado por pasos realizados por alguna máquina abstracta adecuada ...

El modelo matemático contiene varias nociones que, aunque de estilo denotacional, son operativas en espíritu [énfasis agregado]. Estos incluyen la característica de "historia" de la noción de proceso en sí, y el uso de los llamados movimientos silenciosos en el tratamiento de la sincronización y la recursividad.

Aquí vemos a los autores que luchan con las dos nociones de "operacional", una la noción técnica - comportamiento expresado mediante manipulaciones sintácticas, y la otra, la noción conceptual - que es de bajo nivel y detallada. El crédito va en gran medida a Plotkin y Milner por la rehabilitación de la semántica "operativa", por lo que es lo más alto posible y demuestra que puede ser elegante y perspicaz.

A pesar de todo esto, la noción operativa de proceso sigue siendo bastante diferente de la noción denotacional de proceso, la última de las cuales fue desarrollada tanto por De Bakker como por Hoare y sus equipos. Y, creo que hay muchas cosas misteriosas y hermosas sobre el concepto de proceso de denotación que aún no se comprende.

Esta respuesta adicional es amplificar el punto de que los modelos semánticos denotacionales están diseñados para "explicar" los fenómenos computacionales. Daré una serie de ejemplos de la semántica de los lenguajes de programación imperativos (también llamados lenguajes "similares a Algol").

Primero estaba el modelo semántico formulado por Scott y Strachey. (Cf. Gordon: Descripción denotacional de los lenguajes de programación: mi favorito de todos los tiempos o el libro de Winskel.) Este modelo postula que existe un estado global , compuesto por el estado de todas las ubicaciones asignadas por un programa. Cada comando se interpreta como una especie de función desde estados globales a estados globales.

Reynolds dijo que no modelaba la disciplina de la pila de variables locales. Cuando se ingresa un alcance local, sus variables se asignan y se desasignan cuando se sale del alcance. Básicamente, esta es la pregunta, "¿en qué sentido las variables locales son locales?" ¿Cómo la semántica captura la localidad? Para explicar esto, inventó un modelo de categoría functor. (Cf. Reynolds: La esencia de Algol y Tennent: Semántica de los lenguajes de programación).

Tennent quería modelar los principios de razonamiento formulados en la lógica de especificación de Reynolds (una extensión de Hoare Logic para procedimientos de orden superior). La lógica tiene ideas como cálculos tipo expresión (solo lectura), no interferencia entre cálculos tipo comando y expresión, y algunos principios de razonamiento de abstracción de datos. Refinó el modelo de categoría functor de Reynolds para encontrar uno nuevo. Esto se llama el modelo "SASL", también cubierto en el libro de Tennent.

Meyer y Sieber, y también O'Hearn y Tennent, notaron que ninguno de estos modelos aún capturaba completamente la localidad de las variables locales. Cuando dos implementaciones de un tipo de datos abstracto o una clase difieren en sus variables locales pero las manipulan de manera que tienen el mismo comportamiento cuando se ven desde afuera, son observacionalmente equivalentes. La semántica denotacional debería igualarlos. Para modelar esto, O'Hearn y Tennent agregaron paramétrica relacional a una variante del modelo de categoría de functor de Reynolds.

Cuando miré el problema al mismo tiempo, no creía en el enfoque de categoría de functor. También pensé que era demasiado técnico y creí que debía haber un modelo más simple. Esto me llevó a inventar el modelo "Estado global considerado innecesario", que es más bien como un modelo de trazas CSP, pero para un lenguaje de orden superior. Como una ventaja adicional, este modelo también captó la irreversibilidad del cambio de estado, que no estaba presente en los modelos anteriores.

Mi modelo solo funcionaba para un sublenguaje de Algol que se comportaba bien, llamado Control sintáctico de interferencia . Abramsky y McCusker extendieron mi modelo usando ideas semánticas de juegos para que pueda funcionar para Algol completo. Entonces, su modelo explica los mismos fenómenos que el mío, pero para el lenguaje más grande.

En cada caso, podemos demostrar que los nuevos modelos capturan equivalencias observacionales (u otras formas de fórmulas lógicas) que exhiben los fenómenos computacionales mencionados, que no fueron validados por los modelos anteriores. Entonces, hay un sentido muy preciso en el que estos modelos están "explicando" los fenómenos computacionales.

[Todo el trabajo que mencioné aquí se puede encontrar en los volúmenes "Idiomas similares a Algol": enlace y enlace ]