Teoria da realizabilidade: diferença de potência entre o cálculo Lambda e as máquinas de Turing

48

Eu tenho três subquestões relacionadas, destacadas pelos pontos abaixo (não, eles não podem ser divididos, se você estiver se perguntando). Andrej Bauer escreveu, aqui , que algumas funções são realizáveis ​​através de uma máquina de Turing, mas não através do cálculo lambda. Um passo fundamental de seu raciocínio é:

Entretanto, se usarmos o cálculo lambda, então [o programa] c deve calcular um numeral representando uma máquina de Turing a partir de um termo lambda representando uma função f. Isso não pode ser feito (posso explicar por que, se você fizer isso como uma pergunta separada).

  • Eu gostaria de ver uma explicação / prova informal.

Não vejo como aplicar o teorema de Rice aqui; isso se aplicaria ao problema "essa máquina de turing T e esse termo lambda em L equivalente?", porque a aplicação desse predicado em termos equivalentes gera o mesmo resultado. No entanto, a função necessária pode calcular TMs diferentes, mas equivalentes, para termos lambda diferentes, mas equivalentes.

  • Além disso, se o problema é com a introspecção de um termo lambda, acho que passar uma codificação de Gödel de um termo lambda também seria aceitável, não seria?

Por um lado, dado que seu exemplo envolve calcular, no cálculo lambda, o número de etapas necessárias para uma máquina de Turing para concluir uma determinada tarefa, não estou muito surpreso.

  • Mas como aqui o cálculo lambda não pode resolver um problema relacionado à máquina de Turing, pergunto-me se é possível definir um problema semelhante para o cálculo lambda e provar que ele é insolúvel em máquinas de Turing, ou se há realmente uma diferença de poder em favor de Máquinas de Turing (o que me surpreenderia).
Blaisorblade
fonte

Respostas:

56

John Longley tem um artigo de pesquisa muito extenso discutindo as questões envolvidas, "Noções de Computabilidade em Tipo Superior" .

A idéia básica é que a tese de Church-Turing é apenas sobre funções de - e há muito mais em computação do que isso! Em particular, quando escrevemos programas, usamos funções de tipo superior (como ).NN(NN)N

Para definir completamente um modelo de computação de tipo superior, precisamos especificar a convenção de chamada para funções, a fim de permitir que uma função chame outra função que recebe como argumento. No cálculo lambda, a convenção de chamada padrão é que representamos funções por termos lambda, e a única coisa que você pode fazer com um lambda no cálculo lambda é aplicá-lo. Em codificações típicas com máquinas de Turing, passamos funções como argumentos, fixando uma codificação Godel específica e, em seguida, strings representando o índice da máquina que você deseja transmitir como argumento.

A diferença na codificação significa que você pode analisar a sintaxe do argumento com uma codificação no estilo da TM e não pode com uma representação padrão do cálculo lambda. Portanto, se você receber um termo lambda para uma função do tipo , poderá testar apenas seu comportamento passando específicos - você não pode analisar a estrutura do termo de qualquer forma. Essas informações não são suficientes para descobrir o código do termo lambda.NNn

Uma coisa que vale a pena notar é que, com tipos mais altos, se uma linguagem é menos expressiva em uma ordem, é mais expressiva uma ordem acima, porque as funções são contrárias. Da mesma forma, existem funções que você pode escrever no LC que não pode com uma codificação no estilo TM (porque elas dependem do fato de que você pode transmitir argumentos funcionais e sabe que o receptor não pode olhar dentro da função que você atribui) .

EDIT: Aqui está um exemplo de uma função definível no PCF, mas não nas codificações TM + Goedel. Vou declarar a isAlwaysTruefunção

 isAlwaysTrue : ((unit → bool) → bool) → bool

que deve retornar true se o argumento ignorá-lo e sempre retornar true, deve retornar false se o argumento retornar false em qualquer entrada e entra em loop se o argumento entra em loop em qualquer entrada. Podemos definir essa função facilmente, da seguinte maneira:

isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

onde é a computação em loop e é o operador e nos booleanos. Isso funciona porque há apenas três habitantes unit → boolno PCF e, portanto, podemos enumerá-los exaustivamente. No entanto, em um modelo de estilo de codificação TM + Goedel, ppoderia testar quanto tempo seu argumento leva para retornar uma resposta e retornar respostas diferentes com base nisso. Portanto, a implementação das isAlwaysTrueTMs falharia em atender às especificações.

Neel Krishnaswami
fonte
11
Esta é uma excelente pesquisa. Obrigado pelo link !
Suresh Venkat
Acabei de perceber que tinha esquecido de aceitar uma resposta, embora pretendesse aceitar a sua. Desculpa!
Bluesorblade 5/10
“A diferença na codificação significa que você pode analisar a sintaxe do argumento com uma codificação no estilo TM e não com uma representação padrão do cálculo lambda.”: Mas se você tiver representações para a composição da função? Além disso, o que você diz parece sugerir que a HOL é mais do que uma teoria de um cálculo lambda digitado, é mais do que isso?
Hibou57
Além disso, o que acontece com isso: cs.virginia.edu/~evans/cs150/classes/class39/lecture39.pdf . Isso está errado de alguma forma?
precisa
Caro Neel, você tem um exemplo para uma função que pode ser realizada no modelo de cálculo lambda, mas não no modelo de Turing?
Ingo Blechschmidt
29

