new format for SRSs

[ffrohn]

Let's move this topic to a separate discussion, I'll copy the corresponding comments.

[ffrohn]

(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!

Originally posted by @jwaldmann in #83 (comment)

[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...

Originally posted by @ffrohn in #83 (reply in thread)

[ffrohn]

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

Originally posted by @jwaldmann in #83 (reply in thread)

[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 ;)

Originally posted by @ffrohn in #83 (reply in thread)

[ffrohn]

(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))))))))))))))))))))))))))))))))))))))))))))))))) ...

Originally posted by @jwaldmann in #83 (reply in thread)

[ffrohn]

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+)? )

Originally posted by @AkihisaYamada in #83 (comment)

[ffrohn]

(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))))))))))))))))))))))))))))))))))))))))))))))))) ...

Clearly there are more readable alternatives for SRSs. My main concern is this:

I think it's good to have a uniform format.

Imagine that SMT-Lib would use two different formats, a general one for non-linear arithmetic and a specialized one for linear arithmetic. Then people like us build tools on top of SMT solvers. Some of the SMT problems that our tools have to solve are linear, others are non-linear. Now unfortunately, the most powerful solvers for linear arithmetic only support the specialized format. So you either have twice as much work with your SMT interface, or you stick with the full-fledged solvers and ignore the specialized ones.

Luckily, SMT-Lib uses a uniform format, so I can easily do the following:

if (SMT problem is linear) then use SPASS-SATT else use Z3

As far as I can see, we're in precisely the same situation: I think it's good if

if (TRS is an SRS) then use Matchbox else use AProVE

works without implementing a second interface.

I think (rule (a b c d) (e f g)) is nice

That's also a valid rule according to the TRS format, but there it has a different meaning. That might be quite confusing.

[ffrohn]

I created a poll to see what the majority prefers.

[DieterHofbauer]

The focus should be on the uniformity of formats, further special cases would probably not be a good idea. Adding or removing parentheses is no problem, but I'd like to avoid writing yet another converter from the SRS to the TRS format -- SRS are in fact linear TRS.

[DieterHofbauer]

Important point, apart form syntax discussions: What's the definition of a SRS or TRS? I hope we do agree that an SRS is a set of rules, and a rule is a a pair of arbitrary strings. Similarly, a TRS is a set of rules, and a rule is a pair of arbitrary terms. PLEASE do not stick to the definition in Baader/Nipkow and the like. This makes rewrite systems much nicer mathematical objects; e. g., the inverse of a rewrite system is again a rewrite system. So as a left hand side, we should allow an empty string for SRS, similarly a single variable for TRS. Also for relative termination, this makes relevant statements possible in the first place (example: a a -> a b a is terminating relative to epsilon -> b).

For TRS also extra variables in right hand sides should be possible, for the same reason (nicer mathematical objects). (Question: What is the induced rewrite relation? Answer: Instantiate variables by arbitrary terms.) This was allowed before (e. g., in Transformed_CSR_04/PEANO_nosorts-noand_L), so please keep it this way.

Quoting Büchi (1989): "You will ask, why include the monsters? I give you three reasons: 1) A nice theorem may go through for [the] general [definition]; monsters share some important properties with the good boys. 2) Monsters are useful as counterexamples to happy conjectures; they serve to sharpen one's idea about the real things. 3) What looks like a monster to one person may be a useful member of society to the other. The other (he may be you at a later date) may have deeper thoughts on the matter, and may be right!"

[ffrohn]

I think this question definitely deserves it's own discussion.

[ffrohn]

We got a draw in the poll, which is the worst possible outcome. However, we have one vote for XTC from Dieter, and he also made clear that he's in favor of a uniform format. I'd say that tips the scales in favor of ARI. If you have a better idea to break the tie, please let me know ;)

[DieterHofbauer]

Just to avoid any misunderstandings: This issue no longer appears to be controversial, referring to more recent papers. Quoting Aart: "We do not impose the common variable conditions, i.e., the restriction that \ell is not a variable and all variables in r are contained in \ell."

[jwaldmann]

... (rule (a b c d) (e f g)) is nice

That's also a valid rule according to the TRS format, but there it has a different meaning.

Indeed. By all means avoid that.

My proposal (referring to Clojure) was (rule [a b c d] [e f g h]) and prohibit [ ] (also other forms of parentheses and punctuation) as parts of identifiers. (see below.)

We don't have new insights or arguments here? So I'm fine with what the committee decides.

[enter rant mode] [deleted]

[ffrohn]

instead of re-inventing the wheel, the definition of identifier (and of many other things) should be/should have been copied from SMTLIB

What other things do you mean?

have we already discussed number formats

Here's the ARI definition of LCTRSs.

[AkihisaYamada]

... (rule (a b c d) (e f g)) is nice

That's also a valid rule according to the TRS format, but there it has a different meaning.

Indeed. By all means avoid that.

I don't think the syntax should depend on the "meaning". The string "(a b c)" can mean $a(b,c)$ or $a(b(c(x)))$ or $((a b) c)$, etc.

[AkihisaYamada]

and the semantics is specified by the competition categories. The $a(b,c)$-semantics is due to the TRS categories.

[AkihisaYamada]

That said, I'm not strongly against using [a b c]. Then I propose to limit symbols in identifiers as in Common Lisp, i.e., [+\-*/@$%^&_=<>~.], in general TPDB.
Cf. https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node27.html

[jwaldmann]

re: ARI LCTRS bitvector example: what is the token class of #x00000002? it is derivable from (ARI) identifier (any sequence of printable chars) and from (SMT) hexadecimal. (ARI) identifier is reachable from (ARI) smt-term. (SMT) s-expr derives to (SMT) spec_constant to (SMT) hexadecimal.

[AkihisaYamada]

The original idea was not to allow things that needs special parsing in the left and right hand sides of rules. (But now I'm not completely sure.)

[ffrohn]

Let's continue the discussion about identifiers here, as it's not specific to SRSs. Regarding the syntax for SRSs, I'll ask the SC whether they are in favor of [a b c] or not.