Henson, (01)
Fabian Neuhaus raised the general issue of representing partial
functions in Common Logic. Special-purpose solutions, such as NaN
in IEEE arithmetic, can be useful. But it would be better to have
a more general solution. (02)
> The topos axioms simply provide a built in ontology that has been
> well validated... (03)
Yes. A thoroughly analyzed subject such as topos theory would be
a good test case for developing a systematic way of handling
partial functions in CL. It could become a recommended method for
handling a wide range of applications. (04)
> 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)
Since all functions in CL are total, some such solution could be
adapted to CL. Another possibility is to represent "maps" by dyadic
relations in CL. Quantified variables could refer to maps as a special
type of relation. (06)
Since Common Logic is intended to support an open-ended variety of
dialects with any kind of syntax, you could use any syntax for maps
that anyone might prefer. But when such a dialect is translated
to CLIF, maps would look like relations. (07)
Would something like that work? (08)
John (09)
-------- Original Message --------
Subject: Re: Giving SysML a formal semantics
Date: Sun, 6 Oct 2013 14:44:22 -0500
From: Henson (010)
John, (011)
I am glad that you agree with the basic premise. (012)
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. (013)
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. (014)
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. (015)
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 "marriage" 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. (016)
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. (017)
Henson (018)
_________________________________________________________________
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 (019)
|