Propositions As Types
MyWikiBiz, Author Your Legacy — Tuesday April 16, 2024
Jump to navigationJump to searcho~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
IDS -- PAT
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 1
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Identity, or the Identifier
Step 1.
Given a syntactic specification (or paraphrastic definition):
x = xI
where "x = x..." is the definiens,
or defining context, and "I" is
the definiendum,
Find a pure interpretant for I, that is, an equivalent term
in <<K, S>>, the combinatory algebra generated by K and S,
that does as I does.
Observe:
x = (xK)(xK) = x(K(KS))
=>
I = K(KS)
and so K(KS) constitutes a syntactic algorithm for I.
Step 2.
Assign types in the specification:
x_A = x_A I_(A=>A)
to arrive at a propositional typing for I : A => A,
whose type, read as a proposition, is a theorem of
intuitionistic propositional calculus.
Step 3 (optional).
Check that A => A is a theorem of classical propositional calculus.
A A
o---o o---o
| |
@ = @ = @
Check.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 2
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Identity, or the Identifier (cont.)
Step 4.
If we start from the parse tree of the term I in terms of
the primitive combinators K and S, that is, the articulation
or construction corresponding to the term equation I = (K(KS)),
K S
o o
K \ /
o (o)
\ /
I = (o) ,
then adding appropriate type-indices to the nodes of this tree will
leave us with a proof tree for the propositional type of I : A => A.
Thus, the construal or construction of I as K(KS) constitutes a hint
or clue to the proof of A => A in the intuitionistic propositional
calculus. Although guesswork may succeed in easy cases such as this,
a more systematic procedure is to follow the development in Step 1,
that takes us from contextual specification to operational algorithm,
and to carry along the type information as we go, ending up with
a typed parse tree for I, tantamount to a proof tree for A => A.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 3
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Identity, or the Identifier (cont.)
Step 4 (cont.)
Term Development: Contextual Definition ~~~> Combinator Construction
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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 4
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
| NB. I am working from rough notes that
| I wrote out in the Fall of 1996, and it
| is not always easy to reconstruct what
| I had in mind at the time. I misread
| this passage in my last posting of it,
| causing me to leave out a few steps.
1. Identity, or the Identifier (cont.)
Step 5.
Existential Graph Format,
Application Triples with
Structure Sharing.
Same development in Existential Graph notation.
Here I am carrying out the term development in
reverse, that is, in application order.
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
| I am still not sure what order I intended for the
| application triples, but this is one likely guess:
For example:
The nodes that are right-labeled <K, KS, K(KS)>,
in that order, constitute an application triple.
The type of the applicand K is A=>(B=>A).
The type of the applicator KS is (A=>(B=>A))=>(A=>A).
Therefore, the type of the application K(KS) is A=>A.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 5
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer
Step 1.
Given a specification of the "composition combinator",
or the "composer" P, that has the following effects:
x(y(zP)) = (xy)z
find an explication of P in terms of primitive combinators.
Proceed as follows:
(xy)z = (xy)(x(zK)) = x(y((zK)S))
(zK)S = (zK)(z(SK)) = z(K((SK)S))
=>
x(y(zP)) = (xy)z = x(y(z(K((SK)S))))
=>
P = (K((SK)S))
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 6
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer (cont.)
Step 2.
Assign types in the specification:
B C
((x: y:): z:):
A A B B C
=
B C (A=>B)=>(A=>C) A=>C C
(x: (y: (z: P: ): ):):
A A B B=>C A=>B A C
Here, a notation of the form:
x:
A
means that x is of the type A,
while a notation of the form:
B
x:
A
means that x is of the type A=>B.
Note that the explication of P as a term K((SK)S) of
type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof
of P's type proposition as a theorem of intuitionistic
propositional calculus, based on the combinator axioms,
K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 7
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer (cont.)
Step 3 (optional).
Check that the propositional type of the composer P is a theorem
of classical propositional calculus, which is logically necessary
to its being a theorem of intuitionistic propositional calculus,
but easier to check.
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.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 8
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer (cont.)
Step 4.
Repeat the development in Step 1,
but this time articulating the
type information as we go.
o---------------------------------------------------------------------o
| |
| x y A |
| 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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 9
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer (cont.)
Step 4 (concl.)
The foregoing development has taken us from the
typed parse tree for the definiens ((xy)z) to the
typed parse tree for the explicated definiendum
(x(y(z(K((SK)S)) ))), which gives us both the
construction of the composition combinator P
in terms of primitive combinators:
P = (K((SK)S))
and also the proof tree for the proposition type of P:
S K
o o
\ / S
(o) o
K \ /
o (o)
\ /
P = (o)
P = (K((SK)S)) : (B=>C)=>((A=>B)=>(A=>C))
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 10
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Composition, or the Composer (concl.)
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
NB. Graphic convention used in the above style of display:
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.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 11
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Self-Documentation
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:
x = (xK)(xK) = x(K(KS))
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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 12
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Self-Documentation, Developmental Data Structures (cont.)
Redo the entire development of the Composer in existential graph format:
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.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 13
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Triadic Analogy: Analogy Between a Couple of Three-Place Relations
o-------------------------------------------------o
| |
| proof hint : proof : proposition |
| |
o=================================================o
| |
| untyped term : typed term : type |
| |
o-------------------------------------------------o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 14
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer
x(y(zT)) = y(xz)
This equation constitutes a "paraphrastic definition"
of T, a definition-in-context, or a formal syntactic
specification of how the operator is required to act
on other symbols.
Step 1.
Find a "pure interpretant" for T, that is, an equivalent term
doing the job of T which is constructed purely in terms of the
primitive combinators K and S.
This will constitute an operational algorithm for T, though
still operating at the level of abstract syntax, understood
as a sequence of manipulations on formal identifiers, or on
symbols taken as objects in themselves.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 15
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
x(y(zT)) = y(xz)
Step 1 (concl.)
Observe that y(xz) matches (xy)(xz) on the right,
and that we can express y as x(yK), consequently:
y(xz) = (x(yK))(xz)
= x((yK)(zS))
thus completing the abstraction (or disentanglement)
of x from the expression.
Working on the remainder of the expression,
the next item of business is to abstract y.
Notice that:
(yK)(zS) = (yK)(y((zS)K))
= y(K(((zS)K)S))
thus completing the abstraction of y.
Next, work on K(((zS)K)S) to extract z, starting from
the center (zS)K of the labyrinth and working outward:
(zS)K = (zS)(z(KK))
= z(S((KK)S))
For the sake of brevity in the rest of this development,
rename the operator on the right so that (S((KK)S)) = F.
Continue with K((zF)S), to extract z:
(zF)S = (zF)(z(SK))
= z(F((SK)S))
Rename the operator on the right, letting (F((SK)S)) = G.
Continue with K(zG), to extract z:
K(zG) = (z(KK))(zG)
= z((KK)(GS))
Filling in the abbreviations:
y(xz) = x(y(z((KK)(GS)) ))
= x(y(z((KK)((F((SK)S))S)) ))
= x(y(z((KK)(((S((KK)S))((SK)S))S)) ))
Thus we have:
T = (KK)(((S((KK)S))((SK)S))S)
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 16
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 2.
Using the contextual definition of the transposer T,
y(xz) = x(y(zT)),
find a minimal generic typing (simplest non-degenerate typing) of
each term in the specification that makes all of the applications
on each side of the equation go through.
For example, here is one such typing:
B=>C C B=>C B=>(A=>C) A=>C C
(y: (x: z: ): ): = (x: (y: (z: T: ): ): ):
B A A B C A B A A=>(B=>C) B A C
In a contextual, implicit, or paraphrastic definition of this sort,
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
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:
B=>C B=>(A=>C) A=>C C B=>C C
(x: (y: (z: T: ): ): ): = (y: (x: z: ): ):
A B A A=>(B=>C) B A C B A A B C
Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type,
read as a proposition, is a theorem of intuitionistic
propositional calculus.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 17
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 3 (optional).
At this juncture we might want to verify that the proposition corresponding
to the type of T is actually a theorem of classical propositional calculus.
Since nothing can be a theorem of intuitionistic propositional calculus
wihout also being a theorem of classical propositional calculus, this
is a necessary condition of our work being correct up to this point.
Although it is not a sufficient condition, classical theoremhood
is easier to test and so provides a quick and useful check on
our work.
In existential graph format, T has the following generic typing:
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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 18
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 4.
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
progress of this work. Renaming is the natural operation that substitution
is the reverse of. With these humble beginnings we have reached a birthplace,
a native ground, of the sign relation, an irreducible three-place relationship
among what is indicated, what happens to indicate it, and all of the equivalent
or associated indications we may find or create in reference to it.
For example, let "G", the interposed interpretant,
denote whatever it is, the supposed object, that
"(F((SK)S))", the occurrent sign, denotes.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 19
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 4 (cont.)
Consider the following data:
The parse tree of the term T = ((KK)(((S((KK)S))((SK)S))S))
and the typing of the term T : (A=>(B=>C))=>(B=>(A=>C)).
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:
o-----------------------------------------------------------o
| |
| B=>C C |
| (y: (x: z: ): ): |
| B A A B C |
| |
o===========================================================o
| |
| A=>B B B=>C C |
| ((x: (y: K: ): ): (x: z: ): ): |
| A B B A B A A B C |
| |
o===========================================================o
| |
| A=>B B B=>C (A=>B)=>(A=>C) A=>C C |
| (x: ((y: K: ): (z: S: ): ): ): |
| A B B A A A=>(B=>C) A=>B A C |
| |
o===========================================================o
| |
| ... |
| |
o-----------------------------------------------------------o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 20
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 4 (cont.)
If this strategy is successful it suggests that the proof tree can
be grown in a stepwise equational fashion from a seed term of the
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.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 21
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 4 (concl.)
Repeat the development in Step 1,
but this time articulating the
type information as we go.
o---------------------------------------------------------------------o
| |
| 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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 22
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 5.
Rewrite the final proof tree in existential graph format,
implementing structure sharing among application triples
by overlaying the type propositions that attach to terms.
Graphic Conventions: Square bracketed nodes mark subtrees
to be pruned from one tree and grafted into another at the
indicated site, tantamount to recycling "Facts" as "Cases".
Square brackets are also used to indicate the final result.
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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 23
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note 24
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types -- Commentary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Commentary Note 1
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
I think it's best to begin with a few simple observations,
as I frequently find it necessary to return to the basics
again and again, even if I take a different path each time.
Observation 1
If we have the information that an element x
is constrained to be of the type X
and we have the information that a function f
is constrained to be of the type X -> Y
then we have the information that the element f(x)
is constrained to be 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:
x : X
f : X -> Y
-----------
f(x) : Y
In this scheme of inference, the notations "x", "f", and "f(x)"
are taken to be names of formal objects. Some people will call
these notations by the name of "terms", while other people will
somewhat more confusedly say that the formal objects themselves
are the terms. Because it is so important to distinguish signs
denoting from objects denoted, I will make some effort to avoid
the latter usage, and recommend sticking with the first option.
In the same context, the notations "X", "X -> Y", and "Y" give us
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", one may of course elect to
view these types as a species of formal objects existing in their
own right, inhabiting their own niche, as it were.
If a moment's spell of double vision leads us to see the
functional arrow "->" as the logical arrow "=>", then we
may observe that the right side of this inference scheme
follows the pattern of logical deduction that is usually
called "modus ponens". And so we forge a tentative link
between the pattern of information conversion implicated
in functional application and the pattern of information
conversion involved in the logical rule of modus ponens.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Commentary Note 2
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Re: PAT. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872
Notice that I am carrying out combinator applications "on the right",
so the formulas might be backwards from what many people are used to.
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.,
|'To Mock a Mockingbird, And Other Logic Puzzles,
| Including an Amazing Adventure in Combinatory Logic',
| Alfred A. Knopf, New York, NY, 1985.
| Hindley, J.R. and Seldin, J.P.,
|'Introduction to Combinators and [Lambda]-Calculus',
| London Mathematical Society Student Texts No. 1,
| Cambridge University Press, Cambridge, UK, 1986.
| Lambek, J. and Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
| http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521356539
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Commentary Note 3
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Work Area
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
I have been posting excerpts to the ONT List, between note_01 & note_30:
note_01 = http://suo.ieee.org/ontology/msg03373.html
note_30 = http://suo.ieee.org/ontology/msg03418.html
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 -> A
| such that 1_A(a) = a for all a in A. Moreover, morphisms
| f : A -> B and g : B -> C may be 'composed' to produce
| a morphism gf : A -> C such that (gf)(a) = g(f(a))
| for all a in A.
| We shall now progress from concrete categories
| to abstract ones, in three easy stages.
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 "f : A -> B" for "source f = A and target f = B".
| A graph is said to be 'small' if the classes of objects and
| arrows are sets.
Deductive System
| A 'deductive system' is a graph in which to each object A there
| is associated an arrow 1_A : A -> A, the 'identity' arrow, and to
| each pair of arrows f : A -> B and g : B -> C there is associated
| an arrow gf : A -> C, the 'composition' of f with g. A logician
| may think of the objects as 'formulas' and of the arrows as
| 'deductions' or 'proofs', hence of
|
| f : A -> B g : B -> C
| ---------------------------
| gf : A -> C
|
| as a 'rule of inference'.
Category
| A 'category' is a deductive system in which the following equations hold,
| for all f : A -> B, g : B -> C, and h : C -> D.
|
| f 1_A = f = 1_B f,
|
| (hg)f = h(gf).
Functor
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
| first of all a morphism of graphs (see Example C4),
| that is, it sends objects of $A$ to objects of $B$
| and arrows of $A$ to arrows of $B$ such that, if
| f : A -> A', then F(f) : F(A) -> F(A'). Moreover,
| a functor preserves identities and composition;
| thus:
|
| F(1_A) = 1_F(A),
|
| F(gf) = F(g)F(f).
|
| In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves
| objects and arrows unchanged and the composition of functors
| F : $A$ -> $B$ and G : $B$ -> $C$ is given by:
|
| (GF)(A) = G(F(A)),
|
| (GF)(f) = G(F(f)),
|
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
Natural Transformation
| Definition 2.1. Given functors F, G : $A$ -> $B$,
| a 'natural transformation' t : F -> G is a family
| of arrows t(A) : F(A) -> G(A) in $B$, one arrow for
| each object A of $A$, such that the following square
| commutes for all arrows f : A -> B in $A$:
|
| t(A)
| 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).
Graph
| We recall (Part 0, Definition 1.2) that, for categories,
| a 'graph' consists of two classes and two mappings
| between them:
|
| o--------------o source o--------------o
| | | ----------------> | |
| | Arrows | | Objects |
| | | ----------------> | |
| o--------------o target o--------------o
|
| In graph theory the arrows are usually called "oriented edges"
| and the objects "nodes" or "vertices", but in various branches
| of mathematics other words may be used. Instead of writing
|
| source(f) = A,
|
| target(f) = B,
| f
| one often writes f : A -> B or A ---> B. We shall
| look at graphs with additional structure which are
| of interest in logic.
Deductive System
| A 'deductive system' is a graph with a specified arrow
|
| 1_A
| R1a. A -----> A,
|
| and a binary operation on arrows ('composition')
|
| f g
| A ---> B B ---> C
| R1b. ----------------------
| gf
| A ----> C
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
| 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.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types -- 2004
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types A
Inquiry List
00. http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
00. http://stderr.org/pipermail/inquiry/2004-July/thread.html#1677
01. http://stderr.org/pipermail/inquiry/2004-June/001643.html
02. http://stderr.org/pipermail/inquiry/2004-June/001644.html
03. http://stderr.org/pipermail/inquiry/2004-June/001645.html
04. http://stderr.org/pipermail/inquiry/2004-June/001660.html
05. http://stderr.org/pipermail/inquiry/2004-June/001648.html
06. http://stderr.org/pipermail/inquiry/2004-June/001649.html
07. http://stderr.org/pipermail/inquiry/2004-June/001656.html
08. http://stderr.org/pipermail/inquiry/2004-June/001657.html
09. http://stderr.org/pipermail/inquiry/2004-June/001658.html
10. http://stderr.org/pipermail/inquiry/2004-June/001659.html
11. http://stderr.org/pipermail/inquiry/2004-June/001661.html
12. http://stderr.org/pipermail/inquiry/2004-June/001662.html
13. http://stderr.org/pipermail/inquiry/2004-June/001664.html
14. http://stderr.org/pipermail/inquiry/2004-June/001665.html
15. http://stderr.org/pipermail/inquiry/2004-June/001666.html
16. http://stderr.org/pipermail/inquiry/2004-June/001667.html
17. http://stderr.org/pipermail/inquiry/2004-June/001668.html
18. http://stderr.org/pipermail/inquiry/2004-June/001670.html
19. http://stderr.org/pipermail/inquiry/2004-June/001671.html
20. http://stderr.org/pipermail/inquiry/2004-June/001672.html
21. http://stderr.org/pipermail/inquiry/2004-June/001673.html
22. http://stderr.org/pipermail/inquiry/2004-June/001674.html
23. http://stderr.org/pipermail/inquiry/2004-July/001677.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types B
Inquiry List
00. http://stderr.org/pipermail/inquiry/2004-June/thread.html#1647
00. http://stderr.org/pipermail/inquiry/2004-July/thread.html#1684
01. http://stderr.org/pipermail/inquiry/2004-June/001647.html
02. http://stderr.org/pipermail/inquiry/2004-June/001663.html
03. http://stderr.org/pipermail/inquiry/2004-June/001669.html
04. http://stderr.org/pipermail/inquiry/2004-July/001684.html
NKS Forum
00. http://forum.wolframscience.com/showthread.php?threadid=490
01. http://forum.wolframscience.com/showthread.php?postid=1517#post1517
02. http://forum.wolframscience.com/showthread.php?postid=1548#post1548
03. http://forum.wolframscience.com/showthread.php?postid=1550#post1550
04. http://forum.wolframscience.com/showthread.php?postid=1590#post1590
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types -- 2005
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Propositions As Types
00. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872
01. http://stderr.org/pipermail/inquiry/2005-July/002872.html
02. http://stderr.org/pipermail/inquiry/2005-July/002873.html
03. http://stderr.org/pipermail/inquiry/2005-July/002874.html
04. http://stderr.org/pipermail/inquiry/2005-July/002875.html
05. http://stderr.org/pipermail/inquiry/2005-July/002876.html
06. http://stderr.org/pipermail/inquiry/2005-July/002877.html
07. http://stderr.org/pipermail/inquiry/2005-July/002878.html
08. http://stderr.org/pipermail/inquiry/2005-July/002879.html
09. http://stderr.org/pipermail/inquiry/2005-July/002880.html
10. http://stderr.org/pipermail/inquiry/2005-July/002881.html
11. http://stderr.org/pipermail/inquiry/2005-July/002882.html
12. http://stderr.org/pipermail/inquiry/2005-July/002883.html
13. http://stderr.org/pipermail/inquiry/2005-July/002884.html
14. http://stderr.org/pipermail/inquiry/2005-July/002885.html
15. http://stderr.org/pipermail/inquiry/2005-July/002886.html
16. http://stderr.org/pipermail/inquiry/2005-July/002887.html
17. http://stderr.org/pipermail/inquiry/2005-July/002888.html
18. http://stderr.org/pipermail/inquiry/2005-July/002889.html
19. http://stderr.org/pipermail/inquiry/2005-July/002890.html
20. http://stderr.org/pipermail/inquiry/2005-July/002891.html
21. http://stderr.org/pipermail/inquiry/2005-July/002892.html
22. http://stderr.org/pipermail/inquiry/2005-July/002893.html
23. http://stderr.org/pipermail/inquiry/2005-July/002894.html
PAT. Propositions As Types -- Commentary
00. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2895
01. http://stderr.org/pipermail/inquiry/2005-July/002895.html
02. http://stderr.org/pipermail/inquiry/2005-July/002896.html
03.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
