[Inquiry] Re: Propositions As Types

[Jon Awbrey]

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

PAT.  Note 2

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

1.  Identity, or the Identifier (cont.)

Step 4.

If we start from the parse tree of the term I in terms of
the primitive combinators K and S, that is, the articulation
or construction corresponding to the term equation I = (K(KS)),

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

then adding appropriate type-indices to the nodes of this tree will
leave us with a proof tree for the propositional type of I : A => A.
Thus, the construal or construction of I as K(KS) constitutes a hint
or clue to the proof of A => A in the intuitionistic propositional
calculus.  Although guesswork may suceed 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 I, tantamount to a proof tree for A => A.

Jon Awbrey

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