> I'm interested in proving termination of nested functions and I
> have some questions:
>
> 1- First I noticed that HOL is able to prove the termination of
> this definition
> automatically:
>
> Define `(ack 0 y = 1 + y)
> /\ (ack (SUC u) 0 = ack u (SUC 0))
> /\ (ack (SUC u) (SUC v) = ack u (ack (SUC u) v))`;
>
> I want to know how, because I'm tried to prove it manually using
> Hol_defn and
> I couldn't.
>
Lexicographic combination of <. If you apply TotalDefn.guessR to the
result of Hol_defn on the above recursion equations, you get the
"guesses" that the automated termination prover makes when trying
to find a suitable termination relation. In the above case, there are
two:
- TotalDefn.guessR defn;
> val it =
[``inv_image $< (\(x,y). x + y)``,
``inv_image ($< LEX $<) (\(v1,v2). (v1,v2))``] : term list
and the second one works.
> 2 - Although the function above can be proved automatically the
> following can't:
>
> Define `ack x y = if (x = 0) then (1 + y) else
> if (y = 0) then (ack (x - 1) 1) else
> ack (x - 1) (ack x (y - 1))`;
>
> I wanted to know why, and again if it is possible to prove it
> manually.
>
In recent versions of HOL-4 this is proved automatically.
> 3 - I want to know if it is possible to prove termination of a
> function like this:
>
> val defn = Hol_defn "nest" `nest x = if x = 0 then 0 else nest
> (nest x-1)`
>
No. Your recursive call is ((nest x) - 1). You probably meant to
write (nest (x-1)), and when the function is defined that way, it is
possible to show termination. It's not obvious how to do this, though,
since there is a bit of an involved story. First, the termination
conditions
that need to be proved are phrased in terms of an auxiliary function
"nest_aux":
?R. WF R /\ (!x. ~(x = 0) ==> R (x - 1) x) /\
!x. ~(x = 0) ==> R (nest_aux R (x - 1)) x
The equations and induction theorem for nest_aux can be extracted from
the defn datastructure. They also have to be instantiated to the
desired termination relation (less-than, in this case). Once
instantiated with (<), some of the constraints on the induction
theorem and recursion equations can be eliminated, via Defn.prove_tcs.
val nest_aux_defn = Defn.set_reln (valOf (Defn.aux_defn defn)) ``
(<)``;
val nest_aux_defn' = Defn.prove_tcs nest_aux_defn
(SIMP_TAC arith_ss [prim_recTheory.WF_LESS]);
val nest_aux_ind = valOf (Defn.ind_of nest_aux_defn');
val [E] = Defn.eqns_of nest_aux_defn';
Now the termination proof can most easily be accomplished by proving
that
nest_aux (<) is the constant 0 function, and this is done by
induction with
nest_aux_ind':
val nest_aux_thm = Q.prove
(`!n. nest_aux (<) n = 0`,
recInduct nest_aux_ind' THEN
REPEAT STRIP_TAC THEN RW_TAC arith_ss [DISCH_ALL E]);
With this theorem in hand, termination is quite simple to prove:
val (nest_def,nest_ind) =
Defn.tprove
(defn, WF_REL_TAC `$<` THEN RW_TAC arith_ss [nest_aux_thm]);
which yields the desired recursion equations and induction theorem
for nest:
val nest_def = |- nest x = (if x = 0 then 0 else nest (nest (x -
1)))
val nest_ind =
|- !P. (!x. (~(x = 0) ==> P (nest (x - 1))) /\
(~(x = 0) ==> P (x - 1)) ==> P x) ==> !v. P v
There is some detail on this approach in Chapter 4 of
http://www.cs.utah.edu/~slind/papers/phd.html
Konrad.
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
