[Inquiry] Re: Propositions As Types -- Correction

[Jon Awbrey]

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

PAT.  Note A4

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

| NB.  I am working from rough notes that
| I wrote out in the Fall of 1996, and it
| is not always easy to reconstruct what
| I had in mind at the time.  I misread
| this passage in my last posting of it,
| causing me to leave out a few steps.

1.  Identity, or the Identifier (cont.)

Step 5.

Existential Graph Format,
Application Triples with
Structure Sharing.

Same development in Existential Graph notation.
Here I am carrying out the term development in
reverse, that is, in application order.

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

| I am still not sure what order I intended for the
| application triples, but this is one likely guess:

For example:

The nodes that are right-labeled <K, KS, K(KS)>,
in that order, constitute an application triple.

The type of the applicand K is A=>(B=>A).

The type of the applicator KS is (A=>(B=>A))=>(A=>A).

Therefore, the type of the application K(KS) is A=>A.

Jon Awbrey

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