[SCL] roles and arguments

[pat hayes]

Following our telephone conversation, here is the proposal for 
allowing 'roles' in the SCL syntax.

1. The syntax allows atomic sentences with the structure PredTerm + S 
where S is a *set* of role pairs, each of which is a pair RoleSym + 
Term:
P+{R1+T1, ....Rn+Tn}

RoleSym is a new basic syntactic category treated similarly to the 
other 'constant name' categories, ie required to be disjoint from the 
variables. RoleSym can overlap with FunSym, however.

2. RoleSyms denote functions from tuples of individuals to 
individuals, called role functions. Supplying a role function for 
every RoleSym is part of the job of an interpretation.

I(P(r1:a1 .... rn:an)) = true just when there is a t in ExtI(I(P)) 
and ExtI(I(ri))(t)=ai, 1<=i<=n

ie

just when there is a t in ExtI(I(P)) with ai<>t in  ExtI(I(ri)), 1<=i<=n

and that is all :-)

Discussion.

1. This does not in itself establish any connection between the truth 
of atoms using the different styles, other than that if a role-style 
atom is true then *some* tuple-style atom must be true (which in CL, 
but not legal SCL, we could write as

(exists (@x) (P @x))

2. It does not require the values of the role function to actually be 
in the tuple.  Thus it allows the case sketched in the earlier email 
where the tuple is a singleton representing a 'trope':

P(r1:a1 .... rn:an) <==>  (exists (?x) P(?x) & r1(a1, ?x) & ... & rn(an, ?x) )

but it would also be natural to think of the role functions as 
selection functions. Since these would be functions on sequences, 
i.e. just n-ary functions in our semantics, we can specify them very 
simply by writing things like

Married(?x ?y) implies ?x=wife(?x ?y) and ?y=husband(?x ?y)

and then be able to conclude that

Married(Mary, John) implies Married{ husband:John  wife:Mary}

which avoids the need for the special 'Nth' functions.  All this 
requires is that the syntax allows the categories of RoleSym and 
FunSym to overlap, which is always OK since roles are required to be 
functional. Even SCL syntaxes which don't allow function symbols can 
manage by using the
?r(?r(@x)@x) convention:

Married(?x ?y) implies wife(?x ?x ?y) and husband(?y ?x ?y)

3. This semantics supports the entailment of any subset of the atom, eg

Married{wife:?x husband:?y} implies Married{husband:?y}

The implicand clearly here means "y is somebody's husband", and this 
is analogous to

Married(?x ?y) implies (exists (?z) Married(?z ?y))

so 'missing' roles are implicitly existentially quantified, which 
seems to me to be just right.

Q: Do we need a general syntax for talking about such subsets, so 
that the general form of this implication can be stated? Seqvars 
allow us to generalize over the tuple notation, but we have no 
analogous way to generalize over the role-set notation. We could, I 
guess, invent a set-var notation #x and treat it similarly to seq 
vars, so we could write something like

?P{?x:?y}#s implies ?P#s

Whaddayathink? (Nahhhh.....)

4. On the other hand, we might want to require any syntax allow the 
designation of the empty set, because (in CL, not SCL, syntax:)

?P{ } iff (exists (@x)?P(@x) )

so the empty role set is kind of handy; it adds some expressivity 
which we can't get any other way.

-------

On the whole I think this is fairly neat. It works for the natural 
cases, allows many options, and makes for a very simply way to 
connect roles with tuples. And it allows for a general way to build a 
trope framework if anyone wants one, although to state the trope 
axioms in full generality goes beyond SCL expressivity (it needs at 
least all at -exists? and probably higher, which is outside Lw1w; not 
surprising, really, since tropes seem to me to be more complicated 
than sets.)

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 ihmc.us       http://www.ihmc.us/users/phayes