Apresentação da demonstração da equivalência entre Computabilidade e Lambda-Definibilidade: um estudo do trabalho de alan turing

Abstract

Os conceitos que definem uma máquina de Turing, modelo teórico proposto por Alan Turing em 1937, servem de base para a computação em geral. Tais máquinas foram concebidas para solucionar um problema de decisão vigente na época: dado um algoritmo com um conjunto de axiomas e uma proposição matemática, ele é capaz de decidir que a proposição é ou não é provável pelos axiomas? Pararelo ao trabalho de Turing, Alonzo Church propôs outra solução ao problema, com o uso do Cálculo Lambda.

Turing adicionou um apêndice no seu trabalho descrevendo um pouco sobre a equivalência dos dois modelos teóricos e, mais tarde, escreveu outra publicação que apresentaria com mais detalhes a prova. Nesta publicação, Turing demonstra uma máquina que é capaz de computar Cálculo Lambda.

O objetivo deste trabalho é investigar a publicação de Turing sobre a equivalência de Cálculo Lambda e Máquinas de Turing, além de estudar os conceitos fundamentais e das motivações de ambos os modelos. É notório que os dois são capazes de computar a mesma classe de problemas, mas, a despeito de ambos os modelos serem vistos ao longo do curso, a demonstração da equivalência não é abordada.

The concepts that defines a Turing Machine, theoretical model proposed by Alan Turing in 1937, provides the basis for computing in general. These machines was conceived to solve a decision problem at the time: given an algorithm with a set of axioms and a mathematical setence, it is able to decide wheter or not the sentence is provable by the axioms? Parallel to Turing's work, Alonzo Church proposed another solution to the problem, with the use of Lambda Calculus.

Turing added an appendix on his work describing about the equivalence of the two theoretical models and, later, he wrote another publication that would present with more details the proof. In this publication, Turing demonstrates a machine that is capable of compute Lambda Calculus.

This work intends to investigate the Turing's publication about the equivalence between Lambda Calculus and Turing Machines, in addition to studying the fundamental concepts and motivation of both models It is notorious that both models are capable to compute the same class of problems, but, despite of both models being seen along the course, the demonstration of equivalence isn't addressed.