Alonzo Church
Origem: Wikipédia, a enciclopédia livre.
Alonzo Church (14 de junho de 1903 - Washington, D.C.)
Foi um matemático norte americano que atuou principalmente nas áreas de lógica matemática, teoria de recurso e teoria da computação. Entre suas maiores contribuições, estão Cálculo Lambda, um sistema matemático formal que investiga funções, aplicação de funções. Influenciou as linguagens de programação, principalmente as linguagens funcionais, como o LISP (LISP 'puro' pode ser chamada de uma linguagem funcional verdadeira).
A tese de Church-Turing e etc.:
Partindo em busca do que seria um procedimento efetivo ou mecânico (o que pode ser feito seguindo-se diretamente um algoritmo ou conjunto de regras ), surgiram a sistematização e desenvolvimento das "funções recursivas". O cálculo-lambda (componente característico fundamental da linguagem de programação LISP) de Alonzo Church, tornou pública a possibilidade da definição bem elaborada de processo efetivo.
O teorema de Church §1 consiste fundamentalmente na demonstração de que não existe algoritmo capaz de enumerar as expressões não válidas, de maneira que fica excluído a priori todo procedimento de decisão para as expressões do "Cálculo de predicados".
Church também era interessado no problema de Hilbert (Entscheidungsproblem). Church tinha alcançado resultados, empregando o conceito de lambda-definibilidade (ao invés do computável por uma Máquina de Turing definido por Turing), mostrando assim que lambda-definibilidade é equivalente ao conceito de recursividade de Gödel-Herbrand. O cálculo-lambda, como sistema elaborado por Church para ajudar a fundamentar a Matemática era inconsistente, mas a parte do cálculo-lambda que tratava de funções recursivas estava correta e teve sucesso. Usando sua teoria, Church propôs uma formalização da noção de "efetivamente computável", através do conceito de lambda-definibilidade. Desta forma mostrou que o sistema de procedimentos de Turing eram equivalente à lambda-definibilidade. O trabalho de Church e Turing fundamentalmente liga os computadores com as Maquinas de Turing. Os limites das Maquinas de Turing, de acordo com a tese de Church-Turing, também descreve os limites de todos os computadores.
Como foi observado, a máquina de Turing pode ser interpretada como um algoritmo. Efetivamente toda ação de uma máquina algorítmica, como o computador pode ser considerada, se resume a calcular o valor de uma função §2 com determinados argumentos. Este fato é interessante, pois dá uma maneira de se medir a capacidade computacional de uma máquina. Uma máquina que compute mais funções que outra é mais poderosa. A partir dos resultados de Gödel, Turing e Church, pode-se dizer que existem funções para as quais não existe uma sequência de passos que determinem o seu valor, com base nos seus argumentos. Dizendo-se de outra maneira, "não existem algoritmos para a solução de determinadas funções". São as chamadas "funções não computáveis". Isto significa que para tais funções não há nem haverá capacidade computacional suficiente para resolvê-las. Logo, descobrir as fronteiras entre funções computáveis e não computáveis é equivalente a decobrir os limites do computador em geral. A tese de Church-Turing representa um importante passo nesse sentido. Eles perceberam que o poder computacional das Maquinas de Turing se resumia a qualquer processo algoritmico, ou seja, todas as funções computáveis que pudessem ser descritas por algoritmos. Isto foi a contribuição dada pelo trabalho de Turing e Church. As funções computáveis são as mesmas funções Turing-computáveis. A importância disso está na possibilidade de se verificar o alcance e limites de um computador.
§1 Um célebre teorema de Alonzo Church (1903-1995) demonstrou em 1936 que não pode existir um procedimento geral de decisão para todas as expressões do Cálculo de Predicados de 1a ordem, ainda que exista tal procedimento para classes especiais de expressões de tal cálculo.
§2 O processo que determina o valor de uma função através dos argumentos dessa função é chamado de cálculo da função (ou computar uma função).
