Hi, I think i made a mistake when copying the function. What I wanted to show was this (the difference is in the precondition):
Define `faa x = if x >= 2 then if x=3 then 3 else faa(x-1) else ARB`; Now using the ARB I can prove the termination, but the function is clearly not terminating if the input is '2'. This is what I call the unsoundness although maybe the term is not quite correct for this situation. The only way to prove the non termination of this function is using manual proof (Hol_defn) and '(\x.(x-3))'. as measure. I don't know why this happens. Is it because using nats HOL assumes they are going to finish in 0 anyway so the function must terminate because there is no more nats. But in normal programming languages a call for this function with '2' as input would lead to a infinite loop or a run-time error. Cheers, Augusto Silva On Apr 5, 2008, at 3:06 AM, Konrad Slind wrote: > > On Apr 4, 2008, at 9:51 AM, Augusto Ribeiro wrote: > >> Dear All, >> >> Sorry for the extensive background if you prefer please go straight >> to the PROBLEM that is a bit below in the mail. >> >> ------------> BACKGROUND <------------ >> >> I'm trying to use HOL to prove termination of recursive functions >> with preconditions in VDM. What I plan to do is generate the >> termination conditions myself by inspecting the VDM source file and >> then trying to prove them in HOL. I know HOL doesn't support sub- >> typing so what I'm doing at the moment is for example: >> >> f(x) = if (x=3) then 3 else f(x-1) >> precondition: x >= 3 > > One trick for sneaking in subtyping is to define > the function as > > f(x) = > if x >= 3 then > if x = 3 then 3 > else f(x-1) > else ARB > > With that, termination should be proved automatically > by Define. You can subsequently prove > > |- x >= 3 ==> (f x = if x=3 then 3 else f(x-1)) > >> >> >> What is inserted into HOL is a goal like this: >> >> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`; >> >> The thing if I try to prove this using the command: >> >> e (WF_REL_TAC `measure (\x.x)`) >> >> I am successful because '<' is well founded and the rest of the >> equation is true. But the proof is unsound because inserting the >> '(x>=3)' assumption makes this statement "~(x=3) /\ (x>=3) ==> R >> (x-1) x" true. This could be solved if I use (\x.x-3) instead of >> '(\x.x)'. But what I'm trying to do is for use of general use so I >> don't want people to incur in the risk of making unsound proofs. > > There is no danger of unsoundness using WF_REL_TAC, just > of providing a witness relation that doesn't actually lead to > provable termination conditions. > > > Konrad. > > >> >> ------------> PROBLEM <------------ >> >> So what I tried to follow other approach and define the 'measure' >> relation myself, like this: >> >> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`; >> - val measure2 = Define `measure2 f x y = if (x>= 3 /\ y >= 3) then f >> x < f y else F`; >> - e (WF_REL_TAC `measure2 (\x.x)`) >> - e (RW_TAC arith_ss [measure2]) >> >> And using this tactic all goes alright until I get stuck with: >>> val it = >> WF (measure2 (\x. x)) >> >> : goalstack >> Although the relation is well founded because it's just a restriction >> of the Naturals. I couldn't prove it until now. Is there a tactic to >> prove this or at least to do some simplification. I couldn't do >> nothing to continue this proof yet. Or maybe there is other ways to >> do this. Thank you for your time and help. >> >> Cheers, >> Augusto Silva >> >> >> >> --------------------------------------------------------------------- >> ---- >> This SF.net email is sponsored by the 2008 JavaOne(SM) Conference >> Register now and save $200. Hurry, offer ends at 11:59 p.m., >> Monday, April 7! Use priority code J8TLD2. >> 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 > ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Register now and save $200. Hurry, offer ends at 11:59 p.m., Monday, April 7! Use priority code J8TLD2. 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
