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

[Jon Awbrey]

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

PAT.  Note A19

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

Transposition, or the Transposer (cont.)

Step 4 (cont.)

Consider the following data:

The parse tree of the term T = ((KK)(((S((KK)S))((SK)S))S))
and the typing of the term T : (A=>(B=>C))=>(B=>(A=>C)). 

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

Can proofs be developed by tracing the stepwise articulation or
explication of the untyped proof hint, typing each term as we go?

For example, we might begin as follows:

o-----------------------------------------------------------o
|                                                           |
|            B=>C  C                                        |
|   (y: (x: z:    ): ):                                     |
|     B   A  A     B  C                                     |
|                                                           |
o===========================================================o
|                                                           |
|             A=>B  B         B=>C  C                       |
|   ((x: (y: K:    ): ): (x: z:    ): ):                    |
|      A   B  B     A  B   A  A     B  C                    |
|                                                           |
o===========================================================o
|                                                           |
|             A=>B  B   B=>C  (A=>B)=>(A=>C)  A=>C  C       |
|   (x: ((y: K:    ): (z:    S:              ):    ): ):    |
|     A    B  B     A   A     A=>(B=>C)       A=>B  A  C    |
|                                                           |
o===========================================================o
|                                                           |
|   ...                                                     |
|                                                           |
o-----------------------------------------------------------o

Jon Awbrey

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