El vínculo profundo que equipara pruebas matemáticas y programas informáticos | Revista Quanta

Algunos descubrimientos científicos son importantes porque revelan algo nuevo: la estructura de doble hélice del ADN, por ejemplo, o la existencia de agujeros negros. Sin embargo, algunas revelaciones son profundas porque muestran que dos viejos conceptos, que alguna vez se consideraron distintos, en realidad son los mismos. Tomemos como ejemplo las ecuaciones de James Clerk Maxwell que muestran que la electricidad y el magnetismo son dos aspectos de un solo fenómeno, o la vinculación de la gravedad con un espacio-tiempo curvo según la relatividad general.

La correspondencia Curry-Howard hace lo mismo pero a mayor escala, vinculando no sólo conceptos separados dentro de un campo, sino disciplinas enteras: Ciencias de la Computación y lógica matemática. También conocido como isomorfismo de Curry-Howard (un término que significa que existe algún tipo de correspondencia uno a uno entre dos cosas), establece un vínculo entre las pruebas matemáticas y los programas de computadora.

En pocas palabras, la correspondencia Curry-Howard postula que dos conceptos de la informática (tipos y programas) son equivalentes, respectivamente, a proposiciones y pruebas: conceptos de la lógica.

Una ramificación de esta correspondencia es que la programación, a menudo vista como un oficio personal, se eleva al nivel idealizado de las matemáticas. Escribir un programa no es sólo “codificar”, sino que se convierte en un acto de demostrar un teorema. Esto formaliza el acto de programar y proporciona formas de razonar matemáticamente sobre la corrección de los programas.

La correspondencia lleva el nombre de los dos investigadores que la descubrieron de forma independiente. En 1934, el matemático y lógico Haskell Curry notó una similitud entre las funciones en matemáticas y la relación de implicación en lógica, que toma la forma de declaraciones "si-entonces" entre dos proposiciones.

Inspirado por la observación de Curry, el lógico matemático William Alvin Howard descubrió un vínculo más profundo entre la computación y la lógica en 1969, demostrando que ejecutar un programa de computadora es muy parecido a simplificar una prueba lógica. Cuando se ejecuta un programa de computadora, cada línea se "evalúa" para producir un resultado único. De manera similar, en una demostración, se comienza con declaraciones complejas que se pueden simplificar (eliminando pasos redundantes, por ejemplo, o sustituyendo expresiones complejas por otras más simples) hasta llegar a una conclusión: una declaración más condensada y sucinta derivada de muchas declaraciones intermedias. .

Si bien esta descripción transmite un sentido general de la correspondencia, para comprenderla completamente necesitamos aprender un poco más sobre lo que los científicos informáticos llaman "teoría de tipos".

Empecemos por una famosa paradoja: en un pueblo vive un barbero que afeita a todos los hombres que no se afeitan ellos mismos, y sólo a ellos. ¿El barbero se afeita solo? Si la respuesta es sí, entonces no debe afeitarse (porque sólo afeita a hombres que no se afeitan). Si la respuesta es no, entonces debe afeitarse (porque afeita a todos los hombres que no se afeitan). Esta es una versión informal de una paradoja que Bertrand Russell descubrió al intentar establecer los fundamentos de las matemáticas utilizando un concepto llamado conjuntos. Es decir, es imposible definir un conjunto que contenga todos los conjuntos que no se contienen a sí mismos sin encontrar contradicciones.

Para evitar esta paradoja, demostró Russell, podemos utilizar "tipos". En términos generales, se trata de categorías cuyos valores específicos se denominan objetos. Por ejemplo, si hay un tipo llamado "Nat", que significa números naturales, sus objetos son 1, 2, 3, etc. Los investigadores suelen utilizar dos puntos para indicar el tipo de objeto. El número 7, de tipo entero, se puede escribir como “7: Entero”. Puede tener una función que tome un objeto de tipo A y escupe un objeto de tipo B, o una que combine un par de objetos que eran de tipo A y B en un nuevo tipo, llamado "A × B".

