This site is supported by donations to The OEIS Foundation.

Propositions As Types Analogy

From OeisWiki
(Redirected from Propositions As Types)
Jump to: navigation, search

Author: Jon Awbrey

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

Identity, or the Identifier

Step 1

Consider the following problem requirements:

One is given a syntactic specification of the following form:

In effect, this specification amounts to a so-called paraphrastic definition of the operator one in which the syntactic frame may be regarded as the defining context, or definiens, and is regarded as the object to be defined, or definiendum.

One is asked to find a pure interpretant for that is, an equivalent term in the combinatory algebra generated by and that does as does.

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

Thus the sequence of operations indicated by is a proxy for

Step 2

Assign types in the following specification:

A suitable type assignment provides a propositional typing for whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

Step 3 (Optional)

Check that is a theorem of classical propositional calculus.

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

Check.

Step 4

Term Development : Contextual Definition Combinator Construction

Consider the parse tree of the term in terms of the primitive combinators and that is, the articulation or construction corresponding to the term equation as shown here:

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

Adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of Thus, the construal or construction of as constitutes a hint or clue to the proof of 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 tantamount to a proof tree for

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

Step 5

Existential Graph Format : Application Triples with Structure Sharing

Redo the same development in Existential Graph notation. In the work below, the term development is carried out in reverse, that is, in application order.

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

NB. Looking at my notes from Fall Term 1996, I'm still not sure what order I intended for the application triples, but the above is one likely guess:

For example:

  • The nodes that are right-labeled in that order, constitute an application triple.
  • The type of the applicand is
  • The type of the applicator is
  • Therefore, the type of the application is

Composition, or the Composer

Step 1

We are given a specification of the composition combinator, or the composer in terms of the following effects:

We are asked to find an explication of in terms of primitive combinators.

Proceed as follows:

Step 2

Assign types in the following specification:

Here, a notation of the form means that is of the type while a notation of the form means that is of the type

Note that the explication of as a term of type serves as a clue to the proof of type proposition as a theorem of the intuitionistic propositional calculus, that is, using only the following two combinator axioms:

Step 3 (Optional)

Check that the propositional type of the composer is a theorem of classical propositional calculus, which is logically necessary to its being a theorem of intuitionistic propositional calculus, but easier to check.

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

QED.

Step 4

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

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

The foregoing development has taken us from the typed parse tree for the definiens to the typed parse tree for the explicated definiendum which gives us both the construction of the composition combinator in terms of primitive combinators:

and also the proof tree for the type proposition of as follows:

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

Step 5

Rewrite the final proof tree in existential graph format:

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

Self-Documentation : Developmental Data Structures

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

For example, the development of the Identity combinator:

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

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

Step 5 (extended)

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

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

Triadic Analogy : Analogy Between Two Triadic Relations

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

Transposition, or the Transposer

Definition

This equation provides a contextual definition for the operator in effect, a formal syntactic specification that tells how the operator is required to act on other symbols.

Step 1

Construction

Find a pure interpretant for that is, an equivalent term doing the job of which is constructed purely in terms of the primitive combinators and

Doing this yields an operational algorithm for understood as a sequence of manipulations on formal identifiers, or on symbols taken as objects in their own rights.

Observe that matches on the right, and that we can express as consequently:

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

Notice that:

thus completing the abstraction of

Next, work on to extract starting from the center of the labyrinth and working outward:

For the sake of brevity in the rest of this development, rename the operator on the right so that

Continue with to extract as follows:

Rename the operator on the right, letting

Continue with to extract as follows:

Filling in the abbreviations:

Thus we have:

Step 2

Using the contextual definition of the transposer

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:

In a contextual, implicit, or paraphrastic definition of this sort, the definiendum is the symbol to be defined, in this case, and the definiens is the entire rest of the context, in this case, the frame that ostensibly defines, or as one says, is supposed to define the symbol 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 has to be, in order to function properly in the standard context, in this case,

Again, this gives:

Thus we have whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

Step 3 (Optional)

At this juncture we might want to verify that the proposition corresponding to the type of 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, has the following generic typing:

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

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

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

Step 4

The construction of the term of the appropriate type in terms of the primitive typed combinators of the forms and is analogous to the proof of the corresponding proposition from the intuitionistic axiom schemes attached to those forms.

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

For example, let the interposed interpretant denote the supposed object, namely, whatever it is that the occurrent sign denotes.

Consider the following data:

  • The parse tree for the term
  • The type marker of the term
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:

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

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

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

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

Step 5

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

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

Step 5 (Extended)

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

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

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

Commentary

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.

Comment 1

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

