[Termtools] TODAY: Input for TermComp Presentation

[Johannes Waldmann]

Dear all,


I revived star-exec-presenter [1]
and you can use it to browse competition results
and compare with last year(s).

Pick job numbers from official results tables

http://termcomp2020.herokuapp.com/
http://group-mmm.org/termination/competitions/Y2019/

and put at the end of the query (separated by slashes)


Examples: SRS standard last year/this year

https://termcomp.imn.htwk-leipzig.de/flexible-table/Query%20[]/33458/41485

SRS standard certified vs. not

https://termcomp.imn.htwk-leipzig.de/flexible-table/Query%20[]/41485/41502

also, "use virtual best solvers"  to get the broader picture.

Have some patience - data is fetched from star-exec in the background.


I add some comments specifically on SRS and Matchbox
with some input from Dieter for Multum-Non-Multa.
These comments  may be too specific for the "outside" world
(as Jürgen was asking).
But, since we don't have the Termination Workshop this year,
take the following as my "inside" coffee table chat contribution.


* There aren't any new proof methods, but some combinations are new:
  MnM has sparse tiling (for RFC) now,   and can follow this
  with the search for large sparse matrices (that no-one else does).
  Matchbox used DP-transform then sparse-tiling
  for overlap closures last year, and now sparse-tiling for RFC
  first, and only then DP transform  (and no tiling after that)
  What gives? I don't know, really. It's an instance of:

* Performance depends on the strategy for proof search,
  and that requires a lot of delicate trade-offs
  (what branches of the search tree to cut early).
  I am sure every-one has a nice strategy language to express these
  (e.g., matchbox and TTT2 print strategy expression at end of proof)
  but I find that the outcome of changes in the strategy expression
  is non-predictable (with the resources that I wanted to spend).

* The printed proof is the truth (we hope) but sometimes
  not the whole truth: e.g., matchbox prints an arctic matrix
  interpretation, but it is actually a transformed quasi-periodic
  interpretation (QPI). The reason is not obfuscation,
  but an eye towards certification: CeTA does not know  about QPI,
  and that's fine, because the transformation works.

* Still there is a slowly growing set of SRS termination techniques
  that are not formally verified. I am listing them here,
  not to complain, but to raise interest in the community.

  - RFC matchbounds: matchbounds are certified, but we don't have RFC.
  Would require formal proof of theorems about (forward) closures,
  and while we're at it, overlap closures as well.  I think that's
  independent from the match (or other bounds) annotations.

  - Matrices: MnM uses "standard" matrix interpretations
  but it's incompatible with CeTA's version - which also has "standard"
  matrices but for TRS. The difference is that the TRS version,
  when translated to SRS, has a fixed "0 .. 0 1" last row.

  - Sparse tiling: CeTA can do semantic labelling (full tiling).
  Sparse tiling is semantic labelling w.r.t. a partial algebra,
  for local termination (i.e., for a restricted starting language).

  Now can we trust these un-certified methods? I'd say, more in 2020
  than in 2019, since Dieter's implementation (of sparse tiling)
  is independent, and we get the exact same numbers (of tiles,
  of rules, etc.)  - in case both provers decided
  to follow an identical proof search path. Example: see [2]

* Finally, about number of rules, and sizes of proofs:
  RFC matchbound certificates do get large. Huge, even!
  Look at all the certifier-timeouts (red blocks, but not all)  [3]
  This could get worse with tiling (semantic labelling).

  Also, we were running out of disk quota. Do we really want
  to see and store all proofs? They could be piped from the prover
  to the certifier - and then be forgotten?

  Perhaps there's a different solution - but it needs research:
  invent a compressed format for automata, or for sets of tiles,
  that can still be verified in linear time.
  But that's not enough - we use these automata for semantic labelling,
  so we need to compress the labelled system as well.
  And then, of course, we want to find the interpretation
  (the labeling, etc.) without uncompression.


Best regards, Johannes.


[1] it was broken since some tomcat internals changed
https://github.com/jwaldmann/star-exec-presenter/issues/192

[2] look for the number  "8820" in
https://termcomp.imn.htwk-leipzig.de/pairs/487516866
https://termcomp.imn.htwk-leipzig.de/pairs/487516864

[3] https://github.com/StarExec/StarExec/issues/294