¿Cómo se manejan los efectos secundarios en la semántica?

En la sección "Introducción a los lenguajes de programación" de Anthony Aaby sobre semántica , hace la siguiente observación:

Gran parte del trabajo en la semántica de los lenguajes de programación está motivado por los problemas encontrados al tratar de construir y comprender programas imperativos, programas con comandos de asignación. Como el comando de asignación reasigna valores a variables, la asignación puede tener efectos inesperados en partes distantes del programa.

Esto me parece una admisión notable, que permitir los efectos secundarios motivaría una parte importante del trabajo en semántica.

¿Cómo afecta la existencia de efectos secundarios en un lenguaje de programación la capacidad de asignar un programa a un modelo computacional? ¿Existen enfoques para administrar el estado que puedan mejorar este proceso y al mismo tiempo permitir efectos secundarios?

Sobre la base de la respuesta de Charles, la principal dificultad en la teoría de los lenguajes de programación es que la noción natural de equivalencia de los programas generalmente no es la igualdad estricta ni en la semántica matemática más directa que puede dar, ni en el modelo de máquina subyacente. Por ejemplo, considere el siguiente bit de código similar a Java:

Object x = new Object();
Object y = new Object();
... some more code ...

Entonces, este programa crea un objeto y lo nombra x, y luego crea un segundo objeto llamado y, y luego continúa ejecutando más código. Ahora, suponga que un programador decide cambiar el orden de asignación de estos dos objetos:

Object y = new Object();
Object x = new Object();
... some more code ...

Ahora, haga la pregunta: ¿esta refactorización cambia el comportamiento del programa? Por un lado, en la máquina subyacente, x e y se asignarán en diferentes ubicaciones en las dos ejecuciones del programa. Entonces, en este sentido, el programa se comporta de manera diferente.

Pero en un lenguaje similar a Java, solo puede probar las referencias para la igualdad, y no para el orden, por lo que esta es una diferencia que el "algún código más" no puede observar . Como resultado, la mayoría de los programadores esperarán que invertir el orden no haga ninguna diferencia en la respuesta final, y la mayoría de los escritores de compiladores esperan poder realizar reordenamientos y optimizaciones sobre esta base. (Por otro lado, en un lenguaje similar a C, puede comparar punteros para ordenar, convirtiéndolos primero en enteros, por lo que este reordenamiento no necesariamente conserva un comportamiento observable).

Una de las preguntas centrales de la semántica es responder a la pregunta de cuándo dos programas son observablemente equivalentes. Dado que nuestra noción de observación depende de las características del lenguaje de programación, terminamos con una definición como "dos programas son equivalentes cuando ningún programa cliente puede calcular diferentes respuestas basadas en recibir esos programas como entradas". La cuantificación de todos los programas cliente es lo que hace que esta pregunta sea difícil: parece que terminas teniendo que decir algo sobre todos los posibles programas cliente para decir algo sobre dos piezas de código en particular.

El truco con la semántica denotacional es dar una interpretación matemática que le permita evitar esta cuantificación universal: usted dice que el significado de un fragmento de código es un valor matemático, y los compara verificando si son matemáticamente iguales o no. Esto es local (es decir, de composición) y no implica la cuantificación de todos los clientes posibles. (Es necesario demostrar que la semántica denotacional implica equivalencia contextual para que sea sólida, por supuesto. Cuando está completa, cuando la igualdad denotacional es exactamente la misma que la equivalencia contextual, decimos que la semántica es "completamente abstracta").

Pero significa que debe asegurarse de que la semántica denotacional valida esas equivalencias. Entonces, para este ejemplo, si desea dar una semántica denotacional para este lenguaje similar a Java, debe asegurarse no solo de que llamar a nuevo toma un montón y le devuelve un nuevo montón con el objeto recién creado, sino que el significado del programa es invariante igual bajo todas las permutaciones del montón de entrada. Esto puede implicar estructuras matemáticas bastante complejas (por ejemplo, en este caso trabajar en una categoría que garantiza que todo funcione en un grupo de permutación adecuado).

Por supuesto, hay formas de tratar los efectos en la semántica (denotacional). Por ejemplo, podemos usar la idea de Eugenio Moggi de que los efectos computacionales son mónadas (esta idea también se ha utilizado en el diseño de Haskell). Uno de los problemas con esto es que las mónadas son difíciles de combinar. Gordon Plotkin y John Power sugirieron un refinamiento de las mónadas de Moggi a las teorías de Lawvere , o teorías algebraicas como también se las llama, que abarca los efectos algebraicos (los efectos más comunes son algebraicos, como estado, E / S, no determinismo, pero las continuas son no). Para un tratamiento integral, vea la tesis de Matija Pretnar .

