Hi John, thanks for the help, but I came to that conclusion myself after the last help Konrad gave me. Yes, the proof is sound, the program will indeed terminate with an error. To ensure that it terminates without an error is a different matter. But anyway, thanks for the input.
Cheers, Augusto On Apr 10, 2008, at 6:34 PM, John Harrison wrote: > > Hi Augusto, > > | 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. > > I don't see why you say that. The call faa(2) generates a recursive > call to faa(1), but then the x >= 2 guard fails and you return ARB. > Here's a similar function in OCaml: > > # let rec faa x = if x >= 2 then if x=3 then 3 else faa(x-1) else > 9999;; > val faa : int -> int = <fun> > # faa 2;; > val it : int = 9999 > > On the question of "soundness", it might also be useful to distinguish > two things: > > 1. The function would, when executed in a programming language, > terminate > > 2. Adding the definition is logically consistent > > In general a definition may satisfy (2) without satisfying (1). In > particular, any tail-recursive definition satisfies (2), as J Moore > once pointed out to me. For example: > > f(x) = f(x + 1) > > is obviously not terminating. But it is entirely logically consistent, > because you could have defined, say > > f(x) = 42 > > and it would satisfy that recursion equation. > > John. ------------------------------------------------------------------------- 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
