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: ontologforumbounces@xxxxxxxxxxxxxxxx [mailto:ontologforum
>bounces@xxxxxxxxxxxxxxxx] On Behalf Of henson
>Sent: Wednesday, October 09, 2013 9:17 AM
>To: John F Sowa
>Cc: '[ontologforum] '; cl@xxxxxxxxxxxxxxxxx
>Subject: Re: [ontologforum] 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: '[ontologforum] ' ; 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 naturaldeduction
>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. 172188.
>
>Sowa, John F. (2011) Peirce’s tutorial on existential graphs, Semiotica
>186:14, 345394. 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/ontologforum/
>Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
>Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
>Shared Files: http://ontolog.cim3.net/file/
>Community Wiki: http://ontolog.cim3.net/wiki/
>To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
>
(05)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J (06)
