[SCL] SCL and XML syntax translation questions

[Bill Andersen]

On Sunday, Dec 22, 2002, at 04:55 US/Eastern, Tanel Tammet wrote:

I personally like something like this (#2), except with a modification 
to make the predicate and function terms themselves analogs to the 
existing abstract syntax.  See below.

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

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

Here, the parser needs to know about the hierarchy of formulas:

   formula
     quant-formula
       forall
       exists
     connective-formula
       implies
       and
       or
       not
     equals

with the appropriate partitions, and the hierarchy of terms

   term
     fnterm

where fnterm is just a specialization of term

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

How is order handled in XML normally?

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

Great.  Is this part of existing CL?  I thought we (the CL group) had 
agreed that this was just a shorthand for restricted quantification.

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

No necessarily.  Add XML is cumbersome enough, at least in terms of 
readability, so requiring quantifiers to bind one variable doesn't seem 
to be a big price to pay especially if it makes the syntax simpler.

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

Agreed.  Seems like we can do without '?'.  I think that the XML syntax 
ought to require formulas to be written as explicitly as possible, 
given that the goal (IMHO) should be to develop a syntax for exchange 
of formulas, not a syntax designed for human readability.  The 
Prolog-like conventions are one example of a convention for the sake of 
readability.

   .bill

--
Bill Andersen
Chief Scientist
Ontology Works, Inc.
1132 Annapolis Road, Suite 104
Odenton, Maryland 21113
United States
Office: 410-674-7600
Mobile: 443-858-6444