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

[Jon Awbrey]

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

PAT.  Note A14

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

Transposition, or the Transposer

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

This equation constitutes a "paraphrastic definition"
of T, a definition-in-context, or a formal syntactic
specification of how the operator is required to act
on other symbols.

Step 1.

Find a "pure interpretant" for T, that is, an equivalent term
doing the job of T which is constructed purely in terms of the
primitive combinators K and S.

This will constitute an operational algorithm for T, though
still operating at the level of abstract syntax, understood
as a sequence of manipulations on formal identifiers, or on
symbols taken as objects in themselves.

Jon Awbrey

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