O que Neel disse, e também o seguinte.

Eu gostaria de enfatizar ( de novo , de novo e de novo ) que a representação de assuntos de entrada e saída. Se for permitido alterar representações, podemos obter praticamente qualquer coisa (por exemplo, tornar qualquer função computável). Portanto, passar de uma representação das funções por -terms para uma representação pelos números de Gödel não é aceitável se nosso modelo de computação for -calculus (porque, então, a operação de currying torna-se incontestável por -calculus).NNλλλ

Uma declaração que é realizável no modelo -term, mas não no modelo da máquina de Turing é "nem todas as funções têm um código Gödel", o que é meio bobo. Vou tentar encontrar uma melhor e editar esta resposta.λNN


Editar em 07-10-2013: Aqui está o que eu quis dizer com "currying torna-se incontestável". Suponha que usemos o -calculus sem tipo como nosso modelo computacional, mas depois decidimos que devemos representar os mapas com códigos Gödel (de máquinas de Turing, codificadas como números de Igreja). Parece inofensivo, certo? Afinal, acreditamos no mantra "Máquinas de Turing e cálculo são equivalentes".λNNλ

Bem, para que essa nova representação seja realmente uma representação válida de , precisamos também realizar aplicação e currying (porque "representar funções" significa a mesma coisa que "representar um objeto exponencial "). Especificamente, é necessário um -termo de tal modo que, sempre que o numeral Church representa , em seguida, é representado por . (Aqui escrevo para o número da Igreja que representa o número .) TalNNλappn¯f:NNf(k)appn¯k¯n¯nappestá prontamente disponível porque equivale a um intérprete para máquinas de Turing, implementado no -calculus.λ

Mas e o curry? Para isso, precisamos do seguinte. Suponha que é um conjunto representado. Dado qualquer mapa calculado por um -term , precisamos mostrar que a transposição também é calculado por alguns -term . Mas considere o exemplo em que é o conjunto de fmaps representado por -terms é a aplicação. Então seria um mapa que atua como identidade emf : X × NN λ t ˜ f : X ( NN ) λ s X NN λ f ˜ f NN λ λ NN λXf:X×NNλtf~:X(NN)λsXNNλff~NN, mas seu realizador é um -term que converte -terms representando maps nos códigos Gödel correspondentes. Esse termo não existe (por exemplo, porque seria descontínuo em um modelo semântico topológico).λλNNλ

Você pode tentar objetar que eu não deveria ter usado o conjunto representado específico dos mapas representado por -terms, porque "concordamos" que esses sejam representados pelos códigos de Gödel . Mas você estaria errado. Antes de tudo, eu poderia ter usado um diferente com uma prova mais complicada que escaparia de você, mas continuaria obtendo o mesmo resultado. Segundo, está lá na categoria e a definição de exponencial exige que o curry trabalhe com relação a todos os objetos. Você tem que respeitar a categoria. Você não pode simplesmente matá-lo aleatoriamente e tirar alguns objetos (bem, você pode, mas depois é um açougueiro).NN X X XXNNλXX

Andrej Bauer
fonte
2
ainda à espera de que o melhor exemplo ...
Jacques Carette
11
Bem, posso pensar em muitas afirmações que são realizáveis ​​com máquinas de Turing, mas não com termos . Suponho que você queira o contrário. Hummm. λ
Andrej Bauer
Não entendo como o curry pode se tornar incomputável. Você deve poder reutilizar o teorema smn, pois sua prova constrói uma função em dados de primeira ordem (naturais). Pela tese de Church-Turing, esse comportamento sobre os naturais pode ser implementado como um termo lambda (que usa funções nativas internamente, mas não vejo como isso é proibido). Da mesma forma, pode-se provar o teorema do utm; portanto, de acordo com o seu post , devemos concluir. o que estou perdendo?
Blaisorblade
11
Expliquei na resposta o que significa que o curry se torna incontestável, a saber, que o objeto sugerido não é um exponencial na categoria de conjuntos representados.
Andrej Bauer
Obrigada pelo esclarecimento! Infelizmente não posso votar novamente. Eu posso acompanhar a maioria dos detalhes técnicos; Não estou familiarizado com modelos topológicos, mas estou familiarizado com "você não pode inspecionar funções em programação funcional / cálculo-λ". Seu último parágrafo também explica por que não posso passar pelo smn, porque o curry fornecido pelo smn produz os códigos de Gödel novamente, e não as funções padrão necessárias. Vou meditar sobre esse parágrafo.
Bluesorblade #