Classe de fonctions calculables par Coq

Benjamin Werner a prouvé l'interprétabilité mutuelle de ZFC avec d'innombrables inaccessibles et le calcul des constructions inductives, dans son article Sets in Types, Types in Sets .

Cela signifie, en gros, que toute fonction dont on peut montrer qu'elle est totale dans ZFC avec un nombre innombrable d'inaccessibles peut être définie dans Coq. Donc, à moins que vous ne soyez un théoricien des ensembles travaillant sur de grands cardinaux, il est peu probable qu'aucune fonction calculable que vous ayez jamais souhaitée ne puisse être définie dans Coq.

Neel Krishnaswami
la source

Sauf un interprète Coq ...

Jules

En fait, vous pouvez implémenter un interpréteur Coq (en effet, des fonctions récursives générales arbitraires) à l'intérieur de Coq. Si CIC est cohérent, vous ne pourrez pas prouver que l'interprète est une fonction totale, bien sûr, mais vous pouvez certainement l'implémenter.

Neel Krishnaswami

Vous pouvez utiliser la monade d'élévation constructive, , pour écrire des fonctions récursives générales. Votre vérificateur de type aura alors le type

. Il s'agit essentiellement de l'approche Bove / Capretta. (Voir aussi Benton, Kennedy et Varming, «Some Domain Theory and Denotational Semantics in Coq», dl.acm.org/citation.cfm?id=1616077.1616090. )

A_{⊥} ≜ ν α . A + α

$A_\bot \triangleq \nu \alpha.\; A + \alpha$

c o n t e x t \to t e r m \to t y p e \to {b o o l}_{⊥}

$\mathsf{context} \to \mathsf{term} \to \mathsf{type} \to \mathsf{bool}_\bot$

Neel Krishnaswami

@Neel: c'est de la triche. Et pour une bonne raison, sinon nous aurions une incohérence.

Andrej Bauer

C'est de la triche parce que la fonction d'évaluation est censée évaluer les choses, pas vous donner une non-réponse.

Andrej Bauer

Classe de fonctions calculables par Coq

Réponses: