SUO: technical questions about definite descriptions in the new KIF

["Robert E. Kent" <rekent@ontologos.org>]

Chris,
 
I have some questions about the appropriate use of the definite description notation in the new KIF. This started out as a quest to eliminate the "helper terms" that I use in the IFF Foundation Ontology, but has ended up as a logical code optimization effort using definite descriptions. Although I am cc-ing this to the SUO list because of their possible interest in helper terms and definite descriptions, I am principally addressing this to you, since you are the author of the definite description capability in the new KIF.
 
In the IFF Foundation Ontology on which I have been working, there is an practical partition of terms into three kinds: core terms, helper terms and convenience terms. These term kinds are defined in terms of two distinctions: required terms versus optional terms and desired terms, representing common terminology, versus artificial terms.

• Core terms are both necessary (required) and represent common terminology (desired). As examples, in the core (SET) namespace of the IFF Foundation Ontology [http://suo.ieee.org/IFF-Foundation-Ontology.pdf], all the terms listed in Diagram 2 (Core Conglomerates and Functions) are core terms. These include, 'class', 'function', 'source', 'target', etc. 
• Convenience terms are desired (in common use), but unnecessary. Although unnecessary, they are useful, since they help reduce expression size in applications. One example of a convenience term is 'projection1' in the pullback namespace (SET.LIM.PBK). This is very convenient in applications, but could be ignored, since it is definable in terms of the pullback namespace core terms 'first' and 'limiting-cone'. Here I will not discuss convenience terms, since they can logically be ignored.
• Helper terms seem to be required in the IFF Foundation Ontology, in order to define either core terms or convenience terms. However, they are not common terminology, and are questionable as far as being absolutely necessary. As an example, in the large graph namespace (GPH) of the IFF Foundation Ontology the term 'multiplication-opspan' is a helper term. Its raisson d'etre is to help define the term 'multiplication', which represents the horizontal composition of two large (directed) graphs having the same class of objects (nodes).

To recap, I have used helper terms in the IFF Foundation Ontology, but they are not common terminology, and, if possible, I would like to remove them and replace them with something else. The first thought was to use a special notation such as type construction in programming languages. However, what I came up with looked a lot like definite descriptions. In hindsight this is not surprising, since definite descriptions implicitly define a function of the free variables involved, and in the IFF Foundation Ontology I am usually defining parametric functions, as the example below illustrates. Unfortunately, when I tried to use definite descriptions in an optimal fashion, I still needed to give them a name, which essentially was the helper term. The positive result is that it optimized the logical code. My question to you is whether the resulting code is accurate.

 

As a concrete example, here are the original definitions of the helper term 'multiplication-opspan' and the core term 'multiplication' in the large graph namespace in the IFF Foundation Ontology. The 'CNG$function' term has already been axiomatized to return a unique value for any input. The term 'graph' represents a large directed graph consisting of a class of objects (nodes), a class of morphisms (edges), and source and target functions mapping morphisms to objects. The term 'opspan' represents the appropriate diagram for a pullback; namely, two functions 'opfirst' and 'opsecond' with a common target class 'opvertex'. The "multiplication-opspan" function maps a pair of graphs with common object (node) class to the opspan consisting of the target function of the first graph and the source function of the second graph. The "multiplication" function maps a pair of graphs with common object (node) class to their horizontal composition -- a third graph whose morphisms are "composable" pairs of morphisms from the input pair of graphs. Axiom (1) declares the helper term 'multiplication-opspan' to be a function. Axiom (2) gives its signature. Axiom (3.a) defines its domain of definition. And axiom (3.b) gives its definition, since opspans are uniquely determined by their triple (opvertex, opfirst, opsecond). The same comments hold for the axioms that represent the core term 'multiplication'.
 
(1)   (CNG$function multiplication-opspan)
(2)   (CNG$signature multiplication-opspan graph graph SET.LIM.PBK$opspan)
(3.a) (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
          (<=> (exists (?s (SET.LIM.PBK$opspan ?s))
                   (= (multiplication-opspan ?g0 ?g1) ?s))
               (= (object ?g0) (object ?g1))))
(3.b) (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
          (=> (= (object ?g0) (object ?g1))
              (and (= (SET.LIM.PBK$opvertex (multiplication-opspan ?g0 ?g1))
                      (object ?g0))
                   (= (SET.LIM.PBK$opfirst (multiplication-opspan ?g0 ?g1))
                      (target ?g0))
                   (= (SET.LIM.PBK$opsecond (multiplication-opspan ?g0 ?g1))
                      (source ?g1)))))
 
(4)   (CNG$function multiplication)
(5)   (CNG$signature multiplication graph graph graph)
(6.a) (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
          (<=> (exists (?g (graph ?g))

                   (= (multiplication ?g0 ?g1) ?g))
               (= (object ?g0) (object ?g1))))
(6.b) (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
          (=> (= (object ?g0) (object ?g1))
              (and (= (object (multiplication ?g0 ?g1))
                      (object ?g0))
                   (= (morphism (multiplication ?g0 ?g1))
                      (SET.LIM.PBK$pullback (multiplication-opspan ?g0 ?g1)))
                   (= (source (multiplication ?g0 ?g1))
                      (SET$composition
                          (SET.LIM.PBK$projection1 (multiplication-opspan ?g0 ?g1))
                          (source ?g0)))
                   (= (target (multiplication ?g0 ?g1))
                      (SET$composition
                          (SET.LIM.PBK$projection2 (multiplication-opspan ?g0 ?g1))
                          (target ?g1))))))

 

And here are the new definitions of the helper term 'multiplication-opspan' and the core term 'multiplication' that use definite descriptions. As you can see, I have not gotten rid of the helper term 'multiplication-opspan', but I have optimized the code somewhat. In both term definitions (axiomatizations), the domain of definition axiom has moved to become the antecedent of the definite description.

 

(1)  (CNG$function multiplication-opspan)
(2)  (CNG$signature multiplication-opspan graph graph SET.LIM.PBK$opspan)
(3') (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
         (= (multiplication-opspan ?g0 ?g1)
            (the (?s (SET.LIM.PBK$opspan ?s))
                 (=> (= (object ?g0) (object ?g1))
                     (and (= (SET.LIM.PBK$opvertex ?s) (object ?g0))
                          (= (SET.LIM.PBK$opfirst ?s)  (target ?g0))
                          (= (SET.LIM.PBK$opsecond ?s) (source ?g1)))))))

 

(4)  (CNG$function multiplication)
(5)  (CNG$signature multiplication graph graph graph)
(6') (forall (?g0 (graph ?g0) ?g1 (graph ?g1))
         (= (multiplication ?g0 ?g1)
            (the (?g (graph ?g))
                 (=> (= (object ?g0) (object ?g1))
                     (and (= (object ?g)
                             (object ?g0))
                          (= (morphism ?g)
                             (SET.LIM.PBK$pullback (multiplication-opspan ?g0 ?g1)))
                          (= (source ?g)
                             (SET$composition
                                 (SET.LIM.PBK$projection1 (multiplication-opspan ?g0 ?g1))
                                 (source ?g0)))
                          (= (target ?g)
                             (SET$composition
                                 (SET.LIM.PBK$projection2 (multiplication-opspan ?g0 ?g1))
                                 (target ?g1))))))))

Is this a correct use of the definite description notation, and is the new code is equivalent to the original code? In particular, what happens off the domain of definition? And also, can you see any optimal way of removing the helper term  'multiplication-opspan' -- optimal in the sense of getting equivalent, but more streamlined, code?
 
Robert E. Kent
rekent@ontologos.org