También debo mencionar la posible semántica de mundos para el estado local, desarrollada por Frank Oles y John Reynolds (lo siento, no puedo encontrar un mejor enlace, esto es de 1982), que es anterior a las mónadas de Moggi. Usaron categorías de preajustes para proporcionar una semántica de un lenguaje similar a algol que modeló correctamente muchos aspectos del estado local (pero no todos, creo que el modelo permitió el retroceso, pero tal vez mi memoria me sirve mal).

Matthias Felleisen presentó una solución convincente para el problema de los efectos secundarios en semántica en su serie sobre "Teorías sintácticas de control y estado".

Esa línea de trabajo dio como resultado la máquina CESK, un marco simple de máquina abstracta capaz de modelar de manera concisa lenguajes funcionales, orientados a objetos, imperativos e incluso lógicos. El marco CESK maneja no solo los efectos secundarios, sino también construcciones de control "complejas" como excepciones, continuaciones, pereza e incluso subprocesos.

La máquina CESK, y la semántica operativa de pequeños pasos en general, han sido el estándar de facto en la teoría del lenguaje de programación durante aproximadamente dos décadas.

En resumen, una máquina CESK es una máquina de pequeños pasos con cuatro componentes para describir cada estado de la máquina: la cadena de control (una generalización del contador del programa), el entorno, una tienda (también llamada el montón) y la continuación actual.

El entorno asigna variables a direcciones; la tienda asigna direcciones a valores.

Esto hace que sea sencillo modelar variables mutables: simplemente cambie el valor en su dirección.

También facilita el modelado de punteros y la asignación dinámica: solo haga que las direcciones de las tiendas sean valores de primera clase.

De manera similar, las continuaciones de primera clase resultan de hacerlos valores direccionables.

¿Cómo afecta la existencia de efectos secundarios en un lenguaje de programación la capacidad de asignar un programa a un modelo computacional?

No necesariamente lo hace difícil, pero impone restricciones en la forma en que la semántica de las expresiones más grandes puede construirse a partir de las más pequeñas. Puede interactuar muy mal con ciertas otras construcciones de programación, por ejemplo, si se quiere dar una semántica denotativa al estilo Scott para un lenguaje que permita la asignación de funciones de orden superior a referencias globales.

No son simplemente los efectos secundarios como el estado los que causan el problema. Lenguajes imperativos simples como el lenguaje de comando protegido de Dijkstra tienen este tipo de efectos secundarios y tienen una semántica agradable. Surgen problemas con las extensiones del cálculo lambda con el tipo de semántica operativa que se espera de los lenguajes de programación incluso en ausencia de efectos secundarios: el PCF de Plotkin más temprano recibió modelos denotacionales relativamente temprano, pero la semántica no era completamente abstracta, lo que significa que La semántica denotacional era demasiado general, no correspondía exactamente a su semántica operativa. PCF finalmente recibió una semántica denotacional completamente abstracta a fines de la década de 1980 con la semántica de juegos, que no se parece en nada a la semántica de la teoría del orden de Scott. La concurrencia aún no ha recibido un tratamiento denotacional totalmente adecuado.

Muchos cuestionan la importancia de este tipo de semántica. Siempre podemos proporcionar algún tipo de semántica operativa, incluso si esa "semántica" es solo la fuente del programa y los nombres de algunas máquinas que han compilado y ejecutado el programa: por esta razón, Strachey condenó la semántica operativa. Pero la semántica de operación estructural de Plotkin ha mostrado cómo la semántica operacional puede separarse de los modelos de máquina, y el trabajo de Pitt ha demostrado cómo dicha semántica puede soportar un razonamiento similar sobre programas y lenguajes de programación para la semántica denotacional. Por lo tanto, la semántica operativa es una alternativa viable a la semántica denotacional, y se ha aplicado con éxito a un número sustancial de lenguajes de programación como el ML estándar.

¿Existen enfoques para administrar el estado que puedan mejorar este proceso y al mismo tiempo permitir efectos secundarios?

Hasta cierto punto, las dificultades para proporcionar semántica corresponden a la dificultad de proporcionar lenguajes de programación potentes que se comporten de la manera que uno esperaría. Las decisiones de diseño motivadas pragmáticamente, como evitar el uso del estado global junto con la concurrencia, generalmente a través de la concurrencia de transmisión de mensajes, hacen que sea más fácil proporcionar semántica.