[Why3-club] cannot prove termination

Cláudio Amaral coa at dcc.fc.up.pt
Wed Nov 13 00:19:41 CET 2013


Yes, that is the algorithm's intention.

The size of the list increases but the head of the list is smaller. It
actually works out and terminates.
I think that flattening of heterogeneous lists of lists is a close example
(with the weird step f ((x:xs):xss) = f (x:(xs:xss))), although

It would be nice if I could tell why3 something to help it noticing the
arguments are 'smaller' in the recursive call


On Tue, Nov 12, 2013 at 10:56 PM, Mário Pereira <mariojppereira at gmail.com>wrote:

>  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 listWhy3-club at lists.gforge.inria.frhttp://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
>
>
> _______________________________________________
> 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/d2cc3e2c/attachment.html>


More information about the Why3-club mailing list