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

[Jon Awbrey]

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

PAT.  Note A11

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

Self-Documentation

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

For example, the development of the Identity combinator:

   x  =  (xK)(xK)  =  x(K(KS))

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

Jon Awbrey

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