Termination prover not strong enough

[acjf3]

The following fails:

val test_def = Define test n l s = if n = 0 then l else test (n - 1) (s::l) s;

All variants fail as well. I actually want something similar to

val test_def = Define test (l, n) s = if n = 0 then l else test (s::l, n - 1) s;

or

val test_def = Define test (n, l) s = if n = 0 then l else test (n - 1, s::l) s;

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[xrchz]

What's wrong with

> Define`(test 0 l s = l) /\ (test (SUC n) l s = test n (s::l) s)`;
<<HOL message: inventing new type variable names: 'a>>
Definition has been stored under "test_def"
val it =
   |- (∀l s. test 0 l s = l) ∧ ∀n l s. test (SUC n) l s = test n (s::l) s:
   thm

?

[acjf3]

This isn't handwritten HOL, it is being generated. Changing the function's form isn't a good/viable option.

[acjf3]

It may be worth noting that HOL can cope with

val test_def = Define test n l = if n = 0 then l else test (n - 1) (T::l);

just fine. That's why I've categorised this issue as bug (the extra argument shouldn't really lead to failure).

[konrad-slind]

val test_def = Define
test n l s = if n = 0 then l else test (n - 1) (s::l) s;

This works fine, for my installation. It may be that I've not checked in
some fix I've made
locally. (My clumsiness with Git has been a disincentive to attempt
checkins.)

Will look into synchronizing my version with the Git version.

Cheers,
Konrad.

On Sat, Nov 3, 2012 at 10:46 AM, acjf3 notifications@github.com wrote:

The following fails:

val test_def = Define
test n l s = if n = 0 then l else test (n - 1) (s::l) s;

All variants fail as well. I actually want something similar to

val test_def = Define
test (l, n) s = if n = 0 then l else test (s::l, n - 1) s;

or

val test_def = Define
test (n, l) s = if n = 0 then l else test (n - 1, s::l) s;

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/101.

[acjf3]

That's good to know. If you can do a check-in then that would be very helpful. If that's looking too painful in the short term then you can always send me the appropriate files and I'll do the check-in.

(The more principled approach would be for you to fork HOL on GitHub. You could then do your public commits/pushes there, without worrying about mucking up mn200/HOL. Other HOL developers could then see what you've got and pull things into mn200/HOL as appropriate.)

[xrchz]

@acjf3 did you receive anything from Konrad regarding this?
I observe that your original test_def now (1fffd4b) appears to work without requiring any manual termination proof.

[acjf3]

I'm not aware of a check-in to address this. Note that the definition of interest

val test_def = Definetest (l, n) s = if n = 0 then l else test (s::l, n - 1) s;

still fails.

[konrad-slind]

Right, I haven't done anything on improving the termination prover, which
really
should get that. It may be interesting to note that currying the function
unpacks the "real" termination problem so that the terminator gets it:

Define test l n s = if n=0 then l else test (s::l) (n-1) s;
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "test_def".
Induction stored under "test_ind".
val it =
|- ∀s n l. test l n s = if n = 0 then l else test (s::l) (n − 1) s: thm

Thinking about it, the problem is that the straightforward application of
the size measure treats the pair

(s::l,n-1)

as increasing by 1 in the first arg and decreasing by 1 in the second arg.
A more
refined approach would be to follow that blunt instrument approach with a
pass that
tried to see if any projection from any argument tuple decreases in size.

Konrad.

On Mon, May 25, 2015 at 3:27 AM, acjf3 notifications@github.com wrote:

I'm not aware of a check-in to address this. Note that the definition of
interest

val test_def = Definetest (l, n) s = if n = 0 then l else test (s::l, n -

1. s;

still fails.

—
Reply to this email directly or view it on GitHub
#101 (comment)
.

[konrad-slind]

Looking at this a bit more, if I swap the order of arguments, Define gets
the termination proof:

Define test1 s (l,n) = if n=0 then l else test1 s (s::l,n-1);
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "test1_def".
Induction stored under "test1_ind".
val it =
|- ∀s n l. test1 s (l,n) = if n = 0 then l else test1 s (s::l,n − 1):
thm

So this is definitely an implementation bug: argument order shouldn't
matter.

(Notes following are possibly understandable to KLS only)
Culprit seems to be TotalDefn.guessR, which in the original only returns the
two candidate WF relations:

guessR defn;
val it =
[inv_image $< (λ(x,y). 0),
inv_image $< (λ(x,v). list_size (λv. 0) (FST x) + SND x)]:
term list

Neither of which work. Swapping argument order lets guessR do the
right thing:

guessR defn1;
val it =
[inv_image $< (λ(x,y). 0),
inv_image $< (λ(v,y). list_size (λv. 0) (FST y) + SND y),
inv_image $< (λ(v1,v2,v3). v3)]:
term list

The last measure works.

Note in TotalDefn about how guessR works:

(---------------------------------------------------------------------------)
(* "guessR" guesses a list of termination measures. Quite ad hoc.
)
( First guess covers recursions on proper subterms, e.g. prim. recs. Next
)
( guess measure sum of sizes of all arguments. Next guess generates
)
( lex-combos for Ackermann-style iterated prim. rec. defs. Finally,
)
( generate all lex combinations of arguments that get changed by known
)
( functions, i.e., ones that have corresponding theorems in ref variable
)
( "termination_simps".
)
( Finally, all generated termination relations are simplified and
)
( duplicates are weeded out.
)
(---------------------------------------------------------------------------*)

On Mon, May 25, 2015 at 1:59 PM, Konrad Slind konrad.slind@gmail.com
wrote:

Right, I haven't done anything on improving the termination prover, which
really
should get that. It may be interesting to note that currying the function
unpacks the "real" termination problem so that the terminator gets it:

Define test l n s = if n=0 then l else test (s::l) (n-1) s;
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "test_def".
Induction stored under "test_ind".
val it =
|- ∀s n l. test l n s = if n = 0 then l else test (s::l) (n − 1) s: thm

Thinking about it, the problem is that the straightforward application of
the size measure treats the pair

(s::l,n-1)

as increasing by 1 in the first arg and decreasing by 1 in the second arg.
A more
refined approach would be to follow that blunt instrument approach with a
pass that
tried to see if any projection from any argument tuple decreases in size.

Konrad.

On Mon, May 25, 2015 at 3:27 AM, acjf3 notifications@github.com wrote:

I'm not aware of a check-in to address this. Note that the definition of
interest

val test_def = Definetest (l, n) s = if n = 0 then l else test (s::l, n

• 1. s;

still fails.

—
Reply to this email directly or view it on GitHub
#101 (comment)
.