On Feb 6, 2008, at 12:54 PM, [EMAIL PROTECTED] wrote: > I am trying to defining two mutually recursive funtions. I have to > prove termination. > HOL has introduced INL and INR defined in the sumTheory. Their > introduction has caused a problem for me.
Right. Mutually recursive functions are modelled by a single function over a sum type. Chapter 4 of http://www.cs.utah.edu/~slind/papers/phd.ps.gz spells out the details. > I tried to apply SUM_ss to > check if it can help in simplifying, it fails. Your problem is not with SUM_ss, which is already incorporated into std_ss, arith_ss, and list_ss. What you need to do is come up with a termination relation that operates over the sum type ``:real + real``. For simplicity, I translated your problem to one over nums instead, but the idea should transfer. First, set up the definition and extract termination conditions: val defn = Hol_defn "fn1fn2" `(fn1 x = if x = 0 then 1 else fn1 (x-1) + (fn2 (x-1) - fn2 (x-2))) /\ (fn2 x = if x = 0 then 1 else fn2 (x-1) + (fn1 (x-1) - fn1 (x-2)))`; Then use the sometimes useful function TotalDefn.guessR, which guesses a standard collection of termination measures. Some will work, some won't. TotalDefn.guessR defn; > val it = [``inv_image $< (\v. 0)``, ``inv_image $< (sum_size (\x. x) (\x. x))``] : term list In this case, the second one works: it just measures the size of the injected argument. - val [_,R] = it; > val R = ``inv_image $< (sum_size (\x. x) (\x. x))`` : term - Defn.tgoal defn; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: ?R. WF R /\ (!x. ~(x = 0) ==> R (INL (x - 1)) (INL x)) /\ (!x. ~(x = 0) ==> R (INL (x - 1)) (INR x)) /\ (!x. ~(x = 0) ==> R (INL (x - 2)) (INR x)) /\ (!x. ~(x = 0) ==> R (INR (x - 1)) (INL x)) /\ (!x. ~(x = 0) ==> R (INR (x - 1)) (INR x)) /\ !x. ~(x = 0) ==> R (INR (x - 2)) (INL x) - e (WF_REL_TAC `^R`); OK.. > val it = Initial goal proved. |- ((fn1 x = (if x = 0 then 1 else fn1 (x - 1) + (fn2 (x - 1) - fn2 (x - 2)))) /\ (fn2 x = (if x = 0 then 1 else fn2 (x - 1) + (fn1 (x - 1) - fn1 (x - 2))))) /\ !P0 P1. (!x. (~(x = 0) ==> P0 (x - 1)) /\ (~(x = 0) ==> P1 (x - 1)) /\ (~(x = 0) ==> P1 (x - 2)) ==> P0 x) /\ (!x. (~(x = 0) ==> P0 (x - 1)) /\ (~(x = 0) ==> P0 (x - 2)) /\ (~(x = 0) ==> P1 (x - 1)) ==> P1 x) ==> (!v0. P0 v0) /\ !v0. P1 v0 : goalstack Konrad. > Following is the complete trace with the two erros that I got. I konw > why I am getting the first error, how can we go around. Why I am > getting the second error. > > val TwoMutalRecursive_defn = Hol_defn "TwoMutalRecursive" > `(E x:real = > if x <= 0 then 1 else > E (x - 1) + (F(x - 1) - F(x-2))) > /\ > (F x:real = > if x <= 0 then 1 else > F (x - 1) + (E(x - 1) - E(x-2))) > `; > <<HOL message: more than one resolution of overloading was possible>> >> val TwoMutalRecursive_defn = > HOL function definition (mutual recursion) > > Equation(s) : > [.......] > |- E x = (if x <= 0 then 1 else E (x - 1) + (F (x - 1) - F (x > - 2))) > [.......] > |- F x = (if x <= 0 then 1 else F (x - 1) + (E (x - 1) - E (x > - 2))) > > Induction : > [.......] > |- !P0 P1. > (!x. > (~(x <= 0) ==> P0 (x - 1)) /\ (~(x <= 0) ==> P1 (x - > 1)) /\ > (~(x <= 0) ==> P1 (x - 2)) ==> > P0 x) /\ > (!x. > (~(x <= 0) ==> P0 (x - 1)) /\ (~(x <= 0) ==> P0 (x - > 2)) /\ > (~(x <= 0) ==> P1 (x - 1)) ==> > P1 x) ==> > (!v0. P0 v0) /\ !v0. P1 v0 > > Termination conditions : > 0. !x. ~(x <= 0) ==> R (INL (x - 1)) (INL x) > 1. !x. ~(x <= 0) ==> R (INL (x - 1)) (INR x) > 2. !x. ~(x <= 0) ==> R (INL (x - 2)) (INR x) > 3. !x. ~(x <= 0) ==> R (INR (x - 1)) (INL x) > 4. !x. ~(x <= 0) ==> R (INR (x - 1)) (INR x) > 5. !x. ~(x <= 0) ==> R (INR (x - 2)) (INL x) > 6. WF R : defn > - - Defn.tgoal TwoMutalRecursive_defn; >> val it = > Proof manager status: 1 proof. > 1. Incomplete: > Initial goal: > ?R. > WF R /\ (!x. ~(x <= 0) ==> R (INL (x - 1)) (INL x)) /\ > (!x. ~(x <= 0) ==> R (INL (x - 1)) (INR x)) /\ > (!x. ~(x <= 0) ==> R (INL (x - 2)) (INR x)) /\ > (!x. ~(x <= 0) ==> R (INR (x - 1)) (INL x)) /\ > (!x. ~(x <= 0) ==> R (INR (x - 1)) (INR x)) /\ > !x. ~(x <= 0) ==> R (INR (x - 2)) (INL x) > > > : proofs > ERROR 1: > e (WF_REL_TAC `measure(\x. clg x)`); > OK.. > Type inference failure: the term > measure (\(x :real). clg x) > on line 50, characters 18-35 > which has type > :real -> real -> bool > can not be constrained to be of type > :real + real -> real + real -> bool > unification failure message: unify failed > Exception raised at Tactical.THENL: > at Tactical.THEN: > at Preterm.typecheck: > between frag 0 row 0 col 1 and line 50, character 36: > failed > ! Uncaught exception: > ! HOL_ERR > - > ERROR 2: > - e(RW_TAC SUM_ss []); > ! Toplevel input: > ! e(RW_TAC SUM_ss []); > ! ^^^^^^ > ! Type clash: expression of type > ! ssfrag > ! cannot have type > ! simpset > - > Walid > > > ---------------------------------------------------------------------- > --- > This SF.net email is sponsored by: Microsoft > Defy all challenges. Microsoft(R) Visual Studio 2008. > http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
