[SCL] General sugar: an idea for discussion

[pat hayes]

A presentation at the DAML PI meeting this week by Ben Grosf reported 
on the RuleML initiative. One of the topics he covered was the idea 
of expressing relations not by giving their arguments in an order (ie 
as an n-tuple) but instead by having named 'roles' for each argument, 
rendering the syntactic ordering irrelevant, and also by the way 
allowing partial information to be provided about an atom. Now, this 
is of course an old idea, but it seems to recur with remarkable 
regularity and be adopted again and again, so I wondered perhaps we 
should think about providing a syntax for this in SCL.

I know, I know: we already do, in effect, because this amounts to the 
translation

(R t1 ... tn) <=> (exists x  (R x) & (Role1 x t1) & (Role2 x t2) & 
.... (Rolen x tn) )

and we could even have the roles be parameterised by the relation:

(R x) & ((role1(R) x t1) & ....

But bear with me. The point is not to provide any new expressivity, 
but to allow syntactic sugar which explicitly handles this form of 
usage since it is so popular and gets reinvented over and over again. 
Logicians tend to dismiss such matters, but providing and 
manipulating alternative surface syntaxes is a major part of the 
actual work done by both people and software, so we ought to look at 
this seriously.

OK, next thought. We have already discussed one kind of sugar 
(restricted quantifiers), and now Im suggesting another. Maybe there 
is a general pattern here. Could we give some *general rules* for 
syntactic sugaring? It has to be a syntax extension which doesnt 
interfere with the regular syntax and which comes with an elimination 
equivalence, so that any expression that uses it is equivalent to one 
that does not. Now, here's my thought: both of these examples could 
be handled syntactically by the same general trick as the 
comment-wrapper idea. A restricted quantifier syntax can be just a 
quantifier syntax with a wrapper on variables to attach the 
restriction; and a 'roled' argument is just an argument term with a 
wrapper to attach the role name. So maybe this is a simple but useful 
general technique for allowing a range of special syntactic sugars. 
The only requirement is that it must be possible to somehow recognise 
the kind of wrapper being used (it might be contextual in a 
particular concrete syntax, of course; just so long as the context 
fixes the intended desugaring (souring?) equivalence unambiguously.

Thoughts? Objections? Questions?

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam