La tesis de Church-Turing/Evolución Histórica
Introducción
[editar]En el año 1928 Hilbert y Ackermann publican un libro sobre la lógica de primer orden, proporcionando un conjunto de reglas para la realización de las deducciones lógicas. Demostraron además como la lógica de primer orden formalizaba parte de las matemáticas.
Uno de los mayores problemas de Hilbert y Ackermann era determinar si su inferencia era válida utilizando un algoritmo. Consistía en encontrar un algoritmo que validase la conclusión obtenida utilizando las reglas de Hilbert-Ackermann.
El principal problema de la lógica matemática recibe el nombre del "problema decisorio", ya que si se encuentra un algoritmo que determine si una inferencia es válida o no, esto permitiría resolver cualquier problema matemático utilizando simplemente la lógica de primer orden.
La siguiente ilustración muestra la evolución histórica de la teoría de la computabilidad:
Comentario acerca del Procedimiento Decisorio
[editar]El procedimiento decisorio para un concepto es viable o soluble, si se puede encontrar un algoritmo computacional que, al aplicarlo a un objeto cualquiera en un número finito de pasos, nos permita clasificarlo como ejemplo o contraejemplo de tal concepto.
Si nos encontramos en el caso de que para un mismo concepto existen tanto pruebas positivas como negativas, se dice que dicho problema es soluble, de modo que para cualquier entrada al procedimiento computacional podemos clasificarlo como positivo o negativo.
Los conceptos en los que más nos vamos a centrar son la validez y la satisfacibilidad, mientras que los objetos de entrada van a constituir la notación de la lógica de primer orden.
Entscheidungsproblem
[editar]En 1928 durante un congreso internacional D. Hilbert planteó las siguientes cuestiones:
- ¿Las matemáticas son 'completas', esto es, cada afirmación matemática se puede probar?
- ¿Las matemáticas son 'consistentes', esto es, es posible probar paralelamente una afirmación y su negación?
- ¿Las matemáticas son 'decidibles', esto es, se puede encontrar un método definido aplicable a cualquier afirmación matemática, que nos de cómo resultado si es o no cierta la aseveración evaluada?
La intención de Hilbert era conseguir un modelo matemático formal, completo y consistente, en el que a través de un algoritmo, se pudiese determinar la veracidad o falsedad de cualquier proposición formal. Este problema recibió el nombre de “Entscheidungsproblem”, resolverlo significaría que para cualquier problema bien definido existiría un algoritmo capaz de resolverlo.
Teorema de la Incompletitud
[editar]En 1930 algunos investigadores determinan que es imposible resolver el problema de Hilbert. En el año 1931, Gödel publica el Teorema de la Incompletitud que demuestra que es imposible resolver el sistema propuesto por Hilbert en 1928.
"Todo sistema de primer orden consistente que contenga los teoremas de la aritmética, cuyo conjunto de axiomas sea recursivo no es completo"
La idea genial de la demostración de Gödel se basa en la construcción de una técnica que puede ser comprobada por cualquier sistema descrito, pero no por el propio sistema.
Debido a este problema no es posible construir un sistema formal, en la lógica de primer grado, como pretendía Hilbert, a no ser que se tomase un conjunto no recursivo de axiomas.
Seleccionar un conjunto no recursivo de axiomas supone un gran problema puesto que se desconoce la manera de verificar si una fórmula es o no un axioma y por tanto si una fórmula podemos tratarla o no como un axioma, o lo que es lo mismo, si una demostración es o no válida.
Se podría pensar en sistemas inductivos más potentes que la lógica de predicados de primer orden. Una versión posterior del Teorema de Incompletitud de Gödel lo descarta:
"Ningún sistema deductivo que contenga los teoremas de la aritmética, y con los axiomas recursivamente enumerables puede ser consistente y completo a la vez." (Generalización del Teorema de completitud de Gödel).
Esta afirmación nos indica que resulta imposible encontrar un sistema formal completo y consistente para realizar afirmaciones matemáticas. Trabajos posteriores reafirmaron esta posibilidad.
El aspecto más relevante en el Teorema de Incompletitud de Gödel, tiene su irmportancia al dar origen a Teoría de la Computabilidad. Los pasos seguidos son:
- Se indica un número, numeración de Gödel, mediante el cual se asigna un entero positivo, que es un código a cada fórmula bien formada del sistema (fbf). El lector puede pensar en programa si lo desea.
- Una sucesión finita de fórmulas bien formadas de modo que la fbf o sucesiones finitas de fbfs se recuperen fácilmente a partir del número de código. Gracias a este código los enunciados referentes a valores de enteros positivos pueden considerarse como enunciados referentes a números de expresiones, o incluso a las propias expresiones.
Esta última idea fue utilizada a posteriori para codificar algoritmos con enteros positivos y, de esta forma poder lograr un algoritmo cuyas entradas fuesen enteros positivos y extenderlo a algoritmos cuyas entradas fuesen otros algoritmos.
Tarski fue también un personaje importante que colaboró siempre en esta misma línea, llegando formalmente a conclusiones como que la verdad o veracidad de un sistema aritmético sólo podría ser probado fuera de él.
Calculabilidad efectiva
[editar]En 1936, surgen de un modo casi simultáneo varios modelos distintos del concepto de calculabilidad efectiva. Corresponden a los trabajos de Kleene, Church, Turing y Post. Tanto Kleene como Post trabajaban sobre problemas que eran indecibles mientras que, Church y Turing, además demostraron que el "Entscheidungsproblem" era un problema indecidible.
Church propone como definición de función efectivamente calculable la función-definible. Empleó la notación del "cálculo lambda" para poder expresar de un modo estándar cualquier fórmula matemática. Su origen es de 1923-1933 Church lo introdujo para fundamentar las matemáticas.
Gracias a ello, los teoremas pueden expresarse como la transformación de cadenas de símbolos en otras, usando un conjunto de reglas formales en cálculo lambda.
Años más tarde se demostró que este sistema resultaba inconsistente. La posibilidad de expresar mediante elementos o términos del sistema las funciones numéricas resultó una idea muy atractiva tanto para Church como para sus colaboradores. Church define una función "efectivamente calculable" como función-definible en 1934.
Durante el transcurso de ese mismo año, Gödel había seguido estudiando la idea de Herbrand de que una función podía definirse como un conjunto de ecuaciones entre términos, incluyendo tanto a la misma función así como una serie de símbolos para funciones previamente definidas. Gödel dio forma a esta idea determinando que cada valor de la función f tenía que obtenerse sustituyendo en las ecuaciones las variables por números y, los términos sin variables, por valores que ya se habían probado que designaban. Permitiendo definir la clase de "las funciones recursivas de Herbrand-Gödel".
Enunciado de la tesis de Church
[editar]En 1936, Church logra demostrar que tanto las funciones-definibles como las funciones recursivas de Herbrand-Gödel son equivalentes. Conjetura que este tipo de funciones son las únicas funciones calculables utilizando, para ello, un algoritmo a través de la tesis que lleva su nombre:
"La clase de las funciones que pueden ser calculadas mediante un algoritmo coincide con la clase de las funciones recursivas." (Tesis de Church).
Apoyado en esta tesis junto a la definición de función definible, encontró varios ejemplos de problemas cuya resolución era irresoluble llegando a manifestar que el ‘Entscheidungsproblem’ era uno de estos problemas.
Meses más tarde Kleene llegó a la misma conclusión que Church pero sus ejemplos de problemas irresolubles tenían su base en el concepto de función recursiva.
Enunciado de la tesis de Turing
[editar]La tercera de las definiciones de función calculable tiene su origen en el matemático inglés Alan Turing, que fue durante un tiempo alumno de Von Neumann, y que leyó los argumentos de Hilbert durante sus estudios en Cambridge. En 1936 Turing publicó uno de sus trabajos más importantes: "Números Computables: Una Aplicación al Entscheidumgsproblem".
El objetivo de Turing era el de enfrentarse al problema planteado por Hilbert (el Entscheidumgsproblem) utilizando para ello el concepto abstracto de una máquina, una máquina teórica. El motivo de este acercamiento a la realidad era el de simplificar los cálculos al máximo, describiendo una serie de procedimientos básicos, a los que puede reducirse cualquier otro.
Turing describía en su artículo que a través de su máquina había conseguido caracterizar de un modo matemático el número de funciones calculables, usando para ello un algoritmo, este hecho se conoce como:
La clase de las funciones que pueden ser calculadas mediante un método definido coincide con la clase de las funciones calculables mediante una Máquina de Turing (Tesis de Turing).
Turing expuso su tesis como un teorema demostrado, utilizando su concepto de máquina teórica, logro demostrar que existen funciones que no son calculables o resolubles por un método definido y en concreto que el ‘Entscheidungsproblem’ era uno de estos problemas.
Cuando Turing elaboró su artículo, desconocía los trabajos sobre las funciones definibles y calculables de los trabajos de Church-Kleene, así que cuando tuvo noticias de los mismos, los incluyó en su apéndice en el que demostraba usando su máquina que los conceptos de función-definible y función-calculable, eran equivalentes.
Por este motivo tanto la tesis de Turing como la de Church son similares, al fin vienen a decir lo mismo, y se fusionan: La tesis de Turing afirma que el conjunto de las funciones computables coincide con el número de las funciones que puede calcular la máquina de Turing. Ambas tesis Turing y Church, son equivalentes. Por eso nos referimos a ambas tesis como tesis de Church-Turing.
Por supuesto para llegar a esta conclusión es necesario previamente obtener una definición de función computable. Surgieron otras definiciones de funciones computables que resultaron ser equivalentes a la de Turing, entre ellas destaca la teoría de funciones recursivas y el cálculo lambda desarrollado por Church entre los años 1932 y 1941. Su objetivo era el de captar el aspecto computacional de las funciones. No usaba la definición tradicional de pares dato-resultado, su interés se centraba en la transformación desde el dato de partida hasta el resultado.
Desde un punto de vista sencillo el cálculo lambda consiste en una gramática de términos y unas reglas de transformación entre los mismos, representando estas funciones. La característica más importante del cálculo lambda consiste en que una gramática puede aplicarse a sí misma, se pueden definir funciones recursivas sin usar tener que usar recursividad.
A pesar de lo que pueda parecer en un principio no surge ningún tipo de paradojas o inconsistencias. La tesis de Church-Turing consiste en afirmar que las funciones computables son aquellas que pueden ser expresadas a través del cálculo lambda. Turing logró la equivalencia entre su máquina teórica y este cálculo en 1937.
A raíz de las máquinas de Turing ha surgido una rama en la informática teórica con el nombre de 'Teoría de la Computabilidad'. Mientras que el cálculo lambda supone la base teórica del paradigma de programación funcional.
El trabajo de Post era el delimitar una frontera entre los procedimientos formales y el entendimiento para desarrollar las matemáticas. Post utiliza los sistemas deductivos normales para crear un modelo de procedimientos efectivo.
Permiten deducir sucesiones finitas de símbolos como consecuencia de otras sucesiones de símbolos finitas, utilizando un conjunto de reglas y axiomas. Post señaló en su artículo, que en estos sistemas se podrían encontrar situaciones de indecibilidad e incompletitud.
Post desconocía el trabajo realizado por Turing, aunque conocía el trabajo de Church-Kleene. Esto es patente en el hecho de que el modelo procedimental efectivo que definió Post es diferente del de Turing.
Progresos de Kleene
[editar]En 1938, Kleene fue el primero que se dio cuenta de que había funciones parciales originadas por algoritmos que nunca finalizaban, a partir de ellos se pueden obtener todos los resultados anteriores. El estudio de funciones parcialmente calculables ha sido esencial para el posterior desarrollo de ésta materia. Estos estudios son fundamentales para la demostración del teorema del punto fijo y el teorema de recursión de Kleene de 1952.
Posteriormente se demostró que tanto lo que podía calcular un sistema formal como una máquina de Turing eran equivalentes:
En los sistemas deductivos donde el conjunto de reglas de producción, y el conjunto de axiomas sea recursivamente enumerable, una función(parcial) aritmética es 'calculable' si y solo si es una función (parcial) 'recursiva'.
El primer paso en la teoría computacional
[editar]La tesis de Church-Turing es considerada como el primer axioma en la teoría de la computación, permitiendo comenzar a estudiar los problemas resolubles mediante un algoritmo.