[Why3-club] cannot prove termination
mariojppereira at gmail.com
Tue Nov 12 23:56:35 CET 2013
I made a simple example using your function f, and in the last case of
the 'match (x,y) with' the arguments for f actually "grow", i.e., the
lists ts1 and ts2 actually have one more element.
So, there is no structural descent relation between terms, implying 'f'
may not terminate.
On 12-11-2013 22:13, Cláudio Amaral wrote:
> Hello, all!
> I have a function like the following and why3 cannot prove its
> termination. I can make it a 'let rec', but I would like to know more
> about this issue and if it is possible to change something to enable
> the termination proof.
> module Example
> use import list.List
> type t =
> | A
> | C t t
> type r =
> | D
> | E
> function f (ts1: list t) (ts2: list t) (s: r) : r =
> match (ts1,ts2) with
> | (Nil, Nil) -> s
> | (Nil, Cons _ _) -> D
> | (Cons _ _, Nil) -> D
> | (Cons x xs, Cons y ys) ->
> match (x,y) with
> | (A, A) -> f xs ys s
> | (C xx xxs, C yy yys) ->
> f (Cons xx (Cons xxs xs)) (Cons yy (Cons yys ys)) s
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club