New version (was: Re: [SCL] functions and functional relations:
proposal to change the SCL semantics)
Pat Hayes
phayes at ihmc.us
Tue Feb 10 00:59:14 CST 2004
OK, I wrote up the new version before reading your email, but I didnt
actually overwrite the old version, so you can see the new one (which
IMO is a lot better and will be better still in another working
half-day) at
http://www.ihmc.us/users/phayes/SCL_current_2004_rf.html
(rf for 'relation+function').
There are quite a lot of other rewrites as well. In particular Ive
put the conventional binary = back into the syntax and MT, and
renamed the variadic one 'scl:same' (cf. owl:sameAs), and have
further simplified the 'fitting' idea (now named 'folding' and
presented as an extra structure defined recursively rather than a
condition to be satisfied. This will simplify some proofs, I think.)
There is a new (or newly sharpened) intuitive idea now behind the
design of the whole language, a kind of overall story that makes a
certain global sense, where the entire design is motivated by the
idea of reconciling two different conventional structures which
disagree about the signature to use for a notation. See the
introductory discussion and the later figures and the surrounding
discussion for this.
I'm quite excited by this idea, it seems to make sense of a lot of
stuff that was kind of arbitrary, if elegant, before. For example, it
'explains' why SCL needs to allow variadicity. And it provides a
potentially quite convincing argument for the *utility* of SCL, not
just its semantic elegance. It makes for a much neater story of how
SCL relates to GOFOL (ie one motivated by something more important
than just keeping Ian Horrocks satisfied.) And it handles the full
WW syntax !
>On Thu, Feb 05, 2004 at 12:20:33AM -0600, Pat Hayes wrote:
>> In SCL, however, the same symbol can be used for f and Rf, and the resulting
>> axiom IS a tautology (in the current semantics):
>> (iff (= x (f y)) (f x y) ) ....... (1)
>> This must be true in all interpretations, since the use of the symbol
>> in a functional position requires that it denote a functional
>> relation. In fact the general form
>> (iff (= x (f @y)) (f x @y) ) .....(2)
>> is a tautology also.
>> ...
>> Is this equivalence worth the meta-theoretic complication
>> that it produces? I suggest not, and that we should abandon it.
>>
>> I can see arguments both ways. If the thesis is to keep the status quo,
>> then:
>> Pro:
>> +1 it is semantically more elegant
>> +2 it has been found convenient by KIF users
>> Con:
>> -1 it makes SCL less conventional as a first-order logic, especially
>> in its proof metatheory (eg SCL doesnt obey the deduction theorem)
>
>You've probably show why this is so in an earlier msg, but could you indulge
>me and explain (once again) what this is so? I'm having a great deal of
>trouble believing it.
The issue can be illustrated by the example in the email (also in the
previous version of the draft). Consider the texts
p: (R a b)
q: (= a (R b))
With the old semantics, q entails p but p does not entail q (since p
can be satisfied by interpretations in which I(R) is not functional).
But the killer is that just by *using* the name in a function
position is enough to make it a function, so that (p implies q) *is*
a tautology:
|= (implies (R a b) (= a (R b)) )
but (R a b) |/= (= a (R b))
In the holds-app translation, this is a consequence of the fact that
when R is used both as a function and as a relation, we are obliged
to add an axiom relating the two translations, such as
(iff (holds R x y) (= x (app R y)) )
we have to add this to the translation of
(implies (R a b) (= a (R b)) )
but not to either of the translations of p or of q. Hence the problem.
In the current version, neither of p or q entails the other and the
implication isn't a tautology (though you can assert it as an axiom
if you want it to be true.)
>
> > -2 it complicates the embedding of SCL into FOL (which is
>> complicated enough already because of the treatment of =)
>> -3 if we don't have it as a logical truth, then the equivalence can
> > be restored in particular cases by writing an SCL axiom, so we get
>> the practical benefit in any case.
>> -4 The convention that relates function to relations is arbitrary
>> (value first or last??) and so should not be made into a logical
>> necessity.
>
>I don't get this last argument. Conventionality already reigns in standard
>FOL: the syntax of atomic formulas (e.g., predicates could occur last instead
>of first); the syntax of boolean formulas; the number of variables that can be
>bound by a single quantifier; etc. So what if a little more conventionality
>enters the picture here?
Well, its not a strong point, but even we (ie the CL group ) had some
disagreements about which convention to use, if you recall. So why
not let people choose their own? Particularly as they can state them
using SCL itself.
My thinking on the whole SCL design has become sharpened by the
intuitive idea of an SCL interpretation being the result of a
hypothetical negotiation between two (or more) people all trying to
interpret a vocabulary in a conventional interpretation structure.
Sometimes they can disagree and it doesnt matter: if you think its
n-ary and I think its m-ary, OK it can be both-ary. If you think its
a function and I think its a relation, OK it can be both: in either
case we can regard it as just punning and nothing will require us to
take any special care with inferences: we can both draw the FO
conclusions we like and everything works out fine. Its only when one
of us wants an individual and the other wants a relation or function
(something with an extension which would not not normally be in the
universe) that we need to be particularly careful.
On this view, then, we start with conventional GOFOL and then
negotiate recursively to an accommodation. So Im now assuming that
the guideline should be: do the absolute minimum required to ensure
that *first-order* reasoning will always work for everyone, no matter
what attitude they take to the vocabulary. Then the changes from
conventional FOL are motivated by conventional FOL itself, which has
a nice feel to it. But now, that doesnt require us to identify
functions and relations. GOFOL doesn't identify relations and
functions, and nothing in the negotation requires us to do that
identification. So if we aren't required to do it, lets not do it.
If we do it, in fact, we *break* the holds-app mapping which takes us
back to GOFOL.
> After all, it's not the *convention* that becomes a
>logical necessity, it's the underlying truth; we just adopt a
>certain convention
>about how to express it.
I don't think that is really a defensible position. It seems to me
that since there is a clear *logical* distinction between a
relational extension of, say, pairs which is functional on the first
position versus one that is functional at the second position, to
claim that the connection between functional relations and functions
is a LOGICAL identity is stretching the notion of logic too far. One
can obviously map between functional relations and functions, but
they aren't the SAME thing. Conceptually, a functional extension is
made up of pairs of argument sequences and values, which (I now
think) really is a different kind of animal than a set of sequences.
Functions inherently have a direction: they go from and to. relations
just kind of obtain between things.
At any rate, the use of a function *symbol* invokes a lot of baggage
which is not invoked by its use as a relation symbol, particularly in
the construction of proofs. There's a kind of syntactic convention
built into a function symbol which is missing from a relation symbol.
>
>> Seems to me that -3 cancels +2, and that the remaining cons outweigh
>> the pros, so I propose to modify the FOL semantics so as to allow
>> functions to be distinct from relations. (I have not yet made these
>> changes to the draft document, but will do so very soon unless anyone
>> objects strongly.)
>>
>> Here's how it goes, in a sketch.
>
>I believe we actually considered a semantics like this some time ago.
Could be. I no longer know if I'm inventing things or remembering
them. In fact, come to think of it, I think I might have dreamt that
a while ago.
> It is ok
>by me if you really think it has strong advantages, but it is not clear to me
>that it does. Rather, it seems to me that in cases where the same term being
>used as both a function symbol and a predicate symbol is more likely to be a
>functional relation
Sure, but 'functional relation' isn't well-defined until you specify
HOW its functional, and people could legitimately differ on that
point.
>; in fact, it's hard for me to envision the scenario you
>describe in which A and B disagree over whether R indicates a function or a
>relation unless there are systematic semantic connections between
>the two. And
>if the two uses of the term *are* completely unrelated, then why introduce a
>methodology that permits the punning you suggest? Shouldn't ambiguity be
>identified and *avoided* rather than being tolerated? I guess you wil respond
>with your point about negotiation:
>
>> This satisfies both A and B, but leaves them some room to negotiate further
>> on what connection, if any, there might be between their interpretations of
>> the symbol.
>
>But if there is none, why permit the ambiguity to remain?
But there is some. You might have a relation which is first-argument
functional and I might have one which is last-argument functional..
More seriously, we COULD have completely different kinds of function
in mind. Take the marriage example, and suppose that you have a
database that assumes no bigamy and always lists husband's name
first. Then you could think of it as a function from husbands to
wives, OK. But someone else could treat it as a 3-way relation and
think of it as a function from (husband-wife) pairs to
time-intervals. Both are perfectly good functional readings of the
*same* variadic relation. By agreeing to accept variadicity we have
kind of made things awkward for a 'standard' relation/function
mapping, seems to me, in fact. KIF was much more attached to the
LISP conventions, but that's only one way to think. There's nothing
in relational semantics about tail-recursion, right?
> The existing
>methodology seems to take the opposite tack -- use the same term as both
>function sym and relation sym only if they have a certain close semantic
>connection. Otherwise, choose different symbols.
Yes, but consider: that is advice to one person designing the whole
axiom system. That's exactly the kind of advice we can't possibly
expect the whole world to follow when they try to trade content. And
if some bunch of folks want to do this, they can all agree on it
explicitly:
(forall (r)(implies (functional r) (r (r @x) @x))))
is what they have to agree to, and the current semantics will make
sure that any such r is a functional relation which satisfies the
convention.
>
>> The meta-theoretic gains of this change are considerable, and the
>> above story seems to provide a reasonable justification for the
>> slight extra semantic complication (which is in fact very minimal
>> when written out carefully).
>
>Probably so, and (though I reserve the right to do a 180 on this! :-) the
>metatheoretic simplicity is probably worth the loss of elegance.
Well, take a look at the current draft cited above and let me know
what you think. Note that the requirements of totality of functions
are now a lot easier to state (they boil down to a single condition
on terms.)
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
More information about the SCL
mailing list