[KIF] Re: SUO: tuples

[Chris Menzel]

On Wed, Jul 10, 2002 at 09:22:36AM -0700, Jay Halcomb wrote:
> From: "Mark Stickel" <stickel at ai.sri.com>
> > I also have reservations about sequence variables.
> >
> > 1. They are not commonly used in current theorem-proving systems and
> > it would often be difficult to add this capability.  Implementations
> > of theorem-proving and logic-programming systems often assume that the
> > arity of a term is invariant under substitution, which is false when
> > sequence variables are used.
> 
> Indeed. The current proposed ambiguous usage/underspecification of the
> arities of terms 

Hi Jay.  It wouldn't be accurate to say that arities are ambiguous or
underspecified in CL.  There just *aren't* any arities.

> would have to be resolved at the implementation level by some
> mechanism as yet unspecified, as far as I know, in these discussions.

It's not clear to me exactly what needs resolution here.  If I
understand you, you might have one of two situations in mind.  

(1) a given constant should indicate a strictly binary relation, a
relation that can only hold among pairs of things.

(2) a given constant should only ever be *used* as a binary predicate,
i.e., the only well-formed atomic sentences involving that constant
should contain that constant in predicate position with exactly two
arguments.

In the case of (1), with sequence variables, one could axiomatize the
property Binary noted in an earlier msg to John.  Or, without sequence
variables, one could axiomatize it schematically.  In the case of (2), 
as I've noted several times, you can add arity constraints such as in
the standard language of FOL and still be compliant with CL.  In these
cases, one simply provides a recursive specification of the relevant
restrictions.

Do these answers address your worry?

> For example, how shall it be determined whether some term is meant to
> be functional (designate a proper function, extensionally considered)
> or designate a proper relation? 

This is completely determined by context.  If something of the form 
(F a1 ... an) occurs as a term in an atomic sentence, then F is given a
functional interpretation.  If it occurs on its own as a sentence, then
it is given a relational interpretation.  If you must have some sort of
indication ahead of time, then you can either specify the functionality
of the relation signified by a constant axiomatically, or, again, you
can work in a syntactically restriced language.

Again, one of the early design decisions was to put as few restrictions
on CL as possible to allow maximum flexibility and maximum applicability
of the standard.  One can then add constraints to define restricted
languages that are still compliant in a well-defined sense.

> Are such conditions to be specified axiomatically? If so, is this to
> be done at the object language level or at the metalogical level
> (assuming a formal treatment of the metalogic)? Or is it suggested
> that there is no practical difference, at least in some cases?  How
> shall those cases be distinguished?

> Generally, what about the potential clashes between users using the
> same term but in different arities? 

Isn't that just a straighforward ambiguity, and hence to be resolved by
whatever mechanism you are using to resolve ambiguity generally, e.g.,
explicit namespaces?

> Or who intend relations which are differently functional 

Not sure what you mean by "differently functional".  Different
functional arities?  Again, sounds like a straightforward ambiguity to
me.

> or not in various components of the arities of the relations? 

Not sure what you mean here either.  Example?

> Or even with the same user? Have the proponents of sequence or row
> variables suggestions to put forth about these problems?

Let me know how you feel about the suggestions above.

-chris