[SCL] SCL spec

[Chris Menzel]

On Tue, May 13, 2003 at 05:56:58PM -0500, Pat Hayes wrote:
> 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.

I think the semantics I've defined solves this problem in a KIFish way.
Predicate constants and function symbols both denote relations.
Function symbols are simply required to denote relations with functional
extensions.  Hence, if in some language a given function symbol turns
out out also to be a predicate constant, it will denote a relation (as
predicate constants must) with a functional extension (as the relations
denoted by function symbols must).  So for sych function symbols f,
(f (f @s) @s) is a logical truth.

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

Need more than numerals for this -- need number theory.  Did we ever
decide definitively that we want a basic number theory in SCL?

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

The requisite tweaking is to repalce "iff" with "only if".  There is no 
axiomatizable sufficient condition for Arity without modality.

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

Agreed.

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

The former.  I wasn't clear.

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

No.  I.e., no need for separate treatment, as indicated above.

-chris