Difference between revisions of "Directory:Jon Awbrey/Papers/Propositions As Types"

MyWikiBiz, Author Your Legacy — Monday April 29, 2024
Jump to navigationJump to search
(import raw text)
 
 
(107 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
{{DISPLAYTITLE:Propositions As Types}}
 
{{DISPLAYTITLE:Propositions As Types}}
−
<pre>
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
  
−
IDS -- PAT
+
'''NB.''' In this discussion, combinators are being applied on the right of their arguments.  The resulting formulas will look backwards to people who are accustomed to applying combinators on the left.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
==Identity, or the Identifier==
  
−
PAT.  Propositions As Types
+
===Step 1===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
Consider the following problem requirements:
  
−
PAT.  Note 1
+
One is given a syntactic specification of the following form:
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x & = & x\operatorname{I}\end{matrix}</math>
 +
|}
  
−
Identity, or the Identifier
+
In effect, this specification amounts to a so-called ''paraphrastic definition'' of the operator <math>\operatorname{I},</math> one in which the syntactic frame <math>^{\backprime\backprime} x = x \underline{~~~} \, ^{\prime\prime}</math> may be regarded as the defining context, or ''definiens'', and <math>\operatorname{I}</math> is regarded as the object to be defined, or ''definiendum''.
  
−
Step 1.
+
One is asked to find a ''pure interpretant'' for <math>\operatorname{I},</math> that is, an equivalent term in <math>\langle \operatorname{K}, \operatorname{S} \rangle,</math> the ''combinatory algebra'' generated by <math>\operatorname{K}</math> and <math>\operatorname{S},</math> that does as <math>\operatorname{I}</math> does.
  
−
Given a syntactic specification (or paraphrastic definition):
+
A handle on the problem can be gotten by observing the following relationships:
  
−
  x = xI
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{ccccc}
 +
x
 +
& = &
 +
(x\operatorname{K})(x\operatorname{K})
 +
& = &
 +
x(\operatorname{K}(\operatorname{K}\operatorname{S}))
 +
\\[8pt]
 +
& & \Downarrow
 +
\\[8pt]
 +
\operatorname{I}
 +
& & = & &
 +
\operatorname{K}(\operatorname{K}\operatorname{S})
 +
\end{array}</math>
 +
|}
  
−
where "x = x..." is the definiens,
+
Thus the sequence of operations indicated by <math>\operatorname{K}(\operatorname{K}\operatorname{S})</math> is a <math>\langle \operatorname{K}, \operatorname{S} \rangle</math> proxy for <math>\operatorname{I}.</math>
−
or defining context, and "I" is
 
−
the definiendum,
 
  
−
Find a pure interpretant for I, that is, an equivalent term
+
===Step 2===
−
in <<K, S>>, the combinatory algebra generated by K and S,
 
−
that does as I does.
 
  
−
Observe:
+
Assign types in the following specification:
  
−
  x  = (xK)(xK)  = x(K(KS))
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x_A & = & x_A \operatorname{I}_{A \Rightarrow A}\end{matrix}</math>
 +
|}
  
−
  =>
+
A suitable type assignment provides a propositional typing for <math>\operatorname{I} : A \Rightarrow A,</math> whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.
  
−
  I  = K(KS)
+
===Step 3 (Optional)===
  
−
and so K(KS) constitutes a syntactic algorithm for I.
+
Check that <math>A \Rightarrow A</math> is a theorem of classical propositional calculus.
−
 
 
−
Step 2.
 
−
 
 
−
Assign types in the specification:
 
−
 
 
−
  x_A  =  x_A I_(A=>A)
 
−
 
 
−
to arrive at a propositional typing for I : A => A,
 
−
whose type, read as a proposition, is a theorem of
 
−
intuitionistic propositional calculus.
 
−
 
 
−
Step 3 (optional).
 
−
 
 
−
Check that A => A is a theorem of classical propositional calculus.
 
  
 +
<pre>
 
   A  A
 
   A  A
 
   o---o      o---o
 
   o---o      o---o
 
   |          |
 
   |          |
 
   @    =    @    =    @
 
   @    =    @    =    @
 +
</pre>
  
 
Check.
 
Check.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 4===
  
−
PAT.  Note 2
+
'''Term Development : Contextual Definition <math>\rightsquigarrow</math> Combinator Construction'''
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
Consider the parse tree of the term <math>\operatorname{I}</math> in terms of the primitive combinators <math>\operatorname{K}</math> and <math>\operatorname{S},</math> that is, the articulation or construction corresponding to the term equation <math>\operatorname{I} = (\operatorname{K}(\operatorname{K}\operatorname{S})),</math> as shown here:
−
 
 
−
Identity, or the Identifier (cont.)
 
−
 
 
−
Step 4.
 
−
 
 
−
If we start from the parse tree of the term I in terms of
 
−
the primitive combinators K and S, that is, the articulation
 
−
or construction corresponding to the term equation I = (K(KS)),
 
  
 +
<pre>
 
           K  S
 
           K  S
 
           o  o
 
           o  o
Line 81: Line 75:
 
         o  (o)
 
         o  (o)
 
         \ /
 
         \ /
−
   I  =  (o) ,
+
   I  =  (o)
 +
</pre>
  
−
then adding appropriate type-indices to the nodes of this tree will
+
Adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of <math>\operatorname{I} : A \Rightarrow A.</math>  Thus, the construal or construction of <math>\operatorname{I}</math> as <math>\operatorname{K}(\operatorname{K}\operatorname{S})</math> constitutes a hint or clue to the proof of <math>A \Rightarrow A</math> in the intuitionistic propositional calculus.  Although guesswork may succeed in easy cases such as this, a more systematic procedure is to follow the development in Step&nbsp;1, that takes us from contextual specification to operational algorithm, and to carry along the type information as we go, ending up with a typed parse tree for <math>\operatorname{I},</math> tantamount to a proof tree for <math>A \Rightarrow A.</math>
−
leave us with a proof tree for the propositional type of I : A => A.
 
−
Thus, the construal or construction of I as K(KS) constitutes a hint
 
−
or clue to the proof of A => A in the intuitionistic propositional
 
−
calculus.  Although guesswork may succeed in easy cases such as this,
 
−
a more systematic procedure is to follow the development in Step 1,
 
−
that takes us from contextual specification to operational algorithm,
 
−
and to carry along the type information as we go, ending up with
 
−
a typed parse tree for I, tantamount to a proof tree for A => A.
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 3
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Identity, or the Identifier (cont.)
 
−
 
 
−
Step 4 (cont.)
 
−
 
 
−
Term Development:  Contextual Definition ~~~> Combinator Construction
 
  
 +
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
|                                                          |
 
|                                                          |
Line 153: Line 129:
 
|                                                          |
 
|                                                          |
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 5===
  
−
PAT.  Note 4
+
'''Existential Graph Format : Application Triples with Structure Sharing'''
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
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.
−
 
 
−
| NB.  I am working from rough notes that
 
−
| I wrote out in the Fall of 1996, and it
 
−
| is not always easy to reconstruct what
 
−
| I had in mind at the time.  I misread
 
−
| this passage in my last posting of it,
 
−
| causing me to leave out a few steps.
 
−
 
 
−
1.  Identity, or the Identifier (cont.)
 
−
 
 
−
Step 5.
 
−
 
 
−
Existential Graph Format,
 
−
Application Triples with
 
−
Structure Sharing.
 
−
 
 
−
Same development in Existential Graph notation.
 
−
Here I am carrying out the term development in
 
−
reverse, that is, in application order.
 
  
 +
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
|                                                          |
 
|                                                          |
Line 216: Line 175:
 
|                                                          |
 
|                                                          |
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 +
</pre>
  
