coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Guardedness checker
- Date: Thu, 10 Jan 2013 11:34:32 +0100
Hello Pierre,
thanks for the reference.
I was aware that the current Coq guardedness condition first reduces the body. However, still, the fully reduced version of my example
fix foo (n : nat) : nat :=
match n with
| 0 => 0
| S x => S (foo
((fix minus (n0 m : nat) {struct n0} : nat :=
match n0 with
| 0 => n0
| S k =>
match m with
| 0 => n0
| S l => minus k l
end
end) x 2))
end
is not accepted by Giménez' guardedness condition (there the recursive argument of the recursive call to "foo" should be of the shape "z Q1 ... Qn" with "z" in the set of allowed variables). Here it is a "fix" construct.
I do not directly see whether it it covered by yours. Having a "fix" construct as the recursive argument of the recursive call to "foo" seems to be fine. While checking the body of the inner fix (after using the FixSpec rule) we have
..., minus ▶ ⊥, n0 ▶ <, m ▶ ⊥
After that, to check the body of the "S l" case in the second match, it seems to fail on
minus k l
Am I missing something maybe?
Best,
Robbert
On 01/09/2013 12:17 PM, Pierre Boutillier wrote:
Hi,
The formal description of the current guardedness condition :
http://hal.inria.fr/hal-00651780
Very approximately (and the devil is in the details), it is Giménez
guardedness condition but on the weak head normal form of the body of
the fixpoint
(
match n with
| 0 => 0
| S x => S (foo (x - 2))
end.
in your second example)
All the best,
Pierre B
On 09/01/2013 12:09, Robbert Krebbers wrote:
Hello,
today I noticed that the gcd function on nat is defined as follows
Fixpoint gcd a b :=
match a with
| O => b
| S a' => gcd (b mod (S a')) (S a')
end.
I was quite surprised that this is accepted by Coq's guardedness
checker. After all, it is not obvious that (b mod (S a')) is indeed
structurally smaller than (S a').
Also an example like
Fixpoint foo (n : nat) :=
match n with
| 0 => 0
| S x => S (foo (S x - 3))
end.
is happily accepted.
This does not seem to be covered by, nor to be an obvious extension
of, the guardedness condition as defined in Giménez' 1994 "Codifying
guarded definitions with recursive schemes" to which (Chapter 4 of)
the reference manual refers.
Is there a formal description of the current guardedness condition
that captures the above cases? Or an intuitive explanation on what it
is doing to check these.
Robbert
- [Coq-Club] Guardedness checker, Robbert Krebbers, 01/09/2013
- Re: [Coq-Club] Guardedness checker, Pierre Boutillier, 01/09/2013
- Re: [Coq-Club] Guardedness checker, Robbert Krebbers, 01/10/2013
- Re: [Coq-Club] Guardedness checker, Pierre Boutillier, 01/10/2013
- Re: [Coq-Club] Guardedness checker, Robbert Krebbers, 01/10/2013
- Re: [Coq-Club] Guardedness checker, Pierre Boutillier, 01/09/2013
Archive powered by MHonArc 2.6.18.