John, (01)
I am suggesting a change in model theory, not inference rules. I agree with
you that inference rules must be sound wrt the model theory. In this case
the inference rules are sound wrt the model theory. (02)
A simple example of a partial function that occurs in everyday mathematics
and in engineering modeling languages is composition of operations and path
composition in directed graphs. I will start with path composition. This can
be represented in a first order language with two sorts, Arrow and Node. Use
lower case f,g,h for arrows and X,Y,Z for nodes. The representation that an
arrow has a source and target node can be done by using equality and two
first order function symbols, Source and Target. Each has an argument whose
sort is Arrow, and whose value sort is Node. A three argument predicate
TypeOF(f,X,Y} is used as an abbreviation of Source(f) = X and Target(f) = Y.
This will be written as f:X -> Y. With this composition is represented as a
first order function symbol Comp which has two map arguments. The axioms for
composition are
f:X -> Y, g:Y -> Z => Comp(f,g):X -> Z. The consequent is read as Comp(f,g)
is defined and satisfies the TypeOf predicate. This is pure first order
syntax. Reasoning is pure first order with a definedness predicate. When
arrow symbols are introduced into a signature they are specified with a
source and target type which makes them defined. A valid interpretation of
a composition term only requires that it is defined in a structure when the
term is defined in the theory. (03)
This approach can be used to axiomatize directed graphs with path
composition, further axioms can be given to make it into a deduction system
in the sense of Lambek and Scott. Further axioms to yield a category, and
when the arrow and node constructors are added then a topos which is simply
a more computationally tractable set theory. While a mathematician would
likely use the syntax f:X -> Y, the standard computer science notation would
be f(X):Y. (04)
One advantage of this approach to embedding mathematics into logic is that
the mathematics concept of a functor and a valid interpretation coalesce
which is not the case when operations are represented as relations rather
than partial functions. (05)
Henson (06)
-----Original Message-----
From: John F Sowa
Sent: Tuesday, October 08, 2013 11:09 AM
To: henson
Cc: '[ontolog-forum] ' ; cl@xxxxxxxxxxxxxxxxx
Subject: Re: Giving SysML a formal semantics (07)
Henson, (08)
I think we're converging. I appended a copy of your note below,
because it didn't get through the CL and Ontolog email handlers. (09)
> The suggestion of translating the partial functions into relations
> is actually the way that axiomatization of a topos as a first order
> theory was originally done. It works, but is messy but makes the
> logic embedding very remote from the mathematics. (010)
I agree. I give a similar explanation for using CGIF instead of CLIF
to represent and operate with graphs. They both have the same model
theory. But graph operations that are easy to state in CGIF are often
more complex in CLIF. (011)
> While the functions, such a composition and ordered pairs, are partial,
> they have simple definedness conditions which can easily be checked by
> a tool. One can just do the checks with an ordinary inference engine
> and carry on with the inference. (012)
An inference engine can unify two functional structures very simply.
But it would be harder to state the equivalent conditions on relational
structures and to implement them efficiently. (013)
> By extending/changing the semantics slightly one makes a much better
> convergence between logic and the mathematics done in the category
> theory way, than is done the way you suggested. (014)
Fundamental question: What do you mean by "extending/changing the
semantics slightly"? The model theory? Or the rules of inference? (015)
Many people (including me) consider rules of inference as implications
of the model theory. The choice of rules is a convenience (for human
factors or computational efficiency), not a change in semantics. (016)
For the CGIF <=> CLIF mapping, there is no change to the model theory,
but certain rules of inference, which are trivial to state in CGIF
cannot be stated in CLIF without a major increase in complexity.
See the excerpt below for the question by Larry Wos and the answer
in terms of Peirce's rules of inference. (017)
> If someone wanted to consider how to extend CL to accommodate this
> I would be very pleased for this to be a use case. (018)
I would recommend that as an important use case. Could you state
the definedness conditions and their implications -- preferably in CL
terms, rather than topos theory? (019)
John
______________________________________________________________________ (020)
Excerpt from http://www.jfsowa.com/pubs/semnet.htm (021)
Even today, Peirce’s rules provide insights that have eluded logicians
for many years. As an example, Larry Wos (1988) listed 33 unsolved
research problems in automated reasoning. Problem 24 asks about the
relationship between proofs using Gentzen’s rules for clauses and his
rules of natural deduction: (022)
"Is there a mapping between clause representation and natural-deduction
representation (and corresponding inference rules and strategies) that
causes reasoning programs based respectively on the two approaches or
paradigms to attack a given assignment in an essentially identical
fashion?" (023)
The answer follows from theorems that are easy to prove when stated in
existential graphs (Sowa 2011, Section 6): (024)
1. Any proof by Gentzen’s system of natural deduction can be converted
automatically to a proof by Peirce’s rules. The converse is not true,
because certain proofs by Peirce’s rules can be significantly faster
than proofs by Gentzen’s rules (Dau 2006). (025)
2. Any proof derived by a resolution theorem prover in clause form can
be converted to a proof using Peirce’s rules by negating each step,
reversing the order, and writing each step as an existential graph. (026)
To answer Wos, proofs in either of Gentzen’s systems can be translated,
step by step, to an equivalent EG proof. Some, but not all, can be
translated from EGs to a proof in the other system by Gentzen. Peirce’s
framework is a generalization that subsumes both. (027)
References: (028)
Dau, Frithjof (2006). Some notes on proofs with Alpha graphs. In
Conceptual Structures: Inspiration and Application, (LNAI 4068), H.
Schärfe, P. Hitzler, and P. Øhrstrom (eds.), Berlin: Springer. pp. 172-188. (029)
Sowa, John F. (2011) Peirce’s tutorial on existential graphs, Semiotica
186:1-4, 345-394. http://www.jfsowa.com/pubs/egtut.pdf (030)
Wos, Larry (1988) Automated Reasoning: 33 Basic Research Problems,
Englewood Cliffs, NJ: Prentice Hall. (031)
-------- Original Message --------
Subject: Re: Giving SysML a formal semantics
Date: Mon, 7 Oct 2013 08:14:57 -0500
From: Henson Graves (032)
John, (033)
The suggestion of translating the partial functions into relations is
actually the way that axiomatization of a topos as a first order theory was
originally done. It works, but is messy but makes the logic embedding very
remote from the mathematics. Proofs in the logic would not resemble what an
informal argument would look like and it would be very hard to translate
the
other way. (034)
While the functions, such a composition and ordered pairs, are partial,
they
have simple definedness conditions which can easily be checked by a tool.
one can just do the checks with an ordinary inference engine and carry on
with the inference. This situation is not like general partial recursively
enumerable functions. By extending/changing the semantics slightly one
makes
a much better convergence between logic and the mathematics done in the
category theory way, than is done the way you suggested. Don't
misunderstand, your suggestion was what was originally done which had
enormous positive consequences. But I believe the partial function approach
has many practical advantages, is sound from the logic viewpoint, and makes
even more sense when you look at embedding engineering models in logic.
There is of course much more to say technically to advocate this. (035)
If someone wanted to consider how to extend CL to accommodate this I would
be very pleased for this to be a use case. I suspect almost nothing would
have to be changed in an inference engine, only the user's manual would
have
to be changed a bit. (036)
Henson (037)
_________________________________________________________________
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 (038)
|