Re: Example of applying sorted-nucleus? was Re: [TED] CORE Pages on Positive Conditions and Horn Rules Edited: Slots & Constraints

Dave Reynolds <der@hplb.hpl.hp.com> wrote:
> 
> [Interesting discussion snipped.]
> 
> Hassan Aït-Kaci wrote:
> 
> >> I am glad that you agree with the idea of using sorts for extensibility.
> >> I was pretty sure that you would like it :-) I was surprised that a
> >> number of people had difficulty understanding this simple thing.
> > 
> > I agree with you.
> 
> If it's any consolation it is equally frustrating for us non-specialists 
> who are trying to fathom the implications of the approach.
> 
> Perhaps it would be helpful if we could develop a worked example which 
> shows how the approach will be applied in practice. For example, develop 
> an instantiation of this framework that is sufficient to capture 
> (function-free) conditions applicable to RDF data.
> 
> In particular, it would be helpful to illustrate how the various 
> Con->Sort mappings are intended to be captured in the abstract syntax. I 
> assume they *are* supposed to be explicit in the final abstract syntax 
> since we can't tell the difference between the various subsets of Con 
> just at the character sequence level.

Yes, you are right -- the current document is too terse. The intent was to
expand it in due time with examples. Let me elaborate.

Mathematically, a sort is just a set and, in theory, it doesn't matter how
it is defined. But in a concrete KR language there must be a clear and
simple mechanism that tells which symbols belong to which sort.

This kind of thing is done in every programming language to various
degrees.  For instance, in C, things that are sequences of digits belong to
the sort of integers. Things that look like 123.456 are floats, "..." are
strings. Alphanumeric things are variable names, type names, and procedure
names. They are distinguished contextually by their declarations.

So, C and most other programming languages use a combination of syntax and
explicit declarations to classify their symbols into sorts.

Now, RIF will need to make similar kinds of decisions. Since RIF is a
family of languages rather than a single language, our job is harder and we
need to come up with a simple yet extensible framework for specifying sorts
to which RIF symbols belong. I am not proposing anything right now, but am
simply indicating what the choices might be.

The most flexible framework is based on declarations. That is, each symbol
can be explicitly or implicitly declared to belong to one of the sorts
(ints, dates, URIs, predicate symbols, etc.)
Unfortunately, this may not be a practical solution (at least, I don't know
of a practical one).

There are also flexible syntactic solutions. For instance, in RDF they use
symbol^^type to indicate the sorts of the literals. We could extend that.
Unfortunately, this syntax is UGLY. It also is not very flexible if we want
some sorts to be non-disjoint (e.g., one to extend the other, which is very
useful; such logics are called order-sorted).

But all this has to do with the abstract syntax only. In XML things are
quite simple. We could use a combination of implicit sorts based on syntax
(suitable for primitive data types like strings, integers, time, and date)
and explicit declarations using the type attribute (for user-defined and
dialect-defined sorts).

Now, regarding the RDF instantiation, we could use
&^$#$%%rdf(prop,object,subject), where &^$#$%%rdf is a special
predicate symbol for RDF triples.

The sort of the symbol &^$#$%%rdf would have to be the Boolean sort

    iri x iri x (iri+literal)

where iri is a sort that contains all iri symbols and "literal" is a sort
that contains all primitive data types. iri+literal is the least upper
bound of the sorts iri and literal.

>From this follows a requirement that sorts have to be partially ordered
(order-sorted).  Most likely the sorts will be organized in a lattice or
semi-lattice with lub being the union and glb being the intersection of the
respective sorts.



	--michael  



> Dave
> 
> 
> 
>

Received on Monday, 11 December 2006 16:33:44 UTC