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,
fonte
X
, é(identity X)
uma máquina de Turing que pára?" Claro, isso não parece ser sobreidentity
, mas como você define "sobre"?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.
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 ....
fonte