[Why3-club] cannot prove termination

Mário Pereira mariojppereira at gmail.com
Wed Nov 13 01:03:53 CET 2013


Ok Cláudio, I believe I understood now. But if you pass this function to 
a 'let rec' form, what variant would you use?

On 12-11-2013 23:19, Cláudio Amaral wrote:
> 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 <mailto: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 list
>>     Why3-club at lists.gforge.inria.fr  <mailto:Why3-club at lists.gforge.inria.fr>
>>     http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
>
>     _______________________________________________
>     Why3-club mailing list
>     Why3-club at lists.gforge.inria.fr
>     <mailto: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/20131113/09675a6d/attachment.html>


More information about the Why3-club mailing list