Hierarquia de Ackerman para recursão primitiva de ordem superior no Sistema T
Gödel define em seu Sistema T recursividade primitiva sobre tipos mais altos. Encontrei notas de Girard, onde ele explica a implementação do Sistema T em cima do cálculo lambda simplesmente digitado. Na página 50, ele menciona que, quando usamos mais tipos no recursor, obtemos um poder mais expressivo com o sistema.
Não entendo exatamente como isso acontece. É possível criar uma espécie de hierarquia de Ackermann com a recursão primitiva de ordem superior, ou seja, uma hierarquia de funções cada vez mais rápidas, onde cada função é expressável no Sistema T, mas a diagonal não? Acho que sim, mas a construção não me parece evidente e eu estaria interessado em ver como alguém a construiria ou receberia indicações para a literatura.
Estou atrás de algo concreto. Estou ciente do argumento diagonal geral que comprova a existência de uma função que não está em T, mas gostaria de ver como alguém realmente "avançaria na hierarquia de tipos".
Essa é uma boa pergunta. Aposto que a hierarquia segue a classificação do tipo em que a recursão acontece. Quase vale a pena escrever. Voltarei aqui se tiver tempo para fazê-lo.
@AndrejBauer Eu estive pensando sobre isso e acho que seria possível construir novos iteradores com níveis mais altos na hierarquia de tipos e implementar uma hierarquia de rápido crescimento sob . Talvez os níveis de tipo correspondam (com algum deslocamento) à altura da torre dos expoentes em na hierarquia, mas não fui capaz de extrair uma prova (..yet). fϵ0fϵ0ωω...ωω...
A propósito, como você visualiza o próximo nível de recursão após a recursão primitiva? Se estiver em um tipo mais alto, você faria uma recursão geral ativa (para que não terminemos) ou algum tipo de recursão que ainda mantém as coisas terminando (nesse caso, qual seria)?
— Andrej Bauer 22/01
@AndrejBauer Acredito que isso possa ser abordado na definição de iteradores. (Estou usando funções teóricas dos números em vez de cálculo lambda.) Por exemplo, , e definindo , (S é sucessor) em que , . Agora deve ser comparável a . Chegar a para parece factível, mas parece desafiador. Depois de chegar aI(f,0)=f(1)I(f,0)=f(1)I(f,n+1)=f(I(f,n))I(f,n+1)=f(I(f,n))g(0)=Sg(0)=Sg(n)=I(g(n−1))g(n)=I(g(n−1))g:N×NN→NNg:N×NN→NNf:N→Nf:N→Nh(n)=g(n)(n)h(n)=g(n)(n)fωfωfωnfωnn∈Nn∈NfωωfωωfωωfωωEu esperaria que as coisas se esclarecessem.
Seus exemplos e ainda estão no fragmento System T. IIgg
(Essa é uma resposta muito parcial, abordando apenas o primeiro ponto, e não a questão principal sobre a hierarquia.)
Eu não tenho uma prova para apontar para você, mas a idéia é que um único recursor de primeira ordem em naturais como
rec:(nat→nat)→nat→nat→natrec fzn=f(f(…f(z)))(n times f)rec:(nat→nat)→nat→nat→natrec fzn=f(f(…f(z)))(n times f)
seria muito menos poderoso do que ter o esquema de recursão completo (primitivo)
recU:(U→U)→U→nat→UrecU:(U→U)→U→nat→U
uma vez que este se assemelha mais ou menos um termo polimórfica no Sistema F, que pode ser usado em muitos tipos .UU
De fato, o básico apenas nos dá acesso ao esquema de recursão primitiva de primeira ordem, como podemos encontrar em um livro de teoria da computabilidade / recursão. Com apenas isso, sabemos que funções como a de Ackermann não são definíveis. (Bem, isso não é tão óbvio, já que aqui também temos lambdas de ordem superior, é apenas a recursão que é restrita. Mas o ponto deve permanecer assim mesmo, eu acho.)recrec
Com o esquema , podemos escolher , o que nos permite definir a função de Ackermann, como mostra Girard no livro mencionado pelo OP. Portanto, o esquema é estritamente mais poderoso.recUrecUU=nat→natU=nat→nat
Essa é uma pergunta interessante, cuja resposta não é absolutamente trivial.
Darei a resposta curta primeiro: existe uma hierarquia de sistemas, chame-os de , onde os únicos recursores permitidos são com a ordem de , em que a ordem de um tipo é definida como :TkTkrecUrecUU≤kU≤k
ord(nat)=0ord(nat)=0
ord(U→V)=max(ord(V),ord(U)+1)ord(U→V)=max(ord(V),ord(U)+1)
Então o teorema é:
Teorema : para cada , existe um termo , de modo quekktk:nat→nattk:nat→nat
Tk⊢tk:nat→natTk⊢tk:nat→nat
Tk−1⊬tk:nat→natTk−1⊬tk:nat→nat
tktk cresce mais rápido (como uma função de ) do que qualquer função definível em , com .N→NN→NTlTll<kl<k
Observe que .T=⋃kTkT=⋃kTk
Como primeiro passo, provavelmente é útil observar que a função Ackermann pode ser definida assim (como sugerido pela resposta de chi ): modulo um erro da minha parte.
ack(n,m)=recnat→nat(λf.recnat f 0 m) (λp.S p) nack(n,m)=recnat→nat(λf.recnat f 0 m) (λp.S p) n
Isso realmente sugere que tinha "poder" adicional.recnat→natrecnat→nat
Mas como subimos a torre até arbitrário ?TkTk
O truque é considerar uma correspondência tripla entre:
1) Ordinais abaixoε0ε0
2) Fragmentos de da aritmética de Heyting, em que a indução é restrita a declarações com menos de alternações de quantificadores.HAkHAkkk
3) Funções definíveis emTkTk
Para cada ordinal que a torre tem altura , é possível considerar na aritmética de Heyting uma prova de que esse ordinal é bem fundamentado, e extrair dele um termo tipificável no sistema que corresponde à função na hierarquia Grzegorczyk .λk=ωω…ωλk=ωω…ωkktktkTkTkgλkgλk
Esse termo não pode ser bem digitado em devido à correspondência descrita acima, e o fato de que não prova a fundamentação de .Tk−1Tk−1HAk−1HAk−1λkλk
Mentiras e referências :
A correspondência entre , e não é tão limpa quanto sugeri, deve haver realmente , e , cada um relacionado por alguma constante concreta.TkTkHAkHAkλkλkkkk′k′