coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
- To: Ali Assaf <ali.assaf AT inria.fr>
- Cc: croux AT andrew.cmu.edu, Coq Club <coq-club AT inria.fr>, Vladimir Voevodsky <vladimir AT ias.edu>
- Subject: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq
- Date: Fri, 20 Dec 2013 13:07:07 +0100
Hi,
On 20 déc. 2013, at 11:14, Ali Assaf
<ali.assaf AT inria.fr>
wrote:
> The point is precisely to not use primitive recursion for formalization.
> You keep using pattern matching and recursion to formalize what you want,
> e.g. integer division. Behind the curtain, there is a complex algorithm
> that uses intelligent heuristics that tranforms internally the user's
> functions into equivalent ones using only primitive recursion (a.k.a.
> eliminators), but that is invisible to the user (unless he activates some
> low-level feature, like the one for universes, or implicit arguments, etc.).
I’m very sympathetic with that point of view, that’s precisely what my
Equations package does:
compile from pattern-matching and recursion down to eliminators.
> If that algorithm is not satisfying enough then you keep extending it to
> accept more and more user functions (just like what is currently done with
> the kernel code). This time however, the kernel will not be compromised
> since any mistake in the algorithm will be rejected by the kernel.
Yes, that’s a nice benefit of this approach, I think we all agree the de
Bruijn criterion is a good guiding principle.
> On the other hand, if there are functions which simply CANNOT be expressed
> in terms of (Coq's) primitive recursion, then you have certainly defeated
> my point. Do you have examples of such functions that occur in practice,
> e.g. in the standard library? As far as I know, all the usual arithmetic
> functions (even the Ackermann function) can be transformed into
> (higher-order) primitive recursive functions.
I haven’t seen anything like that. HOWEVER, encodings can have a huge
performance cost. To translate mutually recursive
fixpoints on inductive families in full generality, one has to employ
transformations that reduce mutual recursion to
non-mutual one, or pack recursion on inductive families with their index to
become “homogeneous” so that we can use a
well-founded order relation and add equalities/casts everywhere to lift to
the logic the reasoning that is used in
the kernel to show that terms are in the subterm relation. For arithmetic it
isn’t so bad, but for more structured
objects it can become quite an overhead. So while such a solution in
principle could replace the fine tuned bug source
that is the syntactic guardedness check, in practice it is not reasonable yet
to switch to it. There are theoretical
and practical solutions to this, like the Implicit Calculus of Constructions
to actually compute on extracted terms
(erasing most decoration), the use of economic projections to make packing
inoffensive etc… but they’re still work in
progress.
Cheers,
— Matthieu
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, (continued)
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Andrej Bauer, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Vladimir Voevodsky, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Maxime Dénès, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ali Assaf, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Vladimir Voevodsky, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ali Assaf, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ramana Kumar, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Matthieu Sozeau, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Matthieu Sozeau, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Andrej Bauer, 12/17/2013
Archive powered by MHonArc 2.6.18.