Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Guardedness checker

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Guardedness checker


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page