[Why3-club] cannot prove termination
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.
>> 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 <mailto:Why3-club at lists.gforge.inria.fr>
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> <mailto:Why3-club at lists.gforge.inria.fr>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club