Quais são os limites da programação funcional total?

19

Quais são as limitações da programação funcional total? Não está completo com Turing, mas ainda suporta um grande subconjunto dos programas possíveis. Existem construções importantes que você poderia escrever em uma linguagem completa de Turing, mas não em uma linguagem funcional total?

E é correto dizer que os programas escritos em linguagens funcionais totais podem ser completamente analisados ​​estaticamente, enquanto a análise estática em linguagens completas de Turing é limitada por coisas como o problema da parada? Com isso, não quero dizer que em linguagens funcionais totais tudo possa ser determinado estaticamente, porque algumas coisas são conhecidas apenas em tempo de execução, mas quero dizer que, em teoria, programas escritos em uma linguagem de programação funcional total ideal podem ser analisados ​​para que tudo o que poderia, em teoria, ser determinado estaticamente, pode ser determinado estaticamente. Ou ainda existem problemas indecidíveis herdados em linguagens funcionais totais que tornam a análise estática incompleta? Alguns problemas sempre serão indecidíveis, independentemente do idioma em que foram escritos, mas estou interessado em problemas que são herdados pelo idioma,

Matthijs Steen
fonte

Respostas:

16

Depende da linguagem funcional total .

Essa resposta soa como uma imitação, mas nada mais específico pode ser dito. Afinal, considere qualquer programa decidível importante em que esteja interessado. Escreva um programa em seu idioma completo completo de Turing para resolvê-lo. Como o problema é decidível, seu programa será interrompido em todas as entradas.

(Indiscutivelmente, um problema não-decidível pode ter programas interessantes, mas não é o que as pessoas podem usar, porque nunca poderão esperar o tempo suficiente para saber a resposta.)

Agora, defina um novo idioma para que ele tenha apenas um programa de entrada válido: o programa que você acabou de escrever, com a mesma semântica que tinha antes. É certamente total, já que todas as entradas para todos os programas nele escritos (dos quais há apenas um) sempre terminam.

Esse truque barato é realmente útil: a linguagem Coq , por exemplo, é uma linguagem funcional total, na qual nenhum programa verifica tipicamente, a menos que haja uma prova de que ele termina. (Se você renunciasse a esse requisito, ele seria concluído por Turing, portanto o único obstáculo é encontrar uma prova de rescisão.)

Não sei ao certo o que você quer dizer com "tudo o que em teoria pode ser determinado estaticamente pode ser determinado estaticamente"; parece tautologicamente verdadeiro. No entanto, o total de idiomas não é inerentemente fácil de analisar; você sabe que nada diverge, o que é um fato útil, mas a relação entre entrada e saída ainda é complexa. (Em particular, ainda existem infinitamente muitas entradas possíveis, portanto você não pode experimentá-las exaustivamente, mesmo em teoria.)

Paul Stansifer
fonte
Obrigado pela sua resposta. Portanto, ser total ajuda um pouco, mas continua sendo um problema muito difícil. O que eu quis dizer com "tudo o que em teoria pode ser determinado estaticamente pode ser determinado estaticamente" era que seria possível, extremamente difícil ou não, analisar todas as relações entre entrada e saída, se você tivesse recursos suficientes para fazê-lo . Ou são as razões fundamentais pelas quais isso é limitado? Como a teoria de Rice prova que este é o caso de funções parciais. Ou estou entendendo mal o teorema de Rice?
Matthijs Steen
Eu acho que pode depender do que você quer dizer com "relacionamento". Em particular, se você apenas quer dizer "a entrada A vai para a saída B", isso é trivialmente determinável em uma linguagem funcional total; basta executar o programa. Mas você provavelmente está interessado em análises que dizem algo sobre uma classe infinita de entradas.
Paul Stansifer
(opa; aperte enter acidentalmente) ... mas isso abre outro truque bobo, porque eu posso fazer perguntas indecidíveis sobre a função de identidade se eu quiser: "Para alguns X, é (identity X)uma máquina de Turing que pára?" Claro, isso não parece ser sobre identity , mas como você define "sobre"?
Paul Stansifer
Sim, quero saber se isso vale para todos os possíveis valores de entrada de alguma definição, não para entradas individuais. Então, se eu entendi direito, você quer dizer que sempre haverá perguntas indecidíveis, independentemente do tipo de linguagem de programação usada? Embora algumas dessas perguntas indecidíveis possam ser contornadas, impedindo que o problema ocorra em primeiro lugar, como linguagens funcionais totais para o Problema da Parada? Porque sua pergunta sobre a função de identidade não seria decidida em uma linguagem funcional total?
Matthijs Steen
Sim; uma versão modificada do problema, na qual "Máquina de Turing" é substituída por "Quebra após a garantia expirar na máquina de Turing" é trivialmente solucionável. É meio problemático para esses propósitos que o problema da interrupção seja o exemplo principal de um problema indecidível ao examinar programas, cheio de indecidibilidade.
Paul Stansifer
16

