Leo,
Thanks, I will check it out. What is theoretically relevant about the Algos
approach is the engineering of the topos axioms so that one gets "set
building" subtype construction, without paradoxes. That is somewhat more
than application, composition, and abstraction. What I am doing is close to
type theory and its various implementations. The practical difference is
that type theory only uses one type and category theory uses two types, both
a domain and a range type which makes a lot of applications much easier to
formalize. (01)
By the way the axioms and a FOL implementation go back a long way, e.g.,
Graves, H., Blaine, L., The Algos Computational System, Proceeding of the
European Conference on Computer Algebra, Springer, 1985. The implementation
was done in what was or became Common Lisp. Application to engineering and
biological sciences is only in the last 4 years. (02)
Henson (03)
-----Original Message-----
From: Obrst, Leo J.
Sent: Wednesday, October 09, 2013 8:02 PM
To: [ontolog-forum] ; John F Sowa
Cc: cl@xxxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] Giving SysML a formal semantics (04)
Henson, (05)
This looks very like Moortgat's generalized categorial grammar formalism
[1], itself based on Lambek's original calculus (and going back to
Ajdukiewicz), which Moortgat more recently [2] described as categorial type
logics, for linguistic analysis and interpretation. These use function
application, composition, and abstraction. (06)
Thanks,
Leo (07)
[1] Moortgat, Michael. 1988. Categorial Investigations: Logical and
Linguistic Aspects of the Lambek Calculus. Foris Publications, Dordrecht,
Holland.
[2] Moortgat, Michael . 1997. Categorial Type Logics. In: van Benthem, J.,
and A. terMeulen (eds.) 1997. Handbook of Logic and Language. Elsevier. (08)
>-----Original Message-----
>From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
>bounces@xxxxxxxxxxxxxxxx] On Behalf Of henson
>Sent: Wednesday, October 09, 2013 9:17 AM
>To: John F Sowa
>Cc: '[ontolog-forum] '; cl@xxxxxxxxxxxxxxxxx
>Subject: Re: [ontolog-forum] Giving SysML a formal semantics
>
>John,
>
>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.
>
>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.
>
>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.
>
>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.
>
>Henson
>
>-----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
>
>Henson,
>
>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.
>
>> 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.
>
>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.
>
>> 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.
>
>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.
>
>> 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.
>
>Fundamental question: What do you mean by "extending/changing the
>semantics slightly"? The model theory? Or the rules of inference?
>
>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.
>
>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.
>
>> 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 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?
>
>John
>_________________________________________________________________
>_____
>
>Excerpt from http://www.jfsowa.com/pubs/semnet.htm
>
>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:
>
>"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?"
>
>The answer follows from theorems that are easy to prove when stated in
>existential graphs (Sowa 2011, Section 6):
>
> 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).
>
> 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.
>
>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.
>
>References:
>
>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.
>
>Sowa, John F. (2011) Peirce’s tutorial on existential graphs, Semiotica
>186:1-4, 345-394. http://www.jfsowa.com/pubs/egtut.pdf
>
>Wos, Larry (1988) Automated Reasoning: 33 Basic Research Problems,
>Englewood Cliffs, NJ: Prentice Hall.
>
>-------- Original Message --------
>Subject: Re: Giving SysML a formal semantics
>Date: Mon, 7 Oct 2013 08:14:57 -0500
>From: Henson Graves
>
>John,
>
>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.
>
>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.
>
>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.
>
>Henson
>
>
>_________________________________________________________________
>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
> (09)
_________________________________________________________________
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 (010)
_________________________________________________________________
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 (011)
|