¿Cuál es la base teórica de la programación imperativa?

La programación funcional tiene una base teórica en el cálculo lambda y la lógica combinatoria . Como alguien involucrado con la computación estadística, considero que estos conceptos son muy útiles para el modelado.

¿Existe una base matemática equivalente de programación imperativa , o simplemente surgió de la aplicación práctica de hardware en lenguaje máquina y el posterior desarrollo de FORTRAN ?

En general, cuando se usan las matemáticas para estudiar algo de X , primero se necesita un modelo de X , y luego se desarrolla una teoría, un conjunto de resultados sobre ese modelo. Supongo que la teoría puede decirse que es una "base teórica" de X . Ahora establezca X = cálculo. Existen muchos modelos de computación, muchos de los cuales implican "estado". Cada modelo tiene su propia "teoría" y a veces es posible "traducir" entre modelos. Creo que es difícil decir qué modelo es más "básico" --- simplemente están diseñados con diferentes objetivos en mente.

Las máquinas de Turing fueron diseñadas para definir qué es computable . Por lo tanto, son un buen modelo si te importa si existe un algoritmo para un problema determinado. A veces se abusa de este modelo para estudiar la eficiencia de los algoritmos o la dureza de los problemas, con el pretexto de que es lo suficientemente bueno, al menos si solo te interesan los polinomios / no polinomios. El modelo RAM está más cerca de una computadora real y, por lo tanto, es mejor si desea un análisis preciso de un algoritmo. Para poner límites inferiores a la dureza de los problemas, es mejor nouse un modelo que se parezca demasiado a las computadoras de hoy porque desea cubrir una amplia gama de computadoras posibles, sin dejar de ser más preciso que solo polinomio / no polinomio. En este contexto, vi, por ejemplo, el modelo de sonda celular utilizado.

Si le importa la corrección , entonces otros modelos son útiles. Aquí tienes semántica operativa (que diría que es el análogo del cálculo lambda para cálculos completos), semántica axiomática (desarrollada en 1969 por Hoare basada en las afirmaciones inductivas de Floyd de 1967, que Knuth popularizó en The Art of Computer Programming , tomo 1), y otros.

Para resumir, creo que buscas modelos de cálculo. Hay muchos de estos modelos, desarrollados con varios objetivos en mente, y muchos tienen estado, por lo que corresponden a la programación imperativa. Si desea saber si se puede calcular algo, mire las máquinas de Turing. Si le importa la eficiencia, mire los modelos RAM. Si le importa la corrección, observe los modelos que terminan en "semántica", como la semántica operativa.

Finalmente, permítanme mencionar que hay un gran libro en línea solo sobre Modelos de Computación de John Savage. Se trata principalmente de eficiencia. Para la parte de corrección, le recomiendo que comience con los trabajos clásicos de Floyd (1967) , Hoare (1969) , Dijkstra (1975) y Plotkin (1981) . Todos son geniales.

El modelo teórico más simple de un programa imperativo es la propia máquina de turing. Tiene los dos componentes esenciales de un programa imperativo: estado modificable ilimitado y una máquina de estado que opera en él.

También puede basar la programación imperativa en programación funcional al considerar los programas como composiciones de operaciones monádicas que pasan y devuelven versiones modificadas del estado global, como se hace en el lenguaje de programación Haskell.

En resumen, diría que la programación imperativa evolucionó del lenguaje de máquina y la práctica de programación. Por otro lado, las mónadas proporcionan un marco semántico apropiado para describir la semántica de las características imperativas del lenguaje de programación. El documento Nociones de computación y mónadas de Moggi estableció los fundamentos formales. Phil Wadler popularizó la idea y contribuyó significativamente a que fuera la forma clave de incorporar características imprescindibles en el lenguaje de programación Haskell. El trabajo reciente de Plotkin y las nociones de poder de la computación determinan las mónadas va a la inversa, indicando que algunas, pero no todas, las nociones de computación (imperativa) realmente dan una mónada, lo que significa que de una manera muy esencial las mónadas corresponden a nociones imperativas (y otras) de computación.

Si está buscando un tratamiento matemático riguroso de un lenguaje de programación imperativo, el libro de Winskel "La semántica formal de los lenguajes de programación" (1993) es un ejemplo.

En el libro, define un lenguaje de programación imperativo llamado IMP y proporciona semántica operativa, denotacional y axiomática.

Llego tarde a esta pregunta, pero es una pregunta fascinante. Entonces, aquí están mis puntos de vista.

Cuando era estudiante universitario, teníamos un gran profesor de matemáticas, que solía darnos conferencias sobre historia y desarrollo de las matemáticas. Según él, las matemáticas se desarrollaron en oleadas de "expansión" y "consolidación". Durante una fase de expansión, se consideraron e investigaron nuevas ideas que antes eran desconocidas. Luego, durante una fase de consolidación, las nuevas teorías se integraron en el cuerpo de conocimiento existente. Sin embargo, en el siglo XX, dijo, la expansión y la consolidación están sucediendo en paralelo.

La programación imperativa es actualmente una actividad de expansión para las matemáticas. Anteriormente era "desconocido". (Eso puede no ser del todo cierto. Hoare nos dice que Euclides estaba haciendo algo como la programación imperativa en su Geometría. Pero las matemáticas perdieron interés en ella, para bien o para mal). Los matemáticos todavía no están interesados ​​en la programación imperativa. Tanto la pérdida para ellos. Pero considero toda la informática como una rama de las matemáticas en un sentido abstracto. Lo estamos estudiando, expandiendo las matemáticas en el proceso.

Por lo tanto, no me importaría especialmente si existe una base teórica a priori para la programación imperativa. Si no hay ninguno, vamos a buscarlo. Lo que sabemos ya nos dice que la programación imperativa es fantásticamente profunda y hermosa. La programación funcional palidece en comparación. Pero, tenemos mucho trabajo por hacer para llevar toda esta teoría a la gente.

