[Termtools] Termination Competition 2017 - finished

[Florian Frohn]

Dear all,

regarding the conflicts for innermost runtime complexity: Both examples
essentially implement multiplication via addition. E.g., mul.xml
contains (among others) the following rules:

mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
mul0(Nil,y) -> Nil
add0(Cons(x,xs),y) -> add0(xs,Cons(S,y))
add0(Nil,y) -> y

We think that the cubic lower bounds inferred by AProVE are correct. The
short explanation is: The recursive call to mul0 in the first rule is at
add0's first argument and add0's complexity is linear in its first
argument. If the recursive call was at add0's second argument, then the
complexity would indeed be quadratic.


Here's a more detailed explanation, just in case:

Since the elements of the lists don't matter, we can replace them by
natural numbers, resulting in the following algorithm:

mul(s(x), y) -> add(mul(x, y), y)
mul(0, y) -> 0
add(s(x), y) -> add(x, s(y))
add(0, y) -> y

Clearly, we have

add(x, y) ->^{x+1} x+y

Now we can prove

mul(x, y) ->* x*y

by induction on x:

Induction base: mul(0, y) -> 0

Induction step: mul(x+1, y) -> add(mul(x, y), y) ->_IH
add(x*y, y) ->^{x*y+1} x*y + y

This yields the following recurrences for c(x,y) with
mul(x, y) ->^{c(x,y)} x*y:

c(0,y) = 1
c(x,y) = (x-1)*y+2 + c(x-1)

Thus, we have

c(x,y) = 1+1/2*y*x^2-1/2*y*x+2*x

which is cubic.

Best
Florian


On 09/05/2017 04:56 PM, Johannes Waldmann wrote:
> Dear all,
>
>
> Starexec just finished running the competition jobs.
>
> results: https://termcomp.imn.htwk-leipzig.de/competitions/65
>
> inconsistencies this year:
> https://termcomp.imn.htwk-leipzig.de/problems/False/24394/24399/24400/24402
>
> compare to last year:
> https://termcomp.imn.htwk-leipzig.de/combine/Y2016/65
> (but note https://github.com/jwaldmann/star-exec-presenter/issues/178 )
>
> comments welcome.
>
>
> I will be running the "demonstration categories"
> (with just one participant) tomorrow morning.
>
>
> - Johannes.
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools