SUO: IFF interface (control portal)
All,
Now that the core of the IFF Model Theory Ontology (IFF-MT) is in place, I
thought it might be valuable to give some thought to the IFF interface. The
IFF-MT allows us to link object level ontologies with the upper-level
structure, especially the truth concept lattices in the IFF Upper
Classification Ontology (IFF-UCLS) that represent the "concept lattices of
theories." The IFF interface is handled through "portals."
The core of a specific portal, the CG portal for conceptual graphs
<http://suo.ieee.org/IFF/versions/20020515/IFFModelTheoryOntology/Conceptual
GraphsPortal.pdf>,
and the core of a generic portal for traditional many-sorted logic
<http://suo.ieee.org/IFF/versions/20020515/IFFModelTheoryOntology/TraditionP
ortal.pdf>,
have already been defined. And it is assumed the portals for Cyc, DAML-OIL,
etc. can also be specified (although metalevel capabilities will need
special treatment).
But these portals are input portals and do not allow control over any
internal operations. However, a control portal can now readily be created
since most of the internal plumbing is now in place. This is already
evidenced by part of the generic portal -- see the terms "expression",
"sentence", and "satisfaction" which are not part of the input terminology,
but instead reference internal notions. Object level ontologies and
knowledge bases can be internalized in IFF via various input portals. Then
the control portal could be used to manipulate these internal
representations.
Here is a list of standard terminology (with some parametric terms) that
might be useful in this control portal and that can now be linked to the
internal IFF axiomatization. ('^=' means "named", '~=' means "synonymous
with", "==" means logically equivalent)
1. language ^= L
A first order IFF type language named L containing sorts (entity types),
predicate symbols (relation types), and variables.
2. truth-classification(L)
The truth classification associated with the type language L. Its instances
are the models with type language L. Its types are the expressions (or
sentences) of L.
3. truth-concept-lattice(L) ~= lattice-of-theories(L)
The truth concept lattice associated with type language L. This is the
concept lattice of the truth classification of L.
truth-concept-lattice(L) == concept-lattice(truth-classification(L))
The formal intents of its formal truth concepts are the closed theories of
L. The formal extents of its formal truth concepts are all the models of a
theory.
4. interpretation ^= I; source(I) ^= L1; target(I) ^= L2
A first order interpretation named I (see page 74 in Barwise and Seligman
"Information Flow") maps relation types of one language (its source named
L1) to expressions in another language (its target named L2) preserving
arity and signatures. The CG portal represents the relation labels defined
with lambda expressions as interpretations.
5. truth-infomorphism(I) ^= J; source(J) ^= C1; target(J) ^= C2
The truth infomorphism (Barwise op. cit.) associated with the interpretation
I and named J. Its source classification named C1 is the truth
classification of the source of I, and
its target classification named C2 is the truth classification of the target
of I. The (contravariant) instance function maps models of L2 to models of
L1 -- see the model operator axiomatization in the type language namespace
document
http://suo.ieee.org/IFF/versions/20020515/IFFModelTheoryOntology/TypeLanguag
eNamespace.pdf.
The (covariant) type function maps expressions (and sentences) of L1 to
expressions (and sentences) of L2 -- see the extension operator for
interpretations in the type language namespace document.
6. truth-concept-morphism(I) ^= K; source(K) ^= W1; target(K) ^= W2
The truth concept lattice morphism associated with interpretation I. This is
the concept morphism of the truth infomorphism of I.
truth-concept-morphism(L) == concept-morphism(truth-infomorphism(L))
The instance and type functions of its underlying truth infomorphism are
extended to two adjoint monotonic functions that map the formal truth
concepts (theories) of one lattice of theories to the formal concepts
(theories) of the other lattice of theories, with the left adjoint
preserving joins (intersections) of formal truth concepts (theories) and the
right adjoint preserving meets (union followed by closure) of formal truth
concepts (theories).
Other terms of interest:
theory(L) ^= T
truth-concept-lattice(T)
join(T1, T2); meet(T1, T2)
closure(T)
model ~= structure ^= M
type-language(M) ^= L
theory(M) ^= T
expression(L) ^= E
sentence(L) ^= S
Terms for specifying diagrams of concept-lattices-of-theoreis and their
concept-morphisms, along with colimit operations for internalizing into a
single colimit lattice-of-theories.
Terms for expressing internal representations in some external format
(output portals).
What other objects and operations do you think are needed in this control
portal?
Robert E. Kent
rekent@ontologos.org