Observation 1
IF we know element has type
AND we know function has type
THEN we know element has type

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

In this scheme of inference, the notations and are referred to as terms and interpreted as names of formal objects.

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

If a moment's spell of double vision leads us to see the functional arrow 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.

Comment 2

To be continued …

Bibliography

Here are three references on combinatory logic and lambda calculus which 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 -Calculus, London Mathematical Society Student Texts No. 1, Cambridge University Press, Cambridge, UK.
  • Lambek, J. and Scott, P.J. (1986), Introduction To Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.

Basic Concepts from Lambek and Scott (1986)

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

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

Concrete Category

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

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

(Lambek & Scott, 4–5).

Graph

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

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

One writes for A graph is said to be small if the classes of objects and arrows are sets.

(Lambek & Scott, 5).

Deductive System

A deductive system is a graph in which to each object there is associated an arrow the identity arrow, and to each pair of arrows and there is associated an arrow the composition of with A logician may think of the objects as formulas and of the arrows as deductions or proofs, hence of

as a rule of inference.

(Lambek & Scott, 5).

Category

A category is a deductive system in which the following equations hold, for all and

(Lambek & Scott, 5).

Functor

Definition 1.3. A functor is first of all a morphism of graphs …, that is, it sends objects of to objects of and arrows of to arrows of such that, if then Moreover, a functor preserves identities and composition; thus:

In particular, the identity functor leaves objects and arrows unchanged and the composition of functors and is given by:

for all objects of and all arrows in

(Lambek & Scott, 6).

Natural Transformation

Definition 2.1. Given functors a natural transformation is a family of arrows in one arrow for each object of such that the following square commutes for all arrows in :

              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

(Lambek & Scott, 8).

Graph 2

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

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

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

one often writes or We shall look at graphs with additional structure which are of interest in logic.

(Lambek & Scott, 47).

Deductive System 2

A deductive system is a graph with a specified arrow

and a binary operation on arrows (composition)

(Lambek & Scott, 47).

Conjunction Calculus

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

(Lambek & Scott, 47–48).

Positive Intuitionistic Propositional Calculus

A positive intuitionistic propositional calculus is a conjunction calculus with an additional binary operation ( = if). Thus, if and are formulas, so are and (Yes, most people write instead.) We also specify the following new arrow and rule of inference.

(Lambek & Scott, 48–49).

Intuitionistic Propositional Calculus

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

(Lambek & Scott, 49–50).

Classical Propositional Calculus

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

(Lambek & Scott, 50).

Category 2

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

(Lambek & Scott, 52).

Cartesian Category

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

(Lambek & Scott, 52).

Cartesian Closed Category

A cartesian closed category is a cartesian category with additional structure satisfying the additional equations:

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

(Lambek & Scott, 53).

Document History

Inquiry List • Series A • Jun–Jul 2004

  1. http://web.archive.org/web/20060217223327/http://stderr.org/pipermail/inquiry/2004-June/001643.html
  2. http://web.archive.org/web/20060217223346/http://stderr.org/pipermail/inquiry/2004-June/001644.html
  3. http://web.archive.org/web/20060217223352/http://stderr.org/pipermail/inquiry/2004-June/001645.html
  4. http://web.archive.org/web/20130128191457/http://stderr.org/pipermail/inquiry/2004-June/001660.html
  5. http://web.archive.org/web/20130128191500/http://stderr.org/pipermail/inquiry/2004-June/001648.html
  6. http://web.archive.org/web/20130128191502/http://stderr.org/pipermail/inquiry/2004-June/001649.html
  7. http://web.archive.org/web/20130128191504/http://stderr.org/pipermail/inquiry/2004-June/001656.html
  8. http://web.archive.org/web/20060217223450/http://stderr.org/pipermail/inquiry/2004-June/001657.html
  9. http://web.archive.org/web/20060217223458/http://stderr.org/pipermail/inquiry/2004-June/001658.html
  10. http://web.archive.org/web/20130128191512/http://stderr.org/pipermail/inquiry/2004-June/001659.html
  11. http://web.archive.org/web/20130128191513/http://stderr.org/pipermail/inquiry/2004-June/001661.html
  12. http://web.archive.org/web/20130128191515/http://stderr.org/pipermail/inquiry/2004-June/001662.html
  13. http://web.archive.org/web/20060217223522/http://stderr.org/pipermail/inquiry/2004-June/001664.html
  14. http://web.archive.org/web/20060217223528/http://stderr.org/pipermail/inquiry/2004-June/001665.html
  15. http://web.archive.org/web/20130128191522/http://stderr.org/pipermail/inquiry/2004-June/001666.html
  16. http://web.archive.org/web/20130128191524/http://stderr.org/pipermail/inquiry/2004-June/001667.html
  17. http://web.archive.org/web/20130128191526/http://stderr.org/pipermail/inquiry/2004-June/001668.html
  18. http://web.archive.org/web/20130128191528/http://stderr.org/pipermail/inquiry/2004-June/001670.html
  19. http://web.archive.org/web/20130128191530/http://stderr.org/pipermail/inquiry/2004-June/001671.html
  20. http://web.archive.org/web/20130128191532/http://stderr.org/pipermail/inquiry/2004-June/001672.html
  21. http://web.archive.org/web/20130128191534/http://stderr.org/pipermail/inquiry/2004-June/001673.html
  22. http://web.archive.org/web/20130128191536/http://stderr.org/pipermail/inquiry/2004-June/001674.html
  23. http://web.archive.org/web/20061013232850/http://stderr.org/pipermail/inquiry/2004-July/001677.html

