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

[Jon Awbrey]

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

PAT.  Note A9

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

Composition, or the Composer (cont.)

Step 4 (concl.)

The foregoing development has taken us from the
typed parse tree for the definiens ((xy)z) to the
typed parse tree for the explicated definiendum
(x(y(z(K((SK)S)) ))), which gives us both the
construction of the composition combinator P
in terms of primitive combinators:

   P  =  (K((SK)S))

and also the proof tree for the proposition type of P:

        S   K
        o   o
         \ /  S
         (o)  o
        K  \ /
        o  (o)
         \ /
   P  =  (o)

   P  =  (K((SK)S))  :  (B=>C)=>((A=>B)=>(A=>C))

Jon Awbrey

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