Que funções o Sistema F não pode computar?

Em este artigo da Wikipedia sobre Turing completude afirma que:

O cálculo lambda não digitado é Turing completo, mas muitos cálculos lambda digitados, incluindo o Sistema F, não são. O valor dos sistemas digitados é baseado em sua capacidade de representar a maioria dos programas de computador típicos enquanto detecta mais erros.

Qual é um exemplo de uma função computável total que é incontestável pelo sistema F ?

Além disso, como hindley-milner é:

Uma restrição do Sistema F

devido ao facto de:

a verificação de tipo é indecidível para uma variante no estilo Curry do Sistema F, ou seja, que não possui anotações de digitação explícitas.

Isso significa que o cálculo lambda subjacente aos sistemas do tipo hindley-milner também não está completo?

Se isso for verdade, como o haskell está claramente completo e sabemos que sua base é o cálculo lambda e o sistema do tipo hindley-milner, que recursos que não estão presentes no cálculo lambda são adicionados para tornar o haskell completo?

O sistema é bastante expressivo. Conforme comprovado por Girard aqui , as funções do tipo (onde é definido como ) são exatamente as funções definíveis ( ) na segunda ordem Heyting Arithmetic . Observe que isso é o mesmo que as funções definíveis na aritmética Peano de segunda ordem .N → N N ∀ X . X → ( X → X ) → X N → N H A$F$$\mathbb{N}\rightarrow\mathbb{N}$$\mathbb{N}$$\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$$\mathbb{N}\rightarrow\mathbb{N}$$\mathrm{HA}_2$

Você provavelmente desejará verificar Provas e Tipos como uma referência mais legível. Observe que isso significa que muitos programas podem ser escritos no sistema F, da função Ackermann aos intérpretes do sistema Gödel . Como em qualquer linguagem de programação total (com algumas condições moderadas), o sistema não pode implementar um auto-intérprete , ou seja, uma função que usa como entrada um código para um termo do sistema e retorna um (código para a) forma normal paraF e v a l : N → N t F $T$$F$$\mathrm{eval}:\mathbb{N}\rightarrow\mathbb{N}$$t$$F$$t$. A prova envolve uma variante do truque de diagonalização usado para indecidibilidade do problema de parada. Andrej explica lindamente aqui .

Para responder a outras perguntas: O -calculus subjacente aos idiomas Hindley-Milner (HM) também não está completo em Turing. De fato, é significativamente mais fraco que o sistema , mais próximo em expressividade do -calculus simplesmente digitado .F $\lambda$$F$ $\lambda$

Haskell é realmente Turing completo. O recurso mais distintivo que permite isso (embora existam outros) é a presença de recursão irrestrita : a definição de qualquer programa (função) pode se referir ao próprio programa. Isso é semelhante à adição de um combinador , como é feito na definição de PCF que é de tipo simples, mas retém a completude de Turing com o combinador$Y$$Y$

Observe que existem outros recursos que tornam o Haskell Turing completo, mas geralmente não são considerados parte da linguagem principal, por exemplo, referências a funções, tipos de dados irrestritos etc.

É um pouco enganador dizer que o sistema de digitação de Haskell é "o sistema do tipo hinley-milner". Os tipos de Haskell são muito mais poderosos, incluindo, entre outros, tipos de classe superior. De fato, o sistema de digitação é tão poderoso que você pode incorporar linguagens de programação completas do Turing no sistema de digitação, veja aqui . Esta não é a única razão para o poder de Haskell, Cody mencionou alguns outros.