12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 23:54, 6 July 2013
, 23:54, 6 July 2013no edit summary
{{DISPLAYTITLE:Propositions As Types}}
{{DISPLAYTITLE:Propositions As Types}}
'''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==
==Identity, or the Identifier==
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>x_A ~=~ x_A \operatorname{I}_{A \Rightarrow A}</math>
| <math>\begin{matrix}x_A & = & x_A \operatorname{I}_{A \Rightarrow A}\end{matrix}</math>
|}
|}
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
| <math>\begin{matrix}x(y(z\operatorname{P})) & = & (xy)z\end{matrix}</math>
<math>\begin{array}{ccc}
x(y(z\operatorname{P})) & = & (xy)z
\end{array}</math>
|}
|}
===Step 2===
===Step 2===
Assign types in the following specification:
Assign types in the specification:
{| 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>
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:
{| 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>
|}
===Step 3 (Optional)===
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.
propositional calculus, based on the combinator axioms,
<pre>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
QED.
QED.
===Step 4===
===Step 4===
Repeat the development in Step 1, but this time articulating the type information as we go.
<pre>
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
| |
| |
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
The foregoing development has taken us from the
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:
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:
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}\operatorname{P} & = & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))\end{matrix}</math>
|}
and also the proof tree for the proposition type of P:
and also the proof tree for the type proposition of <math>\operatorname{P},</math> as follows:
<pre>
S K
S K
o o
o o
\ /
\ /
P = (o)
P = (o)
</pre>
</pre>
{| align="center" cellpadding="8" width="90%"
|
<math>\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}</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
| |
| |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
; 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==
==Self-Documentation : Developmental Data Structures==
; Observation.
Observation. Notice the "self-documenting" property
: 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.
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:
For example, the development of the Identity combinator:
{| 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
| |
| |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
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 |
| |
| |
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.
==Triadic Analogy : Analogy Between Two Triadic Relations==
==Triadic Analogy : Analogy Between Two Triadic Relations==
<br>
<pre>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
</pre>
<br>
==Transposition, or the Transposer==
==Transposition, or the Transposer==
<pre>
'''Definition'''
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
|}
This equation constitutes a "paraphrastic definition"
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.
specification of how the operator is required to act
on other symbols.
===Step 1===
===Step 1===
'''Construction'''
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
primitive combinators <math>\operatorname{K}</math> and <math>\operatorname{S}.</math>
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.
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
|}
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:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
y(xz)
& = &
(x(y\operatorname{K}))(xz)
\\[8pt]
& = &
x((y\operatorname{K})(z\operatorname{S}))
\end{matrix}</math>
|}
thus completing the abstraction (or disentanglement)
thus completing the abstraction (or disentanglement) of x from the expression.
of x from the expression.
Working on the remainder of the expression,
Working on the remainder of the expression, the next item of business is to abstract <math>y.\!</math>
the next item of business is to abstract y.
Notice that:
Notice that:
{| 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>
|}
thus completing the abstraction of <math>y.\!</math>
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:
{| align="center" cellpadding="8" width="90%"
|
<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>
|}
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>
Continue with <math>\operatorname{K}((z\operatorname{F})\operatorname{S}),</math> to extract <math>z,\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
|
<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>
|}
Rename the operator on the right, letting <math>(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) = \operatorname{G}.</math>
Continue with <math>\operatorname{K}(z\operatorname{G}),</math> to extract <math>z,\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
|
<math>\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}</math>
|}
Filling in the abbreviations:
Filling in the abbreviations:
{| align="center" cellpadding="8" width="90%"
|
<math>\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}</math>
|}
Thus we have:
Thus we have:
{| align="center" cellpadding="8" width="90%"
</pre>
|
<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>
|}
===Step 2===
===Step 2===
Using the contextual definition of the transposer <math>\operatorname{T},</math>
Using the contextual definition of the transposer T,
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
|}
find a minimal generic typing (simplest non-degenerate typing) of
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.
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:
{| align="center" cellpadding="8" width="90%"
|
<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:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{array}{l}
(x \overset{ }{\underset{A}{\Downarrow}} ~
Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type,
(y \overset{ }{\underset{B}{\Downarrow}} ~
read as a proposition, is a theorem of intuitionistic
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
propositional calculus.
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 <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.
===Step 3 (Optional)===
===Step 3 (Optional)===
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.
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:
In existential graph format, <math>\operatorname{T}</math> has the following generic typing:
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
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
| |
| |
===Step 4===
===Step 4===
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.
The construction of the term T of the appropriate type in terms of the
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
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.
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,
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.
denote whatever it is, the supposed object, that
Consider the following data:
Consider the following data:
The parse tree of the term T = ((KK)(((S((KK)S))((SK)S))S))
:* 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>
:* The type marker of the term <math>\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C))</math>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
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:
{| align="center" cellpadding="8" width="90%"
|
<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}} ~
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}</math>
|}
If this strategy is successful it suggests that the proof tree can
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.
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
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.
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,
Repeat the development in Step 1, but this time articulating the type information as we go.
but this time articulating the
type information as we go.
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
| |
| |
===Step 5===
===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.
<pre>
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
</pre>
; 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)===
===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) |
===Commentary Note 1===
===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.
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
{| 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:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{array}{l}
x : X
\\
\underline{f : X \to Y}
\\
f(x) : Y
\end{array}</math>
|}
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.
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.
of information, in the following conventional form:
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''.
===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:
# 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 <math>\lambda</math>-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. [http://suo.ieee.org/ontology/thrd42.html#03373 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===
| Lambek, J. and Scott, P.J.,
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<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>
</pre>
<p>We shall now progress from concrete categories to abstract ones, in three easy stages.</p>
<pre>
<p>(Lambek & Scott, 4–5).</p>
|}
===Graph===
{| 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>
and more generality of perspective with each passing time:
<center><pre>
| Definition 1.1. A 'concrete category' is a collection of two kinds
o--------------o source o--------------o
| of entities, called 'objects' and 'morphisms'. The former are sets
| | ----------------> | |
| which are endowed with some kind of structure, and the latter are
| Arrows | | Objects |
| mappings, that is, functions from one object to another, in some
| | ----------------> | |
| sense preserving that structure. Among the morphisms, there is
o--------------o target o--------------o
| 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
</pre></center>
<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>
<p>(Lambek & Scott, 5).</p>
|}
|
Deductive System
===Deductive System===
| A 'deductive system' is a graph in which to each object A there
{| 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>
| ---------------------------
|-
|
|
| as a 'rule of inference'.
::<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>
<p>(Lambek & Scott, 5).</p>
|}
Category
===Category===
| A 'category' is a deductive system in which the following equations hold,
{| 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
===Functor===
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
{| 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 …, 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>
<p>(Lambek & Scott, 6).</p>
|}
| Definition 2.1. Given functors F, G : $A$ -> $B$,
===Natural Transformation===
{| 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>
<pre>
t(A)
F(A) o------------------>o G(A)
| |
| |
F(f) | | G(f)
| |
v v
F(B) o------------------>o G(B)
t(B)
</pre>
<p>that is to say, such that</p>
|-
|
|
| that is to say, such that
<p><math>G(f)t(A) = t(B)F(f).\!</math></p>
|-
|
|
<p>{Lambek & Scott, 8).</p>
|}
Graph
===Graph 2===
| We recall (Part 0, Definition 1.2) that, for categories,
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>We recall … that, for categories, a ''graph'' consists of two classes and two mappings between them:</p>
<center><pre>
o--------------o source o--------------o
| | ----------------> | |
| Arrows | | Objects |
| | ----------------> | |
o--------------o target o--------------o
</pre></center>
<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>
|-
|
|
::<p><math>\operatorname{source}(f) = A, \quad \operatorname{target}(f) = B,</math></p>
|-
| of mathematics other words may be used. Instead of writing
|
|
<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>
<p>(Lambek & Scott, 47).</p>
|}
Deductive System
===Deductive System 2===
| A 'deductive system' is a graph with a specified arrow
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<p>A ''deductive system'' is a graph with a specified arrow</p>
|-
|
<p><math>\text{R1a.} \quad A ~\xrightarrow{~1_A~}~ A,</math></p>
|-
|
|
<p>and a binary operation on arrows (''composition'')
| R1a. A -----> A,
|-
|
|
| and a binary operation on arrows ('composition')
<p><math>\text{R1b.} \quad \dfrac{~ A ~\xrightarrow{~f~}~ B \quad B ~\xrightarrow{~g~}~ C ~}{A ~\xrightarrow{~gf~}~ C}.</math></p>
|-
|
|
<p>(Lambek & Scott, 47).</p>
|}
| gf
Conjunction Calculus
===Conjunction Calculus===
| A 'conjunction calculus' is a deductive system dealing with truth and
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<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> ( = true) and a binary operation <math>\land</math> ( = 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>
|-
|
|
<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>
|-
|
|
<p>(Lambek & Scott, 47–48).</p>
|}
| C --------> A & B
Positive Intuitionistic Propositional Calculus
===Positive Intuitionistic Propositional Calculus===
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''positive intuitionistic propositional calculus'' is a conjunction calculus with an additional binary operation <math>\Leftarrow</math> ( = 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>
|-
|
|
<p><math>\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 ~}.
| C ----> A <= B
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 48–49).</p>
|}
Intuitionistic Propositional Calculus
===Intuitionistic Propositional Calculus===
| An 'intuitionistic propositional calculus' is more than a
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>An ''intuitionistic propositional calculus'' is more than a positive one; it requires also falsehood and disjunction, that is, a formula <math>\bot</math> ( = false) and an operation <math>\lor</math> ( = or) on formulas, together with the following additional arrows:</p>
| R5. F ------> A,
|-
|
|
<p><math>\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}</math></p>
|-
|
|
<p>(Lambek & Scott, 49–50).</p>
|}
|
Classical Propositional Calculus
===Classical Propositional Calculus===
| If we want 'classical' propositional logic, we must also require:
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| R7. F <= (F <= A) -> A.
<p>If we want ''classical'' propositional logic, we must also require:
|-
|
<p><math>\begin{array}{ll}
\text{R7.} & (\bot \Leftarrow (\bot \Leftarrow A)) \to A.
\end{array}</math></p>
|-
|
<p>(Lambek & Scott, 50).</p>
|}
Category
===Category 2===
| A 'category' is a deductive system in which
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| E1. f 1_A = f,
<p>A ''category'' is a deductive system in which the following equations hold between proofs:</p>
|-
|
|
<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>
|-
|
|
<p>(Lambek & Scott, 52).</p>
|}
| for all f : A -> B, g : B -> C, h : C -> D.
Cartesian Category
===Cartesian Category===
| A 'cartesian category' is both a category
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| E2. f = O_A, for all f : A -> T.
<p>A ''cartesian category'' is both a category and a conjunction calculus satisfying the additional equations:</p>
|-
|
|
<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>
|-
|
|
<p>(Lambek & Scott, 52).</p>
|}
| for all f : C -> A, g : C -> B, h : C -> A & B.
Cartesian Closed Category
===Cartesian Closed Category===
| A 'cartesian closed category' is a cartesian category $A$ with
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<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>
|-
|
|
<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>
|-
|
|
<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>
<p>(Lambek & Scott, 53).</p>
|}
</pre>
==Document History==
==Document History==
# http://stderr.org/pipermail/inquiry/2005-July/002895.html
# http://stderr.org/pipermail/inquiry/2005-July/002895.html
# http://stderr.org/pipermail/inquiry/2005-July/002896.html
# http://stderr.org/pipermail/inquiry/2005-July/002896.html
[[Category:Combinator Calculus]]
[[Category:Combinatory Logic]]
[[Category:Computer Science]]
[[Category:Graph Theory]]
[[Category:Lambda Calculus]]
[[Category:Logic]]
[[Category:Logical Graphs]]
[[Category:Mathematics]]
[[Category:Programming Languages]]
[[Category:Type Theory]]