4
$\begingroup$

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive theories). Note that unlike the axiom CT, Church's rule does not prove any anti-classical results.

Let $\eta$ be an admissible numbering. CR is admissible for a theory $T$ iff for every formula $\phi(x,y)$ such that $$T \vdash \forall x \in \mathbb N. \exists y \in \mathbb N. \phi(x, y)$$ there exists $e \in \mathbb N$ such that $$(*) \text{ } T \vdash \text{$\eta_{\bar e}$ is total} \land \forall x \in \mathbb N. \phi(x, \eta_{\bar e}(x))$$

My question is which proof assistants have implemented this rule?


Notes:

  • I'm fine if $e$ is taken to be a member of some other discrete data structure (like strings or finite trees) instead of $\mathbb N$.
  • It doesn't need to be an official feature, a tool or patch from a third-party is fine.
  • What I'm looking for is not just program extraction (although it is related to it). The implementation must both output $e$ and a proof of $(*)$. Program extraction typically outputs $e$ but not a proof of $(*)$. In particular, if $\phi$ is a function, the proof assistant has proven it is a computable function and can apply theorems about computable functions to $\phi$. (Likewise, there are some systems that assume the axiom CT but don't compute $e$. They also don't count.)
  • $(*)$ is proven within $T$, so the software can't add any extra axioms (like that $T$ is arithmetically sound) when proving it.
$\endgroup$
21
  • 1
    $\begingroup$ Wait, can phi be any formula? What are the conditions on phi? (I realize I misread Wikipedia and thought phi was quantifier free.) $\endgroup$
    – Jason Rute
    Feb 3 at 3:00
  • 1
    $\begingroup$ @JasonRute there are no conditions of $\phi$ other than there being a proof of $\forall x.\exists y. \phi(x,y)$. The reason CR can exist is that in constructive proofs can be turned into programs. The program is found by analyzing the proof, not by analyzing the formula $\phi$. $\endgroup$ Feb 3 at 3:32
  • 1
    $\begingroup$ Is $\exists$ allowed te interpreted as $\Sigma$? $\endgroup$ Feb 3 at 9:13
  • 1
    $\begingroup$ Actually, how is $\eta$ supposed to work? If it's an interpreter for $T$ then there's a problem. $\endgroup$ Feb 3 at 14:53
  • 1
    $\begingroup$ You should ask a separate question: how to formalize computability theory? The answer is very nice and cannot be done justice in a comment. $\endgroup$ Feb 4 at 6:59

2 Answers 2

2
$\begingroup$

You might want to give a look at A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus by Yannick Forster and Fabian Kuntze. They define a set-up in Coq where using tactics they can transform a Coq function into a deeply embedded λ-calculus term, and also provide facilities to relate this function to the original one. There is much more work of this group around similar ideas, including synthetic computability theory using CT (see Yannick's PhD thesis for an overview), all kinds of synthetic computability/complexity results, and work on MetaCoq, which gives facilities for quoting and unquoting Coq terms – although not (yet?) about the relation between the quoted term and the original one.

$\endgroup$
2
  • $\begingroup$ Metacoq already proves that erasure preserves the computational behaviour of the source Coq term for first-order functions, see this module. Since this is the hardest part, I think that CR can be obtained by chaining several theorems lying around the development. $\endgroup$ Feb 7 at 15:26
  • $\begingroup$ But wait, this is not what I meant? I was talking about having a relation between t and the output of MetaCoq Quote t.. $\endgroup$ Feb 7 at 15:51
3
$\begingroup$

Not the answer you would like to hear, but that would be "no proof assistant" (to my knowledge). The first reason is that Church's rule does not hold for classical theories but the constructive proof assistants are all designed to be agnostic about excluded middle, and so will not commit to Church's rule. The second reason is that Church's rule in its original form is at best of a very limited use in practice, while at the same time its implementation would heavily influence the internals of a proof assistant.

Precisely because proof assistants are so conservative and general, anyone is free to implement Church's rule. Some of the mechanisms supporting such an exercise already exist, for example:

  • MetaCoq, and in particular its subpart Template-Coq, allows meta-level manipulation of Coq code, provides representation of Coq code in Coq, etc.
  • Agda reflection & metaprogramming similarly offer meta-level capabilities for reifying and evaluating Agda code.

Perhaps someone has already used these tools to do it?

Lean has nice meta-programming functionality, too. It might be possible to use it, if you can somehow avoid using its non-classical axioms.

$\endgroup$
2
  • $\begingroup$ "The first reason is that Church's rule is anti-classical." Are you sure? I thought CT (the axiom) was anti-classical but CR (the inference rule) wasn't? (Like, CR isn't admissible for in any classical theory, but it doesn't allow you to derive any anti-classical principles.) $\endgroup$ Feb 3 at 14:08
  • 1
    $\begingroup$ Ah yes, we must be careful. In any case, because CT isn't admissible for classical theories, that would be reason enough for agnostic implementors of constructive proof assistants to dislike it. But the main reason really is that it's just not worth doing. If you're going to invest energy into implementing this sort of thing, it's better to just implement program extraction or some such. $\endgroup$ Feb 3 at 14:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.