A classe de funcionais de recursão primitiva é equivalente à classe de funções que o Fetus prova terminar?

O feto, se você nunca ouviu falar, pode ser lido aqui . Ele usa um sistema de 'matrizes de chamada' e 'gráficos de chamada' para encontrar todos os 'comportamentos de recursão' de chamadas recursivas em uma função. Para mostrar que uma função termina, mostra que todos os comportamentos de recursão das chamadas recursivas feitas a uma função obedecem a uma certa "ordem lexicográfica". Seu verificador de terminação permite todas as funções recursivas primitivas e funções como a função Ackermann. Basicamente, permite recursão primitiva com vários argumentos. Este também é basicamente o verificador de rescisão da Agda; Acredito que a Coq também tenha algumas instalações semelhantes, embora talvez mais gerais.

Da leitura do artigo "Programação Funcional Total", de DA Turner . Ele explica que sua linguagem proposta seria capaz de expressar todos os "funcionais recursivos primitivos", como visto no Sistema T estudado por Godel. Ele continua dizendo que esse sistema "é conhecido por incluir todas as funções recursivas cuja totalidade pode ser provada na lógica de primeira ordem".

O Dose Fetus permite todos os funcionais recursivos primitivos? Em caso afirmativo, ele permite funções que não são funcionais recursivas primitivas? Pode ser fornecida uma citação para a resposta? (isso não é realmente necessário, pois estou apenas interessado; apenas algumas leituras conjugais sobre o assunto seriam boas)

Pergunta do bônus: Os funcionais recursivos primitivos têm uma definição muito concisa em termos de combinadores: digitados S e K (que não podem expressar os combinadores de ponto fixo), zero, a função sucessora e a função de iteração; é isso aí. Existem outras linguagens mais gerais que possuem uma definição concisa e em que todas as expressões terminam?

lo.logic computability functional-programming Jake
fonte

Em Agda vs Coq: sempre leio o verificador de terminação da Agda para ser mais avançado e aceita mais funções; a sua é a primeira reivindicação em contrário (essa é uma boa regra geral ao comparar Agda à Coq, exceto pela falta de tática da Agda: Agda é mais pesquisável e aberto a extensões cuja estabilidade é menos estabelecida). Andreas Abel tem trabalhado em verificadores de terminação ainda mais avançados, com base em tipos de tamanho, veja seu trabalho no MiniAgda e também este documento .

Blaisorblade 14/01

Há "aceitar mais definições de funções" e "ter uma classe maior de funções computáveis". Os dois são incomparáveis. A Agda vence na primeira contagem, mas Coq vence claramente na segunda.

Cody

Devo esclarecer que não usei Coq e a Agda apenas um pouco. Parecia que, pelo pouco que li, Coq foi capaz de definir uma classe mais ampla de funções computáveis, mas eu não sabia, então disse: "Acredito que o Coq tenha algumas facilidades semelhantes, embora talvez mais gerais"; "acreditar" e "talvez" foram usados para transmitir que eu não sabia.

Jake

Respostas:

Sim, o verificador Fetus pode verificar tudo em T. do Goedel. Você pode mostrar isso usando o verificador para mostrar que o operador de iteração em T está terminando. Por exemplo, a seguinte definição funcionará:

\begin{array}{lcl} Eu t e r & : & UMA \to (UMA \to UMA) \to N \to UMA \\ Eu t e r Eu f 0 0 & = & Eu \\ Eu t e r Eu f (n + 1 1) & = & f (Eu t e r Eu f n) \end{array}

$\begin{array}{lcl} \mathit{iter} & : & A \to (A \to A) \to \mathbb{N} \to A \\ \mathit{iter} \;i \;f \;0 & = & i \\ \mathit{iter} \;i \;f \;(n+1) & = & f\;(\mathit{iter} \;i \;f \;n) \end{array}$

É muito fácil para o verificador Fetus (ou quase qualquer outro verificador de terminação) verificar, porque é uma definição obviamente estruturalmente recursiva.

A Agda e a Coq permitem provar o término de funções que vão muito além do que é comprovadamente total na aritmética de primeira ordem. O recurso que permite isso é que eles permitem definir tipos por recursão nos dados, que é chamada de "grande eliminação". (Na teoria dos conjuntos ZF, o esquema axioma de substituição serve aproximadamente ao mesmo propósito.)

