a possibly useful bit on sorted logics

In the hope of making things clearer with respect to the use of sorts, I
thought that the following might be useful.

I. Although the normal first-order syntax is not normally called sorted, it
   actually is. It divides all symbols into 3 disjoint types of sorts:

  - constants. these belong to just one sort, the primitive sort Con.
    That is, in regular FOL, all constants are in one big pot
  - function symbols.
    This is not a single sort, but a countable number of arrow sorts (one
    per arity):

    Con -> Con
    Con x Con -> Con
    Con x Con x Con -> Con
    ......

    Typically it is assumed that each func symbol can have exactly one
    arity and therefore it can belong to exactly one sort.

  - predicate symbols.
    This is also not a single sort, but a countable number of Boolean sorts
    (one per arity):

    Con
    Con x Con
    Con x Con x Con
    .........

    Again, it is assumed that each pred symbol belongs to exactly one
    Boolean sort.

    Variables have the sort Con.

II. Multisorted languages

    What is normally called a multi-sorted logic in textbooks is a simple
    extension of the above where

    a. The single primitive sort Con is *partitioned* into a bunch of
       primitive sorts Con1, Con2, ... (in a practical setting they are
       given meaningful names)

    b. The arrow sorts now look like

        Con_i1 x ... x Con_ik -> Con_j

        where Con_** are Con1, Con2, ...

	There can now be several sorts for the same arity because they can
	use different Con_i's in different positions.

    c. Ditto for Boolean sorts.

    Each variable is assigned to one of the primitive sorts.

III.  Order-sorted languages

    This is a syntactic extension that adds partial order on primitive
    sorts, so they are no longer disjoint. For instance, if s1 < s2 and f
    is s symbol of sort s1 then it is also a symbol of sort s2.

    This partial order is extended to arrow sorts and Boolean sorts in a
    natural way. At the very least, we would like to have something similar
    to owl:Thing, which would include all other primitive sorts. This is a
    very simple example of an order-sorted language. 

    It is easy to extend this idea to allow sorts to have non-empty
    intersection (not just inclusion) and also allow the same symbol to
    have multiple sorts within the same category of sorts (primitive,
    arrow, ...).
    
    Each variable is assigned to one of the primitive sorts.

IV.  Unsorted languages

    An unsorted language is one that doesn't have any sorts whatsoever.
    HiLog is an example of such a language. Any symbol can be used anywhere
    and any terms can be used anywhere as well. For example, 

    p(a,?X)(f(?O,k)(a,b,c)(?P,opq), r(a,b))(?Z)

    which has 3 levels of parentheses (!) is a well-formed term.
    (For those who are not familiar with this -- it can actually be useful.)
    Common Logic is built on this idea.

    Note that although such logics have first-order syntax, they can have
    first-order semantics (HiLog/Common Logic do), which means that they
    can be mapped into first-order logic both syntactically and
    semantically. (See http://citeseer.ist.psu.edu/chen89hilog.html for
    details, if unfamiliar.) 

    Since there are no sorts (or just one sort of everything), variables
    unsorted.

V.  RIF

    In RIF we have to combine the unsorted tricks of HiLog with the sorted
    tricks of multi-sorted logics.
    
    The unsorted part is due to the charter where we mention higher-order
    features and because RDFS is essentially such an unsorted language.
    For instance, we would like to be able to use the same URI as a predicate
    name and as a constant.

    The sorted part comes from the requirement to be able to accommodate
    the various other dialects, like first-order logic itself.  We need to
    allow sorts to be extensible because of the primitive data types and
    because we want to retain some control over which symbols should be
    allowed in which syntactic positions. For instance, in OWL and others
    integers and floating numbers cannot denote properties or concepts.

    A very general way to doing this sort of things is described in
    http://citeseer.ist.psu.edu/chen94sorted.html.

    Each variable should be assigned to a single sort. We can allow them to
    be assigned to multiple sorts meaning that they range over the symbols
    that lie in the intersection of the sorts.


	--michael

Received on Wednesday, 13 December 2006 16:55:37 UTC