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

[Jon Awbrey]

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

PAT.  Note A6

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

Composition, or the Composer (cont.)

Step 2.

Assign types in the specification:

         B    C
   ((x: y:): z:):
      A  A B  B C

   =

         B   C  (A=>B)=>(A=>C) A=>C C
   (x: (y: (z: P:             ):   ):):
     A   A   B  B=>C           A=>B A C

Here, a notation of the form:

   x:
    A

means that x is of the type A,
while a notation of the form:

    B
   x:
    A

means that x is of the type A=>B.

Note that the explication of P as a term K((SK)S) of
type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof
of P's type proposition as a theorem of intuitionistic
propositional calculus, based on the combinator axioms,
K : A => (B=>A) and S : (A=>(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