A proposal of "sorts"
Tomas Uribe <uribe@CS.Stanford.EDU>
Date: Fri, 3 Dec 93 21:16:47 -0800
From: Tomas Uribe <uribe@CS.Stanford.EDU>
Message-id: <9312040516.AA27752@Xenon.Stanford.EDU>
To: Interlingua-working-group@ISI.EDU
Subject: A proposal of "sorts"
Cc: uribe@cs.stanford.edu
To the Interlingua Working Group: this is a draft proposal concerning
the issue of sorts and types in KIF. Please send me any comments that
you may have. Once all objections are sorted out (pun intended) we can
send this out to the Interlingua list.
Thanks,
- Tomas E. Uribe uribe@CS.Stanford.EDU
==========================================================================
While the discussion on first vs. higher-order logic simmers
on the Interlingua list, I would like to go back to an earlier
(and simpler!) issue: whether typed variables should be included in KIF.
As far as KIF is concerned, the question is whether types should
be part of the syntax or viewed as unary predicates. I propose the
latter alternative as being the simplest and more flexible one.
It is true, as Fritz Lehmann has pointed out, that sorts can be
very useful in speeding up automated deduction; they can also
help make axiomatizations more readable, compact and natural.
However, all of these advantages can be retained even if sorts
are seen as "only" syntactic sugar for unary predicates.
The only obstacle, perhaps, is that sorts may have to be extracted
automatically from axiomatizations---but this can be done without
much trouble (this was done in, for instance, the Markgraf Karl
theorem prover [3],[4].)
Building sorts into the syntax has the main disadvantage
that either (a) the set of sorts has to be fixed beforehand
with no possibility of extension, or (b) a standard language for
defining sorts has to be decided on. (a) is clearly too limiting;
but (b) is too:
Many systems use sorts, but different systems handle different kinds!
Some choose less expressive ones at the advantage of speedier sort
inference; others allow for more expressive sorts that require more
complex and specialized inference mechanisms. What kind of sorts would
we want to allow? Will the sorted logic be many-sorted, order-sorted,
monomorphic, polymorphic, static, dynamic? What kind of declarations
would be used?
We can simply allow for the most general mechanism commonly used
for defining sorts, namely, the axiomatization of unary predicates
in first-order logic (see e.g. [1], [2]). Note that even when sorts are
built into the syntax, the equivalent effect is obtained through a
"relativization" theorem (e.g. [5]). Systems can be free to translate
some or all of these unary predicates into whatever sort structures
they can handle; and systems that make no provision for sorts will
be happy too.
============================================================================
The proposal is then to use restricted quantifiers as follows:
Add, as syntactic sugar to quantifiers, the constructions
(exists ((?x P)) <Sentence>)
and
(forall ((?x P)) <Sentence>)
as abbreviations for
(exists (?x) (=> P(?x) <Sentence>))
and
(forall (?x) (=> P(?x) <Sentence>)).
In general,
(<quantifier> ((?x1 P1) .. (?xN PN)) <Sentence>)
abbreviates
(quantifier (?x1 ...?xn) (=> (and P1(?x1) ... PN(?xN))
<Sentence>))
A warning: there is the well-known "empty sort problem:" Just writing
[1] (exists ((?x P)) <Sentence>(?x))
does not ensure that
[2] (exists (?x) <Sentence>(?x))
is true, since
[3] (exists (?x) P(?x))
may be false, so that [1] is trivially true. That a "sort" is non-empty
can be ensured simply by asserting [3] for every appropriate predicate P.
(In any case, it sometimes may be desirable to allow for empty
sorts---see [1].)
==========================================================================
References:
[1] A. G. Cohn, "A Many-Sorted Logic with Possibly Empty Sorts",
in CADE-11, pp. 633-647, volume 607 of Lecture Notes in AI,
Springer-Verlag, 1992.
[2] Alan M. Frisch, "The Substitutional Framework for Sorted Deduction:
Fundamental Results on Hybrid Reasoning", Artificial Intelligence
49:161--198, 1991.
[3] Hans-Jurgen Ohlbach and Jorg Siekmann, "The Markgraph Karl
Refutation Procedure", in Computational Logic: Essays in honor of Alan
Robinson (Lassez and Plotkin, eds.), pp. 41-112, 1991.
[4] Manfred Schmidt-Shauss, "Mechanical Generation of Sorts in Clause
Sets", SEKI report 85-VI-KL, Fachbereich Informatik, Universitat
Kaiserslautern, Germany, 1985.
[5] Manfred Schmidt-Shauss, "Computational Aspects of an Order-Sorted
Logic with Term Declarations", volume 395 of Lecture Notes in AI,
Springer-Verlag, 1989.
==========================================================================
- Tomas E. Uribe uribe@CS.Stanford.EDU