A que corresponde a digitação em uma máquina de Turing?

8

Espero que minha pergunta faça sentido: começando com a premissa de que o não digitado λo cálculo é equivalente em potência a uma máquina de Turing; ao que em uma máquina de Turing corresponde a adição de tipos ao cálculo ? Existe algum tipo de autômato analógico para digitação, estático ou dinâmico?λ

turing-machines lambda-calculus type-theory church-turing-thesis BlueBomber
fonte
3
Eu recomendo que você desista da ideia simplista de que as TMs correspondem a -calculus. Isso é enganador. Pela tese de Church-Turing, você pode encontrar codificações entre todas as estruturas computacionais razoáveis. As TMs não correspondem mais ao -calculus do que ao jogo da vida de Conway ou aos sistemas semi-Thue, ou ao Prolog ou .... Podemos encontrar codificações entre todos esses sistemas. As codificações têm ou não propriedades (por exemplo, composicionalidade), e isso pode ou não ser uma coisa boa em uma aplicação específica. λλ
Martin Berger
11
Se é tão enganador, então as pessoas (especialmente os professores) não deveriam parar de enfatizar isso? Parece um resultado importante - de fato, fundamental - na ciência da computação, então por que as pessoas não deveriam procurar e esperar outras conexões entre os dois sistemas?
BlueBomber
@BlueBomber, é importante / fundamental por razões históricas: essas foram duas das formalizações propostas de computação propostas (junto com -recursion) em uma época em que não se sabia qual seria a maneira "correta" de formalizar a computação. . Portanto, a descoberta do fato de que cada um poderia simular o outro foi um grande negócio. No entanto, isso não significa necessariamente que eles tenham uma conexão mais especial do que quaisquer outras duas formalizações de computação. μ
usul

Respostas:

4

Não posso lhe dar uma resposta direta para autômatos, mas para funções em números.

O cálculo lambda não digitado corresponde a μfunções recursivas .

Para sistemas digitados, varia naturalmente para diferentes sistemas.

Um interessante é o Sistema F , também conhecido como cálculo lambda polimórfico. Existe um teorema que diz que

Uma função (em números naturais) é expressável no Sistema F se, e somente se, puder ser provado na aritmética Peano de segunda ordem que a função é total.

Isso significa que no Sistema F você pode expressar basicamente todas as funções totais imagináveis.

Existe um sistema um pouco mais fraco, o Sistema T de Gödel, para o qual existe um teorema muito semelhante para a aritmética Peano de primeira ordem. (No entanto, este sistema não é tão bom quanto o Sistema F. No Sistema F, você pode representar números naturais, booleanos etc. nativamente, enquanto o Sistema T é construído como o cálculo lambda de tipagem simples, com naturais e booleanos adicionados externamente. Também o Sistema F possui polimorfismo de tipo , o que o torna muito mais elegante em muitos casos.)

Veja também:

Petr Pudlák
fonte
2

Eu vou dizer que digitar não corresponde a nada para as Máquinas de Turing. Aqui está o meu raciocínio: digitar não tem a ver com computação, e a Turing Machines apenas modela as computações.

Na maioria das vezes, os tipos de um programa não afetam realmente como esse programa é executado. Em vez disso, são ferramentas em tempo de compilação que são usadas por um de dois motivos. Uma é fazer com que programas mal digitados não sejam compilados. Esta é uma operação puramente em tempo de compilação, que não afeta a maneira como a computação resultante é realizada.

O segundo é permitir que várias funções tenham o mesmo nome. Isso não está realmente afetando a computação subjacente, apenas nos permite escrever programas de uma maneira que é mais fácil de entender.

Tipos não são uma ferramenta de computação. Eles podem ser usados ​​para provas, para entender programas, para estruturá-los de maneiras que são mais fáceis de entender, mas sua presença não muda a maneira fundamental de executar a computação.

jmite
fonte