Por lo tanto, una forma de resolver la paradoja es jerarquizar estos tipos, de modo que sólo puedan contener elementos de un “nivel inferior” que ellos mismos. Entonces un tipo no puede contenerse a sí mismo, lo que evita la autorreferencialidad que crea la paradoja.

En el mundo de la teoría de tipos, demostrar que una afirmación es verdadera puede parecer diferente a lo que estamos acostumbrados. Si queremos demostrar que el número entero 8 es par, entonces es cuestión de demostrar que 8 es efectivamente un objeto de un tipo específico llamado “Par”, donde la regla de pertenencia es ser divisible por 2. Después de verificar que 8 es divisible por 2, podemos concluir que 8 es efectivamente un “habitante” del tipo Even.

Curry y Howard demostraron que los tipos son fundamentalmente equivalentes a las proposiciones lógicas. Cuando una función “habita” en un tipo (es decir, cuando se puede definir con éxito una función que es un objeto de ese tipo), se está demostrando efectivamente que la proposición correspondiente es verdadera. Entonces, las funciones que toman una entrada de tipo A y dan una salida de tipo B, denotada como tipo A → B, deben corresponder a una implicación: "Si A, entonces B". Por ejemplo, tomemos la proposición "Si está lloviendo, entonces el suelo está mojado". En teoría de tipos, esta proposición se modelaría mediante una función del tipo "Raining → GroundIsWet". Las formulaciones que parecen diferentes son, de hecho, matemáticamente iguales.

Por abstracto que pueda parecer ese vínculo, no sólo ha cambiado la forma en que los profesionales de las matemáticas y la informática piensan sobre su trabajo, sino que también ha dado lugar a varias aplicaciones prácticas en ambos campos. Para la informática, proporciona una base teórica para la verificación del software, el proceso de garantizar la corrección del software. Al formular los comportamientos deseados en términos de proposiciones lógicas, los programadores pueden demostrar matemáticamente que un programa se comporta como se esperaba. También proporciona una base teórica sólida para diseñar lenguajes de programación funcionales más potentes.

Y para las matemáticas, la correspondencia ha llevado al nacimiento de asistentes de prueba, también llamados demostradores de teoremas interactivos. Se trata de herramientas de software que ayudan a construir pruebas formales, como Coq y Lean. En Coq, cada paso de la prueba es esencialmente un programa, y ​​la validez de la prueba se verifica con algoritmos de verificación de tipos. Los matemáticos también han estado utilizando asistentes de prueba (en particular, el Probador del teorema Lean — formalizar las matemáticas, lo que implica representar conceptos, teoremas y demostraciones matemáticas en un formato riguroso y verificable por computadora. Esto permite que las computadoras controlen el lenguaje, a veces informal, de las matemáticas.

Los investigadores todavía están explorando las consecuencias de este vínculo entre matemáticas y programación. La correspondencia original entre Curry y Howard fusiona la programación con un tipo de lógica llamada lógica intuicionista, pero resulta que más tipos de lógica también podrían ser susceptibles de tales unificaciones.

"Lo que ha sucedido en el siglo transcurrido desde la idea de Curry es que seguimos descubriendo más y más casos en los que 'el sistema lógico X corresponde al sistema computacional Y'", dijo miguel clarkson, científico informático de la Universidad de Cornell. Los investigadores ya han conectado la programación con otros tipos de lógica, como la lógica lineal, que incluye el concepto de "recursos", y la lógica modal, que se ocupa de los conceptos de posibilidad y necesidad.

Y aunque esta correspondencia lleva los nombres de Curry y Howard, no son de ninguna manera los únicos que la han descubierto. Esto da fe de la naturaleza fundamental de la correspondencia: la gente sigue notándola una y otra vez. "No parece ser casualidad que exista un vínculo profundo entre la computación y la lógica", dijo Clarkson.