Um exemplo fácil de algo que vai além de T é a consistência do próprio T de Goedel! Podemos fornecer a sintaxe como um tipo de dados:

data T : Set where 
   N : T 
   _⇒_ : T → T → T

data Term : T → Set where 
   zero : Term N
   succ : Term (N ⇒ N)
   k    : {A B : T} → Term (A ⇒ B ⇒ A)
   s    : {A B C : T} → Term ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
   r    : {A : T} → Term (A ⇒ (A ⇒ A) ⇒ N ⇒ A)
   _·_  : {A B : T} → Term (A ⇒ B) → Term A → Term B

Observe que a dependência de tipo nos permite definir um tipo de dados com termos contendo apenas os termos bem digitados de T. Podemos então fornecer uma função de interpretação para os tipos:

interp-T : T → Set 
interp-T N       = Nat 
interp-T (A ⇒ B) = (interp-T A) → (interp-T B)

Isso indica que Ndevem ser os números naturais do Agda, e a seta de T deve ser interpretada como o espaço de funções do Agda. Esta é uma eliminação "grande", porque definimos um conjunto por recursão na estrutura do tipo de dados T.

Podemos então definir uma função de interpretação, mostrando que todos os termos do T de Goedel podem ser interpretados por um termo da Agda:

interp-term : {A : T} → Term A → interp-T A
interp-term zero    = 0 
interp-term succ    = \n → n + 1
interp-term k       = \x y → x
interp-term s       = \x y z → x z (y z)
interp-term r       = Data.Nat.fold 
interp-term (f · t) = (interp-term f) (interp-term t)

(Eu não tenho o Agda nesta máquina, portanto, sem dúvida, existem algumas importações ausentes, declarações de fixidez e erros de digitação. Correção é um exercício para o leitor, que também pode ser um editor, se quiser.)

Não sei qual é a força da consistência da Agda, mas Benjamin Werner mostrou que o Cálculo de Construções Indutivas (cálculo de núcleo da Coq) é equiconsistente ao ZFC, além de inúmeros cardeais inacessíveis.

Neel Krishnaswami
fonte

Observe que você não usou grande eliminação no seu exemplo. Uma grande eliminação não adiciona poder computacional. Impredicativo faz: O sistema F não tem o antigo, mas pode expressar funções não expressivos em T. sistema

Cody

@ cody: A função interp-T calcula um conjunto a partir de um termo, o que parece uma grande eliminação para mim! Definitivamente, é o caso de que grandes eliminações acrescentam poder: a teoria do tipo Martin-Loef não pode sequer derivar inconsistência de 0 = 1 sem uma grande eliminação. (Para ver isto, nota que, sem universos / grandes eliminações você pode apagar todas as dependências e obter um termo simplesmente digitado: isto é o que Harper e Pfenning fez na sua prova de adequação para LF.)

Neel Krishnaswami

Sinto muito: sim, a função interp-T realmente usa grande eliminação. Também concordo que provar 0! = 1 realmente exige isso. No entanto, definir funções computáveis não é a mesma coisa que provar declarações matemáticas . Minha resposta esclarece isso um pouco. O Cálculo de Construções puro, por exemplo, não pode provar 0! = 1. Ele pode, no entanto, definir a função Ackermann com relativa facilidade.

Cody

Isso mostra que o Agda tem um senso mais geral de que pode escrever um intérprete para o sistema T, mas não mostra o clima ou não. O feto, um idioma que não é tipicamente dependente, é mais geral. O feto pode fazer isso? A Agda ainda seria capaz de fazer isso se não fosse por "grande eliminação"?

Jake

A documentação da Agda diz que seu verificador de terminação usa o algoritmo Fetus. Se você pegasse T e o estendesse com a correspondência de padrões e as definições recursivas verificadas pelo Fetus, não seria possível escrever nele um intérprete. De fato, você não alteraria as funções computáveis por T - todas as ordens de terminação que o Fetus calcula são comprovadamente bem fundamentadas na aritmética do Peano. (Veja a resposta de cody.) O algoritmo Fetus permite escrever mais definições , sem alterar o conjunto de funções que você pode calcular. As grandes eliminações da Agda realmente aumentam o conjunto de funções.

Neel Krishnaswami

