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

[Jon Awbrey]

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

PAT.  Note A16

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

Transposition, or the Transposer (cont.)

Step 2.

Using the contextual definition of the transposer T,

   y(xz)  =  x(y(zT)),

find a minimal generic typing (simplest non-degenerate typing) of
each term in the specification that makes all of the applications
on each side of the equation go through.

For example, here is one such typing:

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

In a contextual, implicit, or paraphrastic definition of this sort,
the "definiendum" is the symbol to be defined, in this case, "T",
and the "definiens" is the entire rest of the context, in this
case, the frame "y(xz) = x(y(z__))", that ostensibly defines,
or as one says, is supposed to define the symbol "T" that
we find in its slot.  More loosely speaking, the side of
the equation with the more known symbols may be called
its "defining" side.

In order to find a minimal generic typing, start with the defining side
of the equation, freely assigning types in such a way that the successive
applications make sense, but without introducing unnecessary complications
or creating unduly specialized applications.  Then work out what the type
of the defined operator T has to be, in order to function properly in the
standard context, in this case, (x(y(z__))).

Again, this gives:

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

Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type,
read as a proposition, is a theorem of intuitionistic
propositional calculus.

Jon Awbrey

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