Alonzo Church
Mais informações
- Nascimento
- Morte
- Conhecido por
- Cálculo lambda, a tese de Church-Turing, o teorema de Church
- Nacionalidade
- Americano
Respondeu o problema da decisão de Hilbert poucos meses antes de Turing, usando uma ferramenta que se tornaria a ancestral das linguagens de programação.
Church era um matemático em Princeton que desenvolveu o cálculo lambda no início dos anos 1930: um sistema formal em que tudo é função e computar significa reescrever expressões. Na primavera de 1936, usou-o para mostrar que o Entscheidungsproblem não tem solução. Turing chegou à mesma resposta naquele ano com um modelo completamente diferente, tornou-se aluno de doutorado de Church entre 1936 e 1938, e os dois sistemas acabaram calculando exatamente as mesmas coisas — o que hoje chamamos de tese de Church-Turing.
O cálculo lambda não ficou preso à demonstração. Sua variante simplesmente tipada, de 1940, é a ancestral de todo sistema de tipos desde então, e LISP, ML, Haskell e as próprias expressões lambda que depois vazaram para C++, Java e Python descendem diretamente da notação de Church para funções anônimas.
Seu histórico de orientação talvez seja o legado maior: Turing, Kleene, Rosser, Dana Scott, Michael Rabin, Raymond Smullyan. Church era meticuloso a ponto de virar anedota — lavava o quadro-negro antes de escrever nele, mesmo já limpo — e fundou o Journal of Symbolic Logic em 1936, mantendo-o em ordem por quatro décadas.