coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jasper Hugunin <jasperh AT cs.washington.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A reduction for the nat recursor
- Date: Wed, 3 Jan 2018 20:28:29 +0900
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasperh AT cs.washington.edu; spf=None smtp.mailfrom=jasperh AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-oi0-f43.google.com
- Ironport-phdr: 9a23:1/lFpxEad+q8zh8ux/r1Cp1GYnF86YWxBRYc798ds5kLTJ78r8ywAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODw38G/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Oxd48BAPAaPeZAsYb9vUYFoxmjBQmjGePvzD5Ihnnr1qA90eQuCxrG3BQ+ENIUsHTZt8n6NLwIXeG71qbI1jXDb/JQ2Tfy9IjIdRYhreuSUr1tbMrc0E8iHB7LgFWXrIzqJTKV1uIVvmiU7upgSeKvi3M8pA1rozivwd8giobIhoIJylDE6D52zJwpKt2/TU52Z8OvHphItyyCKYd6XscvT3trtSs60LEKp4O3cSsQxJkoyRPSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6U2gxff9VsmwyVpKqStFnsXVunAD2BHe5NKLSvR6/kem1jaP0x7c5vtYLkAzkKrXM58hwrgumZoPqUnPADP6lUHsgKKVdkgo4Pak5/nkb7n8qZKROZd4igTkPaQvnsy/D/44Mg8LX2WD++Szzqbj/VXnT7VQjv07ibXWsIvAKcUVvKG5GA9V0ocl6xawEzem19IYkWMZI11YZRKLl5LpNE3WIPDkEfe/hEyhnytsx/DfJ7HuHpHNLmXYn7r6ZrZ860tcyBIpwtxF5pJUDKsBIPPpVUPrutzYFExxDwvhyOH+Td55y4k2WGSVA6bfPrmBn0WP47cNKvKUaZVdmCvyNv4k4ba6j3YigVIHfYGixt0IYWu4H/JpP0KfJ3fgn4FSQi8xogMiQbmy2xW5WjlJaiPqUg==
Hi.
About eta for iteration, see for instance "A NOTE ON REWRITING THEORY FOR UNIQUENESS OF ITERATION" of M. Okada and P. Scott, Theory and Applications of Categories, 6, 47-64 in 2000:
The rule is:
f = R a h where f : A x nat -> B, R is the recursor on nat and a = \x.f x 0,
if for all x and y, f x (S n) = h x n (f x n).
"(i) It is undecidable,
(ii) Church-Rosser fails, although ground Church-Rosser holds,
(iii) strong normalization (termination) is still valid.
This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system."
Frédéric.
Le 03/01/2018 à 03:13, Jasper Hugunin a écrit :
Hi Cody,
Thanks for your response.Neither of the rules you mentioned seem to quite match what I am looking for (though maybe they imply it).
As I understand it, eta for inductives reduces (fix id n := match n with O => O | S m => S (id m) end) to (fun n => n),or reduces (match n with O => O | S m => S m end) to n.Neither of these seem to apply when defining a function (nat -> A).
Commutative conversions allow to move the application of a function across a match (into and out of the branches).But there is no function applied to the match in (fix shift n := match n with O => a | S m => shift m end),and no shared function that I see applied to the branches (a) and (shift m).
Perhaps you know of a more general meaning for these rules or some tricky set of rewrites to use to derive it?
I'll attach my example below. Modulo this reduction, it is an implementation of coinductive types from nat, pi, and sigma,with an anamorphism and eliminator such that the eliminator computes on the anamorphism.Under the univalence axiom, these types should be equivalent to the ones in the paper below,which were shown to have the correct equality types.
The main ideas are all inNON-WELLFOUNDED TREES IN HOMOTOPY TYPE THEORYBY: BENEDIKT AHRENS, PAOLO CAPRIOTTI, AND RÉGIS SPADOTTIthis development just improves the computational behavior.
I don't have much hope for adding this reduction to Coq, since it seems very specific to nat,but I was thinking it could be interesting to develop a type theory with such a rule,and then get coinductive types for free.
Best,- Jasper Hugunin
On Tue, Jan 2, 2018 at 9:47 PM, roux cody <cody.roux AT gmail.com> wrote:
CodyBest,If you post your complete example, someone may have a workaround which does not require such a powerful conversion rule!See also this discussion: https://github.com/coq/coq/issues/3119Hi Jasper!This rule is sometimes called "eta for inductives" or "commutative conversions". In some versions it may break confluence, and in general is quite difficult to implement in Coq.
On Tue, Jan 2, 2018 at 2:20 AM, Jasper Hugunin <jasperh AT cs.washington.edu> wrote:
Hello,
I ran into the following function:(fix shift n := match n with O => a | S m => shift m end) : nat -> Awhich clearly on any concrete n reduces to a.
It would be very convenient if this was judgmentally equal to (fun _ => a).Of course, this is not implemented in Coq, but I haven't been able find any references discussing such a reduction. Does anyone know what the cost of adding such a reduction would be?(does it break decidable type-checking, or introduce unreasonable computational overhead?)
Where this comes from, is that I actually have a family of types A : nat -> Type, along withforall n, A n = A (S n), and a0 : A 0. My function then looks like (fun n => nat_rect A a0 (coerce) n),but for some specific instances A is actually independent of n, and the equalities are eq_refl.In the general case, I don't see how to do a useful reduction, but when given such nice data I wouldhave liked to return just a, independent of n.
- Jasper Hugunin
- [Coq-Club] A reduction for the nat recursor, Jasper Hugunin, 01/02/2018
- Re: [Coq-Club] A reduction for the nat recursor, roux cody, 01/02/2018
- Re: [Coq-Club] A reduction for the nat recursor, Jasper Hugunin, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, Frédéric Blanqui, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, Jasper Hugunin, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, Felix Rech, 01/08/2018
- Re: [Coq-Club] A reduction for the nat recursor, Jasper Hugunin, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, Frédéric Blanqui, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, Jasper Hugunin, 01/03/2018
- Re: [Coq-Club] A reduction for the nat recursor, roux cody, 01/02/2018
Archive powered by MHonArc 2.6.18.