Adapting the ARI format for ITRSs

[ffrohn]

ITRSs are de facto a special case of LCTRSs, for which ARI has a dedicated format. To avoid a proliferation of different formats, it could be good to use this LCTRS format also for ITRSs. Termination analysis of LCTRSs is supported, e.g., by the tool Ctrl, and there is active work on the tools Cora and Crisys2.

Originally posted by @cfuhs in #85 (reply in thread)

[ffrohn]

True, but LCTRSs are very expressive. They allow...

1. other theories
2. Boolean variables
3. disjunction / negation

Dealing with 1. is easy, we just fix the theory (QF_LIA? QF_NIA?). Regarding 2. and 3., I'm not that familiar with our ITRSs. Are these things allowed in ITRSs as well? Are there other features of LCTRSs that might be problematic? What kind of variable conditions do both formalisms impose (i.e., where do they allow extra variables that do not occur on the left-hand side)?

Other "nasty" feature of SMT-Lib (and hence LCTRSs) are let-expressions, if-then-else, somewhat unexpected functions like divides c where c > 0, ... So if we go for LCTRSs, we might want to restrict ourselves to a subset of SMT-Lib...?

[stefandollase]

The following grammar seems to fit what I want to do.

         ITRS ::= ( format ITRS ) theory+ sort-decl* fun-decl* rule*
       theory ::= ( theory Ints )
    sort-decl ::= ( sort sort )
     fun-decl ::= ( fun identifier type )
         type ::= sort | ( -> sort+ sort )
         sort ::= identifier | Int
         rule ::= ( rule lhs rhs (:cost expression)? (:guard (and atom+))? )
          lhs ::= number | identifier | theory-symbol | ( theory-symbol lhs+ )
          rhs ::=          expression | theory-symbol | ( theory-symbol rhs+ )
theory-symbol ::= identifier

1. expression and atom are the same as for ITSs, see Adapting the ARI format for ITSs #90.
2. expression and atom cannot contain theory-symbols.
3. The left-hand side of a rule can neither be a variable nor a number.
4. For non-int-variables, all variables that occur on the right-hand side also have to occur on the left-hand side.
5. For int-variables, there is no such restriction.
   This allows for rules such as f(x) -> y :|: y<x.
6. Substitutions can neither contain int-operations nor theory-symbols or variables with return type int, i.e., if x is substituted by t, then all int-typed subterms of t are actual integers.
7. All variables in the cost or guard are int-typed.

[ffrohn]

Some comments:

Points 3. and 4. are in contrast to what's discussed here.

Regarding 7. and the definition of rule, I don't think we should restrict the format to conjunctions, forbid Booleans, etc. For ITSs, we'll presumably allow whatever the imported theory defines.

Regarding costs, @juergengiesl pointed out that allowing costs allows for modelling relative rewriting, such that dependency pairs no longer work. So for the termination category, we'll want to / have to forbid costs, most likely.

[jwaldmann]

I don't have all the details available, but if I am reading this right (I hope I'm not)

.. allowing .. such that dependency pairs no longer work. So ... we'll want to / have to forbid ...

No. If one specific proof method does not work for a specific class of problems, then we don't declare these problems illegal, but instead we want to improve the method, or find another one, that does work.

Or do you mean that the DP method is need to define the semantics of problems?

[ffrohn]

Or do you mean that the DP method is need to define the semantics of problems?

No. But so far, we do not have relative rules in the category ITRS Termination, and introducing them changes the problem substantially (I think all tools that ever participated -- AProVE and Ctrl? -- use DPs). So if we want relative rules, we should probably have a dedicated category (analogously to TRS Standard and TRS Relative).

[juergengiesl]

What I meant is that for TRSs, relative rules introduce subtle problems that require completely new proof techniques. The main problems are duplicating relative rules (so this is something that does not occur for SRSs and it also does not occur for ITSs where variables are instantiated by normal forms). The classical example is a TRS with a rule a -> b with cost 1, and a rule f(x) -> c(f(x),x) with cost 0. This TRS is not relatively terminating because of the sequence f(a) -> c(f(a),a) -> c(f(a),b) -> c(c(f(a),a),b) -> c(c(f(a),b),b) -> ...

There are more examples that show that proving termination of relative rules requires fundamentally different techniques than proving termination of ordinary rules. Therefore, it makes sense not add costs for the standard TRS category. And for the same reason it might also make sense not to add costs for ITRSs, to avoid making this even harder than it already is.