[SCL] SCL and XML syntax translation questions

[Tanel Tammet]

Hi,

Wanted to ask your opinion on how should the SCL-lisp <-> SCL-XML 
transformation look like. I think we should get a basic agreement
on this before we attempt to fix the specifics of SCL-lisp
syntax and semantics.

Here are some naive alternative solutions for discussion:

To transform a formula

(implies
    (forall (?x)
      (P (succ ?x)) )
    (P (succ 0)) )

we could have smth like (several different encoding methods):

1) Some untyped nested list translation
    with NO function->tag conversion, but a special
    treatment for varlist (I'd probably prefer this
    format, since it is least restrictive and does
    not convey more information than the lisp syntax):

   <term>
      <term>implies</term>
      <term>
        <term>forall</term>
        <varlist>
          <var>?x</var>
        </varlist>
        <term>
          <term>P</term>
          <term>
            <term>succ</term>
            <term>?x</term>
          </term>
        </term>
      </term>
      <term>
        <term>P</term>
        <term>
          <term>succ</term>
          <term>0</term>
        </term>
      </term>
   </term>

To be really faithful to list syntax we should perhaps
drop the <varlist> tag and simply write:

        <term>
          <term>?x</term>
        </term>

Otherwise the parser/converter must KNOW which functions
are quantifiers and which not. This might be hard to
achieve for exotic logics and specific quantifiers people may
want to use.

2) General nested list translation with function->tag conversion and
    exception for varlist. Here the parser/converter again
    needs to know which functions are quantifiers and which not.

   <implies>
      <forall>
        <varlist>
          <var>?x</var>
        </varlist>
        <P>
          <succ?>?x</succ>
        </P>
      </forall>
      <P>
        <succ>0</succ>
      </P>
   </implies>

3)  Some kind of a rather strongly typed nested list translation
     which explicitly contains information about the formula structure
     apparently NOT present in SCL-lisp syntax (observe that
     it would not be so easy for higher order case where we cannot
     have <literal fun="P"> anymore, since fun may be a complex term).

     Here the parser/converter needs to know an awful lot, putting
     serious restrictions on the practical usage of exotic logics:

   <prop fun="implies">
      <quantifier fun="forall">
        <varlist>
          <var>?x</var>
        </varlist>
        <literal fun="P">
          <term fun="succ">
            <atomicterm term="?x"/>
          </term>
        </literal>
      </quantifier>
      <literal fun="P">
         <term fun="succ">
           <atomicterm term="0"/>
         </term>
      </literal>
   </prop>


4) Something completely different?


About the varlist and variable/constant encodings:

Varlist:

It seems to me that the variable list is the only set
construction in the formula syntax: for other lists the first
element of a list is a distinguished function/predicate/connective/etc
term and the order of elements normally matters.

This seems to require a special treatment in the XML syntax as well.

The XML syntax must also allowed typed variables to be
present in the list, preferably a mix of
typed/untyped like in (?x (int ?y) ?z).

We could, in principle, remove the problem by requiring
a quantifier to bind a SINGLE variable, but I guess this
will be cumbersome to use and is not compatible with KIF
and CL ideology.

The first example above proposes an alternative dumb solution
of treating (?x (int ?y) ?z) as just another term in XML.


Variable/constant encodings:

BTW, is there a reason to REQUIRE that variables start with ?
or is it just a cozy convention we do not have to force?

If we prohibit open formulas at top level, then we do not need vars to
start with ?. In "ordinary" theorem provers which take
clausal input (hence open formulas) the variable/constant
distinction is mostly done using different conventions, like
Prolog-style capital/noncapital or Otter-style first character
convention of x,y,z,u,v,w. If open formulas at top level are
prohibited, then we do not need to force any conventions
upon other people in this respect.

Regards,
         Tanel Tammet