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

[Pat Hayes]

>Hi,
>
>After all this fruitful folding-thread I have got the impression
>that there is a really simple solution that should satisfy all the
>requirements or objectives we have.

I agree, but I don't think we agree on the exact form of the really 
simple solution.

>This is basically your header idea, but formulated in a
>lexical context, not syntactical. I'll give the details
>in the following (there is nothing really new, just
>(important) nuances).
>
>In particular, I see no need for folding: although I thought
>for a while that folding would be nice, we can achieve
>everything we need by much simpler means.

I largely agree. (There is I think a role for this level of technical 
care in an appendix, in order to define carefully a 'minimal' 
structure that serves to be a coherent interpretation. But only model 
theorists need ever read it. )

>
>Coming back to roots, what do we want to achieve?
>
>1) Possibility to give properties to functions/predicates,
>    which requires that functions/predicates have
>    associated constants. The non-contested way to
>   do this is via  app/hold encoding.

Actually I do contest this, if only mildly. That is, I would prefer 
to describe the logic with a clear semantics, and then show that it 
can be accurately embedded into GOFOL by the encoding. In general, 
logics can be encoded in other logics in various ways. The particular 
choice of encoding should not be definitive of the semantics, which 
has an independent motivation. This may just be a matter of style, 
however.

>2) Possibility to express traditional FOL sentences in
>     SCL, with EXACTLY the traditional semantics.
>     In particular, I should be able to say in some
>     concrete syntax (say, SCL-KIF) that
>    (forall (x) (and (P x) (not (Q x)))
>    and this should be satisfiable on a domain with
>    only one element, which would be impossible
>    if we translated the formula with  app/holds
>    encoding. This would automatically take care
>    of the horrocks sentences as well.

Right, exactly. But there is an additional requirement that such a 
sentence can be coherently conjoined with some non-GOFOL syntax, eg

  (forall (x) (and (P x) (not (Q x)))  (exists (z) (z z))

and this can be interpreted smoothly with respect to the same 
interpretations, eg in this case it would  be satisfied by having P 
be the sole thing in the universe with itself in its extension. By 
"smoothly" I mean that the resulting combination should still be 
syntactically legal: it should be parseable as legal SCL. Its 
consistency is another matter, of course.

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

>All these things are - fundamentally - questions
>about SCL concrete syntaxes, not the underlying
>MT, where we can use conventional FOL with
>no tricks.
>
>The suggested way to  go is the following.
>
>We have one unstructured set of domain elements,
>and the goals above are achievable using lexical
>conventions plus a number of axiom schemas.
>
>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.

.......

>Finally I have some notes on data types: numbers, strings,
>etc. The XML schema datatypes are a complex structure
>and the W3C documents contain no axioms we would need.

There is a sketch of an approach in
http://www.w3.org/TR/lbase/#using
(Scroll down to 'datatyped literal axioms' ).  This uses a fixed 
binary function taking the datatype as an argument, but I think the 
constructor-function approach is simpler in SCL.

>I will describe why the approach taken in ECL is a necessary
>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.

>Fortunately, the axiomatisation is not hard: I wrote it
>down in the ECL paper, in a conventional way.

I think we largely agree on the details.

>In order to make datatypes easy to use and understand,
>we have to define and axiomatise a few basic datatypes
>with all details. We have no time or initiative to do this
>for all XML schema types. Instead, we should then
>give a detailed description of how to add new datatypes
>as modules to SCL.

Quite

>The basic datatypes like integers and strings should
>be defined lexically.

I agree. Strings and numerals have been in SCL since day one.

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

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

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.

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.

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

Since in SCL we can state things like this as axioms, I think the 
logic itself should make no such assumptions but leave it to the user 
to decide. I was planning to write a generic datatype axiom scheme as 
an importable SCL ontology.

Pat


>
>Regards,
>           Tanel


-- 
---------------------------------------------------------------------
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20040527/eeee0624/attachment.html