new format for SRSs -- poll

[ffrohn]

See this discussion for details.

Suggestions for a dedicated format are:

• (a a b b)
• [a a b b]

A restricted version of the ARI format could, e.g., be defined as follows:

 SRS ::= ( format SRS ) fun* rule*
 fun ::= ( fun identifier 1 )
rule ::= ( rule term term )
term ::= identifier | ( identifier term )

[AkihisaYamada]

Another option would be just the unary subset of ARI-TRSs.

[ffrohn]

How does that differ from the 2nd option? Do you mean that we shouldn't modify the grammar, but just add the side-condition that all function symbols have to have arity 1?

[AkihisaYamada]

Yes, I mean just to use (format TRS). I'd reserve (format SRS) for those who actually want to parse specialized syntax, in this case.

[ffrohn]

Okay, I'd say that's also covered by "a restricted version of the ARI format". The grammar is just an example / a starting point for a discussion. Let's first decide whether we want to use the ARI format or something else, and then we can discuss the details afterwards.

[DieterHofbauer]

Whatever will be defined, please do not forget to allow empty left hand sides of rules. Also for TRS, a variable should be allowed as a left hand side -- think of relative termination.