[SCL] SCL spec

[pat hayes]

>I've put an SCL spec on the web: http://cl.tamu.edu/docs/scl.html .
>It is not highly polished, but it will do as a start to get ideas fixed.
>
>Features (all negotiable):
>
>* No distinction between predicates and individual constants.

For the record, I would prefer that we do make such a distinction in 
the abstract syntax, with appropriate (and conventional) assignments 
to the various parts of the term and atom syntax, and conventional 
semantic requirements expressed using extension mappings (ie function 
symbols have functional extensions, relation symbols have relational 
extensions);  but not require that these categories are disjoint in 
any concrete syntax. This keeps the exposition maximally 
conventional-seeming.

The MT should assign a functional extension (set of pairs of tuples 
and things) to every function symbol and a relational extension (set 
of tuples, a different mapping!) to each relation symbol.   Then 
there is a separate question, of how  to relate the extensions of a 
symbol with two extensions (ie which is both a relation and a 
function). Different sublanguages can approach this differently, eg a 
conventional Principa syntax could allow this kind of overloading but 
give it no semantic significance whatever. A more KIFish version 
could allow it and require that the relational extension of a symbol 
with a functional extension be related in one of the obvious ways. 
One of these (<<...> a> = <a ...>) can be axiomatized:
(?x (?x @y) @y)
The other obvious one breaks the @ syntax, ho hum. But whatever, we 
at least keep the core free of arbitrary conventions about which 
people might be inclined to fight.

>* Hence, no syntactic notion of arity (though arity could be enforced
>   axiomatically for any given constant).

Some thoughts on arity arising from todays telecon.

There are two different notions of what it means to say that a 
predicate symbol R  has an arity. On one view, it means that any 
atomic expression using R which has a different number of arguments 
is ill-formed, a syntactic error; on the other view, it means that 
any such expression is logically false.  Call these respectively 
syntactic and semantic arities.

It is relatively easy to introduce semantic arity into SCL: it is 
simply a predicate on predicates. If we have numerals in the language 
than it is trivial to write such a predicate as a relation between 
predicates and numbers, and define it by using a recursively defined 
function which counts the number of arguments:

LengthOfTuple(0) and (LengthOfTuple(n, at x) implies 
LengthOfTuple(+1(n), ?y, @x) )

Arity(?x, n) iff ( ?x(@y) implies LengthOfTuple(n, @y) )

(This gives the universally false predicate every possible arity, so 
might need to be tweaked slightly)

If we want to have syntactic arity, however, then we need something 
which we do not have at present, which is some principled way to 
state a syntactic constraint on an SCL language. Syntactic 
constraints have to be superficial  - they cannot require the 
exercise of semantic deductions in order to reveal their truth, and 
must be checkable by a parser. So the question arises, what 
computational abilities can be reasonably assumed of a parser which 
is expected to process these constraints? For example, the very idea 
of having arity as a constraint seems to suppose that a parser can be 
expected to be able to count the number of items of a certain 
syntactic category occurring in a span of a document defined by some 
other category. This is not a trivial ability: a parser based 
entirely on matching regular expressions would be unable to check it, 
for example. If we were to contemplate more elaborate syntactic 
constraints - say, having a sorted syntax with a sort hierarchy 
defined by declarations - then the burden on a parser could get 
considerably greater.

Let me propose that as a fallback position we simply rely in the core 
on semantic arity, and meanwhile discuss whether we wish to try to 
define a systematic notion of a syntactic constraint on an SCL 
language, and if so how it can be described.


>* Semantically there is a distinction between individuals and relations,

Well, some individuals are relations, right? Or do you mean 
'individual' to exclude relations by definition?

>   but nothing prevents the class of relations from overlapping or being
>   included in the class of individuals.

Apparently not.

>* Relations do not come with fixed arities (though of course nothing
>   prevents introducing such relations).
>* There is a separate class of function symbols.
>* Function symbols are variably polyadic.

As far as adicity goes I don't see that we need to treat functions 
differently from relations (? Am I missing something here?)

>* Sequence variables can only occur in tail position in function terms
>   and atomic formulas.

Right, I guess. Im still a bit worried about that tail position 
thing, but I will worry in private :-).

>* Sequence variables never explicitly quantified; semantically, they are
>   implicitly universally quantified by quantifiers with widest possible
>   scope.

Right.

>
>Comments/criticism/discussion/correction welcome.
>
>-chris
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


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