12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 19:26, 24 March 2009
, 19:26, 24 March 2009→Step 4: markup
===Step 4===
===Step 4===
Repeat the development in Step 1, but this time articulating the type information as we go.
<pre>
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
| |
| |
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
The foregoing development has taken us from the
The foregoing development has taken us from the typed parse tree for the definiens <math>((xy)z)\!</math> to the typed parse tree for the explicated definiendum <math>(x(y(z(\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))~))),</math> which gives us both the construction of the composition combinator <math>\operatorname{P}</math> in terms of primitive combinators:
typed parse tree for the definiens ((xy)z) to the
typed parse tree for the explicated definiendum
(x(y(z(K((SK)S)) ))), which gives us both the
construction of the composition combinator P
in terms of primitive combinators:
{| align="center" cellpadding="8" width="90%"
| <math>\begin{matrix}\operatorname{P} & = & (\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S}))\end{matrix}</math>
|}
and also the proof tree for the proposition type of P:
and also the proof tree for the type proposition of <math>\operatorname{P},</math> as follows:
<pre>
S K
S K
o o
o o