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