−
| I am still not sure what order I intended for the
+
'''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:
−
| application triples, but this 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>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
==Composition, or the Composer==
  
−
PAT.  Note 5
+
===Step 1===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
We are given a specification of the ''composition combinator'', or the ''composer'' <math>\operatorname{P},</math> in terms of the following effects:
  
−
Composition, or the Composer
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x(y(z\operatorname{P})) & = & (xy)z\end{matrix}</math>
 +
|}
  
−
Step 1.
+
We are asked to find an explication of <math>\operatorname{P}</math> in terms of primitive combinators.
−
 
 
−
Given a specification of the "composition combinator",
 
−
or the "composer" P, that has the following effects:
 
−
 
 
−
  x(y(zP))  =  (xy)z
 
−
 
 
−
find an explication of P in terms of primitive combinators.
 
  
 
Proceed as follows:
 
Proceed as follows:
  
−
  (xy)z = (xy)(x(zK)) = x(y((zK)S))
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{ccccc}
 +
(xy)z
 +
& = &
 +
(xy)(x(z\operatorname{K}))
 +
& = &
 +
x(y((z\operatorname{K})\operatorname{S}))
 +
\\[8pt]
 +
(z\operatorname{K})\operatorname{S}
 +
& = &
 +
(z\operatorname{K})(z(\operatorname{S}\operatorname{K}))
 +
& = &
 +
z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))
 +
\\[6pt]
 +
& & \Downarrow
 +
\\[8pt]
 +
x(y(z\operatorname{P}))
 +
& = &
 +
(xy)z
 +
& = &
 +
x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))))
 +
\\[8pt]
 +
& & \Downarrow
 +
\\[8pt]
 +
\operatorname{P}
 +
& & = & &
 +
(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))
 +
\end{array}</math>
 +
|}
  
−
  (zK)S  = (zK)(z(SK))  = z(K((SK)S))
+
===Step 2===
  
−
  =>
+
Assign types in the following specification:
  
−
  x(y(zP)) = (xy)z  =  x(y(z(K((SK)S))))
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \overset{ }{\underset{A}{\Downarrow}} ~
 +
  y \overset{A}{\underset{B}{\Downarrow}}
 +
  ) \overset{ }{\underset{B}{\Downarrow}} ~
 +
  z \overset{B}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{A}{\underset{B}{\Downarrow}} ~
 +
(z \overset{B}{\underset{C}{\Downarrow}} ~
 +
P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
) \overset{A}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\end{array}</math>
 +
|}
  
−
  =>
+
Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math>
  
−
  P =  (K((SK)S))
+
Note that the explication of <math>\operatorname{P}</math> as a term <math>\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})</math> of type <math>(B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))</math> serves as a clue to the proof of <math>\operatorname{P}'\text{s}</math> type proposition as a theorem of the intuitionistic propositional calculus, that is, using only the following two combinator axioms:
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
\operatorname{K} : A \Rightarrow (B \Rightarrow A)
 +
\\ \\
 +
\operatorname{S} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))
 +
\end{array}</math>
 +
|}
  
−
PAT.  Note 6
+
===Step 3 (Optional)===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
Check that the propositional type of the composer <math>\operatorname{P}</math> is a theorem of classical propositional calculus, which is logically necessary to its being a theorem of intuitionistic propositional calculus, but easier to check.
−
 
 
−
Composition, or the Composer (cont.)
 
−
 
 
−
Step 2.
 
−
 
 
−
Assign types in the specification:
 
−
 
 
−
        B    C
 
−
  ((x: y:): z:):
 
−
      A  A B  B C
 
−
 
 
−
  =
 
−
 
 
−
        B  C  (A=>B)=>(A=>C) A=>C C
 
−
  (x: (y: (z: P:            ):  ):):
 
−
    A  A  B  B=>C          A=>B A C
 
−
 
 
−
Here, a notation of the form:
 
−
 
 
−
  x:
 
−
    A
 
−
 
 
−
means that x is of the type A,
 
−
while a notation of the form:
 
−
 
 
−
    B
 
−
  x:
 
−
    A
 
−
 
 
−
means that x is of the type A=>B.
 
−
 
 
−
Note that the explication of P as a term K((SK)S) of
 
−
type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof
 
−
of P's type proposition as a theorem of intuitionistic
 
−
propositional calculus, based on the combinator axioms,
 
−
K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 7
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Composition, or the Composer (cont.)
 
−
 
 
−
Step 3 (optional).
 
−
 
 
−
Check that the propositional type of the composer P is a theorem
 
−
of classical propositional calculus, which is logically necessary
 
−
to its being a theorem of intuitionistic propositional calculus,
 
−
but easier to check.
 
  
 +
<pre>
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 
|                                                |
 
|                                                |
Line 404: Line 362:
 
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 +
</pre>
  
 
QED.
 
QED.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 4===
  
−
PAT. Note 8
+
Repeat the development in Step&nbsp;1, but this time articulating the type information as we go.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
<pre>
−
 
+
o---------------------------------------------------------------------o
−
Composition, or the Composer (cont.)
 
−
 
 
−
Step 4.
 
−
 
 
−
Repeat the development in Step 1,
 
−
but this time articulating the
 
−
type information as we go.
 
−
 
 
−
o---------------------------------------------------------------------o
 
 
|                                                                    |
 
|                                                                    |
 
|          x      y A                                              |
 
|          x      y A                                              |
Line 552: Line 502:
 
|                                                                    |
 
|                                                                    |
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
The foregoing development has taken us from the typed parse tree for the definiens <math>((xy)z)\!</math> to the typed parse tree for the explicated definiendum <math>(x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))~))),</math> which gives us both the construction of the composition combinator <math>\operatorname{P}</math> in terms of primitive combinators:
  
−
PAT.  Note 9
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}\operatorname{P} & = & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))\end{matrix}</math>
 +
|}
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
and also the proof tree for the type proposition of <math>\operatorname{P},</math> as follows:
−
 
 
−
Composition, or the Composer (cont.)
 
−
 
 
−
Step 4 (concl.)
 
−
 
 
−
The foregoing development has taken us from the
 
−
typed parse tree for the definiens ((xy)z) to the
 
−
typed parse tree for the explicated definiendum
 
−
(x(y(z(K((SK)S)) ))), which gives us both the
 
−
construction of the composition combinator P
 
−
in terms of primitive combinators:
 
−
 
 
−
  P  =  (K((SK)S))
 
−
 
 
−
and also the proof tree for the proposition type of P:
 
  
 +
<pre>
 
         S  K
 
         S  K
 
         o  o
 
         o  o
Line 582: Line 521:
 
         \ /
 
         \ /
 
   P  =  (o)
 
   P  =  (o)
 +
</pre>
  
−
  P = (K((SK)S)) : (B=>C)=>((A=>B)=>(A=>C))
+
{| align="center" cellpadding="8" width="90%"
−
 
+
|
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
<math>\begin{matrix}
−
 
+
\operatorname{P}
−
PAT.  Note 10
+
& = &
−
 
+
(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
& : &
−
 
+
(B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))
−
Composition, or the Composer (concl.)
+
\end{matrix}</math>
 +
|}
  
−
Step 5.
+
===Step 5===
  
 
Rewrite the final proof tree in existential graph format:
 
Rewrite the final proof tree in existential graph format:
  
 +
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
|                                                          |
 
|                                                          |
Line 638: Line 580:
 
|                                                          |
 
|                                                          |
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 +
</pre>
  
−
NB.  Graphic convention used in the above style of display:
+
; Note on the graphic conventions used in the above style of diagram
−
    Square bracketed nodes mark subtrees to be pruned from
+
: Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, amounting in effect to ''Facts'' being recycled as ''Cases''. Square brackets are also used to mark the intended result.
−
    one tree and grafted into another at the indicated site,
 
−
    amounting in effect to "Facts" being recycled as "Cases".
 
−
    Square brackets are also used to mark the intended result.
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 11
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
  
−
Self-Documentation
+
==Self-Documentation : Developmental Data Structures==
  
−
Observation. Notice the "self-documenting" property
+
; Observation.
−
of proof developments in the existential graph format,
+
: Notice the "self-documenting" property of proof developments in the existential graph format, that is, the property of a developing structure that remembers its own history.
−
that is, the property of a developing structure that
 
−
remembers its own history.
 
  
 
For example, the development of the Identity combinator:
 
For example, the development of the Identity combinator:
  
−
  x = (xK)(xK) = x(K(KS))
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{matrix}
 +
x
 +
& = &
 +
(x\operatorname{K})(x\operatorname{K})
 +
& = &
 +
x(\operatorname{K}(\operatorname{K}\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
 +
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
|                                                          |
 
|                                                          |
Line 703: Line 645:
 
|                                                          |
 
|                                                          |
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
−
 
+
</pre>
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 12
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Self-Documentation, Developmental Data Structures (cont.)
 
  
 
Redo the entire development of the Composer in existential graph format:
 
Redo the entire development of the Composer in existential graph format:
  
−
Step 5 (extended).
+
'''Step 5 (extended)'''
  
 +
<pre>
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 
| Hypotheses:  x : A,  y : A=>B,  z : B=>C                            |
 
| Hypotheses:  x : A,  y : A=>B,  z : B=>C                            |
Line 805: Line 741:
 
|                                                                    |
 
|                                                                    |
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 +
</pre>
  
 
That's the sketch as best I can reconstruct it from my notes.
 
That's the sketch as best I can reconstruct it from my notes.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
==Triadic Analogy : Analogy Between Two Triadic Relations==
  
−
PAT.  Note 13
+
<br>
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Triadic Analogy:  Analogy Between a Couple of Three-Place Relations
 
  
 +
<pre>
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 
|                                                |
 
|                                                |
Line 825: Line 759:
 
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
<br>
  
−
PAT.  Note 14
+
==Transposition, or the Transposer==
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
'''Definition'''
  
−
Transposition, or the Transposer
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
 +
|}
  
−
  x(y(zT))  =  y(xz)
+
This equation provides a contextual definition for the operator <math>\operatorname{T},</math> in effect, a formal syntactic specification that tells how the operator is required to act on other symbols.
  
−
This equation constitutes a "paraphrastic definition"
+
===Step 1===
−
of T, a definition-in-context, or a formal syntactic
 
−
specification of how the operator is required to act
 
−
on other symbols.
 
  
−
Step 1.
+
'''Construction'''
  
−
Find a "pure interpretant" for T, that is, an equivalent term
+
Find a ''pure interpretant'' for <math>\operatorname{T},</math> that is, an equivalent term doing the job of <math>\operatorname{T}</math> which is constructed purely in terms of the
−
doing the job of T which is constructed purely in terms of the
+
primitive combinators <math>\operatorname{K}</math> and <math>\operatorname{S}.</math>
−
primitive combinators K and S.
 
  
−
This will constitute an operational algorithm for T, though
+
Doing this yields an operational algorithm for <math>\operatorname{T},</math> understood as a sequence of manipulations on formal identifiers, or on symbols taken as objects in their own rights.
−
still operating at the level of abstract syntax, understood
 
−
as a sequence of manipulations on formal identifiers, or on
 
−
symbols taken as objects in themselves.
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
 +
|}
  
−
PAT.  Note 15
+
Observe that <math>y(xz)\!</math> matches <math>(xy)(xz)\!</math> on the right, and that we can express <math>y\!</math> as <math>x(y\operatorname{K}),</math> consequently:
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
−
 
+
|
−
Transposition, or the Transposer (cont.)
+
<math>\begin{matrix}
−
 
+
y(xz)
−
  x(y(zT))  = y(xz)
+
& = &
 +
(x(y\operatorname{K}))(xz)
 +
\\[8pt]
 +
& = &
 +
x((y\operatorname{K})(z\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
−
Step 1 (concl.)
+
thus completing the abstraction (or disentanglement) of x from the expression.
  
−
Observe that y(xz) matches (xy)(xz) on the right,
+
Working on the remainder of the expression, the next item of business is to abstract <math>y.\!</math>
−
and that we can express y as x(yK), consequently:
 
−
 
 
−
  y(xz)  =  (x(yK))(xz)
 
−
 
 
−
          =  x((yK)(zS))
 
−
 
 
−
thus completing the abstraction (or disentanglement)
 
−
of x from the expression.
 
−
 
 
−
Working on the remainder of the expression,
 
−
the next item of business is to abstract y.
 
  
 
Notice that:
 
Notice that:
  
−
  (yK)(zS) = (yK)(y((zS)K))
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{matrix}
 +
(y\operatorname{K})(z\operatorname{S})
 +
& = &
 +
(y\operatorname{K})(y((z\operatorname{S})\operatorname{K}))
 +
\\[8pt]
 +
& = &
 +
y(\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
−
            =  y(K(((zS)K)S))
+
thus completing the abstraction of <math>y.\!</math>
  
−
thus completing the abstraction of y.
+
Next, work on <math>\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S})</math> to extract <math>z,\!</math> starting from the center <math>(z\operatorname{S})\operatorname{K}</math> of the labyrinth and working outward:
  
−
Next, work on K(((zS)K)S) to extract z, starting from
+
{| align="center" cellpadding="8" width="90%"
−
the center (zS)K of the labyrinth and working outward:
+
|
 +
<math>\begin{matrix}
 +
(z\operatorname{S})\operatorname{K}
 +
& = &
 +
(z\operatorname{S})(z(\operatorname{K}\operatorname{K}))
 +
\\[8pt]
 +
& = &
 +
z(\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
−
  (zS)K =  (zS)(z(KK))
+
For the sake of brevity in the rest of this development, rename the operator on the right so that <math>(\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S})) = \operatorname{F}.</math>
  
−
          =  z(S((KK)S))
+
Continue with <math>\operatorname{K}((z\operatorname{F})\operatorname{S}),</math> to extract <math>z,\!</math> as follows:
  
−
For the sake of brevity in the rest of this development,
+
{| align="center" cellpadding="8" width="90%"
−
rename the operator on the right so that (S((KK)S)) = F.
+
|
 +
<math>\begin{matrix}
 +
(z\operatorname{F})\operatorname{S}
 +
& = &
 +
(z\operatorname{F})(z(\operatorname{S}\operatorname{K}))
 +
\\[8pt]
 +
& = &
 +
z(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
−
Continue with K((zF)S), to extract z:
+
Rename the operator on the right, letting <math>(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) = \operatorname{G}.</math>
  
−
  (zF)S  =  (zF)(z(SK))
+
Continue with <math>\operatorname{K}(z\operatorname{G}),</math> to extract <math>z,\!</math> as follows:
  
−
          = z(F((SK)S))
+
{| align="center" cellpadding="8" width="90%"
−
 
+
|
−
Rename the operator on the right, letting (F((SK)S)) = G.
+
<math>\begin{matrix}
−
 
+
\operatorname{K}(z\operatorname{G})
−
Continue with K(zG), to extract z:
+
& = &
−
 
+
(z(\operatorname{K}\operatorname{K}))(z\operatorname{G})
−
  K(zG)  =  (z(KK))(zG)
+
\\[8pt]
−
 
+
& = &
−
          = z((KK)(GS))
+
z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S}))
 +
\end{matrix}</math>
 +
|}
  
 
Filling in the abbreviations:
 
Filling in the abbreviations:
  
−
  y(xz) = x(y(z((KK)(GS)) ))
+
{| align="center" cellpadding="8" width="90%"
−
 
+
|
−
          = x(y(z((KK)((F((SK)S))S)) ))
+
<math>\begin{array}{lll}
−
 
+
y(xz)
−
          = x(y(z((KK)(((S((KK)S))((SK)S))S)) ))
+
& = &
 +
x(y(z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S}))~))
 +
\\[8pt]
 +
& = &
 +
x(y(z((\operatorname{K}\operatorname{K})((\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~))
 +
\\[8pt]
 +
& = &
 +
x(y(z((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~))
 +
\end{array}</math>
 +
|}
  
 
Thus we have:
 
Thus we have:
  
−
  T = (KK)(((S((KK)S))((SK)S))S)
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{matrix}
 +
\operatorname{T}
 +
& = &
 +
(\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S})
 +
\end{matrix}</math>
 +
|}
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 2===
  
−
PAT.  Note 16
+
Using the contextual definition of the transposer <math>\operatorname{T},</math>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
 +
|}
  
−
Transposition, or the Transposer (cont.)
+
find a minimal generic typing (simplest non-degenerate typing) of each term in the specification that makes all of the applications on each side of the equation go through.
−
 
 
−
Step 2.
 
−
 
 
−
Using the contextual definition of the transposer T,
 
−
 
 
−
  y(xz)  =  x(y(zT)),
 
−
 
 
−
find a minimal generic typing (simplest non-degenerate typing) of
 
−
each term in the specification that makes all of the applications
 
−
on each side of the equation go through.
 
  
 
For example, here is one such typing:
 
For example, here is one such typing:
  
−
            B=>C  C                    B=>C  B=>(A=>C) A=>C  C
+
{| align="center" cellpadding="8" width="90%"
−
  (y: (x: z:    ): ):  =   (x: (y: (z:    T:        ):    ): ):
+
|
−
    B  A A     B C         A  B   A    A=>(B=>C)  B     A  C
+
<math>\begin{array}{l}
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
  z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
 +
  ) \overset{B}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
 +
  T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
  ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
) \overset{A}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\end{array}</math>
 +
|}
  
−
In a contextual, implicit, or paraphrastic definition of this sort,
+
In a contextual, implicit, or paraphrastic definition of this sort, the ''definiendum'' is the symbol to be defined, in this case, <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime},</math> and the ''definiens'' is the entire rest of the context, in this case, the frame <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime},</math> that ostensibly defines, or as one says, is supposed to define the symbol <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime}</math> that we find in its slot.  More loosely speaking, the side of the equation with the more known symbols may be called its ''defining'' side.
−
the "definiendum" is the symbol to be defined, in this case, "T",
 
−
and the "definiens" is the entire rest of the context, in this
 
−
case, the frame "y(xz) = x(y(z__))", that ostensibly defines,
 
−
or as one says, is supposed to define the symbol "T" that
 
−
we find in its slot.  More loosely speaking, the side of
 
−
the equation with the more known symbols may be called
 
−
its "defining" side.
 
  
−
In order to find a minimal generic typing, start with the defining side
+
In order to find a minimal generic typing, start with the defining side of the equation, freely assigning types in such a way that the successive applications make sense, but without introducing unnecessary complications or creating unduly specialized applications.  Then work out what the type of the defined operator <math>\operatorname{T}</math> has to be, in order to function properly in the standard context, in this case, <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime}.</math>
−
of the equation, freely assigning types in such a way that the successive
 
−
applications make sense, but without introducing unnecessary complications
 
−
or creating unduly specialized applications.  Then work out what the type
 
−
of the defined operator T has to be, in order to function properly in the
 
−
standard context, in this case, (x(y(z__))).
 
  
 
Again, this gives:
 
Again, this gives:
  
−
            B=>C  B=>(A=>C)  A=>C  C                   B=>C C
+
{| align="center" cellpadding="8" width="90%"
−
  (x: (y: (z:    T:        ):    ): ):  =   (y: (x: z:    ): ):
+
|
−
    A   B   A    A=>(B=>C) B     A  C         B  A  A    B C
+
<math>\begin{array}{l}
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
 +
  T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
  ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
  ) \overset{A}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
 +
) \overset{B}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\end{array}</math>
 +
|}
  
−
Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type,
+
Thus we have <math>\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C)),</math> whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.
−
read as a proposition, is a theorem of intuitionistic
 
−
propositional calculus.
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 3 (Optional)===
  
−
PAT.  Note 17
+
At this juncture we might want to verify that the proposition corresponding to the type of <math>\operatorname{T}</math> is actually a theorem of classical propositional calculus.  Since nothing can be a theorem of intuitionistic propositional calculus wihout also being a theorem of classical propositional calculus, this is a necessary condition of our work being correct up to this point.  Although it is not a sufficient condition, classical theoremhood is easier to test and so provides a quick and useful check on our work.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
In existential graph format, <math>\operatorname{T}</math> has the following generic typing:
−
 
 
−
Transposition, or the Transposer (cont.)
 
−
 
 
−
Step 3 (optional).
 
−
 
 
−
At this juncture we might want to verify that the proposition corresponding
 
−
to the type of T is actually a theorem of classical propositional calculus.
 
−
Since nothing can be a theorem of intuitionistic propositional calculus
 
−
wihout also being a theorem of classical propositional calculus, this
 
−
is a necessary condition of our work being correct up to this point.
 
−
Although it is not a sufficient condition, classical theoremhood
 
−
is easier to test and so provides a quick and useful check on
 
−
our work.
 
−
 
 
−
In existential graph format, T has the following generic typing:
 
  
 +
<pre>
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 
|                                                |
 
|                                                |
Line 1,004: Line 975:
 
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 +
</pre>
  
 
And here is a classical logic proof of the type proposition:
 
And here is a classical logic proof of the type proposition:
  
 +
<pre>
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 
|                                                |
 
|                                                |
Line 1,039: Line 1,012:
 
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 4===
  
−
PAT. Note 18
+
The construction of the term <math>\operatorname{T}</math> of the appropriate type in terms of the primitive typed combinators of the forms <math>\operatorname{K}</math> and <math>\operatorname{S}</math> is analogous to the proof of the corresponding proposition from the intuitionistic axiom schemes attached to those forms.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
Incidentally, note the inobtrusive appearance of renaming strategies in the progress of this work.  Renaming is the natural operation that substitution is the reverse of.  With these humble beginnings we have reached a birthplace, a native ground, of the [[sign relation]], an irreducible three-place relationship among what is indicated, what happens to indicate it, and all of the equivalent or associated indications we may find or create in reference to it.
  
−
Transposition, or the Transposer (cont.)
+
For example, let the interposed interpretant <math>^{\backprime\backprime} \operatorname{G} ^{\prime\prime}</math> denote the supposed object, namely, whatever it is that the occurrent sign <math>^{\backprime\backprime} (\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) ^{\prime\prime}</math> denotes.
  
−
Step 4.
+
Consider the following data:
  
−
The construction of the term T of the appropriate type in terms of the
+
:* The parse tree for the term <math>\operatorname{T} = ((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))</math>
−
primitive typed combinators of the forms K and S is analogous to the
 
−
proof of the corresponding proposition from the intuitionistic axiom
 
−
schemes attached to those forms.
 
  
−
Incidentally, note the inobtrusive appearance of renaming strategies in the
+
:* The type marker of the term <math>\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C))</math>
−
progress of this work.  Renaming is the natural operation that substitution
 
−
is the reverse of.  With these humble beginnings we have reached a birthplace,
 
−
a native ground, of the sign relation, an irreducible three-place relationship
 
−
among what is indicated, what happens to indicate it, and all of the equivalent
 
−
or associated indications we may find or create in reference to it.
 
−
 
 
−
For example, let "G", the interposed interpretant,
 
−
denote whatever it is, the supposed object, that
 
−
"(F((SK)S))", the occurrent sign, denotes.
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 19
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Transposition, or the Transposer (cont.)
 
−
 
 
−
Step 4 (cont.)
 
−
 
 
−
Consider the following data:
 
−
 
 
−
The parse tree of the term T = ((KK)(((S((KK)S))((SK)S))S))
 
−
and the typing of the term T : (A=>(B=>C))=>(B=>(A=>C)).
 
  
 +
<pre>
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 
|                                                |
 
|                                                |
Line 1,107: Line 1,055:
 
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
 +
</pre>
  
−
Can proofs be developed by tracing the stepwise articulation or
+
Can proofs be developed by tracing the stepwise articulation or explication of the untyped proof hint, typing each term as we go?
−
explication of the untyped proof hint, typing each term as we go?
 
  
 
For example, we might begin as follows:
 
For example, we might begin as follows:
  
−
o-----------------------------------------------------------o
+
{| align="center" cellpadding="8" width="90%"
−
|                                                          |
+
|
−
|            B=>C  C                                        |
+
<math>\begin{array}{l}
−
|  (y: (x: z:    ): ):                                    |
+
(y \overset{ }{\underset{B}{\Downarrow}} ~
−
|    B  A A     B C                                     |
+
(x \overset{ }{\underset{A}{\Downarrow}} ~
−
|                                                          |
+
  z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
−
o===========================================================o
+
  ) \overset{B}{\underset{C}{\Downarrow}}
−
|                                                          |
+
  ) \overset{ }{\underset{C}{\Downarrow}}
−
|            A=>B B         B=>C  C                       |
+
\\ \\
−
|  ((x: (y: K:    ): ): (x: z:    ): ):                    |
+
=
−
|      A   B  B    A B  A  A    B C                   |
+
\\ \\
−
|                                                          |
+
((x \overset{ }{\underset{A}{\Downarrow}} ~
−
o===========================================================o
+
(y \overset{ }{\underset{B}{\Downarrow}} ~
−
|                                                          |
+
  K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
−
|            A=>B  B  B=>C  (A=>B)=>(A=>C) A=>C C      |
+
  ) \overset{A}{\underset{B}{\Downarrow}}
−
|   (x: ((y: K:    ): (z:    S:              ):    ): ):    |
+
  ) \overset{ }{\underset{B}{\Downarrow}} ~
−
|    A   B  B     A  A     A=>(B=>C)       A=>B  A  C   |
+
(x \overset{ }{\underset{A}{\Downarrow}} ~
−
|                                                          |
+
   z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
−
o===========================================================o
+
   ) \overset{B}{\underset{C}{\Downarrow}}
−
|                                                          |
+
  ) \overset{ }{\underset{C}{\Downarrow}}
−
|  ...                                                    |
+
\\ \\
−
|                                                           |
+
=
−
o-----------------------------------------------------------o
+
\\ \\
−
 
+
(x \overset{ }{\underset{A}{\Downarrow}} ~
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
((y \overset{ }{\underset{B}{\Downarrow}} ~
−
 
+
   K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
−
PAT.  Note 20
+
  ) \overset{A}{\underset{B}{\Downarrow}} ~
−
 
+
  (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
   S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
−
 
+
  ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
−
Transposition, or the Transposer (cont.)
+
   ) \overset{A}{\underset{C}{\Downarrow}}
−
 
+
  ) \overset{ }{\underset{C}{\Downarrow}}
−
Step 4 (cont.)
+
\\ \\
−
 
+
=
−
If this strategy is successful it suggests that the proof tree can
+
\\ \\
−
be grown in a stepwise equational fashion from a seed term of the
+
\ldots
−
appropriate species, in other words, from a contextual, embedded,
+
\end{array}</math>
−
or paraphrastic specification of the desired term.
+
|}
−
 
+
 
−
Thus, these developments culminate in the rather striking and
+
If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term.
−
possibly disconcerting consequence that the apparent flow of
+
 
−
information or reasoning in the proof tree is something of
+
Thus, these developments culminate in the rather striking and possibly disconcerting consequence that the apparent flow of information or reasoning in the proof tree is something of a put-up job, a snapshot likeness or a likely story that calls to mind the anatomy of a justification, but fails to reconstruct the true embryology or living physiology of discovery involved.
−
a put-up job, a snapshot likeness or a likely story that
+
 
−
calls to mind the anatomy of a justification, but fails
+
Repeat the development in Step&nbsp;1, but this time articulating the type information as we go.
−
to reconstruct the true embryology or living physiology
+
 
−
of discovery involved.
+
<pre>
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Note 21
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Transposition, or the Transposer (cont.)
 
−
 
 
−
Step 4 (concl.)
 
−
 
 
−
Repeat the development in Step 1,
 
−
but this time articulating the
 
−
type information as we go.
 
−
 
 
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 
|                                                                    |
 
|                                                                    |
Line 1,551: Line 1,484:
 
|                                                                    |
 
|                                                                    |
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Step 5===
  
−
PAT.  Note 22
+
Rewrite the final proof tree in existential graph format, implementing structure sharing among application triples by overlaying the type propositions that attach to terms.
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Transposition, or the Transposer (cont.)
 
−
 
 
−
Step 5.
 
−
 
 
−
Rewrite the final proof tree in existential graph format,
 
−
implementing structure sharing among application triples
 
−
by overlaying the type propositions that attach to terms.
 
−
 
 
−
Graphic Conventions:  Square bracketed nodes mark subtrees
 
−
to be pruned from one tree and grafted into another at the
 
−
indicated site, tantamount to recycling "Facts" as "Cases".
 
−
Square brackets are also used to indicate the final result.
 
  
 +
<pre>
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 
|                                                                    |
 
|                                                                    |
Line 1,703: Line 1,623:
 
|                                                                    |
 
|                                                                    |
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
; Graphic Conventions
−
 
+
: Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, tantamount to recycling ''Facts'' as ''Cases''.  Square brackets are also used to indicate the final result.
−
PAT.  Note 23
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
Transposition, or the Transposer (cont.)
 
  
−
Step 5 (extended).
+
===Step 5 (Extended)===
  
 
Redo the development of the proof tree in existential graph format.
 
Redo the development of the proof tree in existential graph format.
  
−
Each frame of the developmental scheme that follows is divided by
+
Each frame of the developmental scheme that follows is divided by a dotted line, with terms that contribute to the main term under development being shown above it and the main term itself being shown below it.
−
a dotted line, with terms that contribute to the main term under
 
−
development being shown above it and the main term itself being
 
−
shown below it.
 
  
 +
<pre>
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 
| Hypotheses:  x : A,  y : B,  z : A=>(B=>C)                          |
 
| Hypotheses:  x : A,  y : B,  z : A=>(B=>C)                          |
Line 2,268: Line 2,182:
 
|                                                                    |
 
|                                                                    |
 
o---------------------------------------------------------------------o
 
o---------------------------------------------------------------------o
 +
</pre>
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
==Commentary==
  
−
PAT.  Note 24
+
===Commentary Note 1===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time.
  
 +
{| align="center" cellpadding="8" width="90%"
 +
| '''Observation 1'''
 +
|-
 +
| '''IF''' we know that the element <math>x\!</math> is of the type <math>X\!</math>
 +
|-
 +
| '''AND''' we know that the function <math>f\!</math> is of the type <math>X \to Y</math>
 +
|-
 +
| '''THEN''' we know that the element <math>f(x)\!</math> is of the type <math>Y.\!</math>
 +
|}
  
 +
We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
x : X
 +
\\
 +
\underline{f : X \to Y}
 +
\\
 +
f(x) : Y
 +
\end{array}</math>
 +
|}
  
−
PAT. Propositions As Types -- Commentary
+
In this scheme of inference, the notations <math>{}^{\backprime\backprime} x {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} f {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} f(x) {}^{\prime\prime}</math> are referred to as ''terms'' and interpreted as names of formal objects.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
In the same context, the notations <math>{}^{\backprime\backprime} X {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} X \to Y {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} Y {}^{\prime\prime}</math> give us information, or indicate formal constraints, that we may think of as denoting the ''types'' of the formal objects under consideration.  By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.
  
−
PAT.  Commentary Note 1
+
If a moment's spell of double vision leads us to see the functional arrow <math>{}^{\backprime\backprime} \to {}^{\prime\prime}</math> as the logical arrow <math>{}^{\backprime\backprime} \Rightarrow {}^{\prime\prime}</math> then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called ''modus ponens''.  And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of ''modus ponens''.
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Commentary Note 2===
  
−
I think it's best to begin with a few simple observations,
+
Notice that I am carrying out combinator applications "on the right", so the formulas might read backwards from what many people are used to.
−
as I frequently find it necessary to return to the basics
 
−
again and again, even if I take a different path each time.
 
  
−
Observation 1
+
==Bibliography==
  
−
  If we have the information that an element x
+
Here are three references on combinatory logic and lambda calculus, given in order of difficulty from introductory to advanced, that are especially pertinent to the use of combinators in computer science:
−
  is constrained to be of the type X
 
  
−
  and we have the information that a function f
+
# Smullyan, R. (1985), ''To Mock a Mockingbird, And Other Logic Puzzles, Including an Amazing Adventure in Combinatory Logic'', Alfred A. Knopf, New York, NY.
−
  is constrained to be of the type X -> Y
+
# Hindley, J.R. and Seldin, J.P. (1986), ''Introduction to Combinators and <math>\lambda</math>-Calculus'', London Mathematical Society Student Texts No.&nbsp;1, Cambridge University Press, Cambridge, UK.
 +
# Lambek, J. and Scott, P.J. (1986), ''Introduction To Higher Order Categorical Logic'', Cambridge University Press, Cambridge, UK.
  
−
  then we have the information that the element f(x)
+
==Basic Concepts from Lambek and Scott (1986)==
−
  is constrained to be of the type Y.
 
  
−
We can abbreviate this inference, that operates on
+
Notes on basic concepts from Lambek and Scott (1986), ''Introduction To Higher Order Categorical Logic'', Cambridge University Press, Cambridge, UK.  [http://suo.ieee.org/ontology/thrd42.html#03373 Excerpts and discussion on the Ontology List].
−
two pieces of information to produce another piece
 
−
of information, in the following conventional form:
 
  
−
  x : X
+
Here is a synopsis, exhibiting just the layering of axioms &mdash; notice the technique of starting over at the initial point several times and building up both more richness of detail and more generality of perspective with each passing time:
−
  f : X -> Y
 
−
  -----------
 
−
  f(x) : Y
 
  
−
In this scheme of inference, the notations "x", "f", and "f(x)"
+
===Concrete Category===
−
are taken to be names of formal objects.  Some people will call
 
−
these notations by the name of "terms", while other people will
 
−
somewhat more confusedly say that the formal objects themselves
 
−
are the terms.  Because it is so important to distinguish signs
 
−
denoting from objects denoted, I will make some effort to avoid
 
−
the latter usage, and recommend sticking with the first option.
 
  
−
In the same context, the notations "X", "X -> Y", and "Y" give us
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
information, or indicate formal constraints, that we may think of
+
|
−
as denoting the "types" of the formal objects under consideration.
+
<p>'''Definition 1.1.'''  A ''concrete category'' is a collection of two kinds of entities, called ''objects'' and ''morphisms''.  The former are sets which are endowed with some kind of structure, and the latter are mappings, that is, functions from one object to another, in some sense preserving that structure.  Among the morphisms, there is attached to each object <math>A\!</math> the ''identity mapping'' <math>1_A : A \to A</math> such that <math>1_A(a) = a\!</math> for all <math>a \in A.\!</math>  Moreover, morphisms <math>f : A \to B</math> and <math>g : B \to C</math> may be ''composed'' to produce a morphism <math>gf : A \to C</math> such that <math>(gf)(a) = g(f(a))\!</math> for all <math>a \in A.\!</math></p>
−
By an act of "hypostatic abstraction", one may of course elect to
 
−
view these types as a species of formal objects existing in their
 
−
own right, inhabiting their own niche, as it were.
 
  
−
If a moment's spell of double vision leads us to see the
+
<p>We shall now progress from concrete categories to abstract ones, in three easy stages.</p>
−
functional arrow "->" as the logical arrow "=>", then we
 
−
may observe that the right side of this inference scheme
 
−
follows the pattern of logical deduction that is usually
 
−
called "modus ponens".  And so we forge a tentative link
 
−
between the pattern of information conversion implicated
 
−
in functional application and the pattern of information
 
−
conversion involved in the logical rule of modus ponens.
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
<p>(Lambek & Scott, 4&ndash;5).</p>
 +
|}
  
−
PAT.  Commentary Note 2
+
===Graph===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 +
|
 +
<p>'''Definition 1.2.'''  A ''graph'' (usually called a ''directed graph'') consists of two classes:  the class of ''arrows'' (or ''oriented edges'') and the class of ''objects'' (usually called ''nodes'' or ''vertices'') and two mappings from the class of arrows to the class of objects, called ''source'' and ''target'' (often also ''domain'' and ''codomain'').</p>
  
−
Re: PAT.  http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872
+
<center><pre>
  
−
Notice that I am carrying out combinator applications "on the right",
+
o--------------o      source      o--------------o
−
so the formulas might be backwards from what many people are used to.
+
|              | ----------------> |              |
 +
|  Arrows    |                  |  Objects    |
 +
|              | ----------------> |              |
 +
o--------------o      target      o--------------o
  
−
Here are a three references on combinatory logic and lambda calculus,
+
</pre></center>
−
given in order of difficulty from introductory to advanced, that are
 
−
especially pertinent to the use of combinators in computer science:
 
  
−
| Smullyan, R.,
+
<p>One writes <math>^{\backprime\backprime} f : A \to B \, ^{\prime\prime}</math> for <math>^{\backprime\backprime} \operatorname{source}\ f = A ~\operatorname{and}~ \operatorname{target}\ f = B \, ^{\prime\prime}.</math>  A graph is said to be ''small'' if the classes of objects and arrows are sets.</p>
−
|'To Mock a Mockingbird, And Other Logic Puzzles,
 
−
| Including an Amazing Adventure in Combinatory Logic',
 
−
| Alfred A. Knopf, New York, NY, 1985.
 
  
−
| Hindley, J.R. and Seldin, J.P.,
+
<p>(Lambek & Scott, 5).</p>
−
|'Introduction to Combinators and [Lambda]-Calculus',
+
|}
−
| London Mathematical Society Student Texts No. 1,
 
−
| Cambridge University Press, Cambridge, UK, 1986.
 
  
−
| Lambek, J. and Scott, P.J.,
+
===Deductive System===
−
|'Introduction To Higher Order Categorical Logic',
 
−
| Cambridge University Press, Cambridge, UK, 1986.
 
−
| http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521356539
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 +
|
 +
<p>A ''deductive system'' is a graph in which to each object <math>A\!</math> there is associated an arrow <math>1_A : A \to A,</math> the ''identity'' arrow, and to each pair of arrows <math>f : A \to B</math> and <math>g : B \to C</math> there is associated an arrow <math>gf : A \to C,</math> the ''composition'' of <math>f\!</math> with <math>g.\!</math>  A logician may think of the objects as ''formulas'' and of the arrows as ''deductions'' or ''proofs'', hence of</p>
 +
|-
 +
|
 +
::<p><math>\dfrac{~ f : A \to B \quad g : B \to C ~}{gf : A \to C}</math></p>
 +
|-
 +
|
 +
<p>as a ''rule of inference''.</p>
  
−
PAT. Commentary Note 3
+
<p>(Lambek & Scott, 5).</p>
 +
|}
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Category===
  
 +
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 +
|
 +
<p>A ''category'' is a deductive system in which the following equations hold, for all <math>f : A \to B,</math> <math>g : B \to C,</math> and <math>h : C \to D.</math></p>
 +
|-
 +
|
 +
::<p><math>f 1_A = f = 1_B f, \quad (hg)f = h(gf).</math></p>
 +
|-
 +
|
 +
<p>(Lambek & Scott, 5).</p>
 +
|}
  
 +
===Functor===
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 +
|
 +
<p>'''Definition 1.3.'''  A ''functor'' <math>F : \mathcal{A} \to \mathcal{B}</math> is first of all a morphism of graphs &hellip;, that is, it sends objects of <math>\mathcal{A}</math> to objects of <math>\mathcal{B}</math> and arrows of <math>\mathcal{A}</math> to arrows of <math>\mathcal{B}</math> such that, if <math>f : A \to A',</math> then <math>F(f) : F(A) \to F(A').</math>  Moreover, a functor preserves identities and composition;  thus:</p>
 +
|-
 +
|
 +
::<p><math>F(1_A) = 1_{F(A)}, \quad F(gf) = F(g)F(f).</math></p>
 +
|-
 +
|
 +
<p>In particular, the identity functor <math>1_\mathcal{A} : \mathcal{A} \to \mathcal{A}</math> leaves objects and arrows unchanged and the composition of functors <math>F : \mathcal{A} \to \mathcal{B}</math> and <math>G : \mathcal{B} \to \mathcal{C}</math> is given by:</p>
 +
|-
 +
|
 +
::<p><math>(GF)(A) = G(F(A)), \quad (GF)(f) = G(F(f)),</math></p>
 +
|-
 +
|
 +
<p>for all objects <math>A\!</math> of <math>\mathcal{A}</math> and all arrows <math>f : A \to A'</math> in <math>\mathcal{A}.</math></p>
  
−
PAT. Work Area
+
<p>(Lambek & Scott, 6).</p>
 +
|}
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
===Natural Transformation===
  
−
I have been posting excerpts to the ONT List, between note_01 & note_30:
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 +
|
 +
<p>'''Definition 2.1.'''  Given functors <math>F, G : \mathcal{A} \rightrightarrows \mathcal{B},</math> a ''natural transformation'' <math>t : F \to G</math> is a family of arrows <math>t(A) : F(A) \to G(A)</math> in <math>\mathcal{B},</math> one arrow for each object <math>A\!</math> of <math>\mathcal{A},</math> such that the following square commutes for all arrows <math>f : A \to B</math> in <math>\mathcal{A}</math>:</p>
  
−
note_01 = http://suo.ieee.org/ontology/msg03373.html
+
<pre>
−
note_30 = http://suo.ieee.org/ontology/msg03418.html
 
  
−
Here is a synopsis, exhibiting just the layering of axioms --
+
                  t(A)
−
notice the technique of starting over at the initial point
+
    F(A) o------------------>o G(A)
−
several times and building up both more richness of detail
+
          |                  |
−
and more generality of perspective with each passing time:
+
          |                  |
 +
    F(f) |                  | G(f)
 +
          |                  |
 +
          v                  v
 +
    F(B) o------------------>o G(B)
 +
                  t(B)
  
−
Concrete Category
+
</pre>
  
−
| Definition 1.1.  A 'concrete category' is a collection of two kinds
+
<p>that is to say, such that</p>
−
| of entities, called 'objects' and 'morphisms'.  The former are sets
+
|-
−
| which are endowed with some kind of structure, and the latter are
+
|
−
| mappings, that is, functions from one object to another, in some
+
<p><math>G(f)t(A) = t(B)F(f).\!</math></p>
−
| sense preserving that structure.  Among the morphisms, there is
+
|-
−
| attached to each object A the 'identity mapping' 1_A : A -> A
+
|
−
| such that 1_A(a) = a for all a in A.  Moreover, morphisms
+
<p>{Lambek & Scott, 8).</p>
−
| f : A -> B and g : B -> C may be 'composed' to produce
+
|}
−
| a morphism gf : A -> C such that (gf)(a) = g(f(a))
 
−
| for all a in A.
 
  
−
| We shall now progress from concrete categories
+
===Graph 2===
−
| to abstract ones, in three easy stages.
 
  
−
Graph
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
 
 
−
| Definition 1.2.  A 'graph' (usually called a 'directed graph') consists
 
−
| of two classes:  the class of 'arrows' (or 'oriented edges') and the class
 
−
| of 'objects' (usually called 'nodes' or 'vertices') and two mappings from
 
−
| the class of arrows to the class of objects, called 'source' and 'target'
 
−
| (often also 'domain' and 'codomain').
 
 
|
 
|
−
| o--------------o      source      o--------------o
+
<p>We recall &hellip; that, for categories, a ''graph'' consists of two classes and two mappings between them:</p>
−
| |              | ----------------> |              |
 
−
| |  Arrows    |                  |  Objects    |
 
−
| |              | ----------------> |              |
 
−
| o--------------o      target      o--------------o
 
−
|
 
−
| One writes "f : A -> B" for "source f = A and target f = B".
 
−
| A graph is said to be 'small' if the classes of objects and
 
−
| arrows are sets.
 
  
−
Deductive System
+
<center><pre>
  
−
| A 'deductive system' is a graph in which to each object A there
+
o--------------o      source      o--------------o
−
| is associated an arrow 1_A : A -> A, the 'identity' arrow, and to
+
|             | ----------------> |              |
−
| each pair of arrows f : A -> B and g : B -> C there is associated
+
|   Arrows    |                  |   Objects    |
−
| an arrow gf : A -> C, the 'composition' of f with g.  A logician
+
|             | ----------------> |              |
−
| may think of the objects as 'formulas' and of the arrows as
+
o--------------o      target      o--------------o
−
| 'deductions' or 'proofs', hence of
 
−
|
 
−
| f : A -> B    g : B -> C
 
−
| ---------------------------
 
−
|        gf : A -> C
 
−
|
 
−
| as a 'rule of inference'.
 
  
−
Category
+
</pre></center>
  
−
| A 'category' is a deductive system in which the following equations hold,
+
<p>In graph theory the arrows are usually called ''oriented edges'' and the objects ''nodes'' or ''vertices'', but in various branches of mathematics other words may be used.  Instead of writing</p>
−
| for all f : A -> B, g : B -> C, and h : C -> D.
+
|-
 
|
 
|
−
| f 1_A  = f  =  1_B f,
+
::<p><math>\operatorname{source}(f) = A, \quad \operatorname{target}(f) =  B,</math></p>
 +
|-
 
|
 
|
−
| (hg)f  =  h(gf).
+
<p>one often writes <math>f : A \to B</math> or <math>A \xrightarrow{~f~} B.</math> We shall look at graphs with additional structure which are of interest in logic.</p>
−
 
 
−
Functor
 
  
−
| Definition 1.3.  A 'functor' F : $A$ -> $B$ is
+
<p>(Lambek & Scott, 47).</p>
−
| first of all a morphism of graphs (see Example C4),
+
|}
−
| that is, it sends objects of $A$ to objects of $B$
 
−
| and arrows of $A$ to arrows of $B$ such that, if
 
−
| f : A -> A', then F(f) : F(A) -> F(A').  Moreover,
 
−
| a functor preserves identities and composition;
 
−
| thus:
 
−
|
 
−
| F(1_A)  =  1_F(A),
 
−
|
 
−
| F(gf)  =  F(g)F(f).
 
−
|
 
−
| In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves
 
−
| objects and arrows unchanged and the composition of functors
 
−
| F : $A$ -> $B$ and G : $B$ -> $C$ is given by:
 
−
|
 
−
| (GF)(A)  =  G(F(A)),
 
−
|
 
−
| (GF)(f)  =  G(F(f)),
 
−
|
 
−
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
 
  
−
Natural Transformation
+
===Deductive System 2===
  
−
| Definition 2.1.  Given functors F, G : $A$ -> $B$,
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| a 'natural transformation' t : F -> G is a family
 
−
| of arrows t(A) : F(A) -> G(A) in $B$, one arrow for
 
−
| each object A of $A$, such that the following square
 
−
| commutes for all arrows f : A -> B in $A$:
 
 
|
 
|
−
|              t(A)
+
<p>A ''deductive system'' is a graph with a specified arrow</p>
−
| F(A) o------------------>o G(A)
+
|-
−
|      |                  |
 
−
|      |                  |
 
−
| F(f) |                  | G(f)
 
−
|      |                  |
 
−
|      v                  v
 
−
| F(B) o------------------>o G(B)
 
−
|              t(B)
 
 
|
 
|
−
| that is to say, such that
+
<p><math>\text{R1a.} \quad A ~\xrightarrow{~1_A~}~ A,</math></p>
 +
|-
 
|
 
|
−
| G(f)t(A)  =  t(B)F(f).
+
<p>and a binary operation on arrows (''composition'')
−
 
+
|-
−
Graph
 
−
 
 
−
| We recall (Part 0, Definition 1.2) that, for categories,
 
−
| a 'graph' consists of two classes and two mappings
 
−
| between them:
 
−
|
 
−
| o--------------o      source      o--------------o
 
−
| |              | ----------------> |              |
 
−
| |  Arrows    |                  |  Objects    |
 
−
| |              | ----------------> |              |
 
−
| o--------------o      target      o--------------o
 
−
|
 
−
| In graph theory the arrows are usually called "oriented edges"
 
−
| and the objects "nodes" or "vertices", but in various branches
 
−
| of mathematics other words may be used.  Instead of writing
 
 
|
 
|
−
| source(f)  =  A,
+
<p><math>\text{R1b.} \quad \dfrac{~ A ~\xrightarrow{~f~}~ B \quad B ~\xrightarrow{~g~}~ C ~}{A ~\xrightarrow{~gf~}~ C}.</math></p>
 +
|-
 
|
 
|
−
| target(f) =  B,
+
<p>(Lambek & Scott, 47).</p>
−
|                                  f
+
|}
−
| one often writes f : A -> B or A ---> B.  We shall
 
−
| look at graphs with additional structure which are
 
−
| of interest in logic.
 
  
−
Deductive System
+
===Conjunction Calculus===
  
−
| A 'deductive system' is a graph with a specified arrow
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 
|
 
|
−
|          1_A
+
<p>A ''conjunction calculus'' is a deductive system dealing with truth and conjunction.  Thus we assume that there is given a formula <math>\operatorname{T}</math> (&nbsp;=&nbsp;true) and a binary operation <math>\land</math> (&nbsp;=&nbsp;and) for forming the conjunction <math>A \land B</math> of two given formulas <math>A\!</math> and <math>B.\!</math>  Moreover, we specify the following additional arrows and rules of inference:</p>
−
| R1a.  A -----> A,
+
|-
 
|
 
|
−
| and a binary operation on arrows ('composition')
+
<p><math>\begin{array}{ll}
 +
\text{R2.}  & A ~\xrightarrow{~\bigcirc_A~}~ \operatorname{T};
 +
\\[8pt]
 +
\text{R3a.} & A \land B ~\xrightarrow{~\pi_{A, B}~}~ A,
 +
\\[8pt]
 +
\text{R3b.} & A \land B ~\xrightarrow{~\pi'_{A, B}~}~ B,
 +
\\[8pt]
 +
\text{R3c.} & \dfrac{~ C ~\xrightarrow{~f~}~ A \quad C ~\xrightarrow{~g~}~ B ~}{C ~\xrightarrow{~\langle f, g \rangle~}~ A \land B}.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
|          f          g
+
<p>(Lambek & Scott, 47&ndash;48).</p>
−
|        A ---> B    B ---> C
+
|}
−
| R1b.  ----------------------
 
−
|                 gf
 
−
|              A ----> C
 
  
−
Conjunction Calculus
+
===Positive Intuitionistic Propositional Calculus===
  
−
| A 'conjunction calculus' is a deductive system dealing with truth and
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| conjunction.  Thus we assume that there is given a formula 'T' (= true)
 
−
| and a binary operation '&' (= and) for forming the conjunction A & B of
 
−
| two given formulas A and B.  Moreover, we specify the following additional
 
−
| arrows and rules of inference:
 
 
|
 
|
−
|          O_A
+
<p>A ''positive intuitionistic propositional calculus'' is a conjunction calculus with an additional binary operation <math>\Leftarrow</math> (&nbsp;=&nbsp;if). Thus, if <math>A\!</math> and <math>B\!</math> are formulas, so are <math>\operatorname{T},</math> <math>A \land B,</math> and <math>A \Leftarrow B.</math>  (Yes, most people write <math>B \Rightarrow A</math> instead.)  We also specify the following new arrow and rule of inference.</p>
−
| R2.   A -----> T,
+
|-
 
|
 
|
−
|              p1_A,B
+
<p><math>\begin{array}{ll}
−
| R3a.   A & B --------> A,
+
\text{R4a.} & (A \Leftarrow B) \land B ~\xrightarrow{~\varepsilon_{A, B}~}~ A,
 +
\\[8pt]
 +
\text{R4b.} & \dfrac{~ C \land B ~\xrightarrow{~h~}~ A ~}{~ C ~\xrightarrow{~h^*~}~ A \Leftarrow B ~}.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
|              p2_A,B
+
<p>(Lambek & Scott, 48&ndash;49).</p>
−
| R3b.  A & B --------> B,
+
|}
−
|
 
−
|          f          g
 
−
|        C ---> A    C ---> B
 
−
| R3c.  ----------------------.
 
−
|          <f, g>
 
−
|       C --------> A & B
 
  
−
Positive Intuitionistic Propositional Calculus
+
===Intuitionistic Propositional Calculus===
  
−
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| with an additional binary operation '<=' (= if).  Thus, if A and B are formulas,
 
−
| so are T, A & B, and A <= B.  (Yes, most people write B => A instead.)  We also
 
−
| specify the following new arrow and rule of inference:
 
 
|
 
|
−
|                    !e!_A,B
+
<p>An ''intuitionistic propositional calculus'' is more than a positive one;  it requires also falsehood and disjunction, that is, a formula <math>\bot</math> (&nbsp;=&nbsp;false) and an operation <math>\lor</math> (&nbsp;=&nbsp;or) on formulas, together with the following additional arrows:</p>
−
| R4a.  (A <= B) & B ---------> A,
+
|-
 
|
 
|
−
|              h
+
<p><math>\begin{array}{ll}
−
|        C & B ---> A
+
\text{R5.}  & \bot ~\xrightarrow{~\Box_A~}~ A;
−
| R4b. ----------------.
+
\\[8pt]
−
|          h*
+
\text{R6a.} & A ~\xrightarrow{~\kappa_{A, B}~}~ A \lor B,
−
|       C ----> A <= B
+
\\[8pt]
 +
\text{R6b.} & B ~\xrightarrow{~\kappa'_{A, B}~}~ A \lor B,
 +
\\[8pt]
 +
\text{R6c.} & (C \Leftarrow A) \land (C \Leftarrow B) ~\xrightarrow{~\zeta^C_{A, B}~}~ C \Leftarrow (A \lor B).
 +
\end{array}</math></p>
 +
|-
 
|
 
|
 +
<p>(Lambek & Scott, 49&ndash;50).</p>
 +
|}
  
−
Intuitionistic Propositional Calculus
+
===Classical Propositional Calculus===
  
−
| An 'intuitionistic propositional calculus' is more than a
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| positive one;  it requires also falsehood and disjunction,
 
−
| that is, a formula 'F' (= false) and an operation 'v' (= or)
 
−
| on formulas, together with the following additional arrows:
 
 
|
 
|
−
|          []_A
+
<p>If we want ''classical'' propositional logic, we must also require:
−
| R5.    F ------> A,
+
|-
 
|
 
|
−
|          k1_A,B
+
<p><math>\begin{array}{ll}
−
| R6a.  A --------> A v B,
+
\text{R7.} & (\bot \Leftarrow (\bot \Leftarrow A)) \to A.
−
|
+
\end{array}</math></p>
−
|          k2_A,B
+
|-
−
| R6b.  B --------> A v B,
 
−
|
 
−
|                            !z!^C_A,B
 
−
| R6c. (C <= A) & (C <= B) -----------> C <= (A v B).
 
−
 
 
−
Classical Propositional Calculus
 
−
 
 
−
| If we want 'classical' propositional logic, we must also require:
 
 
|
 
|
−
| R7.  F <= (F <= A) -> A.
+
<p>(Lambek & Scott, 50).</p>
 +
|}
  
−
Category
+
===Category 2===
  
−
| A 'category' is a deductive system in which
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| the following equations hold between proofs:
 
−
|
 
−
| E1.  f 1_A  = f,
 
 
|
 
|
−
|     1_B f  =  f,
+
<p>A ''category'' is a deductive system in which the following equations hold between proofs:</p>
 +
|-
 
|
 
|
−
|      (hg)f = h(gf),
+
<p><math>\begin{array}{ll}
 +
\text{E1.} & f 1_A = f, \qquad 1_B f = f, \qquad (hg)f = h(gf),
 +
\\[8pt]
 +
& \text{for all}~ f : A \to B, \quad g : B \to C, \quad h : C \to D.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| for all f : A -> B, g : B -> C, h : C -> D.
+
<p>(Lambek & Scott, 52).</p>
 +
|}
  
−
Cartesian Category
+
===Cartesian Category===
  
−
| A 'cartesian category' is both a category
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| and a conjunction calculus satisfying the
 
−
| additional equations:
 
−
|
 
−
| E2.  f  = O_A,  for all f : A -> T.
 
−
|
 
−
| E3a.  p1_A,B <f, g>  =  f,
 
 
|
 
|
−
| E3b.  p2_A,B <f, g> =  g,
+
<p>A ''cartesian category'' is both a category and a conjunction calculus satisfying the additional equations:</p>
 +
|-
 
|
 
|
−
| E3c. <p1_A,B h, p2_A,B h>  = h,
+
<p><math>\begin{array}{ll}
 +
\text{E2.}  & f = \bigcirc_A, \quad \text{for all}~ f : A \to \operatorname{T};
 +
\\[8pt]
 +
\text{E3a.} & \pi^{}_{A,B} \langle f, g \rangle = f,
 +
\\[8pt]
 +
\text{E3b.} & \pi^\prime_{A,B} \langle f, g \rangle = g,
 +
\\[8pt]
 +
\text{E3c.} & \langle \pi^{}_{A,B} h, \pi^\prime_{A,B} h \rangle = h,
 +
\\[8pt]
 +
& \text{for all}~ f : C \to A, \quad g : C \to B, \quad h : C \to A \land B.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| for all f : C -> A, g : C -> B, h : C -> A & B.
+
<p>(Lambek & Scott, 52).</p>
 +
|}
  
−
Cartesian Closed Category
+
===Cartesian Closed Category===
  
−
| A 'cartesian closed category' is a cartesian category $A$ with
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| additional structure R4 satisfying the additional equations:
 
−
|
 
−
| E4a.  !e!_A,B <h* p1_C,B, p2_C,B>   =  h,
 
 
|
 
|
−
| E4b.  (!e!_A,B <k  p1_C,B, p2_C,B>)*  =  k,
+
<p>A ''cartesian closed category'' is a cartesian category <math>\mathcal{A}</math> with additional structure <math>\text{R4}\!</math> satisfying the additional equations:</p>
 +
|-
 
|
 
|
−
| for all h : C & B -> A,  k : C -> (A <= B).
+
<p><math>\begin{array}{ll}
 +
\text{E4a.} & \varepsilon^{}_{A,B} \langle h^* \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle = h,
 +
\\[8pt]
 +
\text{E4b.} & (\varepsilon^{}_{A,B} \langle k \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle)^* = k,
 +
\\[8pt]
 +
& \text{for all}~ h : C \land B \to A \quad \text{and} \quad k : C \to (A \Leftarrow B).
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| Thus, a cartesian closed category is
+
<p>Thus, a cartesian closed category is a positive intuitionistic propositional calculus satisfying the equations <math>\text{E1}\!</math> to <math>\text{E4}.\!</math>  This illustrates the general principle that one may obtain interesting categories from deductive systems by imposing an appropriate equivalence relation on proofs.</p>
−
| a positive intuitionistic propositional
 
−
| calculus satisfying the equations E1 to E4.
 
−
| This illustrates the general principle that
 
−
| one may obtain interesting categories from
 
−
| deductive systems by imposing an appropriate
 
−
| equivalence relation on proofs.
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
 
 
−
PAT.  Propositions As Types -- 2004
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
<p>(Lambek & Scott, 53).</p>
 +
|}
  
−
PAT.  Propositions As Types A
+
==Document History==
  
−
Inquiry List
+
===Inquiry List, Series A : Jun&ndash;Jul 2004===
  
−
00.  http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
+
* http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
−
00.  http://stderr.org/pipermail/inquiry/2004-July/thread.html#1677
+
* http://stderr.org/pipermail/inquiry/2004-July/thread.html#1677
 +
# http://stderr.org/pipermail/inquiry/2004-June/001643.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001644.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001645.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001660.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001648.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001649.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001656.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001657.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001658.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001659.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001661.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001662.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001664.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001665.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001666.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001667.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001668.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001670.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001671.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001672.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001673.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001674.html
 +
# http://stderr.org/pipermail/inquiry/2004-July/001677.html
  
−
01.  http://stderr.org/pipermail/inquiry/2004-June/001643.html
+
===Inquiry List, Series B : Jun&ndash;Jul 2004===
−
02.  http://stderr.org/pipermail/inquiry/2004-June/001644.html
 
−
03.  http://stderr.org/pipermail/inquiry/2004-June/001645.html
 
−
04.  http://stderr.org/pipermail/inquiry/2004-June/001660.html
 
−
05.  http://stderr.org/pipermail/inquiry/2004-June/001648.html
 
−
06.  http://stderr.org/pipermail/inquiry/2004-June/001649.html
 
−
07.  http://stderr.org/pipermail/inquiry/2004-June/001656.html
 
−
08.  http://stderr.org/pipermail/inquiry/2004-June/001657.html
 
−
09.  http://stderr.org/pipermail/inquiry/2004-June/001658.html
 
−
10.  http://stderr.org/pipermail/inquiry/2004-June/001659.html
 
−
11.  http://stderr.org/pipermail/inquiry/2004-June/001661.html
 
−
12.  http://stderr.org/pipermail/inquiry/2004-June/001662.html
 
−
13.  http://stderr.org/pipermail/inquiry/2004-June/001664.html
 
−
14.  http://stderr.org/pipermail/inquiry/2004-June/001665.html
 
−
15.  http://stderr.org/pipermail/inquiry/2004-June/001666.html
 
−
16.  http://stderr.org/pipermail/inquiry/2004-June/001667.html
 
−
17.  http://stderr.org/pipermail/inquiry/2004-June/001668.html
 
−
18.  http://stderr.org/pipermail/inquiry/2004-June/001670.html
 
−
19.  http://stderr.org/pipermail/inquiry/2004-June/001671.html
 
−
20.  http://stderr.org/pipermail/inquiry/2004-June/001672.html
 
−
21.  http://stderr.org/pipermail/inquiry/2004-June/001673.html
 
−
22.  http://stderr.org/pipermail/inquiry/2004-June/001674.html
 
−
23.  http://stderr.org/pipermail/inquiry/2004-July/001677.html
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
* http://stderr.org/pipermail/inquiry/2004-June/thread.html#1647
 +
* http://stderr.org/pipermail/inquiry/2004-July/thread.html#1684
 +
# http://stderr.org/pipermail/inquiry/2004-June/001647.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001663.html
 +
# http://stderr.org/pipermail/inquiry/2004-June/001669.html
 +
# http://stderr.org/pipermail/inquiry/2004-July/001684.html
  
−
PAT.  Propositions As Types B
+
===NKS Forum===
  
−
Inquiry List
+
* http://forum.wolframscience.com/archive/topic/490-1.html
 +
* http://forum.wolframscience.com/showthread.php?threadid=490
 +
* http://forum.wolframscience.com/printthread.php?threadid=490&perpage=4
 +
# http://forum.wolframscience.com/showthread.php?postid=1517#post1517
 +
# http://forum.wolframscience.com/showthread.php?postid=1548#post1548
 +
# http://forum.wolframscience.com/showthread.php?postid=1550#post1550
 +
# http://forum.wolframscience.com/showthread.php?postid=1590#post1590
  
−
00.  http://stderr.org/pipermail/inquiry/2004-June/thread.html#1647
+
===Inquiry List : Jul 2005===
−
00.  http://stderr.org/pipermail/inquiry/2004-July/thread.html#1684
 
  
−
01. http://stderr.org/pipermail/inquiry/2004-June/001647.html
+
* http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872
−
02. http://stderr.org/pipermail/inquiry/2004-June/001663.html
+
# http://stderr.org/pipermail/inquiry/2005-July/002872.html
−
03. http://stderr.org/pipermail/inquiry/2004-June/001669.html
+
# http://stderr.org/pipermail/inquiry/2005-July/002873.html
−
04. http://stderr.org/pipermail/inquiry/2004-July/001684.html
+
# http://stderr.org/pipermail/inquiry/2005-July/002874.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002875.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002876.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002877.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002878.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002879.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002880.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002881.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002882.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002883.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002884.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002885.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002886.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002887.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002888.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002889.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002890.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002891.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002892.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002893.html
 +
# http://stderr.org/pipermail/inquiry/2005-July/002894.html
  
−
NKS Forum
+
===Inquiry List, Commentary : Jul 2005===
  
−
00.  http://forum.wolframscience.com/showthread.php?threadid=490
+
* http://stderr.org/pipermail/inquiry/2005-July/thread.html#2895
−
01.  http://forum.wolframscience.com/showthread.php?postid=1517#post1517
+
# http://stderr.org/pipermail/inquiry/2005-July/002895.html
−
02.  http://forum.wolframscience.com/showthread.php?postid=1548#post1548
+
# http://stderr.org/pipermail/inquiry/2005-July/002896.html
−
03.  http://forum.wolframscience.com/showthread.php?postid=1550#post1550
 
−
04.  http://forum.wolframscience.com/showthread.php?postid=1590#post1590
 
  
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
[[Category:Combinator Calculus]]
−
 
+
[[Category:Combinatory Logic]]
−
PAT.  Propositions As Types -- 2005
+
[[Category:Computer Science]]
−
 
+
[[Category:Graph Theory]]
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
[[Category:Lambda Calculus]]
−
 
+
[[Category:Logic]]
−
PAT.  Propositions As Types
+
[[Category:Logical Graphs]]
−
 
+
[[Category:Mathematics]]
−
00.  http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872
+
[[Category:Programming Languages]]
−
01.  http://stderr.org/pipermail/inquiry/2005-July/002872.html
+
[[Category:Type Theory]]
−
02.  http://stderr.org/pipermail/inquiry/2005-July/002873.html
 
−
03.  http://stderr.org/pipermail/inquiry/2005-July/002874.html
 
−
04.  http://stderr.org/pipermail/inquiry/2005-July/002875.html
 
−
05.  http://stderr.org/pipermail/inquiry/2005-July/002876.html
 
−
06.  http://stderr.org/pipermail/inquiry/2005-July/002877.html
 
−
07.  http://stderr.org/pipermail/inquiry/2005-July/002878.html
 
−
08.  http://stderr.org/pipermail/inquiry/2005-July/002879.html
 
−
09.  http://stderr.org/pipermail/inquiry/2005-July/002880.html
 
−
10.  http://stderr.org/pipermail/inquiry/2005-July/002881.html
 
−
11.  http://stderr.org/pipermail/inquiry/2005-July/002882.html
 
−
12.  http://stderr.org/pipermail/inquiry/2005-July/002883.html
 
−
13.  http://stderr.org/pipermail/inquiry/2005-July/002884.html
 
−
14.  http://stderr.org/pipermail/inquiry/2005-July/002885.html
 
−
15.  http://stderr.org/pipermail/inquiry/2005-July/002886.html
 
−
16.  http://stderr.org/pipermail/inquiry/2005-July/002887.html
 
−
17.  http://stderr.org/pipermail/inquiry/2005-July/002888.html
 
−
18.  http://stderr.org/pipermail/inquiry/2005-July/002889.html
 
−
19.  http://stderr.org/pipermail/inquiry/2005-July/002890.html
 
−
20.  http://stderr.org/pipermail/inquiry/2005-July/002891.html
 
−
21.  http://stderr.org/pipermail/inquiry/2005-July/002892.html
 
−
22.  http://stderr.org/pipermail/inquiry/2005-July/002893.html
 
−
23.  http://stderr.org/pipermail/inquiry/2005-July/002894.html
 
−
 
 
−
PAT.  Propositions As Types -- Commentary
 
−
 
 
−
00.  http://stderr.org/pipermail/inquiry/2005-July/thread.html#2895
 
−
01.  http://stderr.org/pipermail/inquiry/2005-July/002895.html
 
−
02.  http://stderr.org/pipermail/inquiry/2005-July/002896.html
 
−
03.
 
−
 
 
−
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
−
</pre>
 

Latest revision as of 23:54, 6 July 2013


NB. In this discussion, combinators are being applied on the right of their arguments. The resulting formulas will look backwards to people who are accustomed to applying combinators on the left.

Identity, or the Identifier

Step 1

Consider the following problem requirements:

One is given a syntactic specification of the following form:

\(\begin{matrix}x & = & x\operatorname{I}\end{matrix}\)

In effect, this specification amounts to a so-called paraphrastic definition of the operator \(\operatorname{I},\) one in which the syntactic frame \(^{\backprime\backprime} x = x \underline{~~~} \, ^{\prime\prime}\) may be regarded as the defining context, or definiens, and \(\operatorname{I}\) is regarded as the object to be defined, or definiendum.

One is asked to find a pure interpretant for \(\operatorname{I},\) that is, an equivalent term in \(\langle \operatorname{K}, \operatorname{S} \rangle,\) the combinatory algebra generated by \(\operatorname{K}\) and \(\operatorname{S},\) that does as \(\operatorname{I}\) does.

A handle on the problem can be gotten by observing the following relationships:

\(\begin{array}{ccccc} x & = & (x\operatorname{K})(x\operatorname{K}) & = & x(\operatorname{K}(\operatorname{K}\operatorname{S})) \\[8pt] & & \Downarrow \\[8pt] \operatorname{I} & & = & & \operatorname{K}(\operatorname{K}\operatorname{S}) \end{array}\)

Thus the sequence of operations indicated by \(\operatorname{K}(\operatorname{K}\operatorname{S})\) is a \(\langle \operatorname{K}, \operatorname{S} \rangle\) proxy for \(\operatorname{I}.\)

Step 2

Assign types in the following specification:

\(\begin{matrix}x_A & = & x_A \operatorname{I}_{A \Rightarrow A}\end{matrix}\)

A suitable type assignment provides a propositional typing for \(\operatorname{I} : A \Rightarrow A,\) whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

Step 3 (Optional)

Check that \(A \Rightarrow A\) is a theorem of classical propositional calculus. 

   A   A
   o---o       o---o
   |           |
   @     =     @     =     @

Check.

Step 4

Term Development : Contextual Definition \(\rightsquigarrow\) Combinator Construction

Consider the parse tree of the term \(\operatorname{I}\) in terms of the primitive combinators \(\operatorname{K}\) and \(\operatorname{S},\) that is, the articulation or construction corresponding to the term equation \(\operatorname{I} = (\operatorname{K}(\operatorname{K}\operatorname{S})),\) as shown here: 

          K   S
          o   o
        K  \ /
        o  (o)
         \ /
   I  =  (o)

Adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of \(\operatorname{I} : A \Rightarrow A.\) Thus, the construal or construction of \(\operatorname{I}\) as \(\operatorname{K}(\operatorname{K}\operatorname{S})\) constitutes a hint or clue to the proof of \(A \Rightarrow A\) in the intuitionistic propositional calculus. Although guesswork may succeed in easy cases such as this, a more systematic procedure is to follow the development in Step 1, that takes us from contextual specification to operational algorithm, and to carry along the type information as we go, ending up with a typed parse tree for \(\operatorname{I},\) tantamount to a proof tree for \(A \Rightarrow A.\) 

o-----------------------------------------------------------o
|                                                           |
|                   x                                       |
|                  (o)A                                     |
|                                                           |
o===========================================================o
|                                                           |
|      x     K             x     K                          |
|      o A   o A=>(B=>A)   o A   o A=>((B=>A)=>A)           |
|       \   /               \   /                           |
|        \ /                 \ /                            |
|        (o)B=>A             (o)(B=>A)=>A                   |
|          \                 /                              |
|           \               /                               |
|            \             /                                |
|             \           /                                 |
|              \         /                                  |
|               \       /                                   |
|                \     /                                    |
|                 \   /                                     |
|                  \ /                                      |
|                  (o)A                                     |
|                                                           |
o===========================================================o
|                                                           |
|                    K                 S                    |
|                    o A=>((B=>A)=>A)  o A=>((B=>A)=>A)     |
|                     \               /       =>            |
|                      \             / (A=>(B=>A))=>(A=>A)  |
|                       \           /                       |
|                        \         /                        |
|                         \       /                         |
|                          \     /                          |
|                           \   /                           |
|               K            \ /                            |
|               o A=>(B=>A)  (o)(A=>(B=>A))=>(A=>A)         |
|                \           /                              |
|                 \         /                               |
|                  \       /                                |
|                   \     /                                 |
|                    \   /                                  |
|                x    \ /                                   |
|                o A  (o)A=>A                               |
|                 \   /                                     |
|                  \ /                                      |
|                  (o)A                                     |
|                                                           |
o-----------------------------------------------------------o

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. 

o-----------------------------------------------------------o
|                                                           |
|             B   A          B   A                          |
|             o---o          o---o                          |
|             |              |                              |
|             |   A      A   |          A x   A xI          |
|             o---o      o---o          o-----o             |
|             |          |              |                   |
|         A   |          | K            | K(KS) = I         |
|         o---o          o--------------o                   |
|         |              |                                  |
|         | K            | KS                               |
|         o--------------o                                  |
|         |                                                 |
|         | S                                               |
|         @                                                 |
|                                                           |
o===========================================================o
|                                                           |
|                                        B     A            |
|                                        o-----o            |
|                                        |                  |
|               B     A                  | xK  A            |
|               o-----o     ............[1]---[o](xK)(xK)   |
|               |           .            |                  |
|         A x   | xK        .      A x   | xK               |
|         o----[1]...........      o-----o                  |
|         |                        |                        |
|         | K                      | K                      |
|         @                        @                        |
|                                                           |
o===========================================================o
|                                                           |
|         A                                                 |
|         @ x                                               |
|                                                           |
o-----------------------------------------------------------o

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:

  • The nodes that are right-labeled \((\operatorname{K}, \operatorname{K}\operatorname{S}, \operatorname{K}(\operatorname{K}\operatorname{S})),\) in that order, constitute an application triple.
  • The type of the applicand \(\operatorname{K}\) is \(A \Rightarrow (B \Rightarrow A).\)
  • The type of the applicator \(\operatorname{K}\operatorname{S}\) is \((A \Rightarrow (B \Rightarrow A)) \Rightarrow (A \Rightarrow A).\)
  • Therefore, the type of the application \(\operatorname{K}(\operatorname{K}\operatorname{S})\) is \(A \Rightarrow A.\)

Composition, or the Composer

Step 1

We are given a specification of the composition combinator, or the composer \(\operatorname{P},\) in terms of the following effects:

\(\begin{matrix}x(y(z\operatorname{P})) & = & (xy)z\end{matrix}\)

We are asked to find an explication of \(\operatorname{P}\) in terms of primitive combinators.

Proceed as follows:

\(\begin{array}{ccccc} (xy)z & = & (xy)(x(z\operatorname{K})) & = & x(y((z\operatorname{K})\operatorname{S})) \\[8pt] (z\operatorname{K})\operatorname{S} & = & (z\operatorname{K})(z(\operatorname{S}\operatorname{K})) & = & z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})) \\[6pt] & & \Downarrow \\[8pt] x(y(z\operatorname{P})) & = & (xy)z & = & x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})))) \\[8pt] & & \Downarrow \\[8pt] \operatorname{P} & & = & & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})) \end{array}\)

Step 2

Assign types in the following specification:

\(\begin{array}{l} ((x \overset{ }{\underset{A}{\Downarrow}} ~ y \overset{A}{\underset{B}{\Downarrow}} ) \overset{ }{\underset{B}{\Downarrow}} ~ z \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{A}{\underset{B}{\Downarrow}} ~ (z \overset{B}{\underset{C}{\Downarrow}} ~ P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Here, a notation of the form \(x \underset{A}{\Downarrow}\) means that \(x\!\) is of the type \(A,\!\) while a notation of the form \(x \overset{A}{\underset{B}{\Downarrow}}\) means that \(x\!\) is of the type \(A \Rightarrow B.\)

Note that the explication of \(\operatorname{P}\) as a term \(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})\) of type \((B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))\) serves as a clue to the proof of \(\operatorname{P}'\text{s}\) type proposition as a theorem of the intuitionistic propositional calculus, that is, using only the following two combinator axioms:

\(\begin{array}{l} \operatorname{K} : A \Rightarrow (B \Rightarrow A) \\ \\ \operatorname{S} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C)) \end{array}\)

Step 3 (Optional)

Check that the propositional type of the composer \(\operatorname{P}\) is a theorem of classical propositional calculus, which is logically necessary to its being a theorem of intuitionistic propositional calculus, but easier to check. 

o-------------------------------------------------o
|                                                 |
|                                                 |
|                   A   B     A   C               |
|                   o---o     o---o               |
|                   |         |                   |
|         B   C     |         |                   |
|         o---o     o---------o                   |
|         |         |                             |
|         |         |                             |
|         o---------o                             |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     B   C   A   B                               |
|     o---o   o---o                               |
|      \     /                                    |
|       \   /                                     |
|        \ /                                      |
|       A o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     B   C       B                               |
|     o---o   o---o                               |
|      \     /                                    |
|       \   /                                     |
|        \ /                                      |
|       A o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|       B o---o C                                 |
|         |                                       |
|         |                                       |
|      AB o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         o---o C                                 |
|         |                                       |
|         |                                       |
|      AB o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     ABC o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     ABC o---o                                   |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         o---o                                   |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         @                                       |
|                                                 |
o-------------------------------------------------o

QED.

Step 4

Repeat the development in Step 1, but this time articulating the type information as we go. 

o---------------------------------------------------------------------o
|                                                                     |
|           x       y A                                               |
|           o A     o===>                                             |
|            \     /  B                                               |
|             \   /                                                   |
|              \ /      z B                                           |
|              (o)B     o===>                                         |
|                \     /  C                                           |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|                        B  z       K  B=>C                           |
|                       ===>o       o===========>                     |
|                        C   \     /   A=>(B=>C)                      |
|                             \   /                                   |
|       x       y A     x      \ / A                                  |
|       o A     o===>   o A    (o)=====>                              |
|        \     /  B      \     /   B=>C                               |
|         \   /           \   /                                       |
|          \ /             \ / B                                      |
|          (o)B            (o)===>                                    |
|            \             /   C                                      |
|             \           /                                           |
|              \         /                                            |
|               \       /                                             |
|                \     /                                              |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|             B  z       K  B=>C                                      |
|            ===>o       o===========>                                |
|             C   \     /   A=>(B=>C)                                 |
|                  \   /                                              |
|              A    \ /            S  A=>(B=>C)                       |
|             =====>(o)            o===============>                  |
|              B=>C   \           /  (A=>B)=>(A=>C)                   |
|                      \         /                                    |
|                       \       /                                     |
|                        \     /                                      |
|                         \   /                                       |
|                A  y      \ / A=>B                                   |
|               ===>o      (o)=====>                                  |
|                B   \     /   A=>C                                   |
|                     \   /                                           |
|               x      \ / A                                          |
|               o A    (o)===>                                        |
|                \     /   C                                          |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|                                        A=>(B=>C)                    |
|                                      ===============>               |
|          A=>(B=>C)     S           K  (A=>B)=>(A=>C)                |
|        ===============>o           o==============================> |
|         (A=>B)=>(A=>C)  \         /   (B=>C)                        |
|                          \       /   ===============>               |
|                           \     /     (A=>(B=>C))=>((A=>B)=>(A=>C)) |
|                            \   /                                    |
|  z B     K B=>C      z B    \ /  B=>C                               |
|  o===>C  o=========> o===>  (o)==============================>      |
|   \C    /  A=>(B=>C)  \C    /   (A=>(B=>C))=>((A=>B)=>(A=>C))       |
|    \   /               \   /                                        |
|     \ / A               \ / A=>(B=>C)                               |
|     (o)======>          (o)=============>                           |
|       \ B=>C            /  (A=>B)=>(A=>C)                           |
|        \               /                                            |
|         \             /                                             |
|          \           /                                              |
|           \         /                                               |
|            \       /                                                |
|             \     /                                                 |
|              \   /                                                  |
|     A  y      \ / A=>B                                              |
|    ===>o      (o)======>                                            |
|     B   \     /   A=>C                                              |
|          \   /                                                      |
|    x      \ / A                                                     |
|    o A    (o)===>                                                   |
|     \     /   C                                                     |
|      \   /                                                          |
|       \ /                                                           |
|       (o)C                                                          |
|                                                                     |
o=====================================================================o
|                                                                     |
|  A=>(B=>C)    S           K (A=>(B=>C))=>((A=>B)=>(A=>C))           |
| =============>o           o=======================================> |
| (A=>B)=>(A=>C) \         /  (B=>C)=>((A=>(B=>C))=>((A=>B)=>(A=>C))) |
|                 \       /                                           |
|                  \     /              B=>C                          |
|                   \   /             =========================>      |
|    B=>C            \ /            S  (A=>(B=>C))=>((A=>B)=>(A=>C))  |
| ==================>(o)            o===============================> |
|    A=>(B=>C)         \           /   (B=>C)=>(A=>(B=>C))            |
|  ===============>     \         /   =========================>      |
|   (A=>B)=>(A=>C)       \       /     (B=>C)=>((A=>B)=>(A=>C))       |
|                         \     /                                     |
|                          \   /                                      |
|    B=>C      K            \ / (B=>C)=>(A=>(B=>C))                   |
|   ==========>o            (o)=========================>             |
|    A=>(B=>C)  \           /   (B=>C)=>((A=>B)=>(A=>C))              |
|                \         /                                          |
|                 \       /                                           |
|                  \     /                                            |
|                   \   /                                             |
|          B  z      \ /  B=>C                                        |
|         ===>o      (o)===============>                              |
|          C   \     /   (A=>B)=>(A=>C)                               |
|               \   /                                                 |
|      A  y      \ / A=>B                                             |
|     ===>o      (o)=====>                                            |
|      B   \     /   A=>C                                             |
|           \   /                                                     |
|     x      \ / A                                                    |
|     o A    (o)===>                                                  |
|      \     /   C                                                    |
|       \   /                                                         |
|        \ /                                                          |
|        (o)C                                                         |
|                                                                     |
o---------------------------------------------------------------------o

The foregoing development has taken us from the typed parse tree for the definiens \(((xy)z)\!\) to the typed parse tree for the explicated definiendum \((x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))~))),\) which gives us both the construction of the composition combinator \(\operatorname{P}\) in terms of primitive combinators:

\(\begin{matrix}\operatorname{P} & = & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))\end{matrix}\)

and also the proof tree for the type proposition of \(\operatorname{P},\) as follows: 

        S   K
        o   o
         \ /  S
         (o)  o
        K  \ /
        o  (o)
         \ /
   P  =  (o)

\(\begin{matrix} \operatorname{P} & = & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})) & : & (B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C)) \end{matrix}\)

Step 5

Rewrite the final proof tree in existential graph format: 

o-----------------------------------------------------------o
|                                                           |
|                                       B  C  A  B  A  C    |
|                                       o--o  o--o  o--o    |
|                                       |     |     |       |
|            B  C  A  B  A  C        A  |     |     |       |
|            o--o  o--o  o--o        o--o     o-----o       |
|            |     |     |           |        |             |
|         A  |     |     |     B  C  |        |             |
|         o--o     o-----o     o--o  o--------o             |
|         |        |           |     |                      |
|         |        |           |     |                      |
|         o--------o           o-----o                      |
|         |                    |                            |
|         | S                  | SK                         |
|         o-------------------[1]                           |
|         |                                                 |
|         | K                                               |
|         @                                                 |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|                        B  C        A  B  A  C             |
|                        o--o        o--o  o--o             |
|                        |           |     |                |
|               B  C  A  |     B  C  |     |                |
|               o--o  o--o     o--o  o-----o                |
|               |     |        |     |                      |
|               |     |        |     |                      |
|               o-----o        o-----o                      |
|               |              |                            |
|               | K            | K((SK)S) = P               |
|               o-------------[o]                           |
|               |                                           |
|           SK  | (SK)S                                     |
|        [1]----o                                           |
|         |                                                 |
|         | S                                               |
|         @                                                 |
|                                                           |
o-----------------------------------------------------------o
Note on the graphic conventions used in the above style of diagram
Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, amounting in effect to Facts being recycled as Cases. Square brackets are also used to mark the intended result.

Self-Documentation : Developmental Data Structures

Observation.
Notice the "self-documenting" property of proof developments in the existential graph format, that is, the property of a developing structure that remembers its own history.

For example, the development of the Identity combinator:

\(\begin{matrix} x & = & (x\operatorname{K})(x\operatorname{K}) & = & x(\operatorname{K}(\operatorname{K}\operatorname{S})) \end{matrix}\) 

o-----------------------------------------------------------o
|                                                           |
|         A                                                 |
|         @                                                 |
|                                                           |
|        "1"                                                |
|                                                           |
o===========================================================o
|                                                           |
|                                        B     A            |
|                                        o-----o            |
|                                        |                  |
|               B     A                  |     A            |
|               o-----o     ............[o]----o            |
|               |           .            |                  |
|         A     |           .      A     |                  |
|         o----[o]...........      o-----o                  |
|         |                        |                        |
|         |                        |                        |
|         @                        @                        |
|                                                           |
|        "2"                      "3"                       |
|                                                           |
o===========================================================o
|                                                           |
|               B     A          B     A                    |
|               o-----o          o-----o                    |
|               |                |                          |
|               |     A    A     |          A     A         |
|               o-----o    o-----o         [1]----o         |
|               |          |                |               |
|         A     |          |                |               |
|         o-----o         [2]---------------o               |
|         |                |                                |
|         |                |                                |
|        [3]---------------o                                |
|         |                                                 |
|         |                                                 |
|         @                                                 |
|                                                           |
o-----------------------------------------------------------o

Redo the entire development of the Composer in existential graph format:

Step 5 (extended) 

o---------------------------------------------------------------------o
| Hypotheses:  x : A,  y : A=>B,  z : B=>C                            |
o---------------------------------------------------------------------o
|                                                                     |
| (xy)z                                                               |
|                                                                     |
|                        A   B xy            B   C (xy)z              |
|                       [1]-[2]             [2]-[3]                   |
|                        |                   |                        |
|    A x                 | y                 | z                      |
|   [1]                  @                   @                        |
|                                                                     |
o=====================================================================o
|                                                                     |
| (xy)(x(zK))                                                         |
|                                                                     |
|                B   C (xy)(x(zK))                                    |
|               [2]--o                                                |
|                |                                                    |
|    B  C    A   | x(zK)                                              |
|    o---o  [1]--o                                                    |
|    |       |                                                        |
|    | z     | zK                                                     |
|    o------[4]                                                       |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y((zK)S))                                                         |
|                                                                     |
|        B   C   A   B   A   C x(y((zK)S))                            |
|        o---o   o---o  [1]--o                                        |
|        |       |       |                                            |
|    A   |       | y     | y((zK)S)                                   |
|    o---o       o-------o                                            |
|    |           |                                                    |
|    | zK        | (zK)S                                              |
|   [4]----------o                                                    |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y((zK)(z(SK))))                                                   |
|                                                                     |
|                                  B  C  A  B  A  C x(y((zK)(z(SK)))) |
|                                  o--o  o--o [1]-o                   |
|                                  |     |     |                      |
|       B  C  A  B  A  C        A  |     | y   | y((zK)(z(SK)))       |
|       o--o  o--o  o--o        o--o     o-----o                      |
|       |     |     |           |        |                            |
|    A  |     |     |     B  C  | zK     | (zK)(z(SK))                |
|    o--o     o-----o     o--o [4]-------o                            |
|    |        |           |     |                                     |
|    |        |           | z   | z(SK)                               |
|    o--------o           o-----o                                     |
|    |                    |                                           |
|    | S                  | SK                                        |
|    o-------------------[5]                                          |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(z(K((SK)S))))                                                   |
|                                                                     |
|             B  C  A  B  A  C           B  C        A  B  A  C       |
|             o--o  o--o  o--o           o--o        o--o  o--o       |
|             |     |     |              |           |     |          |
|          A  |     |     |     B  C  A  |     B  C  |     |          |
|          o--o     o-----o     o--o  o--o     o--o  o-----o          |
|          |        |           |     |        |     |                |
|    B  C  |        |           |     |        |     |                |
|    o--o  o--------o           o-----o        o-----o                |
|    |     |                    |              |                      |
|    |     |                    | K            | K((SK)S) = P         |
|    o-----o                    o-------------[o]                     |
|    |                          |                                     |
|    | SK                       | (SK)S                               |
|   [5]-------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o

That's the sketch as best I can reconstruct it from my notes.

Triadic Analogy : Analogy Between Two Triadic Relations


o-------------------------------------------------o
|                                                 |
|   proof hint    :  proof       :  proposition   |
|                                                 |
o=================================================o
|                                                 |
|   untyped term  :  typed term  :  type          |
|                                                 |
o-------------------------------------------------o


Transposition, or the Transposer

Definition

\(\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}\)

This equation provides a contextual definition for the operator \(\operatorname{T},\) in effect, a formal syntactic specification that tells how the operator is required to act on other symbols.

Step 1

Construction

Find a pure interpretant for \(\operatorname{T},\) that is, an equivalent term doing the job of \(\operatorname{T}\) which is constructed purely in terms of the primitive combinators \(\operatorname{K}\) and \(\operatorname{S}.\)

Doing this yields an operational algorithm for \(\operatorname{T},\) understood as a sequence of manipulations on formal identifiers, or on symbols taken as objects in their own rights.

\(\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}\)

Observe that \(y(xz)\!\) matches \((xy)(xz)\!\) on the right, and that we can express \(y\!\) as \(x(y\operatorname{K}),\) consequently:

\(\begin{matrix} y(xz) & = & (x(y\operatorname{K}))(xz) \\[8pt] & = & x((y\operatorname{K})(z\operatorname{S})) \end{matrix}\)

thus completing the abstraction (or disentanglement) of x from the expression.

Working on the remainder of the expression, the next item of business is to abstract \(y.\!\)

Notice that:

\(\begin{matrix} (y\operatorname{K})(z\operatorname{S}) & = & (y\operatorname{K})(y((z\operatorname{S})\operatorname{K})) \\[8pt] & = & y(\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S})) \end{matrix}\)

thus completing the abstraction of \(y.\!\)

Next, work on \(\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S})\) to extract \(z,\!\) starting from the center \((z\operatorname{S})\operatorname{K}\) of the labyrinth and working outward:

\(\begin{matrix} (z\operatorname{S})\operatorname{K} & = & (z\operatorname{S})(z(\operatorname{K}\operatorname{K})) \\[8pt] & = & z(\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S})) \end{matrix}\)

For the sake of brevity in the rest of this development, rename the operator on the right so that \((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S})) = \operatorname{F}.\)

Continue with \(\operatorname{K}((z\operatorname{F})\operatorname{S}),\) to extract \(z,\!\) as follows:

\(\begin{matrix} (z\operatorname{F})\operatorname{S} & = & (z\operatorname{F})(z(\operatorname{S}\operatorname{K})) \\[8pt] & = & z(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) \end{matrix}\)

Rename the operator on the right, letting \((\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) = \operatorname{G}.\)

Continue with \(\operatorname{K}(z\operatorname{G}),\) to extract \(z,\!\) as follows:

\(\begin{matrix} \operatorname{K}(z\operatorname{G}) & = & (z(\operatorname{K}\operatorname{K}))(z\operatorname{G}) \\[8pt] & = & z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S})) \end{matrix}\)

Filling in the abbreviations:

\(\begin{array}{lll} y(xz) & = & x(y(z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S}))~)) \\[8pt] & = & x(y(z((\operatorname{K}\operatorname{K})((\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~)) \\[8pt] & = & x(y(z((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~)) \end{array}\)

Thus we have:

\(\begin{matrix} \operatorname{T} & = & (\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}) \end{matrix}\)

Step 2

Using the contextual definition of the transposer \(\operatorname{T},\)

\(\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}\)

find a minimal generic typing (simplest non-degenerate typing) of each term in the specification that makes all of the applications on each side of the equation go through.

For example, here is one such typing:

\(\begin{array}{l} (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

In a contextual, implicit, or paraphrastic definition of this sort, the definiendum is the symbol to be defined, in this case, \(^{\backprime\backprime} \operatorname{T} ^{\prime\prime},\) and the definiens is the entire rest of the context, in this case, the frame \(^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime},\) that ostensibly defines, or as one says, is supposed to define the symbol \(^{\backprime\backprime} \operatorname{T} ^{\prime\prime}\) that we find in its slot. More loosely speaking, the side of the equation with the more known symbols may be called its defining side.

In order to find a minimal generic typing, start with the defining side of the equation, freely assigning types in such a way that the successive applications make sense, but without introducing unnecessary complications or creating unduly specialized applications. Then work out what the type of the defined operator \(\operatorname{T}\) has to be, in order to function properly in the standard context, in this case, \(^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime}.\)

Again, this gives:

\(\begin{array}{l} (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Thus we have \(\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C)),\) whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

Step 3 (Optional)

At this juncture we might want to verify that the proposition corresponding to the type of \(\operatorname{T}\) is actually a theorem of classical propositional calculus. Since nothing can be a theorem of intuitionistic propositional calculus wihout also being a theorem of classical propositional calculus, this is a necessary condition of our work being correct up to this point. Although it is not a sufficient condition, classical theoremhood is easier to test and so provides a quick and useful check on our work.

In existential graph format, \(\operatorname{T}\) has the following generic typing: 

o-------------------------------------------------o
|                                                 |
|                B  C     A  C                    |
|                o--o     o--o                    |
|             A  |     B  |                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|         T : @                                   |
|                                                 |
o-------------------------------------------------o

And here is a classical logic proof of the type proposition: 

o-------------------------------------------------o
|                                                 |
|                B  C     A  C                    |
|                o--o     o--o                    |
|             A  |     B  |                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|            AB  C    AB  C                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|             X        X                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|             @                                   |
|                                                 |
o-------------------------------------------------o

Step 4

The construction of the term \(\operatorname{T}\) of the appropriate type in terms of the primitive typed combinators of the forms \(\operatorname{K}\) and \(\operatorname{S}\) is analogous to the proof of the corresponding proposition from the intuitionistic axiom schemes attached to those forms.

Incidentally, note the inobtrusive appearance of renaming strategies in the progress of this work. Renaming is the natural operation that substitution is the reverse of. With these humble beginnings we have reached a birthplace, a native ground, of the sign relation, an irreducible three-place relationship among what is indicated, what happens to indicate it, and all of the equivalent or associated indications we may find or create in reference to it.

For example, let the interposed interpretant \(^{\backprime\backprime} \operatorname{G} ^{\prime\prime}\) denote the supposed object, namely, whatever it is that the occurrent sign \(^{\backprime\backprime} (\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) ^{\prime\prime}\) denotes.

Consider the following data:

  • The parse tree for the term \(\operatorname{T} = ((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))\)
  • The type marker of the term \(\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C))\)
o-------------------------------------------------o
|                                                 |
|                K   K                            |
|                o   o                            |
|                 \ /  S   S   K                  |
|                 (o)  o   o   o                  |
|                S  \ /     \ /  S                |
|                o  (o)     (o)  o                |
|                 \ /         \ /                 |
|                 (o)         (o)                 |
|                   \         /                   |
|                    \       /                    |
|                     \     /                     |
|                      \   /                      |
|                K   K  \ /  S                    |
|                o   o  (o)  o                    |
|                 \ /     \ /                     |
|                 (o)     (o)                     |
|                   \     /                       |
|                    \   /                        |
|                     \ /                         |
|                     (o)                         |
|                                                 |
|           (A=>(B=>C))=>(B=>(A=>C))              |
|                                                 |
o-------------------------------------------------o

Can proofs be developed by tracing the stepwise articulation or explication of the untyped proof hint, typing each term as we go?

For example, we might begin as follows:

\(\begin{array}{l} (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ ((x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} ) \overset{A}{\underset{B}{\Downarrow}} ) \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ ((y \overset{ }{\underset{B}{\Downarrow}} ~ K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} ) \overset{A}{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ \ldots \end{array}\)

If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term.

Thus, these developments culminate in the rather striking and possibly disconcerting consequence that the apparent flow of information or reasoning in the proof tree is something of a put-up job, a snapshot likeness or a likely story that calls to mind the anatomy of a justification, but fails to reconstruct the true embryology or living physiology of discovery involved.

Repeat the development in Step 1, but this time articulating the type information as we go. 

o---------------------------------------------------------------------o
|                                                                     |
|                   x       z A                                       |
|                   o A     o======>                                  |
|                    \     /  B=>C                                    |
|                     \   /                                           |
|               y      \ / B                                          |
|               o B    (o)===>                                        |
|                \     /   C                                          |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|          y       K B                                                |
|          o B     o======>                                           |
|           \     /  A=>B                                             |
|            \   /                                                    |
|      x      \ / A      x       z A                                  |
|      o A    (o)===>    o A     o======>                             |
|       \     /   B       \     /  B=>C                               |
|        \   /             \   /                                      |
|         \ /               \ / B                                     |
|         (o)B              (o)===>                                   |
|           \               /   C                                     |
|            \             /                                          |
|             \           /                                           |
|              \         /                                            |
|               \       /                                             |
|                \     /                                              |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|        y         K B       z A       S A=>(B=>C)                    |
|        o B       o=====>   o=====>   o==============>               |
|         \       /  A=>B     \B=>C   / (A=>B)=>(A=>C)                |
|          \     /             \     /                                |
|           \   /               \   /                                 |
|            \ / A               \ / A=>B                             |
|            (o)===>             (o)=====>                            |
|              \ B               /   A=>C                             |
|               \               /                                     |
|                \             /                                      |
|                 \           /                                       |
|                  \         /                                        |
|                   \       /                                         |
|                    \     /                                          |
|                     \   /                                           |
|               x      \ / A                                          |
|               o A    (o)===>                                        |
|                \     /   C                                          |
|                 \   /                                               |
|                  \ /                                                |
|                  (o)C                                               |
|                                                                     |
o=====================================================================o
|                                                                     |
|                  A    z       S A=>(B=>C)                           |
|                 =====>o       o==============>                      |
|                  B=>C  \     / (A=>B)=>(A=>C)                       |
|                         \   /                                       |
|                     A=>B \ /      K (A=>B)=>(A=>C)                  |
|                    =====>(o)      o====================>            |
|                     B=>C   \     /  B=>((A=>B)=>(A=>C))             |
|                             \   /                                   |
|     y       K B       y      \ / B                                  |
|     o B     o=====>   o B    (o)==============>                     |
|      \     /  A=>B     \     /  (A=>B)=>(A=>C)                      |
|       \   /             \   /                                       |
|        \ / A             \ / A=>B                                   |
|        (o)===>           (o)=====>                                  |
|          \ B             /   A=>C                                   |
|           \             /                                           |
|            \           /                                            |
|             \         /                                             |
|              \       /                                              |
|               \     /                                               |
|                \   /                                                |
|          x      \ / A                                               |
|          o A    (o)===>                                             |
|           \     /   C                                               |
|            \   /                                                    |
|             \ /                                                     |
|             (o)C                                                    |
|                                                                     |
o=====================================================================o
|                                                                     |
|         A    z       S A=>(B=>C)                                    |
|        =====>o       o==============>                               |
|         B=>C  \     / (A=>B)=>(A=>C)                                |
|                \   /                                                |
|            A=>B \ /      K (A=>B)=>(A=>C)                           |
|           =====>(o)      o=====================>                    |
|            A=>C   \     /   B=>((A=>B)=>(A=>C))                     |
|                    \   /                                            |
|       B             \ /      S B=>((A=>B)=>(A=>C))                  |
|     ===============>(o)      o========================>             |
|      (A=>B)=>(A=>C)   \     / (B=>(A=>B))=>(B=>(A=>C))              |
|                        \   /                                        |
|             B    K      \ / B=>(A=>B)                               |
|            =====>o      (o)==========>                              |
|             A=>B  \     /   B=>(A=>C)                               |
|                    \   /                                            |
|              y      \ / B                                           |
|              o B    (o)=====>                                       |
|               \     /   A=>C                                        |
|                \   /                                                |
|          x      \ / A                                               |
|          o A    (o)===>                                             |
|           \     /   C                                               |
|            \   /                                                    |
|             \ /                                                     |
|             (o)C                                                    |
|                                                                     |
o=====================================================================o
|                                                                     |
|                                           (A=>B)=>(A=>C)            |
|                                          ======================>    |
|           (A=>B)=>(A=>C)       K       K   B=>((A=>B)=>(A=>C))      |
|          =====================>o       o=======================>    |
|            B=>((A=>B)=>(A=>C)) |      /    A=>(B=>C)                |
|                                |     /   ======================>    |
|   A    z   S  A=>(B=>C)        |    /      (A=>B)=>(A=>C)           |
|  =====>o   o===============>   |   /      =====================>    |
|   B=>C  \  | (A=>B)=>(A=>C)    |  /         B=>((A=>B)=>(A=>C))     |
|          \ |                   | /                                  |
|      A=>B \|       z A         |/ A=>(B=>C)                         |
|     =====>(o)      o=====>    (o)======================>            |
|      A=>C   \       \B=>C     /    (A=>B)=>(A=>C)                   |
|              \       \       /    =====================>            |
|               \       \     /       B=>((A=>B)=>(A=>C))             |
|                \       \   /                                        |
|                 \       \ /(A=>B)=>(A=>C)                           |
|                  \      (o)====================>                    |
|                   \     /   B=>((A=>B)=>(A=>C))                     |
|                    \   /                                            |
|       B             \ /      S  B=>((A=>B)=>(A=>C))                 |
|     ===============>(o)      o=========================>            |
|      (A=>B)=>(A=>C)   \     /  (B=>(A=>B))=>(B=>(A=>C))             |
|                        \   /                                        |
|             B    K      \ / B=>(A=>B)                               |
|            =====>o      (o)==========>                              |
|             A=>B  \     /   B=>(A=>C)                               |
|                    \   /                                            |
|              y      \ / B                                           |
|              o B    (o)=====>                                       |
|               \     /   A=>C                                        |
|                \   /                                                |
|          x      \ / A                                               |
|          o A    (o)===>                                             |
|           \     /   C                                               |
|            \   /                                                    |
|             \ /                                                     |
|             (o)C                                                    |
|                                                                     |
o=====================================================================o
|                                                                     |
|                    K       K    A=>(B=>C)                           |
|                    o       o   ======================>              |
|                     \     /      (A=>B)=>(A=>C)                     |
|                      \   /      =====================>              |
|   A=>(B=>C)           \ /    S    B=>((A=>B)=>(A=>C))               |
|  ====================>(o)    o===================================>  |
|    (A=>B)=>(A=>C)       \    |  (A=>(B=>C))=>((A=>B)=>(A=>C))       |
|   =====================> \   | ==================================>  |
|     B=>((A=>B)=>(A=>C))   \  |  (A=>(B=>C))=>(B=>((A=>B)=>(A=>C)))  |
|                            \ |                                      |
|        A=>(B=>C)     S      \| (A=>(B=>C))=>((A=>B)=>(A=>C))        |
|      ===============>o      (o)==================================>  |
|       (A=>B)=>(A=>C)  \     /  (A=>(B=>C))=>(B=>((A=>B)=>(A=>C)))   |
|                        \   /                                        |
|             A    z      \ / A=>(B=>C)                               |
|            =====>o      (o)====================>                    |
|             B=>C  \     /   B=>((A=>B)=>(A=>C))                     |
|                    \   /                                            |
|       B             \ /      S  B=>((A=>B)=>(A=>C))                 |
|     ===============>(o)      o=========================>            |
|      (A=>B)=>(A=>C)   \     /  (B=>(A=>B))=>(B=>(A=>C))             |
|                        \   /                                        |
|             B    K      \ / B=>(A=>B)                               |
|            =====>o      (o)==========>                              |
|             A=>B  \     /   B=>(A=>C)                               |
|                    \   /                                            |
|              y      \ / B                                           |
|              o B    (o)=====>                                       |
|               \     /   A=>C                                        |
|                \   /                                                |
|          x      \ / A                                               |
|          o A    (o)===>                                             |
|           \     /   C                                               |
|            \   /                                                    |
|             \ /                                                     |
|             (o)C                                                    |
|                                                                     |
o=====================================================================o
|                                                                     |
|                                          B=>((A=>B)=>(A=>C))        |
|                                        ==========================>  |
|    B=>((A=>B)=>(A=>C))     S         K  (B=>(A=>B))=>(B=>(A=>C))    |
|  =========================>o         o===========================>  |
|   (B=>(A=>B))=>(B=>(A=>C))  \        |   A=>(B=>C)                  |
|                              \       | ==========================>  |
|                    K   K      \      |    B=>((A=>B)=>(A=>C))       |
|                    o   o       \     |  =========================>  |
|                     \ /  S      \    |   (B=>(A=>B))=>(B=>(A=>C))   |
|                     (o)  o       \   |                              |
|                    S  \ /         \  |                              |
|                    o  (o)          \ |                              |
|           A    z    \ /   A    z    \|  A=>(B=>C)                   |
|          =====>o    (o)  =====>o    (o)==========================>  |
|           B=>C  \    |    B=>C  \    |    B=>((A=>B)=>(A=>C))       |
|                  \   |           \   |  =========================>  |
|                   \  |            \  |   (B=>(A=>B))=>(B=>(A=>C))   |
|                    \ |             \ |                              |
|       B             \|              \|  B=>((A=>B)=>(A=>C))         |
|     ===============>(o)             (o)========================>    |
|      (A=>B)=>(A=>C)   \             /  (B=>(A=>B))=>(B=>(A=>C))     |
|                        \           /                                |
|                         \         /                                 |
|                          \       /                                  |
|                           \     /                                   |
|                            \   /                                    |
|                 B    K      \ / B=>(A=>B)                           |
|                =====>o      (o)==========>                          |
|                 A=>B  \     /   B=>(A=>C)                           |
|                        \   /                                        |
|                  y      \ / B                                       |
|                  o B    (o)=====>                                   |
|                   \     /   A=>C                                    |
|                    \   /                                            |
|              x      \ / A                                           |
|              o A    (o)===>                                         |
|               \     /   C                                           |
|                \   /                                                |
|                 \ /                                                 |
|                 (o)C                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| Define the following abbreviations:                                 |
|                                                                     |
| L  =   M=>N                                                         |
|                                                                     |
| M  =   B=>((A=>B)=>(A=>C))                                          |
|                                                                     |
| N  =  (B=>(A=>B))=>(B=>(A=>C))                                      |
|                                                                     |
|                                                                     |
|                       S       K  L                                  |
|                       o L     o===============>                     |
|                        \     /  (A=>(B=>C))=>L                      |
|                         \   /                                       |
|                A=>(B=>C) \ /                S (A=>(B=>C))=>L        |
|               ==========>(o)                o================>      |
|                L           \               /   (A=>(B=>C))=>M       |
|                             \             /   ===============>      |
|                      K   K   \           /     (A=>(B=>C))=>N       |
|                       \ /  S  \         /                           |
|                       (o)  o   \       /                            |
|                      S  \ /     \     /                             |
|                      o  (o)      \   /                              |
|            A=>(B=>C)  \ /         \ / (A=>(B=>C))=>M                |
|           ===========>(o)         (o)===============>               |
|            M            \         /   (A=>(B=>C))=>N                |
|                          \       /                                  |
|                           \     /                                   |
|                            \   /                                    |
|                 A    z      \ / A=>(B=>C)                           |
|                =====>o      (o)========================>            |
|                 B=>C  \     /  (B=>(A=>B))=>(B=>(A=>C))             |
|                        \   /                                        |
|             B    K      \ / B=>(A=>B)                               |
|            =====>o      (o)==========>                              |
|             A=>B  \     /   B=>(A=>C)                               |
|                    \   /                                            |
|              y      \ / B                                           |
|              o B    (o)=====>                                       |
|               \     /   A=>C                                        |
|                \   /                                                |
|          x      \ / A                                               |
|          o A    (o)===>                                             |
|           \     /   C                                               |
|            \   /                                                    |
|             \ /                                                     |
|             (o)C                                                    |
|                                                                     |
o=====================================================================o
|                                                                     |
|                               K   K                                 |
|                               o   o                                 |
|                                \ /  S   S   K                       |
|                                (o)  o   o   o                       |
|                               S  \ /     \ /  S                     |
|                               o  (o)     (o)  o                     |
|   B    K     K B=>(A=>B)       \ /         \ /                      |
|  =====>o     o===========>     (o)         (o)                      |
|   A=>B  \    |  A=>(B=>C)        \         /                        |
|          \   | ==========>        \       /                         |
|           \  |  B=>(A=>B)          \     /                          |
|            \ |                      \   /                           |
|    A    z   \|  A=>(B=>C)   z A      \ / A=>(B=>C)                  |
|   =====>o   (o)==========>  o=====>  (o)========================>   |
|    B=>C  \   |  B=>(A=>B)    \B=>C   /  (B=>(A=>B))=>(B=>(A=>C))    |
|           \  |                \     /                               |
|            \ |                 \   /                                |
|        B    \|                  \ / B=>(A=>B)                       |
|       =====>(o)                 (o)==========>                      |
|        A=>B   \                 /   B=>(A=>C)                       |
|                \               /                                    |
|                 \             /                                     |
|                  \           /                                      |
|                   \         /                                       |
|                    \       /                                        |
|                     \     /                                         |
|                      \   /                                          |
|                y      \ / B                                         |
|                o B    (o)=====>                                     |
|                 \     /   A=>C                                      |
|                  \   /                                              |
|            x      \ / A                                             |
|            o A    (o)===>                                           |
|             \     /   C                                             |
|              \   /                                                  |
|               \ /                                                   |
|               (o)C                                                  |
|                                                                     |
o=====================================================================o
|                                                                     |
|                      K   K                                          |
|                      o   o                                          |
|                       \ /  S   S   K                                |
|                       (o)  o   o   o                                |
|                      S  \ /     \ /  S                              |
|                      o  (o)     (o)  o                              |
|                       \ /         \ /                               |
|                       (o)         (o)                               |
|                         \         /                                 |
|                          \       /                                  |
|                           \     /         A=>(B=>C)                 |
|                            \   /        =========================>  |
|     A=>(B=>C)               \ /       S  (B=>(A=>B))=>(B=>(A=>C))   |
|   =========================>(o)       o==========================>  |
|    (B=>(A=>B))=>(B=>(A=>C))  |       /   (A=>(B=>C))=>(B=>(A=>B))   |
|                              |      /   =========================>  |
|    B    K    K B=>(A=>B)     |     /     (A=>(B=>C))=>(B=>(A=>C))   |
|   =====>o    o===========>   |    /                                 |
|    A=>B  \   |  A=>(B=>C)    |   /                                  |
|           \  | ==========>   |  /                                   |
|            \ |  B=>(A=>B)    | /                                    |
|   A=>(B=>C) \|               |/ (A=>(B=>C))=>(B=>(A=>B))            |
|  ==========>(o)             (o)=========================>           |
|   B=>(A=>B)   \             /   (A=>(B=>C))=>(B=>(A=>C))            |
|                \           /                                        |
|                 \         /                                         |
|                  \       /                                          |
|                   \     /                                           |
|                    \   /                                            |
|         A    z      \T/ A=>(B=>C)                                   |
|        =====>o      (o)==========>                                  |
|         B=>C  \     /   B=>(A=>C)                                   |
|                \   /                                                |
|          y      \ / B                                               |
|          o B    (o)=====>                                           |
|           \     /   A=>C                                            |
|            \   /                                                    |
|      x      \ / A                                                   |
|      o A    (o)===>                                                 |
|       \     /   C                                                   |
|        \   /                                                        |
|         \ /                                                         |
|         (o)C                                                        |
|                                                                     |
o---------------------------------------------------------------------o

Step 5

Rewrite the final proof tree in existential graph format, implementing structure sharing among application triples by overlaying the type propositions that attach to terms. 

o---------------------------------------------------------------------o
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     |           |                |
|    o-----o     o--o           o--o     o-----------o                |
|    |           |              |        |                            |
|    |           |              |        |                            |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o-------------------------[1]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                             A  B  A  C              |
|                                             o--o  o--o              |
|                                             |     |                 |
|             B  C  A  B  A  C     B  C       |     |                 |
|             o--o  o--o  o--o     o--o       o-----o                 |
|             |     |     |        |          |                       |
|          A  |     |     |     A  |       B  |                       |
|          o--o     o-----o     o--o       o--o                       |
|          |        |           |          |                          |
|          |        |           |          |                          |
|          o--------o           o----------o                          |
|          |                    |                                     |
|          | S                  | S((KK)S)                            |
|          o-------------------[2]                                    |
|          |                                                          |
|      KK  | (KK)S                                                    |
|   [1]----o                                                          |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                           A  B  A  C   A  B   A  C  |
|                                           o--o  o--o   o--o   o--o  |
|                                           |     |      |      |     |
|       A  B  A  C   A  B   A  C            |     |   B  |   B  |     |
|       o--o  o--o   o--o   o--o            o-----o   o--o   o--o     |
|       |     |      |      |               |         |      |        |
|       |     |   B  |   B  |      B  C  B  |         |      |        |
|       o-----o   o--o   o--o      o--o  o--o         o------o        |
|       |         |      |         |     |            |               |
|    B  |         |      |      A  |     |            |               |
|    o--o         o------o      o--o     o------------o               |
|    |            |             |        |                            |
|    |            |             |        |                            |
|    o------------o             o--------o                            |
|    |                          |                                     |
|    | S                        | SK                                  |
|    o-------------------------[3]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                        A  B     A  C                |
|                                        o--o     o--o                |
|                                        |        |                   |
|                               B  C  B  |     B  |                   |
|                               o--o  o--o     o--o                   |
|                               |     |        |                      |
|                            A  |     |        |                      |
|                            o--o     o--------o                      |
|                            |        |                               |
|                            |        |                               |
|                            o--------o                               |
|                            |                                        |
|                  S((KK)S)  | (S((KK)S))((SK)S)                      |
|               [2]---------[4]                                       |
|                |                                                    |
|      SK        | (SK)S                                              |
|   [3]----------o                                                    |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                B  C     A  B                                        |
|                o--o     o--o                                        |
|                |        |                                           |
|       A  B  A  |     B  |                                           |
|       o--o  o--o     o--o                                           |
|       |     |        |                                              |
|    B  |     |        |                                              |
|    o--o     o--------o                                              |
|    |        |                                                       |
|    | K      | KK                                                    |
|    o-------[5]                                                      |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|    T  =  (KK)(((S((KK)S))((SK)S))S)                                 |
|                                                                     |
|                                                 B  C     A  C       |
|                                                 o--o     o--o       |
|                                                 |        |          |
|                                              A  |     B  |          |
|                                              o--o     o--o          |
|                                              |        |             |
|                                              |        |             |
|                                              o--------o             |
|                                              |                      |
|                           KK                 | T                    |
|                        [5]------------------[o]                     |
|                         |                                           |
|      (S((KK)S))((SK)S)  | ((S((KK)S))((SK)S))S                      |
|   [4]-------------------o                                           |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
Graphic Conventions
Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, tantamount to recycling Facts as Cases. Square brackets are also used to indicate the final result.

Step 5 (Extended)

Redo the development of the proof tree in existential graph format.

Each frame of the developmental scheme that follows is divided by a dotted line, with terms that contribute to the main term under development being shown above it and the main term itself being shown below it. 

o---------------------------------------------------------------------o
| Hypotheses:  x : A,  y : B,  z : A=>(B=>C)                          |
o---------------------------------------------------------------------o
|                                                                     |
| y(xz)                                                               |
|                                                                     |
|    A x                                                              |
|   [1]                                                               |
|                                                                     |
|    B y                                                              |
|   [2]                                                               |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|        B   C y(xz)                                                  |
|       [2]--o                                                        |
|        |                                                            |
|    A   | xz                                                         |
|   [1]--o                                                            |
|    |                                                                |
|    | z                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| (x(yK))(xz)                                                         |
|                                                                     |
|        A   B x(yK)                                                  |
|        o--[3]                                                       |
|        |                                                            |
|    B   | yK                                                         |
|    o---o                                                            |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|        B   C (x(yK))(xz)                                            |
|       [3]--o                                                        |
|        |                                                            |
|    A   | xz                                                         |
|    o---o                                                            |
|    |                                                                |
|    | z                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x((yK)(zS))                                                         |
|                                                                     |
|        A   B                                                        |
|        o---o                                                        |
|        |                                                            |
|    B   | yK                                                         |
|    o--[4]                                                           |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|        B   C   A   B   A   C x((yK)(zS))                            |
|        o---o   o---o   o---o                                        |
|        |       |       |                                            |
|    A   |       | yK    | (yK)(zS)                                   |
|    o---o      [4]------o                                            |
|    |           |                                                    |
|    | z         | zS                                                 |
|    o-----------o                                                    |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x((yK)(y((zS)K)))                                                   |
|                                                                     |
|        A   B                                                        |
|        o---o                                                        |
|        |                                                            |
|    B   | yK                                                         |
|    o--[4]                                                           |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
|        B   C   A   B   A   C                                        |
|        o---o   o---o   o---o                                        |
|        |       |       |                                            |
|    A   |       |       |                                            |
|    o---o       o-------o                                            |
|    |           |                                                    |
|    | z         | zS                                                 |
|    o----------[5]                                                   |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|                        A   B   A   C x((yK)(y((zS)K)))              |
|                        o---o   o---o                                |
|                        |       |                                    |
|    A   B   A   C       | yK    | (yK)(y((zS)K))                     |
|    o---o   o---o      [4]------o                                    |
|    |       |           |                                            |
|    |       |       B   | y((zS)K)                                   |
|    o-------o       o---o                                            |
|    |               |                                                |
|    | zS            | (zS)K                                          |
|   [5]--------------o                                                |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(K(((zS)K)S)))                                                   |
|                                                                     |
|        B   C   A   B   A   C                                        |
|        o---o   o---o   o---o                                        |
|        |       |       |                                            |
|    A   |       |       |                                            |
|    o---o       o-------o                                            |
|    |           |                                                    |
|    | z         | zS                                                 |
|    o----------[5]                                                   |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
|                        A   B   A   C                                |
|                        o---o   o---o                                |
|                        |       |                                    |
|    A   B   A   C       |       |                                    |
|    o---o   o---o       o-------o                                    |
|    |       |           |                                            |
|    |       |       B   |                                            |
|    o-------o       o---o                                            |
|    |               |                                                |
|    | zS            | (zS)K                                          |
|   [5]-------------[6]                                               |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|        A   B   A   C      A   B      A   C x(y(K(((zS)K)S)))        |
|        o---o   o---o      o---o      o---o                          |
|        |       |          |          |                              |
|        |       |      B   |      B   | y(K(((zS)K)S))               |
|        o-------o      o---o      o---o                              |
|        |              |          |                                  |
|    B   |              | K        | K(((zS)K)S)                      |
|    o---o              o----------o                                  |
|    |                  |                                             |
|    | (zS)K            | ((zS)K)S                                    |
|   [6]-----------------o                                             |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(K(((zS)(z(KK)))S)))                                             |
|                                                                     |
|       B  C  A  B  A  C                                              |
|       o--o  o--o  o--o                                              |
|       |     |     |                                                 |
|    A  |     |     |                                                 |
|    o--o     o-----o                                                 |
|    |        |                                                       |
|    | z      | zS                                                    |
|    o-------[5]                                                      |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     | zS        | (zS)(z(KK))    |
|    o-----o     o--o           o--o    [5]---------[7]               |
|    |           |              |        |                            |
|    |           |              | z      | z(KK)                      |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o--------------------------o                                     |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|       A  B  A  C      A  B      A  C                                |
|       o--o  o--o      o--o      o--o x(y(K(((zS)(z(KK)))S)))        |
|       |     |         |         |                                   |
|       |     |      B  |      B  | y(K(((zS)(z(KK)))S))              |
|       o-----o      o--o      o--o                                   |
|       |            |         |                                      |
|    B  |            | K       | K(((zS)(z(KK)))S)                    |
|    o--o            o---------o                                      |
|    |               |                                                |
|    | (zS)(z(KK))   | ((zS)(z(KK)))S                                 |
|   [7]--------------o                                                |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(K((z(S((KK)S)))S)))                                             |
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     |           |                |
|    o-----o     o--o           o--o     o-----------o                |
|    |           |              |        |                            |
|    |           |              |        |                            |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o-------------------------[8]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
|                      A B  A C                         A B  A C      |
|                      o-o  o-o                         o-o  o-o      |
|                      |    |                           |    |        |
|           A B  A C   |    |     B C  A B  A C   B C   |    |        |
|           o-o  o-o   o----o     o-o  o-o  o-o   o-o   o----o        |
|           |    |     |          |    |    |     |     |             |
|      B C  |    |   B |        A |    |    |   A |   B |             |
|      o-o  o----o   o-o        o-o    o----o   o-o   o-o             |
|      |    |        |          |      |        |     |               |
|    A |    |        |          |      |        | z   | z(S((KK)S))   |
|    o-o    o--------o          o------o        o----[9]              |
|    |      |                   |               |                     |
|    |      |                   | S             | S((KK)S)            |
|    o------o                   o---------------o                     |
|    |                          |                                     |
|    | KK                       | (KK)S                               |
|   [8]-------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|       A  B  A  C      A  B     A  C x(y(K((z(S((KK)S)))S)))         |
|       o--o  o--o      o--o     o--o                                 |
|       |     |         |        |                                    |
|       |     |      B  |     B  | y(K((z(S((KK)S)))S))               |
|       o-----o      o--o     o--o                                    |
|       |            |        |                                       |
|    B  |            | K      | K((z(S((KK)S)))S)                     |
|    o--o            o--------o                                       |
|    |               |                                                |
|    | z(S((KK)S))   | (z(S((KK)S)))S                                 |
|   [9]--------------o                                                |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(K((z(S((KK)S)))(z(SK)))))                                       |
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     |           |                |
|    o-----o     o--o           o--o     o-----------o                |
|    |           |              |        |                            |
|    |           |              |        |                            |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o-------------------------[8]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
|                      A B  A C                         A B  A C      |
|                      o-o  o-o                         o-o  o-o      |
|                      |    |                           |    |        |
|           A B  A C   |    |     B C  A B  A C   B C   |    |        |
|           o-o  o-o   o----o     o-o  o-o  o-o   o-o   o----o        |
|           |    |     |          |    |    |     |     |             |
|      B C  |    |   B |        A |    |    |   A |   B |             |
|      o-o  o----o   o-o        o-o    o----o   o-o   o-o             |
|      |    |        |          |      |        |     |               |
|    A |    |        |          |      |        | z   | z(S((KK)S))   |
|    o-o    o--------o          o------o        o----[9]              |
|    |      |                   |               |                     |
|    |      |                   | S             | S((KK)S)            |
|    o------o                   o---------------o                     |
|    |                          |                                     |
|    | KK                       | (KK)S                               |
|   [8]-------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|                                       x(y(K((z(S((KK)S)))(z(SK))))) |
|                                                 ^                   |
|                               A B A C  A B  A C |                   |
|                               o-o o-o  o-o  o-o                     |
|                               |   |    |    |                       |
|      A B A C  A B  A C        |   |  B |  B |                       |
|      o-o o-o  o-o  o-o        o---o  o-o  o-o                       |
|      |   |    |    |          |      |    |                         |
|      |   |  B |  B |    B C B |      | K  | K((z(S((KK)S)))(z(SK))) |
|      o---o  o-o  o-o    o-o o-o      o----o                         |
|      |      |    |      |   |        |                              |
|    B |      |    |    A |   |        | (z(S((KK)S)))(z(SK))         |
|    o-o      o----o    o-o  [9]-------o                              |
|    |        |         |     |                                       |
|    |        |         | z   | z(SK)                                 |
|    o--------o         o-----o                                       |
|    |                  |                                             |
|    | S                | SK                                          |
|    o------------------o                                             |
|    |                                                                |
|    | K                                                              |
|    @                       [9] = z(S((KK)S))                        |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(K(z((S((KK)S))((SK)S)))))                                       |
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     |           |                |
|    o-----o     o--o           o--o     o-----------o                |
|    |           |              |        |                            |
|    |           |              |        |                            |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o-------------------------[8]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
|                      A B  A C                         A B  A C      |
|                      o-o  o-o                         o-o  o-o      |
|                      |    |                           |    |        |
|           A B  A C   |    |     B C  A B  A C   B C   |    |        |
|           o-o  o-o   o----o     o-o  o-o  o-o   o-o   o----o        |
|           |    |     |          |    |    |     |     |             |
|      B C  |    |   B |        A |    |    |   A |   B |             |
|      o-o  o----o   o-o        o-o    o----o   o-o   o-o             |
|      |    |        |          |      |        |     |               |
|    A |    |        |          |      |        |     |               |
|    o-o    o--------o          o------o        o-----o               |
|    |      |                   |               |                     |
|    |      |                   | S             | S((KK)S)            |
|    o------o                   o-------------[10]                    |
|    |                          |                                     |
|    | KK                       | (KK)S                               |
|   [8]-------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
|                               A B A C  A B  A C                     |
|                               o-o o-o  o-o  o-o                     |
|                               |   |    |    |                       |
|      A B A C  A B  A C        |   |  B |  B |                       |
|      o-o o-o  o-o  o-o        o---o  o-o  o-o                       |
|      |   |    |    |          |      |    |                         |
|      |   |  B |  B |    B C B |      |    |                         |
|      o---o  o-o  o-o    o-o o-o      o----o                         |
|      |      |    |      |   |        |                              |
|    B |      |    |    A |   |        |                              |
|    o-o      o----o    o-o   o--------o                              |
|    |        |         |     |                                       |
|    |        |         |     |                                       |
|    o--------o         o-----o                                       |
|    |                  |                                             |
|    | S                | SK                                          |
|    o----------------[11]                                            |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|            A B A C  A B  A C     A B A C      A B  A C x(y(K(zG)))  |
|            o-o o-o  o-o  o-o     o-o o-o      o-o  o-o              |
|            |   |    |    |       |   |        |    |                |
|            |   |  B |  B |  B C  |   |  B C B |  B | y(K(zG))       |
|            o---o  o-o  o-o  o-o  o---o  o-o o-o  o-o                |
|            |      |    |    |    |      |   |    |                  |
|      B C B |      |    |  A |  B |    A |   | K  | K(zG)            |
|      o-o o-o      o----o  o-o  o-o    o-o   o----o                  |
|      |   |        |       |    |      |     |                       |
|    A |   |        |       |    |      | z   | zG                    |
|    o-o   o--------o       o----o      o-----o                       |
|    |     |                |           |                             |
|    |     |                | F         | G                           |
|    o-----o               [10]---------o                             |
|    |                      |                                         |
|    | SK                   | (SK)S                                   |
|   [11]--------------------o                                         |
|    |                                                                |
|    | S                      F = S((KK)S)                            |
|    @                        G = F((SK)S) = (S((KK)S))((SK)S)        |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y((z(KK))(z((S((KK)S))((SK)S)))))                                 |
|                                                                     |
|                    B   C       A   B                                |
|                    o---o       o---o                                |
|                    |           |                                    |
|        A   B   A   |       B   |                                    |
|        o---o   o---o       o---o                                    |
|        |       |           |                                        |
|    B   |       | z         | z(KK)                                  |
|    o---o       o---------[12]                                       |
|    |           |                                                    |
|    | K         | KK                                                 |
|    o-----------o                                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|                                                   x(y((z(KK))(zG))) |
|                                                        ^            |
|            A B A C  A B  A C     A B A C      A B  A C |            |
|            o-o o-o  o-o  o-o     o-o o-o      o-o  o-o              |
|            |   |    |    |       |   |        |    |                |
|            |   |  B |  B |  B C  |   |  B C B |  B | y((z(KK))(zG)) |
|            o---o  o-o  o-o  o-o  o---o  o-o o-o  o-o                |
|            |      |    |    |    |      |   |    |                  |
|      B C B |      |    |  A |  B |    A |   |    | (z(KK))(zG)      |
|      o-o o-o      o----o  o-o  o-o    o-o  [12]--o                  |
|      |   |        |       |    |      |     |                       |
|    A |   |        |       |    |      | z   | zG                    |
|    o-o   o--------o       o----o      o-----o                       |
|    |     |                |           |                             |
|    |     |                | F         | G                           |
|    o-----o                o-----------o                             |
|    |                      |                                         |
|    | SK                   | (SK)S                                   |
|    o----------------------o                                         |
|    |                                                                |
|    | S                      F = S((KK)S)                            |
|    @                        G = F((SK)S) = (S((KK)S))((SK)S)        |
|                                                                     |
o=====================================================================o
|                                                                     |
| x(y(z((KK)(((S((KK)S))((SK)S))S))))                                 |
|                                                                     |
|                    B   C       A   B                                |
|                    o---o       o---o                                |
|                    |           |                                    |
|        A   B   A   |       B   |                                    |
|        o---o   o---o       o---o                                    |
|        |       |           |                                        |
|    B   |       |           |                                        |
|    o---o       o-----------o                                        |
|    |           |                                                    |
|    | K         | KK                                                 |
|    o---------[13]                                                   |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
|            A B A C   A B   A C        A B A C         A B   A C     |
|            o-o o-o   o-o   o-o        o-o o-o         o-o   o-o     |
|            |   |     |     |          |   |           |     |       |
|            |   |   B |   B |    B C   |   |     B C B |   B |       |
|            o---o   o-o   o-o    o-o   o---o     o-o o-o   o-o       |
|            |       |     |      |     |         |   |     |         |
|      B C B |       |     |    A |   B |       A |   |     |         |
|      o-o o-o       o-----o    o-o   o-o       o-o   o-----o         |
|      |   |         |          |     |         |     |               |
|    A |   |         |          |     |         |     |               |
|    o-o   o---------o          o-----o         o-----o               |
|    |     |                    |               |                     |
|    |     |                    | S((KK)S)      | (S((KK)S))((SK)S)   |
|    o-----o                    o-------------[14]                    |
|    |                          |                                     |
|    | SK                       | (SK)S                               |
|    o--------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
|                                                                     |
|                A  B     A  C     B  C     A  B     B  C     A  C    |
|                o--o     o--o     o--o     o--o     o--o     o--o    |
|                |        |        |        |        |        |       |
|       B  C  B  |     B  |     A  |     B  |     A  |     B  |       |
|       o--o  o--o     o--o     o--o     o--o     o--o     o--o       |
|       |     |        |        |        |        |        |          |
|    A  |     |        |        |        |        |        |          |
|    o--o     o--------o        o--------o        o--------o          |
|    |        |                 |                 |                   |
|    |        |                 | KK              | T                 |
|    o--------o                [13]--------------[o]                  |
|    |                          |                                     |
|    | (S((KK)S))((SK)S)        | ((S((KK)S))((SK)S))S                |
|   [14]------------------------o                                     |
|    |                                                                |
|    | S                                                              |
|    @                            T = (KK)(((S((KK)S))((SK)S))S)      |
|                                                                     |
o---------------------------------------------------------------------o

Commentary

Commentary Note 1

I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time.

Observation 1
IF we know that the element \(x\!\) is of the type \(X\!\)
AND we know that the function \(f\!\) is of the type \(X \to Y\)
THEN we know that the element \(f(x)\!\) is of the type \(Y.\!\)

We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:

\(\begin{array}{l} x : X \\ \underline{f : X \to Y} \\ f(x) : Y \end{array}\)

In this scheme of inference, the notations \({}^{\backprime\backprime} x {}^{\prime\prime},\) \({}^{\backprime\backprime} f {}^{\prime\prime},\) and \({}^{\backprime\backprime} f(x) {}^{\prime\prime}\) are referred to as terms and interpreted as names of formal objects.

In the same context, the notations \({}^{\backprime\backprime} X {}^{\prime\prime},\) \({}^{\backprime\backprime} X \to Y {}^{\prime\prime},\) and \({}^{\backprime\backprime} Y {}^{\prime\prime}\) give us information, or indicate formal constraints, that we may think of as denoting the types of the formal objects under consideration. By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.

If a moment's spell of double vision leads us to see the functional arrow \({}^{\backprime\backprime} \to {}^{\prime\prime}\) as the logical arrow \({}^{\backprime\backprime} \Rightarrow {}^{\prime\prime}\) then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called modus ponens. And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of modus ponens.

Commentary Note 2

Notice that I am carrying out combinator applications "on the right", so the formulas might read backwards from what many people are used to.

Bibliography

Here are three references on combinatory logic and lambda calculus, given in order of difficulty from introductory to advanced, that are especially pertinent to the use of combinators in computer science:

  1. Smullyan, R. (1985), To Mock a Mockingbird, And Other Logic Puzzles, Including an Amazing Adventure in Combinatory Logic, Alfred A. Knopf, New York, NY.
  2. Hindley, J.R. and Seldin, J.P. (1986), Introduction to Combinators and \(\lambda\)-Calculus, London Mathematical Society Student Texts No. 1, Cambridge University Press, Cambridge, UK.
  3. Lambek, J. and Scott, P.J. (1986), Introduction To Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.

Basic Concepts from Lambek and Scott (1986)

Notes on basic concepts from Lambek and Scott (1986), Introduction To Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK. Excerpts and discussion on the Ontology List.

Here is a synopsis, exhibiting just the layering of axioms — notice the technique of starting over at the initial point several times and building up both more richness of detail and more generality of perspective with each passing time:

Concrete Category

Definition 1.1. A concrete category is a collection of two kinds of entities, called objects and morphisms. The former are sets which are endowed with some kind of structure, and the latter are mappings, that is, functions from one object to another, in some sense preserving that structure. Among the morphisms, there is attached to each object \(A\!\) the identity mapping \(1_A : A \to A\) such that \(1_A(a) = a\!\) for all \(a \in A.\!\) Moreover, morphisms \(f : A \to B\) and \(g : B \to C\) may be composed to produce a morphism \(gf : A \to C\) such that \((gf)(a) = g(f(a))\!\) for all \(a \in A.\!\)

We shall now progress from concrete categories to abstract ones, in three easy stages.

(Lambek & Scott, 4–5).

Graph

Definition 1.2. A graph (usually called a directed graph) consists of two classes: the class of arrows (or oriented edges) and the class of objects (usually called nodes or vertices) and two mappings from the class of arrows to the class of objects, called source and target (often also domain and codomain).


o--------------o      source       o--------------o
|              | ----------------> |              |
|   Arrows     |                   |   Objects    |
|              | ----------------> |              |
o--------------o      target       o--------------o

One writes \(^{\backprime\backprime} f : A \to B \, ^{\prime\prime}\) for \(^{\backprime\backprime} \operatorname{source}\ f = A ~\operatorname{and}~ \operatorname{target}\ f = B \, ^{\prime\prime}.\) A graph is said to be small if the classes of objects and arrows are sets.

(Lambek & Scott, 5).

Deductive System

A deductive system is a graph in which to each object \(A\!\) there is associated an arrow \(1_A : A \to A,\) the identity arrow, and to each pair of arrows \(f : A \to B\) and \(g : B \to C\) there is associated an arrow \(gf : A \to C,\) the composition of \(f\!\) with \(g.\!\) A logician may think of the objects as formulas and of the arrows as deductions or proofs, hence of

\(\dfrac{~ f : A \to B \quad g : B \to C ~}{gf : A \to C}\)

as a rule of inference.

(Lambek & Scott, 5).

Category

A category is a deductive system in which the following equations hold, for all \(f : A \to B,\) \(g : B \to C,\) and \(h : C \to D.\)

\(f 1_A = f = 1_B f, \quad (hg)f = h(gf).\)

(Lambek & Scott, 5).

Functor

Definition 1.3. A functor \(F : \mathcal{A} \to \mathcal{B}\) is first of all a morphism of graphs …, that is, it sends objects of \(\mathcal{A}\) to objects of \(\mathcal{B}\) and arrows of \(\mathcal{A}\) to arrows of \(\mathcal{B}\) such that, if \(f : A \to A',\) then \(F(f) : F(A) \to F(A').\) Moreover, a functor preserves identities and composition; thus:

\(F(1_A) = 1_{F(A)}, \quad F(gf) = F(g)F(f).\)

In particular, the identity functor \(1_\mathcal{A} : \mathcal{A} \to \mathcal{A}\) leaves objects and arrows unchanged and the composition of functors \(F : \mathcal{A} \to \mathcal{B}\) and \(G : \mathcal{B} \to \mathcal{C}\) is given by:

\((GF)(A) = G(F(A)), \quad (GF)(f) = G(F(f)),\)

for all objects \(A\!\) of \(\mathcal{A}\) and all arrows \(f : A \to A'\) in \(\mathcal{A}.\)

(Lambek & Scott, 6).

Natural Transformation

Definition 2.1. Given functors \(F, G : \mathcal{A} \rightrightarrows \mathcal{B},\) a natural transformation \(t : F \to G\) is a family of arrows \(t(A) : F(A) \to G(A)\) in \(\mathcal{B},\) one arrow for each object \(A\!\) of \(\mathcal{A},\) such that the following square commutes for all arrows \(f : A \to B\) in \(\mathcal{A}\):


                  t(A)
     F(A) o------------------>o G(A)
          |                   |
          |                   |
     F(f) |                   | G(f)
          |                   |
          v                   v
     F(B) o------------------>o G(B)
                  t(B)

that is to say, such that

\(G(f)t(A) = t(B)F(f).\!\)

{Lambek & Scott, 8).

Graph 2

We recall … that, for categories, a graph consists of two classes and two mappings between them:


o--------------o      source       o--------------o
|              | ----------------> |              |
|   Arrows     |                   |   Objects    |
|              | ----------------> |              |
o--------------o      target       o--------------o

In graph theory the arrows are usually called oriented edges and the objects nodes or vertices, but in various branches of mathematics other words may be used. Instead of writing

\(\operatorname{source}(f) = A, \quad \operatorname{target}(f) = B,\)

one often writes \(f : A \to B\) or \(A \xrightarrow{~f~} B.\) We shall look at graphs with additional structure which are of interest in logic.

(Lambek & Scott, 47).

Deductive System 2

A deductive system is a graph with a specified arrow

\(\text{R1a.} \quad A ~\xrightarrow{~1_A~}~ A,\)

and a binary operation on arrows (composition)

\(\text{R1b.} \quad \dfrac{~ A ~\xrightarrow{~f~}~ B \quad B ~\xrightarrow{~g~}~ C ~}{A ~\xrightarrow{~gf~}~ C}.\)

(Lambek & Scott, 47).

Conjunction Calculus

A conjunction calculus is a deductive system dealing with truth and conjunction. Thus we assume that there is given a formula \(\operatorname{T}\) ( = true) and a binary operation \(\land\) ( = and) for forming the conjunction \(A \land B\) of two given formulas \(A\!\) and \(B.\!\) Moreover, we specify the following additional arrows and rules of inference:

\(\begin{array}{ll} \text{R2.} & A ~\xrightarrow{~\bigcirc_A~}~ \operatorname{T}; \\[8pt] \text{R3a.} & A \land B ~\xrightarrow{~\pi_{A, B}~}~ A, \\[8pt] \text{R3b.} & A \land B ~\xrightarrow{~\pi'_{A, B}~}~ B, \\[8pt] \text{R3c.} & \dfrac{~ C ~\xrightarrow{~f~}~ A \quad C ~\xrightarrow{~g~}~ B ~}{C ~\xrightarrow{~\langle f, g \rangle~}~ A \land B}. \end{array}\)

(Lambek & Scott, 47–48).

Positive Intuitionistic Propositional Calculus

A positive intuitionistic propositional calculus is a conjunction calculus with an additional binary operation \(\Leftarrow\) ( = if). Thus, if \(A\!\) and \(B\!\) are formulas, so are \(\operatorname{T},\) \(A \land B,\) and \(A \Leftarrow B.\) (Yes, most people write \(B \Rightarrow A\) instead.) We also specify the following new arrow and rule of inference.

\(\begin{array}{ll} \text{R4a.} & (A \Leftarrow B) \land B ~\xrightarrow{~\varepsilon_{A, B}~}~ A, \\[8pt] \text{R4b.} & \dfrac{~ C \land B ~\xrightarrow{~h~}~ A ~}{~ C ~\xrightarrow{~h^*~}~ A \Leftarrow B ~}. \end{array}\)

(Lambek & Scott, 48–49).

Intuitionistic Propositional Calculus

An intuitionistic propositional calculus is more than a positive one; it requires also falsehood and disjunction, that is, a formula \(\bot\) ( = false) and an operation \(\lor\) ( = or) on formulas, together with the following additional arrows:

\(\begin{array}{ll} \text{R5.} & \bot ~\xrightarrow{~\Box_A~}~ A; \\[8pt] \text{R6a.} & A ~\xrightarrow{~\kappa_{A, B}~}~ A \lor B, \\[8pt] \text{R6b.} & B ~\xrightarrow{~\kappa'_{A, B}~}~ A \lor B, \\[8pt] \text{R6c.} & (C \Leftarrow A) \land (C \Leftarrow B) ~\xrightarrow{~\zeta^C_{A, B}~}~ C \Leftarrow (A \lor B). \end{array}\)

(Lambek & Scott, 49–50).

Classical Propositional Calculus

If we want classical propositional logic, we must also require:

\(\begin{array}{ll} \text{R7.} & (\bot \Leftarrow (\bot \Leftarrow A)) \to A. \end{array}\)

(Lambek & Scott, 50).

Category 2

A category is a deductive system in which the following equations hold between proofs:

\(\begin{array}{ll} \text{E1.} & f 1_A = f, \qquad 1_B f = f, \qquad (hg)f = h(gf), \\[8pt] & \text{for all}~ f : A \to B, \quad g : B \to C, \quad h : C \to D. \end{array}\)

(Lambek & Scott, 52).

Cartesian Category

A cartesian category is both a category and a conjunction calculus satisfying the additional equations:

\(\begin{array}{ll} \text{E2.} & f = \bigcirc_A, \quad \text{for all}~ f : A \to \operatorname{T}; \\[8pt] \text{E3a.} & \pi^{}_{A,B} \langle f, g \rangle = f, \\[8pt] \text{E3b.} & \pi^\prime_{A,B} \langle f, g \rangle = g, \\[8pt] \text{E3c.} & \langle \pi^{}_{A,B} h, \pi^\prime_{A,B} h \rangle = h, \\[8pt] & \text{for all}~ f : C \to A, \quad g : C \to B, \quad h : C \to A \land B. \end{array}\)

(Lambek & Scott, 52).

Cartesian Closed Category

A cartesian closed category is a cartesian category \(\mathcal{A}\) with additional structure \(\text{R4}\!\) satisfying the additional equations:

\(\begin{array}{ll} \text{E4a.} & \varepsilon^{}_{A,B} \langle h^* \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle = h, \\[8pt] \text{E4b.} & (\varepsilon^{}_{A,B} \langle k \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle)^* = k, \\[8pt] & \text{for all}~ h : C \land B \to A \quad \text{and} \quad k : C \to (A \Leftarrow B). \end{array}\)

Thus, a cartesian closed category is a positive intuitionistic propositional calculus satisfying the equations \(\text{E1}\!\) to \(\text{E4}.\!\) This illustrates the general principle that one may obtain interesting categories from deductive systems by imposing an appropriate equivalence relation on proofs.

(Lambek & Scott, 53).

Document History

Inquiry List, Series A : Jun–Jul 2004

  1. http://stderr.org/pipermail/inquiry/2004-June/001643.html
  2. http://stderr.org/pipermail/inquiry/2004-June/001644.html
  3. http://stderr.org/pipermail/inquiry/2004-June/001645.html
  4. http://stderr.org/pipermail/inquiry/2004-June/001660.html
  5. http://stderr.org/pipermail/inquiry/2004-June/001648.html
  6. http://stderr.org/pipermail/inquiry/2004-June/001649.html
  7. http://stderr.org/pipermail/inquiry/2004-June/001656.html
  8. http://stderr.org/pipermail/inquiry/2004-June/001657.html
  9. http://stderr.org/pipermail/inquiry/2004-June/001658.html
  10. http://stderr.org/pipermail/inquiry/2004-June/001659.html
  11. http://stderr.org/pipermail/inquiry/2004-June/001661.html
  12. http://stderr.org/pipermail/inquiry/2004-June/001662.html
  13. http://stderr.org/pipermail/inquiry/2004-June/001664.html
  14. http://stderr.org/pipermail/inquiry/2004-June/001665.html
  15. http://stderr.org/pipermail/inquiry/2004-June/001666.html
  16. http://stderr.org/pipermail/inquiry/2004-June/001667.html
  17. http://stderr.org/pipermail/inquiry/2004-June/001668.html
  18. http://stderr.org/pipermail/inquiry/2004-June/001670.html
  19. http://stderr.org/pipermail/inquiry/2004-June/001671.html
  20. http://stderr.org/pipermail/inquiry/2004-June/001672.html
  21. http://stderr.org/pipermail/inquiry/2004-June/001673.html
  22. http://stderr.org/pipermail/inquiry/2004-June/001674.html
  23. http://stderr.org/pipermail/inquiry/2004-July/001677.html

Inquiry List, Series B : Jun–Jul 2004

  1. http://stderr.org/pipermail/inquiry/2004-June/001647.html
  2. http://stderr.org/pipermail/inquiry/2004-June/001663.html
  3. http://stderr.org/pipermail/inquiry/2004-June/001669.html
  4. http://stderr.org/pipermail/inquiry/2004-July/001684.html

NKS Forum

  1. http://forum.wolframscience.com/showthread.php?postid=1517#post1517
  2. http://forum.wolframscience.com/showthread.php?postid=1548#post1548
  3. http://forum.wolframscience.com/showthread.php?postid=1550#post1550
  4. http://forum.wolframscience.com/showthread.php?postid=1590#post1590

Inquiry List : Jul 2005

  1. http://stderr.org/pipermail/inquiry/2005-July/002872.html
  2. http://stderr.org/pipermail/inquiry/2005-July/002873.html
  3. http://stderr.org/pipermail/inquiry/2005-July/002874.html
  4. http://stderr.org/pipermail/inquiry/2005-July/002875.html
  5. http://stderr.org/pipermail/inquiry/2005-July/002876.html
  6. http://stderr.org/pipermail/inquiry/2005-July/002877.html
  7. http://stderr.org/pipermail/inquiry/2005-July/002878.html
  8. http://stderr.org/pipermail/inquiry/2005-July/002879.html
  9. http://stderr.org/pipermail/inquiry/2005-July/002880.html
  10. http://stderr.org/pipermail/inquiry/2005-July/002881.html
  11. http://stderr.org/pipermail/inquiry/2005-July/002882.html
  12. http://stderr.org/pipermail/inquiry/2005-July/002883.html
  13. http://stderr.org/pipermail/inquiry/2005-July/002884.html
  14. http://stderr.org/pipermail/inquiry/2005-July/002885.html
  15. http://stderr.org/pipermail/inquiry/2005-July/002886.html
  16. http://stderr.org/pipermail/inquiry/2005-July/002887.html
  17. http://stderr.org/pipermail/inquiry/2005-July/002888.html
  18. http://stderr.org/pipermail/inquiry/2005-July/002889.html
  19. http://stderr.org/pipermail/inquiry/2005-July/002890.html
  20. http://stderr.org/pipermail/inquiry/2005-July/002891.html
  21. http://stderr.org/pipermail/inquiry/2005-July/002892.html
  22. http://stderr.org/pipermail/inquiry/2005-July/002893.html
  23. http://stderr.org/pipermail/inquiry/2005-July/002894.html

Inquiry List, Commentary : Jul 2005

  1. http://stderr.org/pipermail/inquiry/2005-July/002895.html
  2. http://stderr.org/pipermail/inquiry/2005-July/002896.html
Retrieved from "https://mywikibiz.com/index.php?title=Directory:Jon_Awbrey/Papers/Propositions_As_Types&oldid=195743"