mysterious failure of termination-checking algorithm

[Aaron Bohannon]

I have a little development that defines freely generated terms of a
signature of symbols with arities.  It uses vectors to ensure that
terms are well-formed.  (I know this was also done in the CoLoR
library.)  Additionally, I want to define terms with holes, so I use a
derived signature with an option type for the one extra symbol.  Now
let's say I want to write a function over these contexts to determine
whether a hole symbol appears in a term.  How does one do this?

You can step through the code below and see that my first attempt,
"no_hole", fails the termination-checker, even though the extremely
similar function "all_term" passes it.  They're so similar, in fact,
that "no_hole" is actually just a specific instance of "all_term", as
you can see from the definition of "no_hole_from_all_term".  So why
does the definition of "no_hole" fail???

Now you ask, "why do I care if I already found a way to define the
function?"  OK, well tell me now how to define a function that tests
whether exactly one hole symbol appears in a term...

 - Aaron

---- Coq code ----

Set Implicit Arguments.

Inductive vector (A: Type): nat -> Type :=
| vnil: vector A O
| vcons: forall len, A -> vector A len -> vector A (S len).
Implicit Arguments vnil [A].

Definition vall (A: Type) (P: A -> Prop)
: forall len: nat, vector A len -> Prop :=
  fix vall' (len: nat) (xs: vector A len) {struct xs}: Prop :=
    match xs in vector _ len' return Prop with
    | vnil => True
    | vcons len1 a xs1 => P a /\ vall' len1 xs1
    end.

Record signature: Type := mk_signature {
  symbol: Set;
  arity: symbol -> nat
}.

Inductive term (S: signature): Type :=
| term_app: forall a: symbol S, vector (term S) (arity S a) -> term S.

Fixpoint all_term
  (S: signature) (P: symbol S -> Prop) (t: term S) {struct t}: Prop :=
  match t with
  | term_app a ts => P a /\ vall (@all_term S P) ts
  end.

Definition context_signature (S: signature): signature :=
  let context_symbol := option (symbol S) in
  let context_arity a :=
    match a with
    | Some a1 => arity S a1
    | None => 0
    end
  in
  @mk_signature context_symbol context_arity.

Definition context (S: signature): Type :=
  term (context_signature S).

Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
  match c with
  | term_app (Some a) cs => vall (@no_hole S) cs
  | term_app None _ => False
  end.

Definition no_hole_from_all_term (S: signature): context S -> Prop :=
  let isnt_hole (a: symbol (context_signature S)): Prop :=
    match a with
    | Some _ => True
    | None => False
    end
  in
  all_term isnt_hole.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[roconnor]

Interestingly, the following does work:

Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
   match c with
   | term_app a cs => match a with
                       (Some _) => vall (@no_hole S) cs
                       | None => False
                      end
   end.

On Sun, 20 Sep 2009, Aaron Bohannon wrote:

> I have a little development that defines freely generated terms of a
> signature of symbols with arities.  It uses vectors to ensure that
> terms are well-formed.  (I know this was also done in the CoLoR
> library.)  Additionally, I want to define terms with holes, so I use a
> derived signature with an option type for the one extra symbol.  Now
> let's say I want to write a function over these contexts to determine
> whether a hole symbol appears in a term.  How does one do this?
>
> You can step through the code below and see that my first attempt,
> "no_hole", fails the termination-checker, even though the extremely
> similar function "all_term" passes it.  They're so similar, in fact,
> that "no_hole" is actually just a specific instance of "all_term", as
> you can see from the definition of "no_hole_from_all_term".  So why
> does the definition of "no_hole" fail???
>
> Now you ask, "why do I care if I already found a way to define the
> function?"  OK, well tell me now how to define a function that tests
> whether exactly one hole symbol appears in a term...
>
> - Aaron
>
> ---- Coq code ----
>
> Set Implicit Arguments.
>
> Inductive vector (A: Type): nat -> Type :=
> | vnil: vector A O
> | vcons: forall len, A -> vector A len -> vector A (S len).
> Implicit Arguments vnil [A].
>
> Definition vall (A: Type) (P: A -> Prop)
> : forall len: nat, vector A len -> Prop :=
>  fix vall' (len: nat) (xs: vector A len) {struct xs}: Prop :=
>    match xs in vector _ len' return Prop with
>    | vnil => True
>    | vcons len1 a xs1 => P a /\ vall' len1 xs1
>    end.
>
> Record signature: Type := mk_signature {
>  symbol: Set;
>  arity: symbol -> nat
> }.
>
> Inductive term (S: signature): Type :=
> | term_app: forall a: symbol S, vector (term S) (arity S a) -> term S.
>
> Fixpoint all_term
>  (S: signature) (P: symbol S -> Prop) (t: term S) {struct t}: Prop :=
>  match t with
>  | term_app a ts => P a /\ vall (@all_term S P) ts
>  end.
>
> Definition context_signature (S: signature): signature :=
>  let context_symbol := option (symbol S) in
>  let context_arity a :=
>    match a with
>    | Some a1 => arity S a1
>    | None => 0
>    end
>  in
>  @mk_signature context_symbol context_arity.
>
> Definition context (S: signature): Type :=
>  term (context_signature S).
>
> Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
>  match c with
>  | term_app (Some a) cs => vall (@no_hole S) cs
>  | term_app None _ => False
>  end.
>
> Definition no_hole_from_all_term (S: signature): context S -> Prop :=
>  let isnt_hole (a: symbol (context_signature S)): Prop :=
>    match a with
>    | Some _ => True
>    | None => False
>    end
>  in
>  all_term isnt_hole.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Aaron Bohannon]

