SizeChangeTool doesn't check validity wrt XTC format

[fblanqui]

starting lp file:

symbol T : TYPE;
symbol lam : (T → T) → T;
symbol app : T → (T → T);
rule app (lam $f) $x ↪ $f $x; // β

xml file obtained after lambdapi export -o xtc (using branch https://github.com/Deducteam/lambdapi/pull/871):

<?xml version="1.0" encoding="UTF-8"?>
<?xml-stylesheet href="xtc2tpdb.xsl" type="text/xsl"?>
<problem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" type="termination" xsi:noNamespaceSchemaLocation="http://dev.aspsimon.org/xtc.xsd">
  <trs>
    <rules>
      <lhs>
        <funapp><name>tests.OK.hoas.app</name>
          <arg>
            <funapp><name>tests.OK.hoas.lam</name>
               <arg><var>1_0</var></arg>
            </funapp>
          </arg>
          <arg><var>1_1</var></arg>
         </funapp>
      </lhs>
      <rhs>
        <application><var>1_0</var><var>1_1</var></application>
      </rhs>
    </rules>
    <higherOrderSignature>
      <variableTypeInfo>
        <varDeclaration>
          <var>$1_1</var>
          <type><type><basic>tests.OK.hoas.T</basic></type></type>
        </varDeclaration>
        <varDeclaration>
          <var>$1_0</var>
          <type><type><arrow><type><basic>tests.OK.hoas.T</basic></type><type><basic>tests.OK.hoas.T</basic></type></arrow></type></type>
        </varDeclaration>
      </variableTypeInfo>
      <functionSymbolTypeInfo>
        <funcDeclaration>
          <name>tests.OK.hoas.app</name>
          <typeDeclaration><type><arrow><type><basic>tests.OK.hoas.T</basic></type><type><arrow><type><basic>tests.OK.hoas.T</basic></type><type><basic>tests.OK.hoas.T</basic></type></arrow></type></arrow></type></typeDeclaration>
        </funcDeclaration>
        <funcDeclaration>
          <name>tests.OK.hoas.lam</name>
          <typeDeclaration><type><arrow><type><arrow><type><basic>tests.OK.hoas.T</basic></type><type><basic>tests.OK.hoas.T</basic></type></arrow></type><type><basic>tests.OK.hoas.T</basic></type></arrow></type></typeDeclaration>
        </funcDeclaration>
      </functionSymbolTypeInfo>
    </higherOrderSignature>
  </trs>
  <strategy>FULL</strategy>
  <metainformation>
    <originalfilename>tests.OK.hoas.lp</originalfilename>
  </metainformation>
</problem>

Result:

12:19 ~/lambdapi (master) ~/src/SizeChangeTool/sct.native hoas.xml
YES
[Termin] hoas.xml was proved terminating using Dependency Pairs and SCT

But, if t=lam(\x:T.app(x,x)), then app(t,t) ->R (\x:T.app(x,x))t ->beta app(t,t).

[GuillaumeGen]

Ugh! It is a huge issue! It appeared in one of the update, since your example is the same as http://www.lsv.fr/~genestier/Documents/Publi/HOR_2019_Slides#page=9 but the answer is different. I will investigate it soon, and will push an update by the end of the week. Thanks for spotting it.

[GuillaumeGen]

Ok, I investigated it today, it happens that the file you are suggesting is not a valid file of the termination competition. The tags are missing. Hence all the rules were simply ignored by SizeChangeTool.

Action plan: [ ] SCT should emit a warning whenever it did not identify any rule, [ ] Add an option to SCT to check conformance of the input file with xtc.xsd (the extended version), [ ] Fix the generator (so the export command of lambdapi)

[fblanqui]

I fixed the generator. Thank you. (I got the same problem with Wanda and Cynthia answered the same thing to me; Wanda also did not emit any error message...) It would be very useful to have termination checkers check the validity of XTC files + typing + SR.

[fblanqui]

In https://github.com/fblanqui/rainbow/blob/master/ml_of_xsd.ml, we started to write a tool generating an XML parser from an XSD file, based on xml-light. Maybe it could be reused here.