Alonzo Church: o arquiteto esquecido da inteligência computacional
(onepercentrule.substack.com)- Alonzo Church não é tão conhecido do grande público quanto Alan Turing, mas foi o lógico que estabeleceu a base lógica da computação com o λ-calculus e a teoria da computabilidade
- Em 1936, a tese de Church-Turing forneceu a estrutura segundo a qual funções efetivamente calculáveis podem ser computadas por uma máquina de Turing ou por um sistema equivalente
- Ao responder ao Entscheidungsproblem de Hilbert que não existe um algoritmo decisório capaz de determinar todas as proposições matemáticas, deixou claros os limites da computação
- Em Princeton, orientou Stephen Kleene, J. Barkley Rosser, Alan Turing e outros, e Turing concluiu seu Ph.D. sob sua orientação
- Seu trabalho abstrato permanece na linhagem da computação que chega aos compiladores modernos, interpretadores, programação funcional, aplicativos de smartphone e IA
Influência teórica maior que a fama popular
- Alan Turing é citado com mais frequência na história popular da computação e da inteligência artificial por causa do Teste de Turing, mas Church foi uma figura que influenciou profundamente o pensamento e o trabalho de Turing
- O trabalho de Church se tornou uma base importante para entender o que é computação e para formar os conceitos usados na avaliação da IA
- Sem as contribuições de Church, os conceitos atuais de inteligência artificial e de como avaliá-la talvez fossem bastante diferentes
Vida e perfil acadêmico
- Church foi um lógico quieto e de poucas palavras, nascido em 14 de junho de 1903 em Washington, D.C.
- Há registros de que, na infância, ficou cego de um olho ou perdeu parcialmente a visão devido a um acidente com arma de ar comprimido
- Depois de concluir uma preparatory school em Connecticut em 1920, iniciou seus estudos universitários em Princeton no mesmo ano e concluiu o doutorado em 1927
- Após passar um período em Harvard, Göttingen e Amsterdam como National Research Fellow, voltou a Princeton e construiu ali grande parte de sua produção acadêmica
- Era conhecido pela caligrafia impecável no quadro-negro e pelo temperamento meticuloso, chegando a cobrir artigos importantes com Duco cement para preservá-los
λ-calculus e computabilidade
- A contribuição mais profunda de Church foi o λ-calculus, que serviu de base para a área antes mesmo de existir o nome ciência da computação
- Em 1936, Church formulou a tese de Church-Turing, conceito central da ciência da computação teórica
- funções efetivamente calculáveis podem ser computadas por uma máquina de Turing ou por um sistema equivalente
- isso ofereceu uma estrutura para entender o que uma máquina pode fazer em teoria
- e também revelou os limites que procedimentos algorítmicos podem alcançar
- A tese é um conceito fundamental, mas ainda deixa debates e limites em torno da interpretação de ‘effective computability’, da computação física e da natureza da inteligência humana
- Se Turing propôs a máquina de Turing para traduzir procedimentos mecânicos em forma lógica, Church forneceu a abstração pura que dava sustentação teórica a esse tipo de máquina
Programação moderna e pensamento funcional
- A influência do λ-calculus aparece hoje nos princípios de escrita de programas, ligados à composição, funções de ordem superior e abordagens que enfatizam imutabilidade
- Esse sistema formal tornou possível codificar problemas matemáticos abstratos e resolvê-los mecanicamente, servindo de base para arquiteturas modernas de compiladores e interpretadores
- Para programadores atuais, o λ-calculus pode parecer um conjunto de funções aninhadas, como se vê em paradigmas de Lisp, Haskell e em partes de Python ou JavaScript
- A abstração do λ-calculus se tornou a base da programação funcional, na qual funções são tratadas como first-class citizens
Entscheidungsproblem e os limites da computação
- Church também fez contribuições importantes em outras áreas da lógica e da filosofia, e um caso representativo foi seu trabalho sobre o Entscheidungsproblem
- O Entscheidungsproblem era o problema da decisão proposto por David Hilbert em 1928, perguntando se existia um algoritmo decisório capaz de determinar a veracidade de qualquer proposição matemática
- Church deu uma resposta negativa, mostrando que tal algoritmo não existe, e esse resultado ficou conhecido como Teorema de Church
- A descoberta teve profundo impacto na teoria da decisão e destacou os limites daquilo que pode ser alcançado apenas por computação
O centro intelectual de Princeton e seus alunos
- Church foi um mentor de importantes lógicos e cientistas da computação de sua época
- Sua linhagem acadêmica inclui Stephen Kleene, J. Barkley Rosser e Alan Turing
- Turing concluiu seu Ph.D. em Princeton sob a orientação de Church
- Relata-se que David Kaplan recomendava aos novos pós-graduandos que assistissem às aulas de Church, dizendo que, mesmo fora de sua área de interesse, seria uma experiência para contar aos netos
- Nos anos 1930, Princeton foi um centro intelectual do desenvolvimento da lógica moderna, com John von Neumann, Kurt Gödel e Church
Um legado pouco visível
- Church não alcançou o mesmo nível de fama popular que Turing, von Neumann ou Gödel
- Seu legado não tinha uma forma que facilmente capturasse a imaginação popular, como histórias heroicas de criptoanálise em tempos de guerra ou a tragédia de uma morte precoce
- Os bilhões de programas executados em smartphones podem remontar sua lógica até as funções abstratas do λ-calculus
- De aplicativos simples à inteligência artificial, o DNA invisível da computação herda uma linhagem importante do trabalho de Church
- A genialidade de Church não estava no espetáculo, mas em estruturas rigorosas e em uma elegância silenciosa que mudaram o mundo
1 comentários
Comentários do Hacker News
Gostei da origem do nome lambda contada em Paradigms of Artificial Intelligence Programming (PDF/EPUB: https://github.com/norvig/paip-lisp)
A história diz que Alonzo Church pegou o acento circunflexo usado sobre variáveis ligadas na notação de Principia Mathematica de Russell e Whitehead,
x̂(x + x), e o moveu para a frente para adaptá-lo a uma string unidimensional, como em^x(x + x); como o circunflexo sozinho parecia estranho, ele o trocou por lambda maiúsculo,Λx(x + x), e depois por lambda minúsculo,λx(x + x), para evitar confusãoTambém diz que John McCarthy foi aluno de Church em Princeton e, ao criar o Lisp em 1958, usou
(lambda (x) (+ x x))porque os teclados de perfuração da época não tinham letras gregas, e isso permaneceu até hojePor isso, como o tema deste texto sugere, Church aparece com frequência em retrospectivas sobre Lisp e só pode ser uma figura “esquecida” para pessoas com quase nenhum interesse na história da computação
Segundo Dana Scott, o próprio Church disse que a escolha foi uma escolha arbitrária, no estilo “uni duni tê”, e ele também teria contestado a explicação ao estilo Barendregt numa palestra recente na University of Birmingham
Em francês, “personne lambda” significa uma pessoa comum ou anônima, então parece combinar bem com função anônima, e o adjetivo lambda também quer dizer “genérico/comum”, dando a sensação de que uma letra ali pelo meio do alfabeto grego representa algo mediano
https://math.stackexchange.com/questions/64468/why-is-lambda...
Ele cobre vários tópicos de programação e também abre portas para paradigmas que podem parecer estranhos a quem teve pouca exposição à programação funcional
Há outro caso em que Church parece sugerir que foi mais uma escolha arbitrária entre letras gregas do que uma escolha com significado específico em https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...
E também se isso foi antes ou depois de McCarthy começar o Lisp
“O cálculo lambda de Church e as máquinas de Turing têm poder computacional equivalente, mas as máquinas de Turing diferem por usarem estado mutável. A divisão que existe até hoje entre linguagens funcionais e imperativas se deve à separação entre Church e state”
Conheço essa citação há muito tempo, mas não consigo encontrar a fonte original
Edit: pode ter vindo de Guy Steele: “Há pessoas que não querem misturar a parte funcional/de cálculo lambda de uma linguagem com a parte que produz efeitos colaterais. Elas parecem acreditar na separação entre Church e state”
O arquivo original está aqui: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
A piada é que europeus em geral pronunciam corretamente o nome dele, algo como “Nick-louse Veert”, enquanto americanos o estragam transformando em “Nickel's Worth”
Ou seja, os europeus o chamam pelo nome, e os americanos o chamam pelo valor
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
Se quiser ler um texto realmente impressionante sobre Church, recomendo a memória de Rota
É a primeira seção de https://www34.homepage.villanova.edu/robert.jantzen/princeto...
Como links relacionados, há Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - agosto de 2016, e Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - fevereiro de 2015
O livro inteiro vale a leitura
A linguagem de programação Alonzo, batizada em sua homenagem, está quase esquecida
https://dl.acm.org/doi/pdf/10.1145/68127.68139
Em especial, a filosofia da lógica e a teoria de significado/referência que dão continuidade ao trabalho de Frege e Russell foram em grande parte esquecidas
Church publicou muitos artigos sobre esse tema, mas quase não é tratado em lugares como a Wikipedia
Ainda assim, o verbete da Stanford Encyclopedia of Philosophy é um pouco melhor: https://plato.stanford.edu/entries/church/
Mesmo assim, ouvi dizer que ele também deixa passar parte importante da obra dele, e imagino que fosse filosófico demais para matemáticos e técnico demais para filósofos
Não é o ponto principal, mas eu preferiria que evitassem usar ilustrações geradas por IA em posts de blog
Há até fotos reais de Church em domínio público, e essa ilustração nem se parece muito com ele, além de já estar aparecendo nos resultados de busca de imagens à medida que o texto ganha popularidade
Se é uma ilustração que nem vale mais de 5 minutos de geração, talvez fosse melhor simplesmente não colocar
Ainda assim, se fizerem questão de usar uma imagem gerada por “IA”, no mínimo isso deveria aparecer na legenda
Eu não estava muito inclinado a pegar uma foto online, e esta imagem foi o 7º resultado que fiz tentando evitar que virasse uma falsa semelhança; achei que ela tinha alguma semelhança
A imagem do JvN ficou bem boa, mas daqui para frente provavelmente faz mais sentido usar uma imagem simbólica em vez de uma falsa semelhança que pareça uma pessoa real
A expressão “arquiteto da inteligência computacional” parece exagerada
Church de fato foi um grande lógico, mas, se aqui inteligência computacional quer dizer AI/ML, então sua contribuição foi praticamente nula
Separadamente, nem sei bem se o cálculo lambda é matemática de verdade; parece mais uma notação engenhosa
As vantagens de uma notação são subjetivas, e também é interessante que Church não tenha demonstrado muito interesse pelo fato de suas ideias terem inspirado o design de certas linguagens de programação
A STT também é frequentemente identificada com a lógica de ordem superior, porque com os dois tipos primitivos de “indivíduo” e valores de verdade T/F, além apenas do tipo de função
(a --> b), é possível representar qualquer objeto lógico arbitrárioA STT é claramente uma invenção de Church, teve grande influência nas teorias de tipos modernas e também influenciou linguagens de programação com sistemas de tipos complexos, como Haskell
Não consigo provar isso por completo, mas intuitivamente parece que Turing e o que ele simboliza acabam sendo mais valorizados no lado da IA, enquanto Church parece o oposto
O primeiro partiu da pureza, das condições mínimas possíveis, da computação abstrata e “pura”, enquanto o segundo parecia mais interessado em como realmente podemos pensar e mais preocupado com a expansão da expressão e da abstração do que com implementação
Church não tinha experiência prática com computadores e estava mais voltado a expandir a própria teoria matemática
A colaboração entre os dois e a comunicação através do Atlântico consolidaram teorias centrais ao combinar prática e teoria, como a dualidade imperativo/funcional, o teorema de Church-Turing e a relação entre o problema da parada e o teorema de Church
Ver isso como rivalidade é um erro, e a ideia de que a ciência da computação tem “dois pais” faz sentido por vários motivos
Especialmente quando se leva em conta a morte de Turing
Também não se deve omitir que Turing não era indiferente à implementação: ele queria voltar à implementação real, mas não lhe foi permitido
Permanece a grande tragédia e a pergunta sobre o que teria mudado se o sigilo do governo britânico tivesse sido diferente, mas, se tivesse sido assim, talvez tivéssemos perdido, nesta nossa linha do tempo, a colaboração com Church que consolidou tão bem a teoria
Foi uma sorte ter podido encontrar Alonzo Church e Haskell Curry no ACM Symposium on LISP and Functional Programming realizado em agosto de 1982 na CMU
Curry claramente não estava bem de saúde e faleceu cerca de duas semanas depois da conferência, mas Church parecia saudável e viveu por mais uns 13 anos
Na recepção, Gerry Sussman estava visivelmente empolgado enquanto circulava pela sala apresentando os dois, e para nós também foi profundamente emocionante conhecê-los
Uma das grandes contribuições de Church foram seus alunos
Surgiu dali uma quantidade impressionante de pensadores