Inquiry List • Series B • Jun–Jul 2004

  1. http://web.archive.org/web/20060217223358/http://stderr.org/pipermail/inquiry/2004-June/001647.html
  2. http://web.archive.org/web/20060217223516/http://stderr.org/pipermail/inquiry/2004-June/001663.html
  3. http://web.archive.org/web/20130128191544/http://stderr.org/pipermail/inquiry/2004-June/001669.html
  4. http://web.archive.org/web/20061013232825/http://stderr.org/pipermail/inquiry/2004-July/001684.html

NKS Forum • Series B • Jun–Jul 2004

Inquiry List • Jul 2005

  1. http://web.archive.org/web/20061014000520/http://stderr.org/pipermail/inquiry/2005-July/002872.html
  2. http://web.archive.org/web/20130128183518/http://stderr.org/pipermail/inquiry/2005-July/002873.html
  3. http://web.archive.org/web/20061014000205/http://stderr.org/pipermail/inquiry/2005-July/002874.html
  4. http://web.archive.org/web/20061014000323/http://stderr.org/pipermail/inquiry/2005-July/002875.html
  5. http://web.archive.org/web/20061014000419/http://stderr.org/pipermail/inquiry/2005-July/002876.html
  6. http://web.archive.org/web/20061014000249/http://stderr.org/pipermail/inquiry/2005-July/002877.html
  7. http://web.archive.org/web/20061014000220/http://stderr.org/pipermail/inquiry/2005-July/002878.html
  8. http://web.archive.org/web/20061014000332/http://stderr.org/pipermail/inquiry/2005-July/002879.html
  9. http://web.archive.org/web/20110822051414/http://stderr.org/pipermail/inquiry/2005-July/002880.html
  10. http://web.archive.org/web/20061014000313/http://stderr.org/pipermail/inquiry/2005-July/002881.html
  11. http://web.archive.org/web/20061014000224/http://stderr.org/pipermail/inquiry/2005-July/002882.html
  12. http://web.archive.org/web/20110822051422/http://stderr.org/pipermail/inquiry/2005-July/002883.html
  13. http://web.archive.org/web/20061014000408/http://stderr.org/pipermail/inquiry/2005-July/002884.html
  14. http://web.archive.org/web/20110822051441/http://stderr.org/pipermail/inquiry/2005-July/002885.html
  15. http://web.archive.org/web/20061014000455/http://stderr.org/pipermail/inquiry/2005-July/002886.html
  16. http://web.archive.org/web/20110822051447/http://stderr.org/pipermail/inquiry/2005-July/002887.html
  17. http://web.archive.org/web/20061014000404/http://stderr.org/pipermail/inquiry/2005-July/002888.html
  18. http://web.archive.org/web/20061014000232/http://stderr.org/pipermail/inquiry/2005-July/002889.html
  19. http://web.archive.org/web/20061014000357/http://stderr.org/pipermail/inquiry/2005-July/002890.html
  20. http://web.archive.org/web/20110822051506/http://stderr.org/pipermail/inquiry/2005-July/002891.html
  21. http://web.archive.org/web/20061014000344/http://stderr.org/pipermail/inquiry/2005-July/002892.html
  22. http://web.archive.org/web/20061014000445/http://stderr.org/pipermail/inquiry/2005-July/002893.html
  23. http://web.archive.org/web/20061014000422/http://stderr.org/pipermail/inquiry/2005-July/002894.html

Inquiry List • Commentary • Jul 2005

  1. http://web.archive.org/web/20121111053022/http://stderr.org/pipermail/inquiry/2005-July/002895.html
  2. http://web.archive.org/web/20130128183445/http://stderr.org/pipermail/inquiry/2005-July/002896.html