Aha!  Very helpful!  (Although still confusing...)

On Sun, Sep 20, 2009 at 1:53 PM,  <roconnor@...> wrote:

> Interestingly, the following does work:
>
> Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
>  match c with
>  | term_app a cs => match a with
>                      (Some _) => vall (@no_hole S) cs
>                      | None => False
>                     end
>  end.
>
> On Sun, 20 Sep 2009, Aaron Bohannon wrote:
>
>> I have a little development that defines freely generated terms of a
>> signature of symbols with arities.  It uses vectors to ensure that
>> terms are well-formed.  (I know this was also done in the CoLoR
>> library.)  Additionally, I want to define terms with holes, so I use a
>> derived signature with an option type for the one extra symbol.  Now
>> let's say I want to write a function over these contexts to determine
>> whether a hole symbol appears in a term.  How does one do this?
>>
>> You can step through the code below and see that my first attempt,
>> "no_hole", fails the termination-checker, even though the extremely
>> similar function "all_term" passes it.  They're so similar, in fact,
>> that "no_hole" is actually just a specific instance of "all_term", as
>> you can see from the definition of "no_hole_from_all_term".  So why
>> does the definition of "no_hole" fail???
>>
>> Now you ask, "why do I care if I already found a way to define the
>> function?"  OK, well tell me now how to define a function that tests
>> whether exactly one hole symbol appears in a term...
>>
>> - Aaron
>>
>> ---- Coq code ----
>>
>> Set Implicit Arguments.
>>
>> Inductive vector (A: Type): nat -> Type :=
>> | vnil: vector A O
>> | vcons: forall len, A -> vector A len -> vector A (S len).
>> Implicit Arguments vnil [A].
>>
>> Definition vall (A: Type) (P: A -> Prop)
>> : forall len: nat, vector A len -> Prop :=
>>  fix vall' (len: nat) (xs: vector A len) {struct xs}: Prop :=
>>   match xs in vector _ len' return Prop with
>>   | vnil => True
>>   | vcons len1 a xs1 => P a /\ vall' len1 xs1
>>   end.
>>
>> Record signature: Type := mk_signature {
>>  symbol: Set;
>>  arity: symbol -> nat
>> }.
>>
>> Inductive term (S: signature): Type :=
>> | term_app: forall a: symbol S, vector (term S) (arity S a) -> term S.
>>
>> Fixpoint all_term
>>  (S: signature) (P: symbol S -> Prop) (t: term S) {struct t}: Prop :=
>>  match t with
>>  | term_app a ts => P a /\ vall (@all_term S P) ts
>>  end.
>>
>> Definition context_signature (S: signature): signature :=
>>  let context_symbol := option (symbol S) in
>>  let context_arity a :=
>>   match a with
>>   | Some a1 => arity S a1
>>   | None => 0
>>   end
>>  in
>>  @mk_signature context_symbol context_arity.
>>
>> Definition context (S: signature): Type :=
>>  term (context_signature S).
>>
>> Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
>>  match c with
>>  | term_app (Some a) cs => vall (@no_hole S) cs
>>  | term_app None _ => False
>>  end.
>>
>> Definition no_hole_from_all_term (S: signature): context S -> Prop :=
>>  let isnt_hole (a: symbol (context_signature S)): Prop :=
>>   match a with
>>   | Some _ => True
>>   | None => False
>>   end
>>  in
>>  all_term isnt_hole.
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>         http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>
>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Lescuyer-3]

