Como exatamente o cálculo lambda captura a noção intuitiva de computabilidade?

Eu tenho tentado entender o que, por que e como do -calculus, mas não consigo entender o porquê "funciona"? $\lambda$

"Intuitivamente", obtenho o modelo de computabilidade da Turing Machines (TM). Mas essa distração me deixa confusa. $\lambda$

Vamos supor que as TMs não existem - então como alguém pode ser "intuitivamente" convencido sobre a capacidade do -calculus de capturar essa noção de computabilidade. Como ter um monte de funções para tudo e sua composobilidade implica computabilidade? O que estou perdendo aqui? Eu li o jornal de Alonzo Church sobre isso, mas ainda estou confuso e procurando um entendimento mais "entorpecido" do mesmo. $\lambda$

soft-question computability lambda-calculus ho.history-overview intuition Doutorado
fonte

Você tem o mesmo problema com a reescrita de sistemas e gramáticas? No cálculo lambda, as operações básicas são bastante simples: abstração de funções, aplicação de funções por substituição e cálculo é normalização beta. Em outras palavras, não vejo qual é o seu problema em ser um modelo razoável de computação.

Kaveh

Não vi ninguém duvidar que as funções definíveis do cálculo lambda sejam computáveis. Historicamente, a pergunta era se essas são as únicas funções intuitivamente computáveis, o que é uma questão completamente diferente do que você parece perguntar.

Kaveh

Uma coisa que eu achei útil foi o livro de Raymond M Smullyan, "Para Mock a Mockingbird", que substitui funções com pássaros em uma floresta mágica (e é uma boa leitura)

dspyz

Smullyans livro é sobre lógica combinatória

Trismegistos

Respostas:

Você está em boa companhia. Kurt Gödel criticou -calculus (bem como sua própria teoria das funções recursivas gerais) por não ser uma noção satisfatória de computabilidade com base em que ela não é intuitiva ou que não explica suficientemente o que está acontecendo. Por outro lado, ele achou a análise de computabilidade de Turing e a noção que se seguiu de máquina totalmente convincentes. Então não se preocupe. $\lambda$

Por outro lado, para ter uma idéia de como um modelo de computabilidade funciona, é melhor escrever alguns programas nele. Mas você não precisa fazê-lo em -calculus puro , embora seja divertido (da mesma maneira que a caminhada de fogo é). Você pode usar um descendente moderno de -calculus, como Haskell. $\lambda$ $\lambda$

Andrej Bauer
fonte

Se firewalking é tão divertido como você diz, então eu preciso tentar.

Radu GRIGore

Andrej, você conhece alguma referência para isso? Godel não aceitou o modelo de Chruch como capturando todas as funções comutáveis, mas não me lembro de ver em nenhum lugar que ele criticou o modelo muito mais do que isso. Suas críticas ao modelo de cálculo lambada de Church estavam em pé de igualdade com suas críticas a suas próprias funções recursivas gerais de Godel-Herbrand, até onde eu sei.

22415 Kaveh

Acho que você quer K. Godel: "Algumas observações sobre os resultados da indecidibilidade", em Solomon Feferman, John Dawson e Stephen Kleene (eds.), Kurt Gödel: Collected Works vol. Ii. Imprensa da Universidade de Oxford. 305-306 (1972). Veja books.google.si/…

Andrej Bauer

Você programa nele! Dê uma olhada nas codificações da igreja . Você pode ver como praticamente toda aritmética pode ser executada, o que provavelmente deve convencê-lo de que é extremamente poderosa. Eu gosto de ver as operações nas listas, no entanto. Você pode definir praticamente qualquer estrutura de dados em termos de uma função que executa a operação mais importante nela.

Por exemplo, uma codificação de uma lista é a função de dobra que se dobra sobre ela. Note que essa não é a codificação da Igreja, mas que recebi dos tipos e linguagens de programação de Percie. As codificações de pares da Igreja não nos dão recursão; temos que adicioná-lo de volta a nós mesmos com algum tipo de combinador de recursão.

portanto, uma lista leva dois argumentos, uma função para fazer a dobra e um valor inicial para encaixar na dobra em algum momento.

cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a

agora podemos definir um somatório com uma função add (veja as codificações da igreja acima)

sum xs = xs add 0

podemos fazer mais e definir uma função de mapa

consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil

se você ainda não está convencido de que há computação acontecendo aqui e deseja garantir que você possa executar qualquer computação, verifique o combinador de ponto fixo . Dói um pouco a cabeça pensar algumas vezes, no entanto, então não tenho certeza se chamaria de intuitivo, mas se você o avaliar manualmente com alguns argumentos, poderá ver o que está acontecendo.

Jake
fonte