O que Idris não pode fazer renunciando à totalidade de Turing?

35

Eu sei que Idris tem tipos dependentes, mas não está completo. O que isso não pode fazer ao abrir mão da integridade de Turing, e isso está relacionado a ter tipos dependentes?

Acho que essa é uma pergunta bastante específica, mas não sei muito sobre tipos dependentes e sistemas de tipos relacionados.

Squidly
fonte
2
Eu acho que você está procurando um exemplo concreto? Não estou familiarizado com Idris, mas em Isabelle / HOL você não pode escrever (ou melhor, compilar) funções que nem sempre terminam (pior, você precisa fornecer uma prova de encerramento ).
Raphael
Algo nesse sentido sim - eu não tinha muita certeza se haveria algo bastante específico, como você não pode codificar um idioma com certas propriedades no sistema de tipos ou se seria um pouco mais geral (por exemplo, como você disse , todas as funções deve ser comprovada para terminar)
squidly
11
Acho que essa suposição equivocada vem de Edwin Brady dizendo que Idris é "Pacman complete". Eu acho que o ponto principal dele ao dizer "Pacman complete" em vez de "Turing complete" é que ele quer enfatizar a importância de as linguagens serem facilmente compiláveis ​​pelo cérebro humano e não apenas pelas máquinas! .. linguagens tolas como BrainFuck certamente são Turing completo, mas pode levar um cérebro humano um pouco para código comprehend escrito em BrainFuck, desenvolvendo assim, e ainda mais importante a manutenção , um programa de Pacman em BrainFuck leva um grande esforço ..
Michelrandahl
@ Mitzh Na verdade não. Eu acho que é porque eu entendi mal algo que o ouvi dizer em uma conversa.
squidly

Respostas:

50

Idris é Turing completo! Ele verifica a totalidade (término ao programar com dados, produtividade ao programar com codados), mas não exige que tudo seja total.

Curiosamente, ter dados e codados é suficiente para modelar a Completação de Turing, pois você pode escrever uma mônada para funções parciais. Eu fiz isso, anos atrás, no Coq - provavelmente já está com taxas de bits, mas aqui está: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

Você precisa de uma saída para executar essas coisas, mas Idris permite que você faça isso.

Idris não reduzirá funções parciais no nível de tipo, para manter a verificação de tipo decidível. Além disso, apenas programas totais podem razoavelmente ser considerados provas.

Edwin Brady
fonte
4
O próprio homem. O que é produtividade neste contexto?
Squidly
5
Dual à terminação: enquanto uma definição indutiva deve terminar (consumindo todos os seus dados), uma definição coindutiva deve ser produtiva - na prática, isso significa, breve, que qualquer chamada recursiva deve ser protegida por um construtor. Eu encontrei esta explicação para ser a mais clara (ymmv): adam.chlipala.net/cpdt/html/Coinductive.html
Edwin Brady
14

Primeiro, suponho que você já tenha ouvido falar da tese de Church-Turing , que afirma que qualquer coisa que chamamos de “computação” é algo que pode ser feito com uma máquina de Turing (ou qualquer um dos muitos outros modelos equivalentes). Portanto, uma linguagem completa de Turing é aquela em que qualquer cálculo pode ser expresso. Por outro lado, uma linguagem incompleta de Turing é aquela em que há algum cálculo que não pode ser expresso.

Ok, isso não foi muito informativo. Deixe-me dar um exemplo. Há uma coisa que você não pode fazer em qualquer linguagem incompleta de Turing: não é possível escrever um simulador de máquina de Turing (caso contrário, você pode codificar qualquer cálculo na máquina de Turing simulada).

Ok, isso ainda não foi muito informativo. a verdadeira questão é: que programa útil não pode ser escrito em um idioma incompleto de Turing? Bem, ninguém elaborou uma definição de "programa útil" que inclua todos os programas que alguém escreveu em algum lugar para uma finalidade útil, e que não inclua todos os cálculos das máquinas de Turing. Portanto, projetar uma linguagem incompleta de Turing na qual você possa escrever todos os programas úteis ainda é um objetivo de pesquisa a longo prazo.

Agora, existem vários tipos muito diferentes de idiomas incompletos em Turing, e eles diferem no que não podem fazer. No entanto, existe um tema comum: as linguagens completas de Turing devem incluir uma maneira de terminar condicionalmente ou continuar por um tempo que não seja limitado pelo tamanho do programa, e uma maneira de o programa usar uma quantidade de memória que depende da entrada . Concretamente, a maioria das linguagens de programação imperativas fornece essas habilidades através de loops while e alocação dinâmica de memória, respectivamente. A maioria das linguagens de programação funcionais fornece essas habilidades por meio de recursão e aninhamento de estrutura de dados.

