[SCL] more syntactic wrinkles

[pat hayes]

Guys, here are drafty proposals for the other missing parts of the 
SCL syntax. These are boring from a logic point of view but I think 
important for a deployed language.

1. Comment wrappers

The syntax should allow any expression to have a comment added to it 
which is logically invisible. This is awkward to state using 
traditional syntax description techniques since it doubles the number 
of syntax primitives, but it really is a very simple idea.  There is 
a new term generator called Com and every syntax class - App, Id, 
Neg, etc. - has an additional case allowing a comment wrapper to 
count as one of them; so eg

Conj: F* -> F U ConjWrap
ConjWrap: Conj x Com

In addition, a bare Com is allowed as an expression but assigned no 
semantics (it is logically equivalent to 'true'.)

Con is *not* required to be disjoint from anything in particular 
(some apps may wish to include SCL text itself as comment) and 
ideally is not even required to be text; all that matters is that the 
Wrap cases can be clearly distinguished in the concrete syntax. Such 
a syntax extending SCLKIF might use square brackets to enclose a 
wrapper, as in:

[(forall ([?x *Should be @x??]) (implies (P @x)(Q ?x @x))) This is a 
very silly axiom, see http://www.ihmc.us/users/phayes/sillyaxioms .]

which is logically the same as

(forall (?x) (implies (P @x)(Q ?x @x)))

Part of the conformance requirements are that although wrappers have 
no logical meaning, apps which transmit or process ontologies are 
required to retain them as part of an ontology and to provide them to 
users or through APIs when requested.

2. Special term classes (datatyping).

We need a provision for an SCL language to have special terms with 
fixed denotations and some 'standard' way to indicate them. Obvious 
examples are numerals denoting integers and quoted expressions 
denoting character strings, but it would also be useful to have a 
class of well-balanced XML fragments denoting XML documents (maybe in 
some normal form or other) and to be ready for languages which have 
things like dates, airport ID codes, God knows what, as such 
categories. So here's a general proposal for such things, call them 
type classes. This is based on the treatment of datatypes in RDF.

A type T is defined by a set LT  of constants (terms?) called lexical 
forms, a set VT of values and a function L2VT from LT to VT.  Also, 
there is a constant Tname called the 'canonical name' of the type and 
a predicate symbol Tpred.  These could be the same in some CL 
syntaxes.

The base type theory of T is an infinite set of ground atoms

scl:Type(Tname)
Tpred(t)  for every t in LT
not Tpred(t) for every constant t not in LT
t1=t2  for every t1 and t2 in LT with L2VT(t1)=L2VT(t2)
not t1=t2  for every t1, t2 in LT with L2VT(t1)/=L2VT(t2)

Here scl:Type is a special predicate symbol reserved for use in SCL languages.

Obvious examples would be the type of integers mapped from numerals, 
the type of character strings mapped from quoted strings and the type 
of XML documents mapped from well-balanced XML markup strings (both 
of which have trivial L2V mappings), but for other examples see 
http://www.w3.org/TR/xmlschema-2/

An SCL language which supports a type T must provide a distinctive 
syntactic from for all terms in LT, and conforming inference engines 
must somehow provide a means to determine the truthvalue of all 
ground atoms in the base type theory. In particular cases other 
functionality may be appropriate as well (eg see XSD's use of 
'facets' http://www.w3.org/TR/xmlschema-2/#rf-fund-facets), but this 
is a minimum. Note that in the case of numerals this would require an 
engine to know that 4/=7, say, but not to be able to do any 
arithmetic. If y'all want Peano arithmetic, you have to axiomatize it 
yourself.

One way to achieve the distinctive-syntactic-form requirement is to 
include the type name as part of the terms in LT; this is how RDF 
handles typing, so that to write three in RDF you have to write 
"3"^^xsd:integer.  A more, er, normal syntax might use enclosing 
single quotes to mark character strings and have the convention that 
all numerals denote numbers; it would then have to not use numerals 
as simple names, of course.

Now, this does not provide for any particular syntax for defining a 
type, or even for declaring that a given SCL language includes any 
particular types. In an ideal world there would be a uniform general 
way to do this. About the best we can do at present, seems to me (and 
God knows it is not ideal) would be to refer to an existing standard 
set such as the XML schema collection, and require conforming SCL 
languages to use the relevant URIrefs (xsd:integer, xsd:string etc.) 
as type names.

Thoughts?

Pat

-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes