**Mail folder:**Interlingua Mail**Next message:**Richard Fikes: "Comments from Vladimir Lifschitz on the Nonmonotonic Proposal"**Previous message:**Ramesh Patil: "[Ramesh Patil <RAMESH@VAXA.ISI.EDU>: Re: Recursive Defs]"

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.