ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Giving SysML a formal semantics

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>, John F Sowa <sowa@xxxxxxxxxxx>
Cc: "cl@xxxxxxxxxxxxxxxxx" <cl@xxxxxxxxxxxxxxxxx>
From: "Obrst, Leo J." <lobrst@xxxxxxxxx>
Date: Thu, 10 Oct 2013 01:02:09 +0000
Message-id: <FDFBC56B2482EE48850DB651ADF7FEB02E70D7FB@xxxxxxxxxxxxxxxxxx>
Henson,
    (01)

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.
    (02)

Thanks,
Leo
    (03)

[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.
    (04)

>-----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

>
    (05)

_________________________________________________________________
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    (06)

<Prev in Thread] Current Thread [Next in Thread>