In the recent discussions, I was responding to comments about the
"type free" Common Logic, but I didn't bring up a very important
point: Conceptual Graphs have had a very rich type system from
Day 1 -- actually from the first published paper about CGs in 1976: (01)
http://www.jfsowa.com/pubs/cg1976.pdf
Conceptual Graphs for a Database Interface (02)
In that paper, I called CGs a version of sorted logic. But for the
book version in 1984, I used the term 'type' rather than 'sort'.
Following is a brief summary of the CG type system, which evolved
from the original sorted logic in the 1976 paper: (03)
1. A partial ordering of types by generalization and specialization.
Type T1 is a generalization of T2 (and T2 is a specialization of
T1) iff for every model, every instance of T2 is an instance of T1. (04)
2. The universal type, which is true of everything in every model,
is a generalization of every type. The absurd type, which is
true of nothing, is a specialization of every type. (05)
3. Canonical graphs, which specify type constraints for well formed
CGs, are a generalization of the signatures used for specifying
the type constraints in logics and programming languages. A
single relation with type constraints on its arguments, which
is called a star graph, is the simplest kind of canonical graph. (06)
4. Canonical formation rules are a graph grammar for generating
all well formed CGs that preserve the type constraints, but they
don't necessarily preserve truth. (For example, the negation
of any statement would obey the same type constraints.) (07)
5. Inference rules for CGs specify additional constraints
that preserve truth. (08)
6. The CG theory does not use the word 'polymorphism', but it
supports a very general kind of polymorphism that is necessary
for natural language semantics. The polymorphism used in
programming languages is a subset of the CG polymorphism. (09)
For more detail about these topics, see the following paper: (010)
http://www.jfsowa.com/cg/cg_hbook.pdf (011)
To support this type system in Common Logic, I adopted the
following approach: (012)
1. Define an untyped notation, called Core CGIF (Conceptual
Graph Interchange Format), which maps directly to the
Common Logic model theory. In effect, the absence of
a type label designates the universal type, which imposes
no restriction whatever on the domain of quantification. (013)
2. Then define Extended CGIF by a translation to Core CGIF.
Extended CGIF uses the Common Logic mechanism of restricted
quantification. But it does not enforce the constraints
of canonical graphs and the canonical formation rules. (014)
3. The type labels in Extended CGIF, as in the CLIF dialect
of Common Logic, can use any monadic relation to restrict
the domain of quantification. There is no assumption of
a type hierarchy or any constraints on type signatures. (015)
4. Points #1, #2, and #3 are specified in the ISO 24707 standard.
But the system of canonical graphs and formation rules add
the constraints for a type hierarchy and the graph grammar.
Those rules can support the derivation of CGs that preserve
the type constraints and the static testing of CGs to verify
whether the type constraints are satisfied. (016)
5. The CG theory assumes a partial ordering of types, but it
does not require any specific rules or method for determining
that partial ordering. If desired, the techniques used for
Description Logics or the techniques of intuitionistic logic
could be used to specify the type hierarchy. (017)
This is the method that I used to add a type system to Common Logic,
but there is no dependency on a graph grammar. A similar method
could be adapted to any type system that anybody might prefer
to add to Common Logic. (018)
Rick cited the Girard-Reynolds Isomorphism as a desirable feature
for a type hierarchy. The proof of that isomorphism used something
they called "second order logic". However, the only features they
required to prove the theorem were the ability to quantify over
types and relations. They did not require the hierarchy of
infinities that are usually assumed in "true" second order logic.
Common Logic is more than adequate to prove that theorem. (019)
Fundamental principle: The model theoretic semantics for a logic
must be compatible with the logic used to derive a type hierarchy
for a typed version of that logic. Since intuitionistic logic is
a subset of FOL (in the sense that every theorem of intuitionistic
logic is also a theorem of FOL), the use of intuitionistic logic
for specifying the type hierarchy is compatible with Common Logic. (020)
Therefore, the method I outlined for building the CG type system
on top of Common Logic can be adapted to the kinds of typed logics
that Rick was asking for. In particular, intuitionistic logic,
the Girard-Reynolds Isomorphism, the Description Logic constraints,
or many other kinds of constraints can be used for a type system
that is compatible with the semantics of Common Logic. (021)
John (022)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (023)
|