[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]

[Tanel Tammet]

Pat Hayes wrote:

>> 3) Keeping the SCL concrete syntaxes simple
>>     and traditional, with no weird/complex
>>     constructions.
>
>
> Agreed, but we might have different views on what counts as more weird 
> and complex. I find lexical conventions awkward and we have tried to 
> eliminate them as far as possible.
>
Right, it makes sense as well.

However, we need some convention to distinguish between two different kinds
of predicate/function application. The question remaining is which 
convention
is nicer. We cannot avoid using some kind of a convention.

>>
>> In any concrete SCL syntax we split the names,
>> i.e lexical items for constants/predicates/functions
>> into several sets:
>>
>> - ordinary constants (like a, c1, bbx)
>> - numeric constants (like 0, -2, 10)
>> - string constants (like "aab", "1")
>> - possibly date and time constants (like 01.02.2004)
>> - special function and predicate names: any name
>>  prefixed by ! is a special name (like !f, !P)
>
>
> But now this requires a global naming convention to be agreed on. I 
> don't think this is acceptable for a logic to be used on the Web.
>
> Tell you what:I'll see how simple I can make the 'headers' idea come 
> out to be, and then we compare notes. I agree we need to have some 
> simple straightforward way to determine when to translate (P x) 
> correctly as holds_2(P x) and when as itself. I think this is best 
> determined by what is said ABOUT the text rather than in the text 
> itself, however.
>
OK. I'll upgrade the ECL draft later today, following the notes in my 
last email.
Will send mail when it is ready.

Perhaps the lexical and header approach can be combined.
For example (just initial speculations with pseudo-syntax,
assuming that ! is the special lexical prefix), the
following examples might make sense:

-   (header namespace:foo="bar"
        (foo:p 1))
     would translate to (bar:p 1)

-   (header namespace:foo="bar"
        (foo:!p 1))
     would translate to (bar:!p 1)

    and we should treat any  xx:!ff as
    a special predicate as well, like !ff

Some of the following might make
sense too, but they are more problematic.
The idea is to make it easier to declare that something
is a special predicate/function:

-   (header namespace:foo="!bar"
        (foo:p 1))
     would translate to (!bar:p 1)
     which would also be a special
     predicate

-   (header namespace:foo="!"
        (foo:p 1))
     would translate to (!:p 1)
     which would also be a special
     predicate

-   (header namespace="!"
        (p 1))
     would translate to (!:p 1)
     and will translate ALL predicates and functions
     to a special predicate

Anyway, would be great to follow the standard namespace
convention in headers, without bringing in extra
machinery. Then the standard namespace stuff
could be attached directly on SCL concrete syntaxes,
in particular SCL-XML. IMHO this does not
contradict the lexical approach:  rather, it should fit
the lexical approach.

>>
>> We have to axiomatise ourselves that numbers are
>> different from strings and two different numbers are
>> different, etc. We cannot simply point to the W3C documents
>> for datatypes, since they contain no such axioms (they
>> cannot, since they do not use any logic, in particular they
>> do not use SCL, which does not even exist before we publish
>> the SCL description).
>
>
> Quite, but Lbase did; and we can give general schemata for such axiom 
> sets based on any set of datatypes. The ones cited above are 
> reasonably closely based on the RDF/RDFS/OWL uses of the XMLSchema 
> datatypes, and apply in general form to almost any computable datatype 
> scheme.
>
I'll look into the Lbase approach.

> All the new datatypes should be created by constructor
>
>> functions, like boolean(0), analogously to lists,
>> where cons(0,nil) creates a list from a number and a list.
>
>
> I think the general form should be a function applied to strings 
> encoding the lexical form whose value is the datatype value.  This can 
> be used for any XSD datatype and indeed any other I can think of. Then 
> for example we would have truths like
>
> (= 426 (xsd:integer '426'))
>
I agree.

BTW, I'd suggest using double quotes for strings. This
will:

a)  Free the single quotes for use in constant/predicate/function symbols:
     you could write a predicate symbol like this '? 1 +  f'  with 
single quotes.
    Without quoting we can only use a limited set of characters in
    constant/predicate/function symbols, but if we allow quoting, all 
symbols
    are fine.

b) Conform better to the most common conventions of programming languages,
    incl lisp:  almost all languages allow strings in double quotes, but 
just a few
    (mainly, shell and its derivatives) allow single quotes, and then 
typically
    with slightly different semantics than double quotes.
 