La programación funcional tiene una base clara en las matemáticas porque los lenguajes de programación funcional evolucionaron en paralelo con las matemáticas relevantes y sus diseñadores generalmente tenían las matemáticas en alta estima. La relación fuerte y directa es una profecía autocumplida.

La programación imperativa tiene una historia significativamente más desordenada que se vincula mucho más estrechamente con los problemas empresariales y de ingeniería y que históricamente estaba mucho más preocupada con el rendimiento de los compiladores y el código que generan que con el respeto de los formalismos matemáticos.

Muchas personas han intentado explicar la programación imperativa en términos (tradicionalmente) funcionales. Esto puede ser lo más cerca que podemos llegar a lo que está buscando, pero estos intentos son invariablemente incómodos, tediosos, forenses. Estoy bastante seguro de que preferiría arrancarme los ojos de la cara que leer una prueba de progreso / preservación para el CLR.

Por lo general, si llega al final de un libro de texto pl decente (por ejemplo, Tipos y lenguajes de programación de Pierce), comenzará a ver modelos formales de características de lenguaje imperativas. Esto puede ser interesante para ti.

An Axiomatic Basis for Computer Programming por CAR HOARE

En este artículo se intenta explorar los fundamentos lógicos de la programación de computadoras mediante el uso de técnicas que se aplicaron primero en el estudio de la geometría y luego se extendieron a otras ramas de las matemáticas. Esto implica la elucidación de conjuntos de axiomas y reglas de inferencia que pueden usarse en pruebas de las propiedades de los programas de computadora. Se dan ejemplos de tales axiomas y reglas, y se muestra una prueba formal de un teorema simple. Finalmente, se argumenta que importantes ventajas, tanto teóricas como prácticas, pueden derivarse de la búsqueda de estos temas.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Respaldo lo que dijo Alexandre, que la máquina de Turing proporcionó la base teórica original para la programación imperativa. En la medida en que la organización de los lenguajes de programación imperativos refleje la arquitectura de la máquina, creo que el trabajo de John Von Neumann también sería una parte clave de sus fundamentos teóricos.

¿Existe una base matemática equivalente de programación imperativa, o simplemente surgió de la aplicación práctica de hardware en lenguaje máquina y el posterior desarrollo de FORTRAN?

Si quiere decir "base" en el sentido histórico, creo que no hay una "base matemática equivalente". Sin embargo, a pesar de que la programación imperativa surgió de preocupaciones prácticas, hay varias formas de caracterizar de manera integral el significado de la programación imperativa en formas que podría encontrar "útiles para modelar", como la lógica de Hoare .

Las publicaciones que mencionan la lógica hoare y la lógica de separación son las correctas en este asunto. La lógica de Hoare le permite establecer propiedades de toda la configuración de almacenamiento dinámico de un programa, y ​​la lógica de separación es el pariente más moderno que le permite utilizar una "conjunción de separación" que le permite establecer como condiciones previas y posteriores a un segmento de código qué propiedades tienen para la parte del montón que el segmento del programa manipulará mientras se cuantifica sobre el resto del montón.

La respuesta con respecto a las mónadas no es estrictamente precisa, porque en Haskell se usa una mónada simplemente porque es una abstracción que permite la codificación del orden de las restricciones de evaluación y el seguimiento explícito de la propiedad "podría usar IO".

Vale la pena señalar que tanto la lógica de hoare / separación se puede ver como mónadas, y que hay una serie de proyectos contemporáneos como el proyecto ynot en Harvard que están explorando estos temas.

La investigación en lógica de separación es un campo continuo y activo.

Llegaré a esta pregunta incluso más tarde, pero estoy igualmente fascinado por ella.

Por qué la teoría de la programación imperativa se considera menos establecida que la de la programación funcional me evade. Probablemente comenzó a ponerse serio con Scott y de Bakker en 1969 con su análisis del significado de la recursividad en un lenguaje imperativo simple [1]. Cuando el lenguaje imperativo gana características, la historia se vuelve un poco más desordenada, pero ese es solo el precio a pagar por estar más cerca del metal. Para nombrar uno de los esfuerzos más completos, en 1980, de Bakker, de Bruin y Zucker escribieron una monografía sobre el tema [2]. Otros fueron mencionados anteriormente. Estas referencias, por supuesto, tienen una lógica de separación anterior a la fecha, pero [2], sin embargo, abordan las matrices y los procedimientos recursivos mutuos.

[1]: inédito en 1969, pero apareció como Jaco W. de Bakker y Dana S. Scott. Una teoría de los programas , páginas 1-30. En Klop et al. JW de Bakker, 25 años de edad. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: teoría matemática de la corrección del programa. Prentice Hall 1980.

Poco después de hacer su pregunta, Mark Bender de la Universidad McMaster lanzó una tesis: Cálculo de asignación: un lenguaje de razonamiento imperativo puro (8 de septiembre de 2010). Esta tesis describe un lenguaje simple e imperativo que corresponde al cálculo lambda.

El cálculo de asignación consta de solo cuatro construcciones básicas, asignación X:=t, secuencia t;u, formación de ¡tprocedimiento e invocación de procedimiento !t. Se dan tres interpretaciones para AC: una semántica operativa, una semántica denotacional y un sistema de reescritura de términos. Los tres se muestran como equivalentes.

La tesis de Mark Bender continúa explorando variantes extendidas con evaluación perezosa, retroceso, composición del procedimiento. Esto es similar a la exploración del cálculo lambda mediante el uso de pequeñas extensiones.

En general, la tesis proporciona una respuesta relativamente directa a la pregunta OP.