Explicação simples de por que certas funções computáveis ​​não podem ser representadas por um termo digitado?

Lendo o artigo Uma Introdução ao Cálculo Lambda , me deparei com um parágrafo que eu realmente não entendia, na página 34 (em itálico):

Dentro de cada um dos dois paradigmas, existem várias versões do cálculo lambda digitado. Em muitos sistemas importantes, especialmente nos da Igreja, os termos que possuem um tipo sempre possuem uma forma normal. Pela insolubilidade do problema de parada, isso implica que nem todas as funções computáveis ​​podem ser representadas por um termo digitado, ver Barendregt (1990), Teorema 4.2.15. Isso não é tão ruim quanto parece, porque, para encontrar funções computáveis ​​que não podem ser representadas, é preciso ficar de pé. Por exemplo, em 2, o cálculo lambda digitado de segunda ordem, apenas as funções recursivas parciais não podem ser representadas que são totais, mas não provadamente na análise matemática (aritmética de segunda ordem).

Estou familiarizado com a maioria desses conceitos, mas não com o conceito de função recursiva parcial, nem com o conceito de função comprovadamente total. No entanto, não é isso que estou interessado em aprender.

Estou procurando uma explicação simples sobre por que certas funções computáveis ​​não podem ser representadas por um termo digitado, bem como por que essas funções só podem ser encontradas "estando de pé na cabeça".

Dado que você não deseja aprender conceitos precisos, aqui está uma explicação intuitiva. Na discussão abaixo, "função" sempre se refere a uma função que mapeia números naturais para números naturais (possivelmente indefinido em alguns argumentos).

Qualquer linguagem de programação que tenha

1. sintaxe computável e regras de avaliação, e
2. implementa todas as funções computáveis totais

necessariamente implementa algumas funções parciais .

Para ver isso, suponha que todas as funções definíveis nessa linguagem fossem totais. Como a linguagem possui sintaxe computável, podemos enumerar todas as definições de funções (apenas enumerar todas as strings e filtrar aquelas que causam erros sintáticos). Como as regras de avaliação são computáveis, a segunda suposição nos permite concluir que, em nossa linguagem, podemos definir a função total eval(n,m)que avalia a n-a função definível m(essencialmente, esse é um mini-intérprete escrito na própria linguagem). Mas então a função

λ k . (1 + eval(k,k))

é uma função definível total que é diferente de toda função definível total, uma contradição.

O simplesmente digitado $\lambda$-calculus satisfaz a primeira condição e define apenas funções totais. Portanto, não satisfaz a segunda condição.

No que diz respeito a "estar de cabeça para baixo", para uma forte normalização $\lambda$-cálculo é bastante fácil fornecer uma função total que não é definível no cálculo, ou seja, o próprio procedimento de normalização . Não é muito importante o quão sofisticado é o seu cálculo fortemente normalizador, pode ser o polimórfico$\lambda$-cálculo, ou teoria do tipo Martin-Lof, ou Cálculo de construções. (Exercício: se você puder implementar o procedimento de normalização, poderá implementar evalacima.)

Acho que a resposta de Merijn trata muito bem a primeira parte da sua pergunta. Tentarei responder à segunda parte: por que encontrar funções que são computáveis, mas não representáveis, no processo polimórfico?$\lambda$-calculus requer "ficar de pé sobre a cabeça".

Receio que exija alguma explicação dos conceitos nos quais você não está interessado. Uma função recusativa parcial é uma$\lambda$termo que representa uma função de $\mathbb{N}$ para $\mathbb{N}\cup\{\bot\}$. UMA$\lambda$-prazo $t$ aplicado ao representante de um número natural $n$ é enviado para $\bot$ se e apenas se $t\ n$se não tem uma forma normal. Se nenhum número for enviado para$\bot$dizemos que a função é total . Agora, a ideia é que nenhuma teoria lógica$T$ pode provar que um termo $t$ representa uma função total para cada função total $t$, sempre há "pontos cegos" onde $t$ termina em todas as entradas $n$, mas a declaração

é indecidível em $T$. Se a declaração acima for comprovável em$T$, dizemos que a função representada por $t$é comprovadamente total . Que nem todas as funções totais são comprovadamente totais em$T$ é uma conseqüência (uma variante) do Teorema de Godel Incompleteness $T$.

Agora, o ponto é que o amplo programa da maioria que desejamos escrever (classificação de listas, passagem de gráficos, sistemas operacionais) não é apenas funções totais, mas é comprovadamente total em sistemas lógicos razoáveis, como o Peano Arithmetic.

Agora, para o polimórfico $\lambda$-cálculo. Pode-se mostrar que os termos que se pode digitar neste cálculo são exatamente os termos que representam as funções comprovadamente totais na Aritmética Peano de Segunda Ordem. A Aritmética Peano de Segunda Ordem é muito, muito mais poderosa que a Aritmética Peano comum.

Isso significa pelas explicações acima que existem termos que são totais, mas não comprovadamente totais, mas essas funções são extremamente raras, pois já são raras para a Aritmética Peano (e muito mais raras na teoria de segunda ordem). Daí a afirmação "em pé de cabeça".

Estou achando um pouco difícil escrever a prova de forma concisa, mas espero que essa explicação forneça intuição suficiente para ver por que termos simples digitados não podem representar todos os termos não digitados.

O cálculo lambda simplesmente digitado está fortemente normalizando. Cada$\beta$redução nos aproximará da forma normal. Quando a função$f :: \alpha \rightarrow \beta \rightarrow \gamma$ é aplicado a um valor do tipo $\alpha$ será $\beta$ reduzir a uma função do tipo $\beta \rightarrow \gamma$. Dado um número finito de argumentos, é necessário um número finito de etapas de redução para alcançar$\beta$-forma normal, na qual não há mais reduções possíveis.

Para contrastar isso com o cálculo lambda sem tipo. Um dos combinadores UTLC mais famosos é o$Y$-combinador:

$Y = λf.(λx.f\; (x\; x))\; (λx.f\;(x\;x))$

Quando tentamos reduzir o $Y$-combinator acontece o seguinte:

Independentemente das funções em que passamos, ficamos presos em uma sequência infinita de reduções! Se tentarmos fixar um tipo STLC no UTLC$Y$-combinator, rapidamente achamos isso impossível, porque o aplicativo de funções não reduz o tipo, conforme é necessário no STLC. o$Y$-combinator é claramente computável (representa, usando a recursão, o conceito de um loop infinito), mas não pode ser representado no STLC, pois todos os termos do STLC estão fortemente normalizando.