Exports for the format TRS + small improvement to HRS export

[thiagofelicissimo]

This provides an export for the TRS format used by checkers such as Aprove. It can be used to check SN without beta, and only works for rewrite systems that satisfy the property that all LHSs and RHSs are fully-applied patterns (this is way beta is not covered). This is useful for checking confluence: if R is left-linear and locally confluent without using beta to close critical pairs and moreover R is SN then R+beta is confluent.

This also makes a small improvement to the HRS export: now bound variables are prefixed by * instead of $, given that SOL and CSI^ho do not support the character $ in names but both support *.

[fblanqui]

Hi Thiago. Here are a few first questions/remarks:

• Why "if R is locally confluent without using beta to close critical pairs and moreover R is SN then R+beta is confluent"?
• "I have removed qualified names because they render the output file unreadable". It perhaps makes the output less readable but it is important to avoid name clashes between files.
• The HRS and TRS outputs being very similar (the only difference is the type declarations in the HRS case I believe), the code should be factorized. Perhaps something similar can be done with the ASFM output.

[thiagofelicissimo]

* Why "if R is locally confluent without using beta to close critical pairs and moreover R is SN then R+beta is confluent"?

We can conclude confluence of R by Newman's Lemma and then confluence of R + beta using the orthogonal combinations criterion. However, I forgot to add that R must also be left-linear in order to apply this last criterion.

* "I have removed qualified names because they render the output file unreadable". It perhaps makes the output less readable but it is important to avoid name clashes between files.

Indeed, but I was wondering whether we actually use this export to check confluence of multiple files at the same time. The use case that I have in mind is to check confluence/termination of a base file defining the theory over which we want to work, and in the ideal case only this file should declare rewrite rules (though this is not the case with all encodings, for instance in the case of Coq each inductive generates new rewrite rules). If we want to support this I propose that we use a less intrusive way of removing clashes, for instance adding a natural number after the name which increases by one for each file, and is separated from the rest of the name by a character that names should not use.

[fblanqui]

Adding integers does not allow tracing back symbols and rewrite rules. It should be easy to identify in the output what comes from the input. Concerning linearity, please fix your first comment in the PR. I also added the following point above:

• The HRS and TRS outputs being very similar (the only difference is the type declarations in the HRS case I believe), the code should be factorized. Perhaps something similar can be done with the ASFM output.

[thiagofelicissimo]

Adding integers does not allow tracing back symbols and rewrite rules. It should be easy to identify in the output what comes from the input.

There is indeed a trade-off between readability and what you said. However, I think it is problematic when the names of the symbols are so big that the file becomes unreadable, and we are not able to see if the output really corresponds to the input. We could also add a comment in the output file saying id!0 -> fileA.lp, id!1 -> fileB.lp, etc in order to identify the suffixes with the files.

Concerning linearity, please fix your first comment in the PR. I also added the following point above:

* The HRS and TRS outputs being very similar (the only difference is the type declarations in the HRS case I believe), the code should be factorized. Perhaps something similar can be done with the ASFM output.

The function for printing terms is also different: a metavariable M[x0..x1] is translated as just M. Moreover, the printing of metavariables in the TRS output is simpler because we can reuse metavariables across rules, as they are all of the same type, making the output file more readable. I think it would be best to keep them as separate files, however we could factorize some parts of it, such as the sanitize function, by placing it in a utilities file.

[thiagofelicissimo]

I have now put back qualified names, and removed the afsm export as I don't need it anymore