[SCL] functions and functional relations: proposal to change the SCL semantics

[Pat Hayes]

I am seeking feedback on an SCL design issue.

In many respects, the changes made to the SCL presentation in the 
most recent drafts have made SCL more conventional that it used to 
be, in the sense that the SCL model theory leans over backwards in 
order to be as similar to a conventional GOFOL model theory as it 
possibly can. This has thrown into sharper light one way in which SCL 
is rather unconventional, however, even though in this respect SCL 
follows KIF: functions are considered to be identical to functional 
relations.

In a conventional GOFOL syntax, function symbols are lexically 
separated from relation symbols and are required to denote functions. 
Even if a relation symbol happened to denote the same extension as a 
function symbol, the question of their identity would not arise, and 
while the equivalence between them could be expressed by an axiom, 
for example
x=f(y) iff Rf(x,y)
(where Rf is the relation 'corresponding' to the function f) , it 
could not possibly be stated so as to be a tautology. 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.

This mirrors the usage in KIF and is generally considered to be a 
sensible way to proceed, but this equivalence does make SCL 
unconventional in a number of respects, as I outlined in an earlier 
message, and it complicates the translation from SCL into FOL, since 
the relational atoms are translated using holds but the functional 
terms are translated using app, requiring an adequate FOL translation 
to include all axioms of the form
(iff (holds x y z ...) (= y (app x z ...)) )
but only when x  occurs in both a relational and a functional 
position; the resulting sensitivity of the translation to minor 
syntactic changes illustrates the complications which arise. The SCL 
proof theory and the translation into FOL would both be a lot neater 
and more conventional (i.e simpler) if this equivalence between 
functions and functional relations were NOT imposed by the SCL 
semantics.  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)
-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.

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.  The current story explains SCL as 
arising from a process where two agents both use FOL but disagree 
about the lexical role of some symbols: A wants it to be an 
individual but B wants it to be a relation. The process of 
reconciling this disagreement requires that the mapping from relation 
names to relational extensions be projected into the universe so that 
individuals have associated relational extensions where needed, so 
that A's individuals can play B's relational roles. OK, so extend 
this idea to a disagreement about whether f is a function or a 
relation name: A says function, B says relation. In this case, we can 
just let it play both roles, and project them both into the universe 
as required. If the same entity is required to play both a relational 
and a functional role, then it has two extension mappings which apply 
to it: the relational extension is a set of sequences (tuples) and 
the functional extension is a set of pairs of individuals and 
sequences. They need have nothing particularly to do with one 
another. 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.

What this will do in practice is treat a symbol (in fact, any 
expression) used as a function name, and the same symbol used as a 
relation name, as being simply a pun: the same symbol has two 
independent meanings which are selected by the syntactic context of 
use. So there is no *logical* connection between the two f's in the 
following atoms:
(= x (f y))
(f x y)
and they might almost be two different names, in fact; so neither 
atom entails the other. Such punning is of course quite harmless in 
conventional FOL and is treated in the same way (though SCL extends 
this to complex expression which may also denote things in the 
universe.)

It is then up to an SCL axiomatizer to state any connections between 
the functional and relational uses of the same name, if these are 
considered to be desireable; and we might say that such axioms can be 
the result of a process of function/relation negotiation between the 
two hypothetical agents.

The KIF style (value last) can be stated by writing axioms like
(iff (=  (f y z) x) (f y z x) )
for each f (they have to be stated separately) and the current SCL 
convention can be stated succinctly by universally generalizing (2) 
above:
(forall (f x )(iff (= x (f @y))(f x @y))).
which could of course be considered to be part of a 'standard' named header.

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). Finally, the idea that the 
function/relation co-naming should be treated as punning has been 
mooted before by others in the CL group on pragmatic grounds, and 
this change goes along with that option.

Comments? (Howls of protest??)

Pat

PS. Possible objection: this makes SCL differ from KIF. Answer: it 
already differs from KIF in any case by using a different ordering 
convention for function values.


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