> We also need a wellformedness predicate (true of all values for that 
> datatype) ; since these are respectively a function and a predicate we 
> can use the datatype name for both of them:
>
> (scl:integer (xsd:integer '00426'))
> (rdf:XMLLiteral '<kosherXML> love those angle brackets</kosherXML>')
>
Right.

> BTW, there is a delicate issue here that needs care. On one view of 
> the matter, the values of two distinct datatypes are NEVER identical, 
> so that for example this is false:
>
> (= (xsd:hexadecimal '2F') (xsd:integer '47'))
>
> On another view of the matter, this is crazy. We can express either 
> option, of course, but we might want to think about the issue in a 
> little more detail. On the first view, for example, xsd:integers are 
> not in fact integers.
>
Above you also wrote (= 426 (xsd:integer '426'))

The question here is whether xsd:integer  is a type constructor
or type converter. We need both. If xsd:integer is
a type constructor as above, then (= 426 (xsd:integer '426')) and
(= (xsd:hexadecimal '2F') (xsd:integer '47'))  are both false.

It looks crazy, as you said, but I do not think we can avoid
this crazyness. After all, the machine implementation of
different data types is really different, as subtle differences
hold for arithmetics and other operators. When we try
to merge types, we'll have to axiomatise all these subtle
differences, which is a horrendous task.

This is especially critical in the context of logic,
where wrong equalities have drastic effects:
we have no safeguards like "rounding errors", signals,
exceptions etc we have in programming.

In several ordinary programming languages the differences
hold as well, and in others the conversion is done implicitly,
as we know, with lots of rules for these implicit conversions.

These conversions are really there in programming
languages and they do have practical effects.
If you have in C

int x;
double y;
x=1;
y=1.0;
if (x==y) ....

then the explicit conversion is definitely done in the comparison.
Bitwise, x and y are completely different. If you
start doing bit operations on x and y, you'll immediately notice
that x is not equal to y:

if ((x&101)==(y&101)

is syntactically incorrect, you'll have to write

if ((x&101)==((int)y&101)

and the (int)y is in most cases NOT equal to y, i.e.

if (y==(int)y) ...

is of course false if you have y=1.2, for example.

To get a true value one should write
(= 426 (xsd:integer_to_integer (xsd:integer '426')))
and
(= (xsd:hexadecimal_to_integer (xsd:hexadecimal '2F')) 
(xsd:integer_to_integer (xsd:integer '47'))))
assuming that the ..._to_integer functions are type converters.

> We may also need an equational theory for reducing datatype forms to a 
> normal or canonical form (eg leading zero suppression in numerals) and 
> possibly an ordering theory (not all datatypes are ordered). It would 
> be very good 'webcentric' policy to relate all this to the 'facet' 
> terminology used in the XSD documentation.
>
Right. It would be great if we could put XSD stuff into SCL, but
I am afraid that we do not have time to do this in sufficient
detail: maybe I am pessimistic, but IMHO it would take a lot of
nontrivial axiomatisation work.  It would also make SCL
much more complex to read and implement. I hate rising
the barrier of entry.

I'd rather suggest putting SCL out with PROLOG-like
datatypes of its own and not put  all the xsd stuff into SCL.

We should then suggest that a special SCL-XSD module
will/can be added in later extensions to SCL (or maybe CL?).

What we could manage to do is to make sure it will not be
too hard, i.e. the SCL internal datatypes are easily translatable
to XSD datatypes and vice versa. Horrible to say this,
but IMHO they do not have to be exactly the same.

I'd rather have SCL internal datatypes exactly the same as
C datatypes: we know these are implementable and people
are accustomed to these datatypes. The implementations
will be less likely to contradict the datatypes (the datatypes
of most language implementations are based on C datatypes
anyway).

> Some datatypes have special qualities, eg if we allow xsd:boolean, do 
> we want to relate these values (true/false) to our logical true/false, 
> ie (and) and (or) respectively? I would suggest that we do NOT do 
> this, in fact, but the issue kind of comes up automatically, 

I agree. I do not want to do this either. Rather, I'd
push the detailed XSD questions into the SCL-XSD
module to be developed in the future.

> In the RDF specification we felt obliged to specify that a string 
> typed with xsd:string was the same as itself, ie using the conventions 
> I just outlined, that
>
> (forall (x) (implies (scl:string x) (= x (xsd:string x)) ))
>
I see. Such axioms would be one part of the SCL-XSD
module, connecting the SCL basic datatypes with XSD.

Regards,
              Tanel