12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 02:36, 25 March 2009
, 02:36, 25 March 2009→Step 1: markup
Working on the remainder of the expression, the next item of business is to abstract <math>y.\!</math>
Working on the remainder of the expression, the next item of business is to abstract <math>y.\!</math>
Notice that:
Notice that:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
(y\operatorname{K})(z\operatorname{S})
& = &
(y\operatorname{K})(y((z\operatorname{S})\operatorname{K}))
\\[8pt]
& = &
y(\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S}))
\end{matrix}</math>
|}
thus completing the abstraction of <math>y.\!</math>
thus completing the abstraction of y.
<pre>
Next, work on K(((zS)K)S) to extract z, starting from
Next, work on K(((zS)K)S) to extract z, starting from
the center (zS)K of the labyrinth and working outward:
the center (zS)K of the labyrinth and working outward: