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

[Jon Awbrey]

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

PAT.  Note A15

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

Transposition, or the Transposer (cont.)

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

Step 1 (concl.)

Observe that y(xz) matches (xy)(xz) on the right,
and that we can express y as x(yK), consequently:

   y(xz)  =  (x(yK))(xz)

          =  x((yK)(zS))

thus completing the abstraction (or disentanglement)
of x from the expression.

Working on the remainder of the expression,
the next item of business is to abstract y.

Notice that:

   (yK)(zS)  =  (yK)(y((zS)K))

             =  y(K(((zS)K)S))

thus completing the abstraction of y.

Next, work on K(((zS)K)S) to extract z, starting from
the center (zS)K of the labyrinth and working outward:

   (zS)K  =  (zS)(z(KK))

          =  z(S((KK)S))

For the sake of brevity in the rest of this development,
rename the operator on the right so that (S((KK)S)) = F.

Continue with K((zF)S), to extract z:

   (zF)S  =  (zF)(z(SK))

          =  z(F((SK)S))

Rename the operator on the right, letting (F((SK)S)) = G.

Continue with K(zG), to extract z:

   K(zG)  =  (z(KK))(zG)

          =  z((KK)(GS))

Filling in the abbreviations:

   y(xz)  =  x(y(z((KK)(GS)) ))

          =  x(y(z((KK)((F((SK)S))S)) ))

          =  x(y(z((KK)(((S((KK)S))((SK)S))S)) ))

Thus we have:

   T  =  (KK)(((S((KK)S))((SK)S))S)

Jon Awbrey

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