John,
I am glad that you agree with the basic premise. (01)
With regard to fUML, the referenced paper didn't really deal with the
dynamic case. I should have referenced fUML. Actually I didn't find out
about it until after the paper was written. (02)
As I mentioned there is no problem in embedding what were in the paper
called ABD axioms (which is what I call Algos) in a first order language
with two sorts. However, the first order function symbols used for the map
and type constructors are only partially defined. For example composition of
maps is defined only when the domain and range types match appropriately.
These partial functions have predicates for their definedness conditions
which makes them perfectly tractable. It does change the model theory from
standard fol model theory. This turns out to be a plus. In fact the Algos
axioms yield a topos and the valid interpretations are functors in the
sense of category theory. In fact the valid interpretations of an Algos
theory are strict logical functors in the sense of Lambek and Scott. This
kind of thing is well studied. There are good arguments in my opinion for a
topos semantics rather than set theory for practical applications. (03)
What might not be obvious from just the email is that I embed engineering
models, e.g., for a vehicle, or a hydrocarbon molecule, as axiom sets within
the Algos language which contains the constructors for product, sum,
exponent (function), and power types. The combined axiom sets perhaps with
axioms sets for parts, andfor time, if this additional knowledge is
appropriate. The result then generates a topos when provably equal maps are
identified. Of course the topos is degenerate if the theory is inconsistent. (04)
Topos theory, as I am sure you know, is an algebraic generalization of set
theory, and is much more tractable than set theory if you need that kind of
expressiveness. Most any application in science or engineering needs some of
these constructors. Trying do do "marrage" and family relationships even
with HOL, but without type constructors is tedious to say the least. The
topos axioms simply provide a built in ontology that has been well
validated, particularly if you include set theory as a predecessor. I am
certainly up to attempting to convince anybody of this. I agree with you
that you could translate the Algos axioms into CL. A relatively garden
variety inference engine for a FOL system will work. You just work with the
operations as if they were total. In fact I implemented an Algos system many
years ago. (05)
I certainly do not wish to compete with the fUML folks and would like to
cooperate with them. I know some of them and think highly of them and their
work. However, I do think that the kind of type system that Algos provides
is needed to formalize SysML and is needed to formalize any science and
engineering of any complexity. It can make formalization a lot easier, and
it builds on a lot of hard won knowledge. I have been unsure if the time
was right to approach the OMG folks. (06)
Henson (07)
-----Original Message-----
From: John F Sowa
Sent: Sunday, October 06, 2013 11:41 AM
To: henson
Cc: '[ontolog-forum] '
Subject: Re: Giving SysML a formal semantics (08)
Henson, (09)
I completely agree with your summary (copy below), and I have always
believed that sorted logics have some important advantages. That's
the major reason why I have strongly encouraged the use of restricted
quantifiers in Common Logic to represent sorts in other logics. (010)
But there are two important issues: (011)
1. Your article [1] discussed the many reasons why any specification
language must itself have a formal specification. But it didn't
mention the fUML work [2] on specifying UML & SysML. (012)
2. I didn't attempt a complete translation of that article to
Common Logic, but I didn't see any ABD statement that could not
be translated to an equivalent CL statement. Why not adopt CL
model theory as the semantic foundation? (013)
> There is one difference from standard FOL practice. The first order
> operations are partial, but have definedness conditions expressed
> in the logic. (014)
Partial functions have been discussed on the CL list. One way of
handling them is to use the IEEE convention of assigning special
values such as NotANumber (NaN). You can also use quantifier
restrictions to ensure that variables stay within the domain. (015)
> This topos ontology approach enables a lot of statements that are
> higher order in some formalisms to be first order. (016)
That's good. CL has a first-order model theory and proof theory.
But it also supports quantifiers over functions and relations.
You could specify the topos ontology in CL and show how to
translate every ABD statement to an equivalent CL statement. (017)
That approach would enable you to build on and improve the current
fUML work instead of replacing it with something totally different.
It would also enable you to form an alliance with the fUML developers
instead of competing with them. (018)
John (019)
References: (020)
1.
http://www.omgwiki.org/MBSE/lib/exe/fetch.php?media=mbse:10.1007_s10472-011-9267-5.pdf (021)
2. Executable UML/SysML Semantics Project Report (Final), November 2008
To get report, type "xuml sysml fuml" to Google (without quotes). (022)
-------- Original Message --------
Subject: Re: Giving SysML a formal semantics
Date: Sun, 6 Oct 2013 09:19:46 -0500
From: Henson Graves (023)
John, (024)
ABD logic is actually an axiomatization of the map and type (object)
constructions of topos theory in a first order two sorted language. The
sorts are map and type. (025)
There is one difference from standard FOL practice. The first order
operations are partial, but have definedness conditions expressed
in the logic. There are of course FOL systems that admit this. For
example, composition of maps is a first order function symbol, but is
defined only when the appropriate domains and ranges match for the maps
being composed. (026)
What one is doing is not denying FOL its proper place in the sun,
but simply using FOL with definedness conditions for operations and
predicates, and with a specific ontology, based on topos theory, which
has been proven to be sufficient to do a lot of mathematics and science
in. This topos ontology approach enables a lot of statements that are
higher order in some formalisms to be first order. (027)
Henson (028)
_________________________________________________________________
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 (029)
|