Datatypes (was: Re: [SCL] Proposed additions to the SCL draft standard)

[Tanel Tammet]

Hi,

pat hayes wrote:

> Let me make a concrete proposal: Numerals are a class of basic names 
> in the syntax, the semantics requires each to denote its corresponding 
> integer, and there are two built-in predicates, scl:Integer which is 
> true of all, and only, integers, and scl:LessThan which denotes the 
> strictly-less-than relation; and two built-in functions: scl:minus 
> which maps n to -n, and scl:plusOne which maps n to n+1 (needed for 
> stating inductions on sequence lengths, but does not presuppose 
> inductive reasoning to support the basic core meanings.) This keeps 
> the core free of any inductive assumptions which would go beyond FO 
> compactness, but it allows the full SCL language to link sequences 
> with numerals so as to piggyback numerical induction on the inductive 
> version of the infinitary proof rule for seqvars. 

Seems fine for me. The predicates and functions proposed here are fine, 
except that PERHAPS
we could use ordinary plus instead of plusone as a basic function. 
Plusone is, in practice, hardly
useful for anything except defining an ordinary plus, which will then be 
used. Plus, on the other
had, is obviously usable anywhere one would use plusone. (I used to use 
plusone some time ago
in practical apps, but have turned away from it towards using plus 
exclusively). Plusone is
of course very nice  for teaching students about the buildup of 
arithmetics, but we are under
no obligation to carry it over to practical apps.

I understand that we will have numbers and a few basic predicates and 
functions in SCL itself,
not a web layer on top of it (the latter would be IMHO insufficient). I 
would not like to have very extensive
arithmetic as Sowa proposed: it complicates things a lot, while being 
unneccessary for most apps.

>>>>   - Once we have integers in the language, we could in principle
>>>>      (if we want to) encode strings and string equalities as
>>>>      integers (for example, by using ascii or utf) along with
>>>>      the ascii or utf string type constuctor taking an integer as
>>>>      an argument. Strictly speaking we would not need to extend
>>>>      the core language to encode strings (or any other datatypes,
>>>>      for that matter: integers suffice, at least theoretically).
>>>
>>>
>>>
>>> You're losing me.  I believe you are talking much closer to the 
>>> level of
>>> implementation than is any of SCL's business.
>>
>>
>> I am not suggesting to put in strings and other kinds of
>> types into SCL.
>
>
> Ah, but I am :-) In fact I would like to do something like the above 
> for most of the XSD datatypes. We can do this uniformly across almost 
> the entire spectrum of XSD simple datatypes, if we do it carefully. It 
> would be OK to have this as a 'datatyped extension' of the language 
> but we would need to provide for some way of indicating that a given 
> datatype was indeed a datatype, and to provide for some way to 
> indicate wellformedness of a lexical form.
>
> The RDFS/OWL semantic strategy for literals might be relevant here: 
> simple literals are required to denote themselves, thereby 
> guaranteeing that lexical forms are in the domain of discourse; a 
> feature that we could . Typed literals (a form plus a datatype) then 
> denote the value of the lexical form under the datatype. This is 
> awkward for 'normal' types such as integers  but provides a very 
> general framework.  Eg 3 has to be written "3"^^xsd:integer, which we 
> could render as xsd:integer('3') so that xsd:string('3') is meaningful 
> and xsd:date('05262003') is today, rather than a number. The 
> conventional meaning of a numeral could then be considered to be 
> (context-sensitive) syntactic sugar for the xsd-typed form.
>
> All of this could be restricted to the 'Web SCL' special extension I 
> suggested in an earlier message. However, we would need at least 
> simple strings and numerals in the base logic, seems to me.

I have the same opinion that IF we add datatypes to SCL, we should add 
them into base logic.
The web-SCL should probably deal with includes, linking, concrete 
languages and the like:
not data. Web is not about datatypes, but connectivity and (maybe) 
namespaces.

Maybe a separate SCL layer between core and web (something called like 
SCL-DATA)
would be OK.

I have some doubts about putting all the xsd types into base logic. The 
reason for doubts
is that it would be easy and natural for users to start using 
constructors like you did above,
without any need for help from SCL. In other words, a datatype should 
(perhaps) be put into SCL
in case we provide some built-in properties for the datatype, removing 
the need for
the user to axiomatise these properties (sine we build them in, hence 
providing "standard"
axioms in semantics).

For example, an important property would be that datatypes are
disjoint. To say that dates are disjoint from strings we would need to
axiomatise forall x,y. xsd:string(x) != xsd:date(y). Since this is a 
simple axiom
it would be easily axiomatisable by the user, removing a strong need 
need for us to put
the datatypes into SCL. On the other hand, if we DO put the datatypes into
SCL, we should also define some properties (like the disjointness of 
types) in
SCL: otherwise there is little point in adding the types to SCL.

BTW, in the logic context it would be a bit inconvenient to handle
dates stemming from the string like in "for xsd:date('05262003')".
Personally I'd prefer to say date(year(2003),month(5),day(26)" or,
even better, "date(2003,5,26)", taking just integers.  I do not want
to go into such details or make any proposals, though: just an obvious
observation that the built-in datatypes might be nontrivial to
decide upon.

Strings (like integers) are something which might be hard for a user to 
axiomatise
(differently from the date, for example, assuming integers are already 
there).

Strings, differently from dates:
- are unbounded lists of characters
- characters map to integers in various ways, depending on the encoding

Hence I wouldn't worry much about putting strings into the language: it 
is hard
enough (and important enough) to justify the activity,

Doing this would require some work from us, though. I am afraid we would
have to decide the character encoding(s) for this, giving types like 
ascii-string
and utf-string, and possibly also a string constructor from integers, 
something
like  c(char(65), c(char(66),  emptystring))  for a two-element string. 
Not a simple
thing to agree upon. Maybe there exists a sensible compromise between
a detailed axiomatisation in SCL semantics and a nearly-useless claim that
we "simply" have a string type string(...) in SCL. BTW, the proposed 
annotation
strings are strings in the latter meaning: no axioms are given for them, 
they
act just like ordinary constants with no predefined properties whatsoever.

Regards,
            Tanel Tammet