[Why3-club] cannot prove termination

Mário Pereira mariojppereira at gmail.com
Tue Nov 12 23:56:35 CET 2013


Hi Cláudio.

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.
>
> Cheers
> Cláudio
>
> 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
>     end
>   end
>
> end
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131112/a7c5a2f2/attachment-0001.html>


More information about the Why3-club mailing list