Using the ARI format at termCOMP

[ffrohn]

Following up on the corresponding discussion on termtools, we (the termCOMP SC) proposes to use the ARI format in the future. The current specification of the format covers the following categories:

• TRS Standard / Innermost / Outermost
• SRS Standard
• TRS Conditional (where we only need cond-type oriented, I think)
• TRS Context Sensitive
• full / innermost / parallel innermost runtime complexity
• full / innermost derivational complexity

Then the goal of the analysis (i.e., the rewrite strategy and termination vs runtime / derivational complexity) would no longer be stored in the same file as the TRS. These information could be provided explicitly, or they could be implicitly fixed per category (I'd prefer the latter).

I'll open separate discussions for the remaining TRS categories (Equational and Relative Rewriting) that are not yet covered by the ARI format.

A converter from the XTC format to the ARI format is work in progress. From my point of view, the following question is quite important:

Would somebody drop out of the competition due to lack of resources for implementing a parser for the ARI format?

In that case, we'd have to think about also providing a converter from ARI to XTC. Then we'd have to discuss what happens if the converter is buggy (we've had this issue in the category "termination of integer transition systems" in the past).

[jwaldmann]

(half joking) what will happen for SRS? You mention it above, but I don't see it in the text that you linked ( http://project-coco.uibk.ac.at/ARI/) (it's not in the "content" rule of the grammar).

if the people who already work with the ARI format make their parsers available as open-sourced libraries, then adoption should be straightforward? For matchbox: on the linked page, the COCO group publishes trs-conversion (for Haskell), so I think I can use that. (Put it on hackage!)

(other half joking) if you put (A)GPL license on those libraries, then you'd force termination provers to go open source. (good thing.) Oh noh - I cannot use "trs-conversion" because it says "license: none" (in the cabal description) (and hackage would not accept that). Well I think I can write (and publish) my own parser - but it will accept unary symbols only!

[ffrohn]

SRS?

You're right, we should probably define something like:

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

Agreed?

I cannot use "trs-conversion" because it says "license: none"

I already contacted them to clarify if they plan to release it with a proper license, as I want to integrate the conversion from XTC into their tool...

[jwaldmann]

I said "half joking" ... the damage (to world cultural heritage) was already done when we killed "(RULES a a b b -> b b b a a a)". Which several provers still accept ...

Are you suggesting some SRS-specific (sub) grammar, so we can write (a a b b), or do you intend (a (a (b (b x)))) - then that's what the ARI grammar already prescribes?

Readbility by machine is easy - my concern is humans, e.g., showing benchmarks to students.

Here's a thought: Clojure, which generally has s-expression syntax, uses brackets for vectors literals. Assuming [a a b b] is allowed (*) and then de-sugared to a term - what is the name of the variable at the very end? It does not matter, but I recall that CeTA insists that those names are kept.

(*) which would entail that [ and ']' may not be (part of?) an identifier ... ah - the joy of syntax discussions

[ffrohn]

I said "half joking" ...

I know, but still I think that it's a good idea to have a dedicated format for SRSs (which is what you were hinting at, I think), since the restriction from TRSs to SRSs can be specified syntactically.

That's consistent with having separate formats for, e.g., TRSs, CTRSs, and CSTRSs instead of using the format for CSCTRSs for all of them. Still, if you have a parser for CSCTRSs, then that's all you need. So I think it would be reasonable to have a dedicated grammar for SRSs which is a special case of the TRS grammar, so that TRS tools do not have to care about the difference.

Are you suggesting some SRS-specific (sub) grammar, so we can write (a a b b), or do you intend (a (a (b (b x))))

The latter, since I think it's good to have a uniform format.

Readbility by machine is easy

I (partly) disagree -- I have been debugging quite a few parser bugs over the last couple of years...

my concern is humans

I hope / think that S-Expressions are a good trade-off between both, in particular for terms (where prefix notation is quite natural).

ah - the joy of syntax discussions

So let's keep things simple to avoid them ;)

[jwaldmann]

(S (- (e (x (p (r (e (s (s (i (o (n (s (- (a (r (e (- (n (o (t (- (a (- (g (o (o (d (- (t (r (a (d (e (o (f (f (- (f (o (r (- (s (t (r (i (n (g (s x0))))))))))))))))))))))))))))))))))))))))))))))))) ...

[ffrohn]

Let's discuss the new format for SRSs separately.

[AkihisaYamada]

I agree to have an SRS format.
The ARI web page says [ is not excluded from identifiers :( Anyway, as (format SRS) makes the interpretation clear, I think (rule (a b c d) (e f g)) is nice.
My proposal:
SRS ::= ( format SRS ) rule+
rule ::= (rule string string )
string ::= identifier | ( (identifier identifier+)? )

[DieterHofbauer]

We all know that there is no such thing as the right syntactic format. Different use cases come with different and typically incompatible requirements. Here, typical use cases are, among others,

1. manually typing rewrite systems,
2. reading rewrite systems as a human.
3. parsing rewrite systems,
4. processing rewrite systems,
5. automatically generating rewrite systems,
6. archiving rewrite systems.

The same applies to (non)termination proofs and certificates, but in this case I don't see use case 1 to be relevant.

During discussions at WST22, WST23 and partly here, we have often seen these aspects mixed up. For me, only use case 1 is currently not well supported. This has led tool authors to develop new (or reuse old) formats for tests, web interfaces and the like. A unified format for this purpose could be useful, but we also could do without it as long as all other requirements are met.

An analogy: For typing (use case 1) a mathematical formula, LaTeX is appropriate, but for presenting it to an audience (use case 2), we use PDF or the like. In fact, PDF is unreadable ("\202j*G>\326\304i }\206"), but we use software (PDF viewers) to transform it to a readable presentation. For the current XML based format, our community has working tools of this kind to transform systems and proofs into readable form. What's wrong with this presentation (your browser should show nicely align rules and colors)? It is perfectly human readable, and the underlying transformation is easily customizable; XSLT is a rewrite based approach after all. Also (certified) proofs could look pretty, provided cpfHTML.xsl is around.

As a trivial fact, n different formats result in O(n^2) possible conversions. This is a known software anti-pattern, and the solution is to reduce this number to O(n) by introducing one basic format F together with converters from any other format to and from F. A natural choice for F is some XML format, since XML comes with a whole ecosystem of established and reliable tools: Schema definitions plus validating parsers, XSL transformations, language support for all major programming languages, IDE support, even streaming APIs if your concern is huge files, and so on. Many of these tools (e.g., validation and XSL transformations) are part of current browsers, so no further installations are required.

Remarks on the current XML format for TRS and SRS:

No doubt, the current format contains questionable design decisions. (Example: For TRS/SRS, the rules node comprises a sequence of rules plus one relrules child node, which in turn has child nodes of type rule. It would be more natural to have just a sequence of rules, and each rule be tagged as strict or non-strict (by an attribute, e.g.). As an alternative, we could have two sequences of rules, strict rules and non-strict rules.)
PS: As Florian has already pointed out, for the history of moving to XML there is this discussion from 2003 with still interesting comments by Aart (arguing in favour of XML), Albert, Alexander, Alfons, Jürgen and Claude.

Snippets from discussions with comments by me:

• "The current XML format for is terrible." (Example: The specific design decisions for higher-order systems in xtc.xsd has been heavily critized, presumably for good reasons.) Don't blame XML itself for deficiencies of some specific XML language.

• "XML comes with huge files." The current format uses exaggeratedly long element names (e.g., funapp), and elements (e.g., name) where attributes would be better suited. But even now, standard compression algorithms provide a very good compression rate (e.g., for archiving huge proofs, use case 6). In fact, all formats ever discussed differ only by a constant factor in the length of its representations.

• "XML was fashionable in the 90s." XML is a sublanguage of SGML, dating back to 1986 (ISO standard), and it is still fashionable and heavily used in a great variety of application areas. Just one example, apart from industry standards: OSM XML for OpenStreetMap -- and they have huge files indeed.

• "XML doesn't support human readability, and I don't wont to type XML." I fully agree. (Although "XML documents should be human-legible" was one of the design goals for XML.) XML has to be generated by software components.

Remarks on the TPDB formats, dating back to 2004/05:

They are defined by context free grammars plus so called "semantical conditions". If I remember correctly, these grammars were incorrect, inconsistent, and incomplete.

• Example 1: For TRS, listofrules is a blank (whitespace?) separated list of rules (listofrules ::= eps | rule listofrules), whereas for SRS, listofrules is a comma separated list with a trailing comma (listofrules ::= eps | rule , listofrules) after the last rule.
• Example 2: The empty string is not allowed as lhs of a (relative) SRS rule.
  The trailing comma for SRS was always ignored in the real world TPDB, indicating that nobody used the formal definition for parser generation anyway. Corrected (and extended) versions exist, see this definition as used in the web interface of Aprove. PS: Also MnM can still read and write (a restricted and corrected) variant.

Remarks on the new ARI format:

Don't get me wrong: The ARI format looks solid and reasonable, and it is definitely better suited for use case 1 then anything before. It's just that I don't see an urgent need for a new format. If ARI will be used as the basic format for TPDB, the first thing I'll probably do is to write a converter to the previous or some other XML format to continue to benefit from the XML ecosystem.

PS: In the past, it was good practice to complement the introduction of new formats with converters or parsers, see Section Tools at the termination portal. For the ARI format, I find a converter from ARI to COPS, but nothing for XTC. @AkihisaYamada: At Obergurgl, I understood that this was planned?
Although all of us are certainly able to write or generate parsers, it's still a time-consuming and error-prone (and boring) task that I'd like to avoid. Johannes: "Readability by machine is easy." Florian: "I (partly) disagree -- I have been debugging quite a few parser bugs over the last couple of years." I'm definitely with Florian here.

Conclusion:

• Just to improve support for use case 1, not all other use cases should be neglected or abandoned. For tools to participate in the termination competition, use case 1 is irrelevant.

• Let's face it: Syntactic representations of reasonably large trees (terms, rewrite systems, proofs, certificates) are simply not human-readable, regardless of the specific format.

[ffrohn]

Thank you very much for your comments, I agree with many, but not all of them.

Just to improve support for use case 1, not all other use cases should be neglected or abandoned.

True, but I think the ARI format satisfies most of them.

1. manually typing rewrite systems
   Here, ARI is better than XTC.
2. reading rewrite systems as a human
   Here, ARI is better than XTC if you look at the plain files, but we don't have something like xtcHTML.xsl (yet).

For the remaining use cases, I think both XML and S-Expressions are very reasonable.

For tools to participate in the termination competition, use case 1 is irrelevant.

I disagree. For testing, it's very convenient if all tools support a format that can easily be adapted. For examples, if there is a YES-NO conflict, the first thing I usually do is to minimize the system as much as possible. That's quite easy with, e.g., the .koat format for ITSs, but it's very annoying with the XTC format.

Apart from that, I think there is one more (important?) aspect, namely uniformity. More specifically, I think it would be nice to have a uniform format

(1) at termCOMP and
(2) with CoCo.

Regarding (1), the situation for TRSs is fine, but the current zoo of formats for ITSs is terrible, in my opinion (see here and here). So regarding your comment

I don't see an urgent need for a new format

I agree for TRSs, but I disagree for ITSs. Moreover, we're about to introduce new categories (probabilistic TRSs, maybe also probabilistic integer programs). Hence, we have to make decisions about new formats for quite a few categories.

If we want to achieve (1), then these new formats should be variations of the format that we use for TRSs. Moreover, the new formats should not be changed again in a few years, for obvious reasons.

Hence, if we want to achieve (2), then I think we should change the format now.

PS: In the past, it was good practice to complement the introduction of new formats with converters or parsers.

Regarding the transformation ARI --> XTC: The ARI-COPS converter can also export TRSs in the CPF3 format, which is very similar to XTC, as far as I know. So it should be easy to adapt it accordingly.

For the transformation XTC --> ARI, we'll need a converter anyway (if we switch to ARI). Presumably, it will also be implemented in the ARI-COPS converter.

[ffrohn]

Short summary:

• Apparently, nobody would drop out of the competition if we change the format.
• Dieter made some good points for not changing the format. On the other hand, quite a few people contributed to the discussions here and on termtools, and there were very few statements in favor of XTC.
• If we can build upon the ARI-COPS converter, we can presumably have transformations in both directions without too much effort, but it has to be released under a suitable license first.
• It's still unclear how to proceed for SRSs (see here and here).
• For Higher-Order, the details still need to be sorted out.
• I don't think we can/will change the formats for IT(R)Ss this year, so we have plenty of time to finish the corresponding discussions (here and here).
• For all other categories, we reached a consensus, so I closed the corresponding discussions.

[ffrohn]

If we can build upon the ARI-COPS converter, we can presumably have transformations in both directions without too much effort, but it has to be released under a suitable license first.

The ARI converter is now GPL-licensed, see here!

[ffrohn]

Here, the question whether we should adapt the definition of identifiers came up. A problem with the ARI definition is that it clashes with pre-defined SMT-LIB symbols. @AkihisaYamada proposed to change the definition of identifiers to [+\-*/@$%^&_=<>~.].

[ffrohn]

Fabian pointed out that SMT symbol does not start with a digit and is not a reserved word.

Good point, I forgot to quote these in the transformation (but that's easy to fix).

I don't think we want to turn 0 into |0|

From my point of view, |0| would be perfectly fine...

there is no complete list of reserved words

See here, page 95.

I also worry about ! and ?, which are explicitly reserved to the user in Common LISP

I don't think there is such a convention in the SMT-LIB standard. However, if we only allow a subset of the valid SMT-LIB symbols anyway, then it doesn't harm to forbid ! and ? in unquoted identifiers, I guess.

I propose again to stick to the Common LISP letters

Using Common Lisp symbols instead of SMT-LIB symbols is fine for me as well, as long as we stick to an existing standard instead of reinventing the wheel. One big drawback is that you've to pay to access the standard, as far as I can tell. Moreover, I think that 0 is not a valid symbol in Common Lisp either (for good reasons), see here:

if the name of the symbol cannot be mistaken for a number, then the symbol can be notated by the sequence of characters in its name

systematically map other symbols into a string of letters

Then we wouldn't need quoted identifiers, which is nice. On the other hand, it would be quite awful for readability, but it would only affect 220 benchmarks.

However, that does not solve the problem with 0/|0|. We can simply prefix identifiers that start with a digit with $. That wouldn't result in any name clashes on the TPDB, and I think it's still very readable.

[AkihisaYamada]

I'm not proposing to define our identifier as CommonLisp does. (Again, I don't care the format definition, but what TPDB may contain.) I just want to ensure that tools can use any CommonLisp compliant parser.

We can simply prefix identifiers that start with a digit with $. That wouldn't result in any name clashes on the TPDB, and I think it's still very readable.

There are millions of digits in https://github.com/TermCOMP/TPDB/tree/master/SRS_Standard/ICFP_2010. (Well they are SRSs, so if we invent our own format for SRS that'll be fine. But I feel the policy will be inconsistent.)

That said, I agree allowing arbitrary representations of numbers as identifiers can be a problem to some tools. E.g. 0, 0.0, +0 or -0 might be preinterpreted to the same number by a CommonLisp compliant parser.

I think we agree to disallow 1ab etc. as they might be rejected by an SMT-Lib parser. Then options are

1. disallow numbers at all
2. allow numbers that no parser will fail: 0|[1-9][0-9]*
3. allow numbers that are numbers in CommonLisp and identifier in SMT-LIB: +0 etc.

I'd vote for 2 (edit: but I understand 1 with the $-prefixing is also a convenient solution).

[ffrohn]

I just want to ensure that tools can use any CommonLisp compliant parser.

allow numbers that no parser will fail: 0|[1-9][0-9]*

I think these two are contradictory, as Common Lisp compliant parsers will parse 0|[1-9][0-9]* as numbers, not as symbols.

I don't care the format definition, but what TPDB may contain

There's a simple, standard compliant way to allow all identifiers that currently occur in the TPDB: quoted symbols. Any Common Lisp or SMT-LIB compliant parser can deal with them, and with the additional restrictions discussed above (no whitespace, parentheses, or semicolons), they are also easy to parse by hand.

The idea of using URL encoding is nice, but as the discussion above shows, it does not cover all use cases of quoted symbols. Another advantage of quoted symbols is that they are already implemented in the converter. So unless there are more arguments against quoted symbols, I think we should stick to the current definition.

PS: We should come up with our own list of reserved keywords, though. There are some examples with a function symbol called fun in the TPDB, resulting in the declaration

(fun fun 2)

[AkihisaYamada]

allow numbers that no parser will fail: 0|[1-9][0-9]*

I think these two are contradictory, as Common Lisp compliant parsers will parse 0|[1-9][0-9]* as numbers, not as symbols.

One can just say datatype tool_identifier = parser_number | parser_symbol etc.

[AkihisaYamada]

Sorry, the source of this problem is the fact that TPDB has been allowing numbers as identifiers. So I now think we should disallow numbers at all.

For ICFP examples, I propose to rename 1 2 3... to a b c...

[ffrohn]

I started to work on the converter, see here. Essentially, I just plugged Johannes' library into the ARI converter. Current state/limitations:

1. conversion works in both directions
2. so far, I just implemented the conversion for ordinary TRSs
3. the points where we decided to deviate from ARI (i.e., identifiers and variable conditions) are not yet taken into account
4. if you convert from XTC to ARI and back, then the rewrite strategy is lost (as it is not part of the TRS in ARI)
5. the metainformation is lost
6. the line <?xml-stylesheet type="text/xsl" href="../../xml/xtcHTML.xsl"?> is lost

I'll take care of 2. and 3.

I think we cannot do much about 4. Maybe we could add a flag for specifying the rewrite strategy (and other things like termination vs. complexity, startterms, etc.) when converting to XTC.

Regarding 5., @jwaldmann, could you extend your parser to store the metainformation (which is just originalfilename so far)? I think it shouldn't get lost.

Regarding 6., is that a problem? At least for me, the reference to xtcHTML.xsl is not very helpful, as none of my browsers renders it correctly.

[jwaldmann]

I'll look into it jwaldmann/haskell-tpdb#43

[ffrohn]

Short update: The conversion XTC -> ARI is implemented for

• Standard TRSs/SRSs
• Relative TRSs/SRSs
• Equational TRSs
• Conditional TRSs
• Context Sensitive TRSs

Higher order is still missing.

The conversion ARI -> XTC does not work for Equational and Context Sensitive TRSs yet, see here.

Feel free to start testing, I'll create a new repository with the results of transforming the corresponding TPDB categories next week.

[ffrohn]

I just converted the examples from TRS_Standard, see here. I didn't test with the converted benchmarks yet, so let me know if you notice any problems.

[ffrohn]

All first-order TRS categories have been converted.

[ffrohn]

As sanity check, I transformed all TRSs back to XTC and diffed them with the original ones. I found some problems with invalid identifiers, which are now fixed, so that there are no diffs anymore. Hence, I consider the transformation of the first-order TRSs to be complete.

[ffrohn]

I added documentation for the new format to termination-portal.