12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:32, 25 March 2009
, 12:32, 25 March 2009→Transposition, or the Transposer: markup
===Step 2===
===Step 2===
Using the contextual definition of the transposer <math>\operatorname{T},</math>
Using the contextual definition of the transposer T,
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}x(y(z\operatorname{T})) & = & y(xz)\end{matrix}</math>
|}
find a minimal generic typing (simplest non-degenerate typing) of
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.
each term in the specification that makes all of the applications
on each side of the equation go through.
<pre>
For example, here is one such typing:
For example, here is one such typing: