¿Cuál es la diferencia entre pruebas y programas (o entre proposiciones y tipos)?

Dado que la correspondencia de Curry-Howard está tan extendida / extendida, ¿hay alguna diferencia entre pruebas y programas (o entre proposiciones y tipos)? ¿Podemos realmente identificarlos?

Los lenguajes de programación que la gente usa día a día no encajan tan bien en la correspondencia Curry-Howard, porque sus sistemas de tipos son demasiado débiles. Para decir algo interesante usando Curry-Howard para programas imperativos, uno necesita tener un sistema de tipos más sofisticado. El libro Adapting Proofs-as-program empuja este ángulo con el objetivo de sintetizar programas imperativos. Con los tipos dependientes cada vez más populares, ciertamente en los lenguajes funcionales de investigación ( Agda , Epigram ), la distinción se vuelve cada vez más borrosa. Por supuesto, puede hacer la síntesis / extracción del programa dentro del probador de teoremas de Coq (y presumiblemente otros), que por supuesto se basa en Curry-Howard.

La correspondencia de Curry-Howard también se puede utilizar en situaciones en las que las pruebas no corresponden tan claramente a los programas (o no son programas que nadie ejecutará). Un ejemplo de esto está en la autorización para portar pruebas . Las proposiciones corresponden a declaraciones sobre quién está autorizado a hacer qué. Las pruebas proporcionan la evidencia requerida que posee una propuesta, por lo tanto, se permite una solicitud de autorización. Para codificar las pruebas, se introducen términos de prueba (a través de Curry-Howard). Los términos de prueba se envían entre las partes como representaciones de pruebas de la validez de las solicitudes de autorización, pero no se consideran programas.

En Coq, hay 2 tipos (Prop y Set), los usa el programador para separar las pruebas que no producirán el código real y la parte de la prueba que se usará para extraer el código en ejecución (su programa).

Esa es una buena solución para el problema sobre el que pregunta, cómo identificar qué está destinado a generar código de máquina (programa) y qué está presente para completar la prueba de la proposición (o tipo).

AFAIK no hay forma automática de distinguir ambos. ¿Esto podría ser algo interesante para la investigación? ¿O tal vez alguien puede señalar que es claramente imposible?

¡Con los tipos dependientes no solo no hay una distinción clara entre pruebas y programas, sino que tampoco hay una distinción entre programas y tipos! La única distinción será donde aparezca el tipo (o programa), haciéndolo parte del lugar "programa" o del lugar "tipo" de un término dado.

Un ejemplo lo aclarará, espero:

Cuando usa la función de identidad con tipos dependientes, debe pasar el tipo con el que va a usar la función. ¡El tipo se está utilizando como valor en su "programa"!

Cálculo Lambda sin tipo:

$\lambda{x}.x$

Con tipos dependientes:

id: (A: Conjunto) -> A -> A

$(\lambda{A}.(\lambda{x}.x))$

Si está utilizando esta función, entonces lo haría como este ejemplo:

id Naturals 1

Observe que el "tipo" (en este caso, el Conjunto de naturales) que se pasa como un valor se desecha, por lo que nunca se calculará, pero aún está en la parte del "programa" del término. Eso es lo que también sucederá con las partes de "prueba", deben estar allí para que el término verifique los tipos, pero durante el cálculo se descartarán.

Me arriesgaré aquí y diré que, si está dispuesto a entrecerrar los ojos un poco, se pueden identificar pruebas y programas de terminación .

Cualquier programa de terminación es una prueba de que puede tomar su entrada y producir su salida. Este es un tipo muy básico de prueba de implicación.

Por supuesto, para hacer que esta implicación lleve información más significativa que decir lo obvio, debe ser capaz de demostrar que el programa funciona para todas y cada una de las instancias de entrada extraídas de alguna clase con significado lógico. (Y también para la salida).

Desde la otra dirección, cualquier prueba con pasos de inferencia finita es un programa simbólico que manipula objetos en algún sistema lógico. (Si no nos preocupamos demasiado por lo que los símbolos lógicos y las reglas significan computacionalmente).

$\exists x : x \vdash T$

Esto es bastante simplista, pero creo que sugiere la solidez de la idea. (Incluso si a algunas personas no les gusta. ;-))

Prueba de irrelevancia?

Cuando escribe algún programa, está interesado en su rendimiento, consumo de memoria, etc.
Por ejemplo, es mejor usar un algoritmo de clasificación inteligente en lugar de la clasificación de burbujas, incluso si sus implementaciones tienen los mismos tipos (incluso en la configuración de tipo dependiente).

Pero cuando demuestras algún teorema, solo te interesa la existencia de una prueba.

Por supuesto, desde el punto de vista estético, algunas pruebas son más simples / hermosas / inspiradoras / etc. (por ejemplo, las pruebas de El libro).

Si acepta la correspondencia Curry-Howard, entonces la pregunta es principalmente filosófica. "¿Las pruebas y los programas son diferentes? Por supuesto. ¿Cómo? Bueno, llamamos a las pruebas 'pruebas' y llamamos a los programas 'programas'".

O, para decirlo con menos frialdad, si hay un isomorfismo entre las pruebas y los programas, lo que parece claramente que existe, entonces su pregunta es si hay algún oráculo capaz de distinguir los dos. Los seres humanos los clasifican como diferentes (en su mayor parte), por lo que es ciertamente discutible que exista tal oráculo. La pregunta importante se convierte entonces en si existe alguna diferencia significativa entre ellos, lo que está sujeto a debate filosófico. ¿Qué es una "prueba"? No existe una definición formal de lo que constituye una prueba; es un término de arte, muy parecido a la noción de "efectivamente calculable" en la tesis de la Iglesia-Turing. Para el caso, "programa" tampoco tiene una definición formal.

Estas son palabras de lenguaje natural usadas para categorizar diferentes campos de la investigación matemática. Lo que Curry y Howard observaron es que estos dos campos diferentes en realidad estudiaban lo mismo. Notar esta conexión es importante porque dice que estos diferentes investigadores deberían estar hablando entre sí. Pero en otro nivel, notar la conexión es creer la diferencia entre ellos. Al abordar un problema, a veces es más beneficioso pensarlo como un problema de programación, mientras que otras veces es más beneficioso pensarlo como un problema lógico. Esta diferencia de perspectiva es, creo, la diferencia importante entre ellos. Pero si una diferencia de perspectiva constituye una diferencia de identidad es una cuestión filosófica profunda que se ha explorado al menos desde la época de FregeUeber Sinn und Bedeutung .