Integer Transition Systems

The Integer Transition Systems category is concerned with the question "Will every possible sequence of rewrite steps on an integer program terminate?".

Syntax & Semantic

Integer Transition Systems (ITSs) are LCTRSs with the following restrictions:

• The theory is always Ints.
• Rules must comply with the following grammar:

rule ::= (rule lhs rhs (:guard term)? (:var (vars))?)
lhs  ::= (identifier identifier+)
rhs  ::= (identifier term+)

Moreover, ITSs must declare one and only one entrypoint

entrypoint ::= (entrypoint identifier)

where the given identifier refers to a previously declared function symbol.

The goal is to prove termination w.r.t. all well-sorted startterms of the form

(f c_1 ... c_k)

where f is the entrypoint and c_1,...,c_k are constants from the theory Ints (i.e., integers or Booleans).

Problem

Input: An ITS R.

Question: Does R terminate?

Possible Outputs:

• "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
• "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence of R.
• "MAYBE" (indicating that the solver cannot prove termination of R).