Idris é fortemente inspirado pela Agda . Agda é uma linguagem projetada para provar teoremas . Agora, provar que teoremas e executar programas estão intimamente relacionados , portanto, você pode escrever programas no Agda da mesma maneira que prova um teorema. Intuitivamente, uma prova do teorema "A implica B" é uma função que pega uma prova do teorema A como argumento e retorna uma prova do teorema B.

Como o objetivo do sistema é provar teoremas, você não pode deixar o programador escrever funções arbitrárias. Imagine que o idioma permitiu que você escrevesse uma função recursiva boba que apenas se denominava:

oops : A -> B
oops x = oops x

Você não pode deixar a existência de uma função assim convencê-lo de que A implica B, ou então você seria capaz de provar qualquer coisa e não apenas verdadeiros teoremas! Portanto, a Agda (e provadores de teoremas semelhantes) proíbe a recursão arbitrária. Ao escrever uma função recursiva, você deve provar que ela sempre termina , de modo que sempre que executá-la em uma prova do teorema A você sabe que ela construirá uma prova do teorema B.

A limitação prática imediata da Agda é que você não pode escrever funções recursivas arbitrárias. Como o sistema deve ser capaz de rejeitar todas as funções que não terminam, a indecidibilidade do problema de parada (ou mais geralmente o teorema de Rice ) garante que também existam funções terminadas que também são rejeitadas. Uma dificuldade prática adicional é que você precisa ajudar o sistema a provar que sua função termina.

Há muita pesquisa em andamento para tornar os sistemas de prova mais parecidos com a linguagem de programação, sem comprometer a garantia de que, se você tem uma função de A a B, é tão boa quanto uma prova matemática de que A implica B. Estendendo o sistema para aceitar mais funções de encerramento é um dos tópicos de pesquisa. Outras instruções de extensão incluem lidar com preocupações do “mundo real” como entrada / saída e simultaneidade. Outro desafio é tornar esses sistemas acessíveis a meros mortais (ou talvez convencer os meros mortais de que eles são de fato acessíveis).

Eu não estou familiarizado com Idris. É uma visão dos desafios que acabei de mencionar. Tanto quanto eu entendo, de uma olhada superficial na pré-impressão de 2013 , Idris é Turing-completo, mas inclui um verificador de totalidade. O verificador de totalidade verifica se todas as funções anotadas com a palavra-chave totalterminam. O fragmento de linguagem que contém apenas os programas Idris, onde todas as funções são totais, é semelhante em poder expressivo ao Arda (provavelmente não uma correspondência exata devido a diferenças na teoria dos tipos, mas perto o suficiente para que você não notasse a menos que tentasse deliberadamente).

Para outros exemplos de idiomas que não são completos para o Turing de maneiras diferentes, consulte Quais são as limitações práticas de um idioma completo que não seja o turing como o Coq? (da qual essa resposta é amplamente retirada).

Gilles 'SO- parar de ser mau'
fonte
3
"que programa útil não pode ser escrito em um idioma incompleto de Turing?" Uma máquina virtual Java.
precisa saber é o seguinte
@DavidRicherby Você não pode? A JVM é realmente completa em Turing? Há um limite no tamanho de um objeto individual. Você pode alocar e acessar um número ilimitado de objetos? Por exemplo, em C, a resposta parece não ser, porque existem apenas finitos valores de ponteiro.
Gilles 'SO- stop be evil' (
Para os leitores interessados ​​nessa parte, temos outro post sobre por que não pode haver linguagem de programação para exatamente as linguagens sempre terminantes.
Raphael
3
@ Gilles Entendo o seu ponto, mas não é mais ou menos equivalente a dizer que nenhuma linguagem de programação real é Turing-completa? Afinal, qualquer implementação encontrará os tipos de barreiras que você menciona. Parece um elefante muito grande para se ter na sala, considerando o que Idris perde por não ser completo em Turing. Perde mais do que qualquer outro idioma, por exemplo? Se você proibir o armazenamento externo ilimitado (por exemplo, o programa parando para dizer "insira o disco seguinte / anterior"), qualquer idioma não será trivialmente completo para o Turing, portanto qualquer dúvida sobre esse caso será vazia.
precisa saber é o seguinte
3
@DavidRicherby Meus comentários (mas não a minha resposta) estão no modo geek da teoria da linguagem de programação. Se você seguir a especificação formal do SML (por exemplo), é possível projetar (mas é claro que não implementa no mundo físico) uma implementação da linguagem que possa simular todos os programas computáveis. Não é assim em C, porque a finitude da memória está embutida na linguagem ( sizeof(void*)). Na minha resposta, trato as linguagens de maneira idealizada, para que o SML ou C seja considerado completo em Turing.
Gilles 'SO- stop be evil'