12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 19:30, 25 March 2009
, 19:30, 25 March 2009→Step 5
Rewrite the final proof tree in existential graph format, implementing structure sharing among application triples by overlaying the type propositions that attach to terms.
Rewrite the final proof tree in existential graph format, implementing structure sharing among application triples by overlaying the type propositions that attach to terms.
<pre>
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
</pre>
; Graphic Conventions
: Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, tantamount to recycling ''Facts'' as ''Cases''. Square brackets are also used to indicate the final result.
===Step 5 (Extended)===
===Step 5 (Extended)===