12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:36, 24 March 2009
, 12:36, 24 March 2009→Step 5: markup
===Step 5===
===Step 5===
'''Existential Graph Format : Application Triples with Structure Sharing'''
Redo the same development in Existential Graph notation. In the work below, the term development is carried out in reverse, that is, in application order.
reverse, that is, in application order.
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| |
| |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
'''NB.''' Looking at my notes from Fall Term 1996, I'm still not sure what order I intended for the application triples, but the above is one likely guess:
For example:
For example:
The nodes that are right-labeled <K, KS, K(KS)>,
* The nodes that are right-labeled <math>(\operatorname{K}, \operatorname{K}\operatorname{S}, \operatorname{K}(\operatorname{K}\operatorname{S})),</math> in that order, constitute an application triple.
in that order, constitute an application triple.
The type of the applicand K is A=>(B=>A).
* The type of the applicand <math>\operatorname{K}</math> is <math>A \Rightarrow (B \Rightarrow A).</math>
The type of the applicator KS is (A=>(B=>A))=>(A=>A).
* The type of the applicator <math>\operatorname{K}\operatorname{S}</math> is <math>(A \Rightarrow (B \Rightarrow A)) \Rightarrow (A \Rightarrow A).</math>
Therefore, the type of the application K(KS) is A=>A.
* Therefore, the type of the application <math>\operatorname{K}(\operatorname{K}\operatorname{S})</math> is <math>A \Rightarrow A.</math>
</pre>
==Composition, or the Composer==
==Composition, or the Composer==