Quais são as limitações da programação funcional total? Não está completo com Turing, mas ainda suporta um grande subconjunto dos programas possíveis. Existem construções importantes que você poderia escrever em uma linguagem completa de Turing, mas não em uma linguagem funcional total?

LLL

  1. LLLLé consistente. É exatamente isso que o teorema de Goedel exclui, supondo que você possa fazer aritmética. Portanto, sabemos que não podemos escrever auto-intérpretes em linguagens funcionais totais.

  2. O outro lado disso, porém, é que os limites do poder expressivo da linguagem total são essencialmente os limites do poder expressivo da própria matemática . Por exemplo, as funções definíveis no Coq (um assistente de prova) são aquelas que podem ser comprovadas como computáveis ​​usando o ZFC, com muitos cardeais inacessíveis. Portanto, essencialmente qualquer função que você possa provar total para a satisfação de um matemático que trabalha é definível na Coq.

  3. O outro lado da outra parte é que a matemática é difícil! Portanto, não há nenhum senso fácil em que o total de idiomas é "completamente analisável" - mesmo que você saiba que uma função é encerrada, talvez seja necessário muito trabalho criativo para provar que ela possui uma propriedade que você deseja. Por exemplo, apenas saber que uma função de listas para listas é total, não leva muito longe em provar que é uma função de classificação ....

Neel Krishnaswami
fonte
Obrigado pela sua resposta. Eu li o post sobre esse problema no blog Lambda the Ultimate , mas algumas pessoas nos comentários afirmam que, embora não seja possível ter seu próprio avaliador como um termo explicitamente construtível regular, seria possível criar um trabalho auto- avaliador com alguns truques. Então, eu me pergunto: existem problemas que não podem ser resolvidos (ou aproximados) em uma linguagem funcional total com alguns truques de desvio?
Matthijs Steen
Eu diria que a auto-avaliação não conta como um problema, pois varia de acordo com o idioma. O problema "avaliar um programa na linguagem X" é o mesmo problema, independentemente de você tentar resolvê-lo na linguagem X ou Y. Em particular, se a linguagem X é uma linguagem funcional total, o problema é solucionável em alguma linguagem funcional total , usando o mesmo truque bobo que eu usei antes.
Paul Stansifer
Neel, parece que deveria ser consideravelmente mais fácil provar que um idioma total não pode suportar seu próprio intérprete. Estou te entendendo mal? Por uma diagonalização simples, qualquer idioma com uma função sem pontos fixos não pode suportar seu próprio intérprete (seja aritmético ou não). O argumento é elaborado por Conor McBride aqui: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html
Tom Ellis
@ TomEllis: Meu argumento é essencialmente o mesmo que o de Conor. De fato, seu post já faz essa observação (com o humor característico de Conor) quando ele a chama de "o argumento Epimenides / Cantor / Russell / Quine / Godel / Turing".
Neel Krishnaswami