[Inquiry] Re: Propositions As Types -- Series A

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

PAT.  Note A12

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Self-Documentation, Developmental Data Structures (cont.)

Redo the 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.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o