C Integer categories

[ffrohn]

We plan to clean up the categories for integer programs a bit. Currently, there are four categories

1. ITS Termination
2. ITS Complexity
3. C Integer Termination
4. C Integer Complexity

and one program model for each of them:

1. an S-Expression based format
2. the .koat format
3. this fragment of C
4. some fragment of C that isn't specified anywhere -- judging from the examples, it seems like everything but non-integer variables and recursion is allowed

As mentioned here, we might unify the first two formalisms in the future.

The category C Integer Termination suffers from a lack of interesting examples (all but two examples are solved). Moreover, it's just a syntactic variant of ITS Termination.

The formalism for C Integer Complexity is problematic, as there is no specification. Moreover, the model of complexity for this category isn't specified anywhere (C instructions? LLVM instructions? Loop iterations?).

Hence, we propose the following changes:

C Integer Termination

This category should be discontinued. The examples are added to the category C Termination.

C Integer Complexity

I contacted the participants of the ITS and C Integer categories, and apparently there is still interest in having a complexity category with C syntax. Everybody seems to be fine with the following proposal:

• We replace the category C Integer Complexity with a new category C Complexity.
• The initial benchmark set is the one from the C Integer Complexity category.
• We use the same C fragment and semantics as for C Termination.
  • We'd have to adapt the first rule, of course: "The starting point is the main function without arguments." Instead, the entry point should be stated explicitly (as it is the case for the ITS categories). In the C Integer Complexity category, there is just one function per benchmark. So we could use the convention that the entry point can be omitted if there is just one function to make the transition as smooth as possible.
• The notion of complexity is #loop iterations + #execution of gotos + #function invocations. In this way, we do not have to deal with too many low-level details (like C vs. LLVM).
• The size measure for the arguments is part of the input. However, integers are measured by their absolute value, unless specified otherwise.

As the initial benchmark set only contains integer programs, we do not have to fix a formalism for specifying size measures now, but we can postpone that until somebody wants to submit benchmarks with non-integer arguments.

So for the next competition, we'd essentially just change the name, and we'd have proper semantics for the new category. However, we'd allow more complex benchmarks for the future.

If you have comments or questions, please share them.

[ffrohn]

Everybody seems to be happy with the proposal --> closed.