La tesis de Church-Turing es una hipótesis que postula una equivalencia entre la noción intuitiva de computabilidad algorítmica y las nociones estrictamente formalizadas de una función parcialmente recursiva y una función computable en una máquina de Turing . Debido a la naturaleza intuitiva del concepto inicial de computabilidad algorítmica, esta tesis tiene el carácter de un juicio sobre este concepto y no puede ser estrictamente probada o refutada [1] . Antes de una definición precisa de una función computable, los matemáticos a menudo usaban el término informal "efectivamente computable" para describir funciones que se pueden calcular usando métodos de papel y lápiz.
La tesis fue presentada por Alonzo Church y Alan Turing a mediados de la década de 1930 [2] [3] [4] [5] . Esencial para muchas áreas de la ciencia y la filosofía de la ciencia, incluida la lógica matemática , la teoría de la prueba , la informática y la cibernética .
En términos de la teoría de la recursión , la tesis se formula como una descripción precisa de la noción intuitiva de computabilidad por una clase de funciones recursivas generales . Esta formulación se refiere a menudo simplemente como la tesis de Church [6] .
Stephen Kleene dio una formulación más general , según la cual todas las funciones parciales (es decir, no necesariamente definidas para todos los valores de argumento) que son computables por algoritmos son parcialmente recursivas [7] .
En términos de computabilidad de Turing, la tesis establece que para cualquier función algorítmicamente computable, existe una máquina de Turing que calcula sus valores [8] . A veces esta formulación aparece como la tesis de Turing . En vista del hecho de que las clases de funciones parcialmente computables en el sentido de Turing y parcialmente recursivas coinciden, la declaración se combina en una sola tesis de Church-Turing .
Más tarde, se formularon otras versiones prácticas de la declaración:
Un problema importante para los lógicos en la década de 1930 fue el problema de la resolución : si existe un procedimiento mecánico para separar las verdades matemáticas de las falsedades matemáticas. Esta tarea requería que se fijara el concepto de "algoritmo" o "computabilidad efectiva", al menos para poder iniciar la tarea. [9] Desde el principio hasta el día de hoy (a partir de 2007), ha habido un debate continuo: [10] si la noción de "computabilidad efectiva" era (i) "un axioma o axiomas" en un sistema axiomático, o ( ii) solo una definición que "identificó" dos o más oraciones o (iii) una hipótesis empírica para ser probada contra eventos naturales o (iv) o simplemente una oración por el bien del argumento (es decir, "tesis").
En el curso del estudio del problema, Church y su alumno Stephen Kleene introdujeron la noción de funciones definibles en λ y pudieron demostrar que varias clases grandes de funciones que se encuentran con frecuencia en la teoría de números eran definibles en λ. [11] La discusión comenzó cuando Church le sugirió a Kurt Gödel que las funciones "efectivamente computables" se definieran como funciones definibles en λ. Sin embargo, Gödel no estaba convencido y calificó la propuesta de "completamente insatisfactoria". [12] Sin embargo, Gödel, en correspondencia con Church, propuso axiomatizar la noción de "computabilidad efectiva"; En una carta a Kleene y Church, dijo que
Su única idea en ese momento era que podría ser posible definir el término computabilidad efectiva como un concepto indefinido como un conjunto de axiomas que encarnan las propiedades generalmente aceptadas de ese concepto y luego hacer algo basado en eso.
- [13]Pero Gödel no dio más instrucciones. Propuso solo la recursividad , modificada por la sugerencia de Herbrand, que Gödel escribió extensamente en sus conferencias de 1934 en Princeton, Nueva Jersey (Kleene y Rosser transcribieron las notas). Pero no creía que las dos ideas pudieran definirse satisfactoriamente "excepto heurísticamente". [catorce]
Luego fue necesario identificar y probar la equivalencia de las dos nociones de computabilidad efectiva. Equipado con el cálculo λ y la recursividad "general", Stephen Kleene, con la ayuda de Church y J. Barkley Rosser, produjo demostraciones (1933, 1935) para demostrar que los dos cálculos son equivalentes. Church posteriormente modificó sus métodos para incluir el uso de la recursividad de Herbrand-Gödel y luego demostró (1936) que el problema de resolución es indecidible: no existe un algoritmo general que pueda determinar si una fórmula bien formulada está en "forma normal". [quince]
Muchos años después, en una carta a Davis (alrededor de 1965), Gödel dijo que "durante estas conferencias [de 1934] no estaba del todo convencido de que su concepto de recursividad incluyera todas las posibles recurrencias". [16] En 1963, Gödel había abandonado la recursividad de Herbrand-Gödel y el cálculo λ en favor de la máquina de Turing como la definición de "algoritmo" o "procedimiento mecánico" o "sistema formal". [17]
¿ Hipótesis que conduce a la ley natural ? : A fines de 1936, el artículo de Alan Turing (que también demuestra que el problema de la resolución no tiene solución ) se habló oralmente, pero aún no ha aparecido impreso. [18] Por otro lado, apareció el artículo de Emil Post de 1936 y fue certificado independientemente del trabajo de Turing. [19] Post no estuvo de acuerdo con la "identificación" de Church de la computabilidad efectiva con el cálculo λ y la recursividad, afirmando:
De hecho, en el trabajo de Church y otros, esta identificación se afirma con mucha más fuerza que la hipótesis de trabajo. Pero disfrazar esta identificación como una definición... nos ciega a la necesidad de una verificación constante.
— [20]Más bien, consideró la noción de "computabilidad efectiva" simplemente como una "hipótesis de trabajo" que podría conducir mediante un razonamiento inductivo a una "ley natural" en lugar de una "definición o axioma". [21] Esta idea fue "fuertemente" criticada por Church. [22]
Así, Post, en su artículo de 1936, también rechazó la sugerencia de Kurt Gödel a Church en 1934-5 de que una tesis podría expresarse como un axioma o un conjunto de axiomas. [13]
Turing agrega otra definición, Rosser equipara las tres : el artículo de Turing (1936-37) "Sobre los números computables y su aplicación al problema de resolución" apareció en poco tiempo. [18] En él, redefinió el concepto de "computabilidad efectiva" con la introducción de sus máquinas a (ahora conocidas como el modelo computacional abstracto de una máquina de Turing). Y en un bosquejo demostrativo agregado como "Apéndice" a su artículo de 1936-37, Turing mostró que las clases de funciones definidas por el cálculo λ y las máquinas de Turing son las mismas. [23] Church rápidamente se dio cuenta de lo convincente que era el análisis de Turing. En su revisión del trabajo de Turing, dejó en claro que la noción de Turing hacía que "la identificación con la eficiencia en el sentido habitual (no definido explícitamente) fuera inmediatamente obvia". [24]
Unos años más tarde (1939) Turing sugirió, como Church y Kleene habían hecho antes que él, que su definición formal de un agente computacional mecánico era correcta. [25] Así, en 1939 tanto Church (1934) como Turing (1939) habían propuesto individualmente que sus "sistemas formales" fueran definiciones de "computabilidad efectiva"; [26] en lugar de formular sus declaraciones como tesis .
Rosser (1939) identificó formalmente tres conceptos como definiciones:
"Las tres definiciones son equivalentes, por lo que no importa cuál se use".Kleene propone la tesis de Church : se deja aquí la expresión explícita "tesis" utilizada por Kleene. En su artículo de 1943 "Predicados y cuantificadores recursivos", Klin ofreció su "TESIS I":
"Este hecho heurístico [las funciones recursivas generales se calculan eficientemente]... llevó a Church a formular la siguiente tesis ( 22 ). La misma tesis está implícita en la descripción de las computadoras de Turing ( 23 ). "TESIS I. Toda función efectivamente computable (predicado efectivamente decidible) es generalmente [27] recursiva [cursiva Kleene] "Dado que sería deseable una definición matemática precisa del término, efectivamente computable (efectivamente decidible), podemos aceptar esta tesis... como la definición de este término..." [28] ( 22 ) referencia a la Iglesia 1936 ( 23 ) Enlace de Turing 1936-7Kleene señala además que:
“… la tesis tiene el carácter de una hipótesis, punto señalado por Post y Turing ( 24 ). Si consideramos una tesis y su inversa como una definición, entonces una conjetura es una conjetura sobre la aplicación de la teoría matemática derivada de esa definición. Hay, como hemos propuesto, motivos bastante convincentes para aceptar esta hipótesis”. [28] ( 24 ) Enlace a Post 1936 de Post and Church's Definiciones formales en la teoría de los números ordinales , Fondo. matemáticas _ vol 28 (1936) pp.11-21 (ver ref. #2, Davis 1965 :286).