Adapting the ARI format for ITSs

[ffrohn]

Currently, we have two different formats for ITSs, the .koat format for "Complexity of ITSs" and an S-expression based format for "Termination of ITSs". It would be nice to have a uniform format. For consistency, I think we should also adapt the ARI format. Here's a first proposal:

       ITS ::= ( format ITS ) fun* rule*
       fun ::= ( fun identifier number )
      rule ::= ( rule lhs rhs guard? )
       lhs ::= ( identifier identifier+ )
       rhs ::= ( identifier expression+ )
     guard ::= ( :guard ( and atom+ ) )
      atom ::= ( op expression expression )
        op ::= > | < | >= | <= | =
expression ::= number | identifier | add | sub | negate | mult
       add ::= ( + expression+ )
       sub ::= ( - expression expression )
    negate ::= ( - expression )
      mult ::= ( * number expression ) | ( * expression number ) 

Since we'd need to implement the conversions from the two existing formats, switching to such a format might not be feasible for 2024, but rather for 2025.

What do you think?

[AkihisaYamada]

I like this as it will be a subclass of ARI LCTRS (modulo preambles).

[nilslommen]

The .koat-Format also allows (non-negative) costs for transitions/rules. I suggest to extend your proposal by such a notation, too. E.g.,
rule ::= ( rule lhs rhs guard? costs?) and costs ::= expression.

If I understand your expressions correctly, then mult ::= ( * number expression ) | ( * expression number ) does not allow non-linear arithmetic. So, I propose to change it to mult ::= ( * expression expression ).

Furthermore, I personally prefer infix notation instead of prefix notation in expressions as it is more human-readable.

[jwaldmann]

prefer infix notation ...

S-expressions with infix operators seem quite bizarre to me. (Want infix? Then use Agda!)

LISP does fine with prefix only, SMTLIB wisely copied that, so why don't you copy them (keep copying them), whenever possible.

And .. some fine day, SMTLIB might want to include rewriting (e.g., ITS) constraints?

[nilslommen]

In the end, it depends on what this format is supposed to achieve. Do we want a more human-readable format or a format which admits easier parsers? For the former I prefer infix notation, for the latter a format based on S-expressions is more suitable.

[ffrohn]

Neither, in my opinion. The .koat format is easy to read & parse. I rather think the goal is to have a uniform format for all termCOMP and CoCo categories (except programming languages, of course), to establish a de-facto standard for the community (similar to SMT-Lib for SMT and the TPTP format for first-order theorem proving).

[ffrohn]

The .koat-Format also allows (non-negative) costs for transitions/rules. I suggest to extend your proposal by such a notation, too. E.g., rule ::= ( rule lhs rhs guard? costs?) and costs ::= expression.

That's an extension which is not supported by all tools that participated in the past. The original format is described here.

If I understand your expressions correctly, then mult ::= ( * number expression ) | ( * expression number ) does not allow non-linear arithmetic. So, I propose to change it to mult ::= ( * expression expression ).

Yes, that was on purpose.

I think the question is: What's the goal of this category, in particular if we also have a complexity category for C (with unbounded integers). From my point of view, the main advantage of a dedicated category for ITSs is that it's a lot easier to enter the competition for new tools. Hence, the goal of my proposal was to keep the format as simple as possible.

Moreover, if we add more features, it's difficult to draw the line. What about disjunctions? Non-tail recursion? Booleans? ...

I know that the TPDB contains examples with non-linear arithmetic (twn*.koat and size*.koat), but these examples are duplicates of the corresponding examples from Complexity_C_Integer, so they won't be lost.

[juergengiesl]

I think that it would be a pity to restrict the ITS category to linear arithmetic. The original concept and format of ITSs allowed non-linear arithmetic as well and I don't think it is a good idea to remove that. If a tool cannot prove anything for examples with non-linear arithmetic, then it can just return "MAYBE" for these examples.

I also think that adding costs to the format would make sense, because many formalisms with integer programs consider costs. Then there is also a clear reason to have ITSs in addition to C_Integer, because costs would be available for ITSs, but not for C.

[ffrohn]

The idea of my proposal was to keep the format as simple as possible to make life easy for new participants, but we can of course also use a more complex format. Then I'd propose to simply restrict the LCTRS format by changing the definition of rule as above:

      rule ::= ( rule lhs rhs guard? )
       lhs ::= ( identifier identifier+ )
       rhs ::= ( identifier expression+ )

Then one can just import a suitable SMT theory (like LIA or NIA), and ITSs are a proper sub-class of LCTRSs. In this way, it's also easy to split the benchmarks if we want to have separate categories for different theories at some point.

Regarding costs, we should use the same format as here, and I don't see a reason for considering non-negative costs only. Negative costs make perfect sense, e.g., to model free when analyzing space complexity.

Then there is also a clear reason to have ITSs in addition to C_Integer

C Integer Complexity will be replaced by C Complexity, see here.

[AkihisaYamada]

I agree that format allow different theories. We called the concept "logic transition systems" here.
But be careful, SMT theory is "Ints", not LIA or NIA. The latter are called "logic", and ARI doesn't specify logic. Obviously, we should ensure that ITS category will not have theories other than Ints.

[ffrohn]

Right, I always confuse the meaning of "theory" and "logic" in SMT-LIB.

So then we'd have the following:

• we extend LCTRSs with costs (details can be discussed here)
• an ITRS is an LCTRS with theory Ints
• an LTS is an LCTRS where rules are restricted as above
• an ITS is an LTS with theory Ints

If there's interest in other theories in the future, there's no need to discuss details of the format -- we can simply exchange the theory. Is that okay for everybody?

[ffrohn]

I discussed this proposal with the KoAT team. This

an LTS is an LCTRS where rules are restricted as above
an ITS is an LTS with theory Ints

seems to be okay for everyone.

However, this

we extend LCTRSs with costs (details can be discussed here)

is problematic. @eleanoremeyer pointed out that negative costs result in semantic issues in the probabilistic setting. Requiring that the costs are non-negative is also problematic, as it's not even decidable. So the remaining options are

• no costs
• non-negative constant costs only

The latter corresponds to the agreement for relative rewriting.

I'd propose to do it as for TRSs. There, relative rules are allowed by default in complexity categories, but there's a dedicated category for relative termination. Analogously, we could allow non-negative constant costs in ITS Complexity, but not in ITS Termination. If there's interest in relative termination of ITSs, we can create a corresponding category.

[ffrohn]

I'll start working on the conversion soon. So if you're not happy with the last proposal, please speak out now.

[ffrohn]

I converted the ITS both for termination and complexity analysis to the new format. I'll add documentation for the format and the converter soon.

[ffrohn]

The converter (with some documentation) is here. Documentation for the new format is here.

Let me know if there are any issues.