Hi Konrad, thank you very much again for all the time and answers. They have been very helpful in my work.
Cheers, Augusto On Apr 18, 2008, at 12:07 AM, Konrad Slind wrote: > > >> 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
