[Why3-club] cannot prove termination

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


For the smaller example I gave I did not think about it... but something on
the lines of number of A's and C's in the whole lists. It is easy(-ish) to
do in a variant, but if possible it could be better (automatic proving
-wise) if Why3 did it directly.

I guess the question is more: What type structures can Why3 easily deduce
termination for?

/Cláudio


On Wed, Nov 13, 2013 at 12:03 AM, Mário Pereira <mariojppereira at gmail.com>wrote:

>  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>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/20131113/301d1b8a/attachment-0001.html>


More information about the Why3-club mailing list