Pruebas técnicas relacionadas con la correspondencia de Curry-Howard

Estoy buscando fuentes sobre la noción formal de programas. Esto parece estar estrechamente relacionado con la correspondencia de Curry-Howard, pero también podría rastrearse hasta Universal Turing Machines y su capacidad para leer la descripción y la entrada de cualquier TM.

Al leer sobre la correspondencia de Curry-Howard, siento que la primordialidad de los UTM-s puede dañar la investigación en programas con la conclusión única de que cualquier programa puede reducirse a símbolos, estados y reglas. ¿Existe el enfoque opuesto, donde se definen y examinan los sistemas de computación de alto nivel? ¿Cuáles son los buenos recursos al respecto?

Lo que quieres existe y es un área enorme de investigación: es toda la teoría de los lenguajes de programación.

Hablando en términos generales, puede ver la computación de dos maneras. Puedes pensar en máquinas , o puedes pensar en idiomas .

Una máquina es básicamente una especie de control finito aumentado con algo de memoria (posiblemente sin límites). Esta es la razón por la cual las clases introductorias de TOC van desde autómatas finitos a autómatas pushdown a máquinas Turing, cada clase toma un control finito y le agrega más memoria. (Hoy en día, el control finito a menudo se limita aún más, como en los modelos de circuito). Lo esencial es que el control finito se otorga por adelantado, y todo a la vez.

Un lenguaje es una forma de especificar toda una familia de controles, de manera compositiva. Tiene formas primitivas para controles básicos y operadores para construir controles más grandes a partir de controles más pequeños. El lenguaje primordial, el cálculo lambda, de hecho no especifica nada más que control: lo único que puede definir son abstracciones de funciones, aplicaciones y referencias variables.

Puede ir y venir entre estas dos vistas: el teorema es esencialmente una prueba de que las máquinas de Turing pueden implementar abstracción y aplicación de funciones, y las codificaciones de Church demuestran que el cálculo lambda puede codificar datos. Pero hay contenido no trivial en ambos teoremas, por lo que no debe cometer el error de pensar que las dos formas de entender la computación son las mismas.$snm$

Los investigadores en complejidad y algoritmos generalmente toman las máquinas como fundamentales, porque están interesadas en los costos y en los resultados de factibilidad . Para exagerar un poco, la pregunta básica de investigación que tienen es:

¿Cuál es la máquina menos poderosa que puede resolver un cierto tipo de problema?

Los investigadores de idiomas toman los idiomas como fundamentales, porque estamos interesados ​​en resultados de expresividad e imposibilidad . Con una exageración similar, nuestra pregunta básica de investigación es:

¿Cuál es el lenguaje más expresivo que descarta cierto tipo de mal comportamiento?

Como comentario, ¡observe cómo los dos bienes que cada tipo de valores teóricos están directamente en conflicto! Un buen trabajo en algoritmos y complejidad le permite resolver un problema más difícil, utilizando menos recursos. El buen trabajo en idiomas permite a los programadores hacer más cosas, al tiempo que prohíbe más comportamientos malos. (Este conflicto es básicamente por qué la investigación es difícil).

Ahora, puede preguntarse por qué más tipos de Teoría A no usan lenguajes, o por qué más investigadores de Teoría B no usan máquinas. La razón surge de la forma de la pregunta básica de investigación.

Tenga en cuenta que la pregunta de investigación básica estilizada en algoritmos / complejidad es una pregunta de límite inferior: desea saber que tiene la mejor solución y que no hay una forma posible de hacerlo mejor, sin importar cuán inteligente sea. Una definición de idioma corrige los medios de composición del programa y, por lo tanto, si demuestra que hay un límite inferior con un modelo de lenguaje, entonces se le puede preguntar si de alguna manera no sería posible hacerlo mejor si extendiera su idioma con nueva caracteristica. Un modelo de máquina le da todo el control de una vez, y así sabe todo lo que la máquina puede hacer desde el principio.

Pero las especificaciones de la máquina son exactamente lo incorrecto para decir cosas interesantes sobre el bloqueo del mal comportamiento. Una máquina le da un control total por adelantado, pero saber que un programa en particular está bien o mal no lo ayuda cuando desea extenderlo o usarlo como una subrutina, como dice el epigrama de Perlis: "Cada programa es un parte de algún otro programa y rara vez encaja ". Dado que los investigadores de idiomas están interesados ​​en decir cosas sobre clases enteras de programas, los idiomas son mucho más adecuados para su propósito.