Propositions As Types
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 a 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:
- Smullyan, R. (1985), To Mock a Mockingbird, And Other Logic Puzzles, Including an Amazing Adventure in Combinatory Logic, Alfred A. Knopf, New York, NY.
- 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.
- 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 |
|
|
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.\) |
|
|
(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: |
|
|
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: |
|
|
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 |
|
|
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 '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 | R2. A -----> T, | | p1_A,B | R3a. A & B --------> A, | | p2_A,B | R3b. A & B --------> B, | | f g | C ---> A C ---> B | R3c. ----------------------. | <f, g> | C --------> A & B
Positive Intuitionistic Propositional Calculus
| A 'positive intuitionistic propositional calculus' is a conjunction calculus | 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 | R4a. (A <= B) & B ---------> A, | | h | C & B ---> A | R4b. ----------------. | h* | C ----> A <= B |
Intuitionistic Propositional Calculus
| An 'intuitionistic propositional calculus' is more than a | 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 | R5. F ------> A, | | k1_A,B | R6a. A --------> A v B, | | 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.
Category 2
| A 'category' is a deductive system in which | the following equations hold between proofs: | | E1. f 1_A = f, | | 1_B f = f, | | (hg)f = h(gf), | | for all f : A -> B, g : B -> C, h : C -> D.
Cartesian Category
| A 'cartesian category' is both a category | 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, | | E3c. <p1_A,B h, p2_A,B h> = h, | | for all f : C -> A, g : C -> B, h : C -> A & B.
Cartesian Closed Category
| A 'cartesian closed category' is a cartesian category $A$ with | 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, | | for all h : C & B -> A, k : C -> (A <= B). | | Thus, a cartesian closed category is | 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.
Document History
Inquiry List, Series A : Jun–Jul 2004
- http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
- 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
Inquiry List, Series B : Jun–Jul 2004
- 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
NKS Forum
- 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
Inquiry List : Jul 2005
- http://stderr.org/pipermail/inquiry/2005-July/002872.html
- http://stderr.org/pipermail/inquiry/2005-July/002873.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
