Re: [KIF] Re: SUO: tuples
Chris,
I have never been happy with the two kinds of variables in the old KIF.
And the proposed extensions to KIF for the CL standard make me even
less happy. Basically it all looks like an ugly kludge that would be
a nightmare to teach to students. This is, of course, an esthetic
judgment about language design, and as they say, chacun a son gout.
So many of the arguments would have to do with such squishy topics as
ease of reading, teaching, use, and familiarity for students who come
to CL from various backgrounds. The more serious issues relate to the
issues of supporting the various versions of logic-based languages that
we would like to support under the CL umbrella.
Some comments on your comments:
CM> What are you categorizing as a problem? And why? Is it merely the
> fact that there are two kinds of variable? Why is that any more of
> a problem than there being, say, two types of constant (predicate and
> individual) in ordinary predicate logic?
That is a good list of questions, and I'd like to start with the last
one first. Ordinary predicate logic has been around for over a century,
and the distinction between predicates and individuals resembles common
practice in both mathematics and programming languages. When we try
to teach any CL dialect to students (and professors, who are even harder
to teach than most students), we can assume that they are familiar with
object-like things and program-like or function-like things. I have
never found any student who has ever had a problem with the distinction
between predicates and individuals. We can assume that distinction
as something familiar, which would not be a stumbling block. On the
contrary, the absence of such a distinction would be a stumbling block.
The two kinds of variables in the proposed CL are weird for predicate
calculus, for traditional mathematics, and for all common programming
languages. Right there is a major stumbling block for every student.
I could invent an extension to CG syntax to accommodate it, but then I
would have to tell the CG community why that extension is desirable.
Since I myself do not desire it, I would have to argue for something
I don't like, and I'm afraid I would not be very convincing.
CM> These are simply different syntactic types to play different
> semantic roles. And actually, in full CL, there are virtually no
> restrictions at all on how sequence variables can be used. (Let's use
> Pat's suggestion of "row" variables, to avoid the appearance that
> such variables are simply sorted first-order variables that range
> over sequences in the domain.)...
That parenthetical expression is an admission that students are likely
to be confused about "row" or "seq" variables. I would prefer to
avoid that confusion right from the beginning by making them ordinary
variables whose value just happens to be a sequence.
CM> I think you are misremembering. Introduction of sequences would
> involve no foundational problems at all. Sequences are just another
> type of object. The objection (well, my objection) was that row
> variables enable one to capture a variety of linguistic and semantical
> phenomena without having to introduce sequences into the domain as
> first-class objects.
But that is exactly what I want. Sequences, lists, or tuples -- pick
your favorite name -- have proven their worth in LISP and Prolog, and
they are now available in all modern programming languages. Since they
will be essential for most, if not all major applications of CL, there
is no reason to avoid them as first-class objects. And once we have
them, we don't need the kludgy row variables.
CM> But I will make a stronger point here: certain phenomena
> CANNOT be captured via a theory of sequences. Row variables are
> essential....
>
> So you are proposing that we add a first-order theory of sequences to
> CL as an alternative to row variables. Well, we could add a theory
> of sequences, but no such theory will be expressively equivalent to
> row variables. That is easy to show. For example, in CL, as we all
> know, there is no notion of a predicate, let alone an n-place
> predicate.
These are additional aspects of CL that I have never been happy with.
I realize that you have been proposing that idea, but I have not
considered that to be more than a suggestion. I have still been
assuming something closer to the old KIF 3.0. For the purposes of
theorem proving, I would even like to distinguish predicates from
functions.
CM> (There are two reasons for this: (i) relations are not assumed
> to have fixed arity, and (ii) relations are first-class objects that
> can be arguments to other relations.) Nonetheless, relations can
> have a fixed arity. Row variables enable arities to be axiomatized.
In other words, row variables help you dig yourself out of the
hole that was created by some of the other features I don't like.
The sample axiom for Binary is a metalevel example, and we need a
much richer metalevel than that for all the things we want to do.
It was not convincing.
CM> ... the justification of introducing a theory of sequences into
> *CL proper* is less than clear. I do agree that it would be handy
> to have such theories ready to hand for applications. I would just
> balk at considering including them into anything called a Common Logic
> standard, as they are not part of what is traditionally considered
> logic. They are theories, plain and simple, built on top of some
> logic.
Yes, I agree that a theory of sequences is part of ontology, just as
a theory of numbers would be. And I agree that having a collection
of such theories would be useful.
To summarize, there are three related languages that the CL committee
has started with:
1. Traditional predicate calculus in its many different variants,
most of which are closely related syntactic variants.
2. KIF 3.0, which has been and continues to be used in a wide
range of projects as a convenient syntax that express #1 in
an easily parsable form.
3. Conceptual graphs, which have been mapped successfully to and
from both #1 and #2 for various projects.
There are also an open-ended number of other projects that use some
kind of logic-based notation, which could be brought under the CL
umbrella:
4. Prolog and other logic-programming languages, many of which have
subsets that have been mapped to and from #1, #2, and #3.
5. A variety of description logics, many which have also been mapped
successfully to subsets of #1, #2, and #3.
6. The CycL language, which has also been mapped to and from versions
of #2 and #3, but which has features that have not yet been fully
brought into alignment with any version of KIF, CGs, or CL.
7. A large variety of other logic-like notations including UML, RDF,
and various things called topic maps, concept maps, etc.
None of the features in the proposed extensions to KIF 3.0 would help
in any way to simplify the mappings to and from the languages in
#4. #5, #6, and #7. And they certainly don't help in the mappings
to and from #1, #2, and #3. On the contrary, they would make many
of those mappings more difficult. So why are we considering them?
Recommendation: If we add or subtract anything to or from the old
KIF 3.0, it should be for the purpose of simplifying the mappings
to various other languages in this list. If the new features do
not simplify those mappings, then there should be very compelling
reasons for considering them. So far, I haven't seen any such reasons
John Sowa