12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:42, 24 March 2009
, 12:42, 24 March 2009→Step 4: move motto
===Step 4===
===Step 4===
'''Term Development : Contextual Definition <math>\rightsquigarrow</math> Combinator Construction'''
Consider the parse tree of the term <math>\operatorname{I}</math> in terms of the primitive combinators <math>\operatorname{K}</math> and <math>\operatorname{S},</math> that is, the articulation or construction corresponding to the term equation <math>\operatorname{I} = (\operatorname{K}(\operatorname{K}\operatorname{S})),</math> as shown here:
Consider the parse tree of the term <math>\operatorname{I}</math> in terms of the primitive combinators <math>\operatorname{K}</math> and <math>\operatorname{S},</math> that is, the articulation or construction corresponding to the term equation <math>\operatorname{I} = (\operatorname{K}(\operatorname{K}\operatorname{S})),</math> as shown here:
Adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of <math>\operatorname{I} : A \Rightarrow A.</math> Thus, the construal or construction of <math>\operatorname{I}</math> as <math>\operatorname{K}(\operatorname{K}\operatorname{S})</math> constitutes a hint or clue to the proof of <math>A \Rightarrow A</math> in the intuitionistic propositional calculus. Although guesswork may succeed in easy cases such as this, a more systematic procedure is to follow the development in Step 1, that takes us from contextual specification to operational algorithm, and to carry along the type information as we go, ending up with a typed parse tree for <math>\operatorname{I},</math> tantamount to a proof tree for <math>A \Rightarrow A.</math>
Adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of <math>\operatorname{I} : A \Rightarrow A.</math> Thus, the construal or construction of <math>\operatorname{I}</math> as <math>\operatorname{K}(\operatorname{K}\operatorname{S})</math> constitutes a hint or clue to the proof of <math>A \Rightarrow A</math> in the intuitionistic propositional calculus. Although guesswork may succeed in easy cases such as this, a more systematic procedure is to follow the development in Step 1, that takes us from contextual specification to operational algorithm, and to carry along the type information as we go, ending up with a typed parse tree for <math>\operatorname{I},</math> tantamount to a proof tree for <math>A \Rightarrow A.</math>
<pre>
<pre>