[SCL] Proposed additions to the SCL draft standard

[pat hayes]

>Chris Menzel wrote:
>
>>On Sun, May 25, 2003 at 02:38:24PM +0300, Tanel Tammet wrote:
>>
>>
>>>- Integers and bounded existential quantifications (a possibility
>>>  to say that there exist exactly N objects with some property P).
>>>  By 'integers' I mean the use of numerals with a predefined
>>>  property that all lexically different numerals map to
>>>  different elements of the domain. Ie, not(id(4,7)) holds,
>>>  no need for a user to define this.
>>
>>
>>Yes, we talked about this at some length at the last telecon.  There
>>seemed to be general agreement that such quantifiers are necessary and
>>useful.

....

>
>What I guess would be right, though, is that:
>
>- If we have numerals explicitly in SCL, it would be
>   easier to use ordinary, decimal integer representations
>   during actual usage of SCL.
>
>   Otherwise some people would
>   have a tendency to use the successor notation, some
>   would come with a binary (bitwise) encoding scheme,
>   while some would use numerals. The actual formulas
>   in concrete syntaxes would probably represent integers
>   in different ways.
>
>- When we consider actual implementations proving theorems,
>   then it is badly inefficient to use axioms like the one
>   above for basic integer functions and predicates (equality
>   of two integers is a good example). It is normally a good
>   idea to build in some basic operations while using
>   axiomatisations for all the rest.
>
>   It seems to me (though I may be mistaken) that it would
>   be advantageous for implementors to think like "ok, these
>   basic operations like equality of two integers should perhaps be
>   built in, since we have a special domain for integers and
>   special numerals in the language anyway".
>
>   I know: what I said here is vague. One could build in parts
>   of arithmetic without any special support from SCL or like (have
>   done that myself). Strictly speaking, we would not
>   need "help" from SCL for that. However, as I said, IMHO it will
>   be a nice guide for implementors to have integers in the
>   SCL.

I agree with all the above. Decimal notation for referring to the 
natural numbers is about the best-established notational convention 
ever produced by the human race. It would be folly to ask SCL users 
to give it up for a SUCC function, or expect them to slog through 
axiomatizations of it. We should build it in, but minimally and 'FO 
honestly'; axiomatizations of arithmetic are of interest only to 
FOL-oriented logicians, not to practical ontologists.

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.

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

Comments??

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam