Una introducción a la Teoría de la Computabilidad desde una perspectiva de programación lógica

Abstract

El objetivo de este trabajo fue desarrollar un modelo de computabilidad basado en programación lógica pura. Se desarroló un modelo Turing-completo basado en este tipo de programación que nos permitió demostrar algunos resultados clásicos de la Teoría de la Computabilidad. Para ello se establecieron las distintas semánticas de los programas lógicos que se han tomado a lo largo de este trabajo. Se definió el concepto de función computable bajo esta nueva perspectiva y se demostró que se trata de un modelo de cómputo Turing-completo. Una vez probado esto, se desarrollaron resultados clásicos de la Teoría de la Computabilidad bajo esta nueva perspectiva. De este modo, se demostró la existencia de programa lógico universal desarrollando dicho programa y probando formalmente su corrección. Gracias a él fuimos capaces de demostrar la existencia de conjuntos no recursivos y no recursivamente enumerables en el ámbito de la programación lógica, que fue uno de los resultados clave de este trabajo. También se desarrollaron mediante técnicas de reducción numerosos ejemplos de conjuntos no recursivos. Finalmente, se demostraron algunos teoremas fundamentales de la Teoría clásica de la Computabilidad como son el Teorema de Rice, el Teorema s-m-n, el Teorema de Recursión y el Teorema del Punto Fijo. Se adaptó el enunciado de estos teoremas al modelo de computabilidad basado en programación lógica y se probaron bajo esta nueva perspectiva.

The goal of this project was to develop a computation model based on logic programming. We developed a Turing complete model based on this type of programs that allowed us to prove some of the classic results of Computability Theory. We established some different semantics for the logic programming and defined the concept of computable function under this new perspective. According to that definitions, we proved that this model of computation is Turing-complete. Once that had been proved, some important results of the Computability Theory were developed. In that way, the existence of a universal program for logic programming was proved by developing a universal program and formally proving its correctness. Because of it, we were able to prove the existence of non-recurssive and non-recursively enumerable sets under the logic programming paradigm, which was one of the most important results of this project. We used reductions in order to find more examples of non-recursive sets. Finally, we proved some important theorems of the Theory of Computability such as the Rice Theorem, the s-m-n Theorem, the Recursion Theorem and the Fixed Point Theorem. We adapted the statement of these theorems to our model of computation based on logic programming and proved them under this perspective