Como meio de esclarecimento, devo observar que o Fetus é desenvolvido por Andreas Abel , que também desenvolveu o verificador de terminação original da Agda e trabalhou em técnicas de terminação mais avançadas desde então.

A resposta para sua pergunta pode ser um pouco decepcionante: a classe de funções de a é exatamente as funções que podem ser definidas no sistema . A razão para isso: a classe mencionada acima é igual às funções prováveis de terminação na aritmética de segunda ordem ( ), que por sua vez é igual às funções definíveis no sistema (consulte, por exemplo, provas e tipos , capítulo 11) Além disso, se você remover o polimorfismo, cairá nas funções definíveis em , que coincidem com as definíveis em system . $\mathbb{N}$ $\mathbb{N}$ $\mathrm{F}$ $\mathrm{PA}^2$ $\mathrm F$ $\mathrm{PA}$ $\mathrm{T}$

Novamente, a razão para isso é que a diminuição capturada pelas "matrizes de chamada" é comprovadamente bem fundamentada e essa prova pode ser realizada inteiramente em . $\mathrm{PA}$

No entanto, isso não significa que o Fetus não seja mais útil que o sistema ! Na prática, são necessárias análises de terminação mais complexas para poder aceitar determinadas apresentações de funções computáveis. Você não precisa fazer uma prova complicada na aritmética do Peano toda vez que escreve uma função de unificação, por exemplo. Portanto, nesse aspecto, o Fetus é muito poderoso e permite definir funções de uma maneira que não seria aceita pela Coq, pela Agda ou por qualquer outro sistema de prova comum. $\mathrm{T}$

cody
fonte

como uma classe de funções que está provadamente terminando (PA ^ 2) pode ser equivalente à classe de funções no sistema F que não é provável terminar tanto quanto eu sei? Também não entendo como você está me respondendo à pergunta. Você está dizendo que o sistema T tem uma classe maior de funções computáveis ou está dizendo que o feto é? Acho que houve um salto em sua lógica que esperava que eu tivesse mais experiência do que realmente tenho. Além disso, o link que você forneceu parece levar a uma página incorreta que não é renderizada corretamente.

Jake

Todas as funções do sistema F terminam. O Fetus captura uma classe maior de funções computáveis que o sistema T, mas "por acidente", se você remover o polimorfismo, o Fetus captura apenas exatamente o sistema T. Você pode me dizer qual link não funciona para você? (e qual navegador você está usando :)

Cody

Se por funções recursivas primitivas você quer dizer funções recursivas primitivas e sabe que o Fetus contém a função Ackermann, o Fetus não coincide com a classe de funções pr, pois a função Ackermann não é recursiva primitiva. Isso foi demonstrado por Ackermann e, mais tarde, uma prova simplificada foi dada por Rosza Peter em " Konstruktion nichtrekursiver Funktionen " 1935 (infelizmente apenas em alemão, até onde eu sei).

Se você procurar classes maiores de funções recursivas com garantia de término que possam coincidir com a classe de funções capturadas pelo Fetus, algum outro trabalho de Rosza Peter poderá interessá-lo.

$f(a,b)$ $f(a,b-1)$ $f(a-1,b)$

$<$

(uma, b) < (c, d) ⟺ (uma < c \land b \leq d) \lor (uma \leq c \land b < d)

$(a,b) < (c,d) \iff ( a < c \wedge b \leq d ) \vee ( a \leq c \wedge b < d )$

ω^{2}, ω^{3}

$\omega^2, \omega^3$

p_{i}

$p_i$

i

$i$

z = p_{1}^{n} \cdot p_{2}^{x_{1}} \cdot p_{3}^{x_{2}} \cdot \dots

$z = p_1^{n} \cdot p_2^{x_1} \cdot p_3^{x_2} \cdot \dots$

n

$n$

z

$z$

x_{i}

$x_i$

ω^{ω}

$\omega^\omega$

[edit] Funções recursivas primitivas não são iguais a funcionais recursivas primitivas, conforme observado no comentário abaixo. No entanto, acho que se poderia transferir o conceito de recursão transfinita para funcionais. No entanto, não está claro se ainda é mais poderoso criar uma configuração funcional.

John D.
fonte

a classe de funcionais recursivos primitivos do tipo finito é mais geral do que a classe de funções recursivas primitivas. Pode expressar a função de Ackermann, por exemplo, e pode ser visto em T. sistema de Godel

Jake