12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 14:54, 24 March 2009
, 14:54, 24 March 2009→Step 1: markup
We are asked to find an explication of <math>\operatorname{P}</math> in terms of primitive combinators.
We are asked to find an explication of <math>\operatorname{P}</math> in terms of primitive combinators.
Proceed as follows:
Proceed as follows:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{array}{ccccc}
(xy)z
& = &
(xy)(x(z\operatorname{K}))
& = &
x(y((z\operatorname{K})\operatorname{S}))
\\[8pt]
(z\operatorname{K})\operatorname{S}
& = &
</pre>
(z\operatorname{K})(z(\operatorname{S}\operatorname{K}))
& = &
z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))
\\[6pt]
& & \Downarrow
\\[8pt]
x(y(z\operatorname{P}))
& = &
(xy)z
& = &
x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))))
\\[8pt]
& & \Downarrow
\\[8pt]
\operatorname{P}
& = &
(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))
\end{array}</math>
|}
===Step 2===
===Step 2===