La classe des fonctionnelles récursives primitives est-elle équivalente à la classe de fonctions que le fœtus prouve qu'elle se termine?

Le fœtus, si vous n'en avez pas entendu parler, peut être lu ici . Il utilise un système de «matrices d'appel» et de «graphiques d'appel» pour trouver tous les «comportements de récursivité» des appels récursifs dans une fonction. Pour montrer qu'une fonction se termine, cela montre que tous les comportements de récursivité des appels récursifs faits à une fonction obéissent à un certain «ordre lexicographique». Son vérificateur de terminaison permet toutes les fonctions récursives primitives et les fonctions telles que la fonction Ackermann. Fondamentalement, il permet une récursion primitive multi-arguments. C'est aussi fondamentalement le vérificateur de terminaison d'Agda; Je crois que Coq a des installations similaires aussi bien que peut-être plus générales.

De la lecture de l'article "Programmation fonctionnelle totale" par DA Turner . Il explique que le langage qu'il propose proposerait d'exprimer tous les "fonctionnels récursifs primitifs" comme on le voit dans le système T étudié par Godel. Il poursuit en disant que ce système est "connu pour inclure toutes les fonctions récursives dont la totalité peut être prouvée dans une logique de premier ordre".

Dose Foetus autorise toutes les fonctions récursives primitives? Si oui, autorise-t-il des fonctions qui ne sont pas des fonctionnelles récursives primitives? Une citation peut-elle être fournie pour la réponse à cela? (ce n'est pas vraiment nécessaire car je suis juste intéressé; c'est juste qu'une lecture conjugale sur le sujet serait bien)

Question bonus: les fonctionnelles récursives primitives ont une définition très concise en termes de combinateurs: typées S et K (qui ne peuvent pas exprimer les combinateurs à virgule fixe), zéro, la fonction successeur et la fonction d'itération; c'est ça. Existe-t-il d'autres langues plus générales qui ont une définition aussi concise et dans lesquelles toutes les expressions se terminent?

lo.logic computability functional-programming Jake
la source

Sur Agda vs Coq: J'ai toujours lu le vérificateur de terminaison d'Agda pour être plus avancé et accepter plus de fonctions, la vôtre est la première affirmation contraire (c'est une bonne règle de base lorsque l'on compare Agda à Coq, sauf pour le manque de tactique d'Agda: Agda est plus recherchée et ouverte à des extensions dont la stabilité est moins établie). Andreas Abel a travaillé sur des vérificateurs de terminaison encore plus avancés basés sur des types de taille, voir son travail sur MiniAgda et également ce document .

Blaisorblade

Il y a «accepter plus de définitions de fonctions» et «avoir une plus grande classe de fonctions calculables». Les deux sont incomparables. Agda gagne au premier chef, mais Coq gagne clairement au second.

cody le

Je dois préciser que je n'ai pas du tout utilisé Coq et Agda seulement un peu. Il me semblait que d'après le peu que j'avais lu, Coq était capable de définir une classe plus large de fonctions calculables, mais je ne le savais pas. "belive" et "peut-être" ont été utilisés pour exprimer que je ne savais pas.

Jake

Réponses:

Oui, le vérificateur de fœtus peut tout vérifier dans T. de Goedel. Vous pouvez le montrer en utilisant le vérificateur pour montrer que l'opérateur d'itération dans T se termine. Par exemple, la définition suivante fonctionnera:

\begin{array}{lcl} i t e r & : & A \to (A \to A) \to N \to A \\ i t e r i f 0 & = & i \\ i t e r i f (n + 1) & = & f (i t e r i 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}$

Ceci est très facile à vérifier pour le vérificateur de fœtus (ou la plupart des autres vérificateurs de terminaison), car il s'agit d'une définition manifestement structurellement récursive.

Agda et Coq permettent toutes deux de prouver la terminaison de fonctions qui vont bien au-delà de ce qui est prouvablement total en arithmétique de premier ordre. La caractéristique qui permet cela est qu'ils permettent de définir des types par récursivité sur les données, ce qui est appelé "grande élimination". (Dans la théorie des ensembles ZF, le schéma de remplacement des axiomes sert à peu près le même objectif.)

Un exemple simple de quelque chose qui va au-delà de T est la cohérence du T de Goedel lui-même! Nous pouvons donner la syntaxe comme type de données:

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

Notez que la dépendance de type nous permet de définir un type de données de termes contenant uniquement les termes bien typés de T. Nous pouvons alors donner une fonction d'interprétation pour les types:

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

Cela signifie que cela Ndevrait être les nombres naturels Agda, et la flèche de T devrait être interprétée comme l'espace de fonction Agda. Il s'agit d'une "grande" élimination, car nous définissons un ensemble par récursivité sur la structure du type de données T.

On peut alors définir une fonction d'interprétation, montrant que chaque terme du T de Goedel peut être interprété par un terme 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)

(Je n'ai pas Agda sur cette machine, il y a donc sans doute des importations manquantes, des déclarations de fixité et des fautes de frappe. La correction est un exercice pour le lecteur, qui peut également être éditeur, s'il le souhaite.)

Je ne sais pas quelle est la force de cohérence d'Agda, mais Benjamin Werner a montré que le calcul des constructions inductives (calcul du noyau de Coq) est équitablement compatible avec ZFC plus un nombre incalculable de cardinaux inaccessibles.

Neel Krishnaswami
la source

Notez que vous n'avez pas utilisé d'élimination importante dans votre exemple. Une grande élimination n'ajoute pas réellement de puissance de calcul. L'imprédicativité le fait: le système F n'a pas le premier, mais peut exprimer des fonctions non exprimables dans le système T.

cody

@cody: La fonction interp-T calcule un ensemble à partir d'un terme, ce qui ressemble à une grande élimination pour moi! Il est certain que les grandes éliminations ajoutent de la puissance: la théorie de type Martin-Loef ne peut même pas dériver une incohérence de 0 = 1 sans une grande élimination. (Pour voir cela, notez que sans univers / grandes éliminations, vous pouvez effacer toutes les dépendances et obtenir un terme simplement tapé: c'est ce que Harper et Pfenning ont fait dans leur preuve d'adéquation pour LF.)

Neel Krishnaswami

Je suis désolé: oui, la fonction interp-T utilise en effet une grande élimination. Je suis également d'accord que prouver 0! = 1 l'exige en effet. Cependant, définir des fonctions calculables n'est pas la même chose que prouver des instructions mathématiques . Ma réponse clarifie un peu cela. Le calcul pur des constructions, par exemple, ne peut pas prouver 0! = 1. Il peut cependant définir la fonction Ackermann avec une relative facilité.

cody

Cela montre qu'Agda a un sens plus général qu'il peut écrire un interpréteur pour le système T mais qu'il n'affiche pas la météo ou non. Le fœtus, une langue qui n'est pas typée de manière dépendante, est plus générale. Le fœtus peut-il faire cela? Agda serait-elle encore en mesure de le faire sans une "grande élimination"?

Jake

La documentation d'Agda indique que son vérificateur de terminaison utilise l'algorithme du fœtus. Si vous preniez T et l'étendiez avec des définitions de correspondance de motifs et récursives vérifiées par le fœtus, vous ne seriez pas en mesure d'écrire un interpréteur pour T dedans. En fait, vous ne changeriez pas du tout les fonctions calculables par T - toutes les ordonnances de résiliation calculées par le fœtus sont prouvées comme étant bien fondées dans l'arithmétique Peano. (Voir la réponse de cody.) L'algorithme du fœtus vous permet d'écrire plus de définitions , sans changer l'ensemble de fonctions que vous pouvez calculer. Les grandes éliminations d'Agda augmentent en fait l'ensemble des fonctions.

Neel Krishnaswami

À titre de clarification, je dois noter que Fetus est développé par Andreas Abel , qui a également développé le vérificateur de terminaison original pour Agda , et a travaillé sur des techniques de terminaison plus avancées depuis.

$\mathbb{N}$ $\mathbb{N}$ $\mathrm{F}$ $\mathrm{PA}^2$ $\mathrm F$ $\mathrm{PA}$ $\mathrm{T}$

$\mathrm{PA}$

$\mathrm{T}$

cody
la source

comment une classe de fonctions qui se terminent de façon prouvée (PA ^ 2) peut-elle être équivalente à la classe de fonctions du système F qui ne peuvent pas se terminer à ma connaissance? De plus, je ne comprends pas comment vous me répondez à la question. Dites-vous que le système T a une plus grande classe de fonctions calculables ou dites-vous que le fœtus l'est? Je pense qu'il y a eu un saut dans votre logique qui m'attendait à avoir plus de connaissances que je n'en ai réellement. Le lien que vous avez fourni semble également conduire à une mauvaise page qui ne s'affiche pas correctement.

Jake

Les fonctions du système F se terminent toutes. Le fœtus capture une plus grande classe de fonctions calculables que le système T, mais "par accident", si vous supprimez le polymorphisme, alors le fœtus capture uniquement exactement le système T. Pouvez-vous me dire quel lien ne fonctionne pas pour vous? (et quel navigateur vous utilisez :)

cody

Si par fonctionnelles récursives primitives vous entendez des fonctions récursives primitives et que vous savez que le fœtus contient la fonction Ackermann, alors le fœtus ne coïncide pas avec la classe des fonctions pr car la fonction Ackermann n'est pas récursive primitive. Cela a été démontré par Ackermann et plus tard une preuve simplifiée a été donnée par Rosza Peter dans " Konstruktion nichtrekursiver Funktionen " 1935 (malheureusement seulement en allemand pour autant que je sache).

Si vous recherchez de plus grandes classes de fonctions récursives dont la terminaison est garantie et qui pourraient coïncider avec la classe de fonctions capturées par le fœtus, un autre travail de Rosza Peter pourrait vous intéresser.

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

$<$

(a, b) < (c, d) ⟺ (a < c \land b \leq d) \lor (a \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$

[modifier] Les fonctions récursives primitives ne sont pas les mêmes que les fonctions récursives primitives comme indiqué dans le commentaire ci-dessous. Pourtant, je pense que l'on pourrait transférer le concept de récursion transfinie aux fonctionnelles. Cependant, il n'est pas clair s'il est toujours plus puissant par rapport à un paramètre fonctionnel.

John D.
la source

la classe des fonctionnelles récursives primitives de type fini est plus générale que la classe des fonctions récursives primitives. Il peut exprimer la fonction Ackermann par exemple et peut être vu dans le système de Godel T.

Jake