definitions-proposal
schubert@cs.rochester.edu
Date: Sat, 28 Jul 90 06:49:26 -0400
From: schubert@cs.rochester.edu
Message-id: <9007281049.AA03621@ash.cs.rochester.edu>
To: interlingua@venera.isi.edu
Subject: definitions-proposal
PROPOSAL CONCERNING TERMINOLOGICAL KNOWLEDGE (DEFINITIONS)
PREFACE
Judging from the amount of discussion that has gone on, the syntax
and semantics of definitions is considered a very important issue.
The following tentative proposal was produced in response to some
prodding from Rich, who thought that Ron's remarks about
substitutional definitions and my further comments should be
developed into a technical proposal for the interlingua. The
result is rather more lengthy, involved and incomplete than I
had hoped...
INTRODUCTION
I think part of the problem in the ongoing discussion of definitions
has been the fact that we haven't gotten clear about whether
definitions are object language or metalinguistic constructs. My
view is that we can sensibly, and usefully, have both. So I'll first
propose a metalinguistic syntax for substitutional definitions, and
then comment on the meaning of object-language definitions. (I'll
refer to the latter as "analytic definitions", for reasons to be
explained.)
The metasyntax for substitutional definitions is not to be confused
with Mike's syntax of "metalevel knowledge", based on quotation.
The latter, insofar as it is aimed at expressing notions like
necessity and belief, is part of the interlingua proper - the
language used to describe the domain of discourse (which by fiat
includes the entities describable using quotation, viz., expressions).
The metalinguistic constructs below are in "meta-interlingua" (meta-
KIF?); they say NOTHING about the domain. I will later speculate,
however, whether this metalinguistic knowledge can be pulled down
to the object level using the (very rich) resources of KIF.
SUBSTITUTIONAL DEFINITIONS
A substitutional definition provides some new (often more concise)
way of writing some class of object-language expressions. The paradigm
examples are definitions of new symbols in logic texts, such as
phi <=> psi =def (phi=>psi)&(psi=>phi)
or
(E alpha)phi =def ~(alpha)~phi
where phi and psi are wffs and alpha is a variable. These definitions
sanction free use of the defined symbolism in the object language,
and the meanings of the new symbols are not independently defined.
Rather, the constructs in which they participate have whatever meaning
results upon substitution of the defining expressions for the defined
expressions. There is an obvious analogy to macros, EXCEPT that the
defined expressions need not in general be replaced by defining
expressions before inference begins; rules of inference can be DERIVED
>From those originally given, covering the new syntax. In other words,
substitutional definitions can provide genuine EXTENSIONS of the
object language.
The problem, then, is to provide a formalized metasyntax for the above
kinds of informal definitions. One thing that's immediately clear,
if we want to match the flexibility of the logicians' definitions,
is that in general we need to be able to specify not just substitutions
for individual defined symbols, but for PATTERNS OF USE of defined
symbols (like the use of "<=>" flanked by formulas). Sometimes, we
may want to use the same defined symbol in different patterns (see ":"
in examples 3 and 4 below). Occasionally, we may even want to specify
patterns of use involving multiple defined symbols ("E" and ":" in
example 5), or multiple occurrences of the same defined symbol (example
10).
To specify patterns of use, we need METAVARIABLES (schema variables)
to stand for various kinds of expressions of the object language -
variables, sentences, terms, and so on. We need a distinguishable
type of atom for these, and I will use prefix $$ for individual
metavariables and prefix @@ for sequence metavariables. (A couple
of other possibilities:
object-level variables metalevel variables
individual sequence individual sequence
?x $x ??x $$x
?x ??x $x $$x
Comments?)
As header of these definitions, I suggest METADEF, to ensure a clear
distinction from object-level definitions like defrelation and
defprimrelation.
With these preliminaries, a substitutional definition may be
formalized as an expression of form
(METADEF sigma1 sigma2)
where
(1) sigma1 is an (object-level) atom or a list of (object-level)
atoms and metavariables (with repetition allowed);
(2) the sigma1-pattern must not be unifiable with the sigma1-
pattern of any other METADEF (where only metavariables
function as unification variables); this prevents ambiguity;
(3) sigma2 is an (object-level) atom or list structure, whose
ultimate atomic constituents are (a) object-level atoms, but
excluding at least one of the atoms of sigma1; the excluded atoms
are called the DEFINED symbols; (b) metavariables, including all
those and only those appearing in sigma1; and possibly, (c)
metalevel function symbols, which can appear only as heads of
list structures; (metafunctions are distinguished by prefix "#"
and must have algorithmic definitions);
(4) sigma2 must contain no unbound object-level variables (but it
may contain quantified variables); this prevents "accidental
binding" by external quantifiers; and
(5) any defined symbol of the METADEF that appears in another
METADEF must be a defined symbol there as well.
The intended notion of "object-level atom" includes new logical atoms
(such as new quantifiers and logical connectives) and defined
"punctuation" signs (see examples) as well as the atoms listed in
table I of the KIF document.
EXAMPLE 1: renaming an atomic symbol
(METADEF & and) Note: the defined atom is "&"
EXAMPLE 2: changing the logical syntax
(METADEF (@@x ==> $$y) (=>@@x $$y)) Note: the defined atom is "==>"
EXAMPLE 3: introducing a new "exists" syntax
(METADEF (exists $$x : $$y $$z)
(exists $$x (and $$y $$z))) Note: the defined atom is ":"
EXAMPLE 4: introducing a new "forall" syntax
(METADEF (forall $$x : $$y $$z)
(forall $$x (=> $$y $$z))) Note: the defined atom is ":".
Examples 3 and 4 are compatible,
since the patterns do not unify.
EXAMPLE 5: variant of example 3
(METADEF (E $$x : $$y $$z)
(exists $$x (and $$y $$z))) Note: the defined atoms are "E",":"
EXAMPLE 6: introducing a new quantifier ("there is exactly one")
(METADEF (E! $$x $$y)
(exists $$x (and $$y
(forall (#UNUSEDVAR $$y)
(=> (#SUBST (#UNUSEDVAR $$y) $$x $$y)
(= (#UNUSEDVAR $$y) $$x) )))))
where #UNUSEDVAR is a 1-place metafunction whose value is the first
(object-level) individual variable not appearing in the given argument
expression, in some fixed enumeration of infinitely many (object-level)
individual variables; and #SUBST is a 3-place metafunction whose
value is the expression obtained by substituting the expression
given as first argument for all free occurrences of the atom given
as second argument in the formula given as third argument.
EXAMPLE 7: abbreviating a compound formula, using "bachelor"
(METADEF (bachelor $$x) (and (male $$x) (not (married $$x))))
Note: the defined atom is "bachelor"
EXAMPLE 8: abbreviating another compound formula, using "isa"
(METADEF ($$P isa $$Q) (nec-a '(forall $x (=> ($$P $x) ($$Q $x)))))
Note: the defined atom is "isa";
"nec-a" is discussed below
EXAMPLE 9: "abbreviating" a functional expression
(METADEF (paternal-grandfather $$x) (father (father $$x)))
Note: the defined atom is "paternal-grandfather"
EXAMPLE 10: changing the syntax of enumerated sets
(METADEF (: @@x :) (set-of @@x))
Note: the defined atom is ":"; "set-of" is assumed to be
a set-forming object-level function
DISCUSSION OF PROPOSED SYNTAX OF SUBSTITUTIONAL DEFINITIONS
Why at All?
The first question one might ask is, why provide for metalinguistic
substitution at all? In a general KR, one would want such a facility
for convenience, conciseness and perspicuity of expression. But why
allow it in an interlingua? One good reason, I think, is to make it
easier to build translators from other KR's to the interlingua.
Much of the work of building a translator then comes down to writing
METADEFs, rather than programming. (A routine for replacing defined
constructs will presumably already exist.)
Of course, to the extent that substitutional definitions extend the
interlingua itself, the defined constructs in principle need not be
replaced at all - except for a couple of problems: OPERATIONS defined
on the interlingua, such as storage, retrieval, or perhaps inference
probably will be defined only for the "basic" syntax, not for extensions
via substitutional definitions; and translation from one external KR
to another via the interlingua will surely require reduction to the
"basic" syntax.
Quotation Meets Substitution
An important technical question that is raised by the availability of
quotation in the object-level syntax is whether substitution of
defining constructs for defined constructs is permissible within the
scope of quotation. Suppose, for instance, that we have indeed
introduced "&" as a synonym for "and" as per example 1. Can we then
rewrite
(bel john '(and (pretty mary) (intelligent mary)))
as
(bel john '(& (pretty mary) (intelligent mary))),
and vice versa? One is inclined to say "yes" unhesitatingly. But now
consider
(contains-a-3-char-atom '(and (pretty mary) (intelligent mary))).
With "contains-a-3-char-atom" interpreted as you might expect, this is
clearly a true statement. But if we now write
(contains-a-3-char-atom '(& (pretty mary) (intelligent mary))),
we seem to have a false statement. After all, "&" IS a lisp atom, and
quoted expressions are interpreted as denoting those expressions, in
the lisp sense. So we seem to be in a quandary.
One way out would be to make a syntactic distinction between basic
and defined atoms. For instance, defined atoms might all start with
"&". The understanding would be that defined constructs (containing
&-atoms) are not only meaning-equivalent, but even list-structure
equivalent to their definitions. They "appear" to have a certain
structural constitution, but their "actual" structural constitution
is as specified in the appropriate definition. An unattractive aspect
of this solution is that list structures under quotes will no longer
be what they seem; and the notation including defined symbols will
be slightly less concise and readable than one might have hoped
(e.g., in the use of ":" as punctuation). Another possibility would
be to limit the use of defined symbols to unquoted contexts. However,
this has the even greater disadvantage of preventing use of convenient
defined symbolisms in statements expressing belief, necessity, etc.
I am strongly inclined toward the first alternative: we just have to
accept that quotation is transparent to substitutional definitions;
(is-a-3-char-atom '&) is true if "&" has been defined as shorthand
for "and". I have not introduced distinctive atoms for defined
symbols because I am not sure what distinctive notation to use, and
because the distinction could in principle be kept implicit. (It is
certainly easily determinable from the METADEFs which symbols are
defined.)
Expressiveness
The proposed syntax involves some rather difficult choices concerning
expressiveness. The following are some of the issues.
1. One might forego the generality of logicians' definitions, and
insist that sigma1 (the "pattern of use" of the defined atom(s))
always be an atom, namely the one being defined. This would allow
only example 1 above, and abbreviations of ground terms and
closed formulas. However, if the basic interlingua were expanded
to allow lambda abstraction, then predicate and function definitions
with much the same effect as the abbreviatory definitions in
examples 7 and 9 could be specified. For example, we might write
(METADEF bachelor (lambda $x (and (male $x) (not (married $x))))),
which would give the same abbreviations as example 7, after
lambda-conversion. In this more restrictive substitutional syntax,
there would be no need for metavariables and metafunctions. On the
other hand, examples like the definition of "there exists exactly
one" (ex. 6) and "isa" (ex. 8) could not be handled (the latter
because it would require abstraction of PREDICATE variables, which
we would probably not want to allow).
2. One might insist that metafunctions be drawn from a fixed,
predetermined set (including #UNUSEDVAR and #SUBST). The hazards
of not imposing any restrictions are obvious (e.g., lack of
assurance of efficiency, correctness and termination; inability
to do "compile-time" syntax checking on definitions). However,
its unclear to me what a minimally adequate set should contain.
3. One might want to provide for type constraints on metavariables
as a means of facilitating syntax checking. The METADEF syntax
might then be
(METADEF sigma1 sigma2 pi1 ... pik)
where each constraint pij is of form (<metapredicate> <metavariable>),
the metapredicates essentially being those appearing in angle
brackets in tables I-III in the KIF document (e.g., #INDVAR,
#RELCONST, #ATOM, #FUNTERM, #SENTENCE,...) and the metavariables
being those which appear in sigma1 and sigma2.
This would make it possible to check whether a given definition
will give a legal interlingua expression upon replacement of
expressions matching the defined form sigma1 (especially if
the metafunction repertoire is tightly constrained, or at least
their output types are specified). It would also allow more
"fine-grained" distinctions in the patterns of use: patterns
would not be considered unifiable if unification would violate
the type constraints of the metavariables.
I find this refinement quite attractive. However, I wouldn't
favor making constraints obligatory, as that would be a nuisance
for most simple definitions.
4. A question arises whether symbols (and the corresponding constructs)
defined in other METADEFs might be allowable in the replacement
pattern, sigma2. This would appear to be harmless if there is no
cyclic reference to defined symbols (e.g., METADEF1 defines S1
but with introduction of defined symbol S2; METADEF2 defines S2
but with introduction of defined symbol S1). Checking for cycles
is not hard. Thus condition (5) could be weakened.
Other issues
- Constructs defined via METADEF are eliminable, as they should be
(cf., David McAllester's comments)
- David's problem concerning recursive definitions certainly remains,
though as far as I can see that is a problem concerning the
expressiveness of the object-level language which arises independently
of the choice of substitutional metalanguage. Isn't this the same
problem as that of proving universally quantified statements of
arithmetic? If the interlingua allowed axiom SCHEMAS, in particular
an induction axiom schema, we could axiomatize "descendant" as
"level-n descendant, for some n", and prove that all descendants
of a human are human. The alternative of using a minimization
operator to obtain fixed points of recursively defined functions
sounds interesting, and worth exploring.
But I think there are independent reasons for wanting a syntax for
axiom schemas, such as that we often want to give axioms for a whole
class of predicates, or a whole class of sentential forms (such as
the logical axioms of axiomatic logics). Now it may well be (though
I haven't given it much thought) that all the axiom schemas we
want are already expressible in KIF. For instance, we might express
"The first argument of all mental-action predicates is human" as
(forall $p (=> (mental-action-pred-const $p)
(true '(=> (,$p $x @y) (human $x)))))
Despite appearances, this isn't second-order logic, since $p is
a variable over syntactic objects (predicate constants), not over
predicate denotations. (However, I think the semantics of "true"
as given in the July KIF document is in need of amendment.)
Similarly, it seems that even induction can be formalized in this
sort of way, roughly along the lines
For all p, if p is a sentence with one free variable x, then
if subst(0,x,p) is true and [for all x, if p then subst(succ(x),
x,p)] is true, then for all (integers) x, p is true.
So that would allow solution of the "descendant" problem, though
probably not as neatly as one would like. By the way, it's worth
noting here that the KIF document uses equality and arithmetic
functions, it does not assign them any special semantics at this
point, leaving them rather as freely interpretable relations or
functions.
- One may wonder whether the quotation mechanism also allows one
to "pull down" metalinguistic definitions into the object language.
(I imagine that was Mike's intention with the original "defines"
notation, which involved quotation.) One might expect this to be
possible in principle, since KIF can describe list structures and
talk about their meaning. The question is whether the informally
understood meaning of METADEFs - that they LICENCE certain classes
of substitutions, with preservation of meaning - can be declaratively
formalized.
Let's give it a try for a few of the earlier examples. I'll use
a predicate "substitutable" over expressions which I'll later try to
express in terms of other notions.
EX.1: (substitutable '& 'and)
(Note: as long as we only substitute for atoms, without regard
for pattern of use, it doesn't really get any harder than that!)
EX.2: (forall $x (=> (sentence $x)
(forall $y (=> (sentence $y)
(substitutable '(,$x ==> ,$y)
'(=> ,$x ,$y) ))))
EX.6: (forall $x (=> (indvar $x)
(forall $y (=> (sentence $y)
(substitutable '(E! ,$x ,$y)
'(exists ,$x (and ,$y (forall ,(unusedvar $y)
(=> ,(subst (unusedvar $y) $x $y)
(= ,(unusedvar $y) ,$x))
))))))))
Similar axioms can be provided for the remaining examples. The axioms
are not easy to write, because of the worry about getting the quotes
and commas right. In the last example, "unusedvar" and "subst" are
ordinary expression-denoting functions over expressions. However,
it is clear that the axioms will be useless for actually "inferring
explicit substitutions" unless there is a means of inferring standard
names for the values of the functions -- e.g., by computing them.
Now what does "substitutable" mean? Part of it (perhaps all of it) is
that substitution of one for the other preserves meaning:
(forall $x
(forall $y (=> (substitutable $x $y)
(forall $z (synonymous (subst1 $x $y $z) $z)) ))),
where subst1 is the result of substituting $x for the first occurrence
of $y in $z. In turn "synonymous" implies equality of denotation:
(forall $x
(forall $y (=> (synonymous $x $y)
(= (denotation $x) (denotation $y)) )))
However, the converse doesn't hold. For instance, denotationally
equal expressions are not in general interchangable in modal contexts,
and in that sense non-synonymous. At least, that is so if "denotation"
is identified with "extension" (semantic value defined extensionally
as for KIF). I leave the problem there. Clearly it is not a simple
matter to represent metalinguistic substitutional definitions in the
object language, and it appears more practical at this point to make
direct use of a metalinguistic syntax.
ANALYTIC DEFINITIONS
I use the qualifier "analytic", since it seems to me that the kinds
of definitions offered in the KIF document using defrelation,
defprimrelation, and so on, are the basis for what have traditionally
been called "analytic truths", such as that every bachelor is unmarried,
or that if x kills y, then y dies.
Part of what is needed to understand the semantics of definitions, I
suggest, is the recognition that they do not only assert a factual
sentence about a domain (e.g., that bachelors are unmarried males),
but also that this sentence IS definitional (i.e., that the SENTENCE
to the effect that bachelors are unmarried males IS a definitional
sentence). I will call the first part the "domain assertion" implicit
in a definition and the second part the "syntactic assertion".
Something else needed to do definitions semantic justice, I believe,
is some appropriate notion of necessity. Analytic truths are NECESSARY
truths, in virtue of the meanings of the words (predicates, etc.) used.
Let's call this notion of necessity "nec-a".
It's clear that this notion of necessity is dependent on the set of
definitions as a whole. One way of giving expression to this intuition
is to say that (nec-a phi) holds just in case it is a logical
consequence of the domain assertions implicit in the definitions;
i.e., if DEFS(delta) picks out the domain content of analytic
definitions in knowledge base delta, then
t ((nec-a phi)) = true iff DEFS(delta) |= phi
iv
(This is not unproblematic, since it makes truth dependent on entailment,
which is itself dependent on truth. But I will make no attempt to work
out details.) Note that even though DEFS(delta) ignores the syntactic
assertional content of definitions, it is well-defined only to the
extent that definitions are effectively recognizable as such -- and
THAT is what the syntactic assertional content is needed for.
There is also an assumption here that the set of definitions in the
knowledge base is complete, in the sense that there are no "missing
definitions" which, if only we knew them (or had gotten around to
stipulating them) would allow us to prove additional analytic truths.
(If the last condition is not met, nec-a will be nonmonotonic. However,
only negative assertions ~(nec-a phi) may have to be revoked, not
positive ones.) Given this completeness assumption, we also know
that the sentences of the knowledge base NOT asserted to be definitions
aren't.
If the currently proposed KIF syntax for analytic definitions
("defrelation", etc.) is adopted, it will be important not to treat
this syntax as part of the ordinary object language. Rather, such
definitions should be viewed as simultaneously asserting a domain
sentence (whose ordinary object-language form has to be "assembled"
>From several pieces), and the fact that this domain sentence IS
definitional (i.e., part of DEFS(delta)).
A more explicit way of doing the same thing, using only the ordinary
object language (but exploiting quotation), would be to say something
like (definition '(...)) or (meaning-postulate '(...)); e.g.,
(definition '(forall $x (<=> (bachelor $x)
(and (male $x) (not (married $x)))))).
The contribution to DEFS(delta) is then given explicitly by the
quoted argument (without the quote). And in addition, the definition
as a whole makes the needed syntactic assertion about the status of
the domain sentence.
If one wanted to be explicit about what the definition is a definition
OF, one could use the even more explicit syntax (at the risk of
confusion with the other options under consideration)
(defrelation 'bachelor '(forall $x (<=> etc. )))
But at least for the purpose of deducing analytic truths, the 'bachelor
argument is not needed.
I favor the explicit syntax (the second-last or last), because it
involves no extension of the basic syntax or semantics. The semantics
of nec-a, along the lines suggested, is a novelty, but I think
something of this sort is unavoidable no matter what syntax is
chosen for definitions. (Well, maybe nec-a could be encoded as
provability from formulas phi for which (defintion 'phi) is known
to hold. Provability in principle requires no new semantic notions.)
The same syntax, or a slightly different syntax can be used for
primitive relations, except for use of one-way implication. The
treatment of functions is similar, except that it involves universally
quantified equalities, rather than equivalences or implications.
Similarly for object definitions.
So, what is provable from definitions? Well, for one thing, since
the domain sentence phi contributed to DEFS(delta) by a definition
is certainly provable from DEFS(delta), it follows that the sentence
(nec-a phi) is provable as well (in view of the semantic definition
of nec-a). Therein, I think, lies the intensional content of
definitions. As well, it will be provable that this sentence
IS a definition, especially if this has been explicitly asserted as
above. Note that it won't be possible to prove that a sentence is
a definition if it wasn't put in as a definition, since there are
(presumably) no axioms which allow the conclusion that something
is a definition from general premises. It will also be possible to
prove such things as that John does NOT believe there is a married
bachelor, if it is known that John believes no analytic falsehoods:
(forall $x (=> (sentence $x)
(=> (nec-a '(not ,$x)) (not (believes john $x)))))
This seems to me like the right sort of inferential behavior.
None of this is very precise or well-worked out (time is short), but
I hope it provides some clarification, or directions in which to seek
clarification. The upshot for me is that virtually any of the
suggestions concerning defrelation, defprimrelation, etc., that
have been made in the definitional debate could be made formal sense
of, although some of the suggestions will keep the interlingua "purer"
and more uniform than others.