Note that the intermediary pattern variable 'a' (introduced
explicitely by Russell's variant, and not in the original version)
actually appears in the arguments of vall. If you try a version of
terms where the length does not depend on the symbol, say :

Record signature : Type := mk_signature  {
  symbol : Set;
  arity : nat
}.
Inductive term (S: signature): Type :=
| term_app: forall a: symbol S, vector (term S) (arity S) -> term S.

Then your original definition works fine.

I don't know quite what to make of it, but this definitely looks like
a bug and gives a good hint as to where to start investigating.

Stephane

On Sun, Sep 20, 2009 at 8:10 PM, Aaron Bohannon <bohannon@...> wrote:

> Aha!  Very helpful!  (Although still confusing...)
>
> On Sun, Sep 20, 2009 at 1:53 PM,  <roconnor@...> wrote:
>> Interestingly, the following does work:
>>
>> Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
>>  match c with
>>  | term_app a cs => match a with
>>                      (Some _) => vall (@no_hole S) cs
>>                      | None => False
>>                     end
>>  end.
>>
>> On Sun, 20 Sep 2009, Aaron Bohannon wrote:
>>
>>> I have a little development that defines freely generated terms of a
>>> signature of symbols with arities.  It uses vectors to ensure that
>>> terms are well-formed.  (I know this was also done in the CoLoR
>>> library.)  Additionally, I want to define terms with holes, so I use a
>>> derived signature with an option type for the one extra symbol.  Now
>>> let's say I want to write a function over these contexts to determine
>>> whether a hole symbol appears in a term.  How does one do this?
>>>
>>> You can step through the code below and see that my first attempt,
>>> "no_hole", fails the termination-checker, even though the extremely
>>> similar function "all_term" passes it.  They're so similar, in fact,
>>> that "no_hole" is actually just a specific instance of "all_term", as
>>> you can see from the definition of "no_hole_from_all_term".  So why
>>> does the definition of "no_hole" fail???
>>>
>>> Now you ask, "why do I care if I already found a way to define the
>>> function?"  OK, well tell me now how to define a function that tests
>>> whether exactly one hole symbol appears in a term...
>>>
>>> - Aaron
>>>
>>> ---- Coq code ----
>>>
>>> Set Implicit Arguments.
>>>
>>> Inductive vector (A: Type): nat -> Type :=
>>> | vnil: vector A O
>>> | vcons: forall len, A -> vector A len -> vector A (S len).
>>> Implicit Arguments vnil [A].
>>>
>>> Definition vall (A: Type) (P: A -> Prop)
>>> : forall len: nat, vector A len -> Prop :=
>>>  fix vall' (len: nat) (xs: vector A len) {struct xs}: Prop :=
>>>   match xs in vector _ len' return Prop with
>>>   | vnil => True
>>>   | vcons len1 a xs1 => P a /\ vall' len1 xs1
>>>   end.
>>>
>>> Record signature: Type := mk_signature {
>>>  symbol: Set;
>>>  arity: symbol -> nat
>>> }.
>>>
>>> Inductive term (S: signature): Type :=
>>> | term_app: forall a: symbol S, vector (term S) (arity S a) -> term S.
>>>
>>> Fixpoint all_term
>>>  (S: signature) (P: symbol S -> Prop) (t: term S) {struct t}: Prop :=
>>>  match t with
>>>  | term_app a ts => P a /\ vall (@all_term S P) ts
>>>  end.
>>>
>>> Definition context_signature (S: signature): signature :=
>>>  let context_symbol := option (symbol S) in
>>>  let context_arity a :=
>>>   match a with
>>>   | Some a1 => arity S a1
>>>   | None => 0
>>>   end
>>>  in
>>>  @mk_signature context_symbol context_arity.
>>>
>>> Definition context (S: signature): Type :=
>>>  term (context_signature S).
>>>
>>> Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
>>>  match c with
>>>  | term_app (Some a) cs => vall (@no_hole S) cs
>>>  | term_app None _ => False
>>>  end.
>>>
>>> Definition no_hole_from_all_term (S: signature): context S -> Prop :=
>>>  let isnt_hole (a: symbol (context_signature S)): Prop :=
>>>   match a with
>>>   | Some _ => True
>>>   | None => False
>>>   end
>>>  in
>>>  all_term isnt_hole.
>>>
>>> --------------------------------------------------------
>>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>>         http://pauillac.inria.fr/bin/wilma/coq-club
>>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>>
>>
>> --
>> Russell O'Connor                                      <http://r6.ca/>
>> ``All talk about `theft,''' the general counsel of the American Graphophone
>> Company wrote, ``is the merest claptrap, for there exists no property in
>> ideas musical, literary or artistic, except as defined by statute.''
>>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Bruno Barras]

Stéphane Lescuyer a écrit :

> Note that the intermediary pattern variable 'a' (introduced
> explicitely by Russell's variant, and not in the original version)
> actually appears in the arguments of vall. If you try a version of
> terms where the length does not depend on the symbol, say :
>
> Record signature : Type := mk_signature  {
>   symbol : Set;
>   arity : nat
> }.
> Inductive term (S: signature): Type :=
> | term_app: forall a: symbol S, vector (term S) (arity S) -> term S.
>
> Then your original definition works fine.
>
> I don't know quite what to make of it, but this definitely looks like
> a bug and gives a good hint as to where to start investigating.
>
> Stephane

Hi,

This is not exactly a bug.
match tries to be smart when matching on constructor arguments upon
which further arguments depend. Here, the type of cs depends on a. When
you match on a (by deep matching on c), the match macro automatically
generalizes cs so that its type gets more precise. As the error message
says, the expanded fixpoint body (of Aaron's attempt) is:

fun (S : signature) (c : context S) =>
  match c with
  | term_app a0 cs =>
      match a0 with
      | Some a =>
          fun cs0 =>
           @vall (context S) (no_hole S)
            (arity (context_signature S) (@Some (symbol S) a)) cs0
      | None => fun _ => False
      end cs
  end

Unfortunately, this generalization-match-then-introduction is too much
for the termination-checker: it cannot see that cs0 is actually the same
vector as cs.

By splitting the match as Russell did, this automatic generalization is
not done, so recursive calls are really made on cs, which is accepted.

If you really need the most precise type for cs (this is not the case
here), then you could make the match on a0 generate equality (a0 = Some
a) and rewrite the type of cs (the guard condition knows that (match e
return ... with refl_equal => cs end) has the same size as cs). I must
admit this is quite painful to do by hand.

Hope this helps,
Bruno Barras.


--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Lescuyer-3]

Hi Bruno,

Thank you for your explanation, this makes perfect sense indeed, once
you know what's going on under the hood. The issue here is how do you
know the expression which is actually fed to the typechecker ? My
error message only shows the typing context and not the whole fixpoint
body :

Recursive definition of no_hole is ill-formed.
In environment
no_hole : forall S : signature, context S -> Prop
S : signature
c : context S
...
Recursive call to no_hole has principal argument equal to
"a1" instead of cs.

So I can actually see the two cs, cs0 and the corresponding a, a0
which can help understand what's going on, but is there any option
that I'm unaware of which displays the whole fixpoint body ? That
would be pretty useful in such circumstances.

Stéphane L.


2009/9/22 Bruno Barras <bruno.barras@...>:

> This is not exactly a bug.
> match tries to be smart when matching on constructor arguments upon which
> further arguments depend. Here, the type of cs depends on a. When you match
> on a (by deep matching on c), the match macro automatically generalizes cs
> so that its type gets more precise. As the error message says, the expanded
> fixpoint body (of Aaron's attempt) is:
>
> fun (S : signature) (c : context S) =>
>  match c with
>  | term_app a0 cs =>
>     match a0 with
>     | Some a =>
>         fun cs0 =>
>          @vall (context S) (no_hole S)
>           (arity (context_signature S) (@Some (symbol S) a)) cs0
>     | None => fun _ => False
>     end cs
>  end
>
> Unfortunately, this generalization-match-then-introduction is too much for
> the termination-checker: it cannot see that cs0 is actually the same vector
> as cs.
>
> By splitting the match as Russell did, this automatic generalization is not
> done, so recursive calls are really made on cs, which is accepted.
>
> If you really need the most precise type for cs (this is not the case here),
> then you could make the match on a0 generate equality (a0 = Some a) and
> rewrite the type of cs (the guard condition knows that (match e return ...
> with refl_equal => cs end) has the same size as cs). I must admit this is
> quite painful to do by hand.
>
> Hope this helps,
> Bruno Barras.
>
>
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Matthieu Sozeau]

Hi Stéphane,

Le 22 sept. 09 à 09:54, Stéphane Lescuyer a écrit :

> Hi Bruno,
>
> Thank you for your explanation, this makes perfect sense indeed, once
> you know what's going on under the hood. The issue here is how do you
> know the expression which is actually fed to the typechecker ? My
> error message only shows the typing context and not the whole fixpoint
> body :
>
> Recursive definition of no_hole is ill-formed.
> In environment
> no_hole : forall S : signature, context S -> Prop
> S : signature
> c : context S
> ...
> Recursive call to no_hole has principal argument equal to
> "a1" instead of cs.
>
> So I can actually see the two cs, cs0 and the corresponding a, a0
> which can help understand what's going on, but is there any option
> that I'm unaware of which displays the whole fixpoint body ? That
> would be pretty useful in such circumstances.

I added this info to the message in the trunk, it will be part of the
next version.

-- Matthieu

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club