Line 56: |
Line 56: |
| | | |
| ===Step 4=== | | ===Step 4=== |
| + | |
| + | 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: |
| | | |
| <pre> | | <pre> |
− | If we start from the parse tree of the term I in terms of
| |
− | the primitive combinators K and S, that is, the articulation
| |
− | or construction corresponding to the term equation I = (K(KS)),
| |
− |
| |
| K S | | K S |
| o o | | o o |
Line 67: |
Line 65: |
| o (o) | | o (o) |
| \ / | | \ / |
− | I = (o) , | + | I = (o) |
| + | </pre> |
| | | |
− | then adding appropriate type-indices to the nodes of this tree will
| + | 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> |
− | leave us with a proof tree for the propositional type of I : A => A. | |
− | Thus, the construal or construction of I as K(KS) constitutes a hint | |
− | or clue to the proof of A => A 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 I, tantamount to a proof tree for A => A. | |
| | | |
− | Term Development: Contextual Definition ~~~> Combinator Construction | + | {| align="center" cellpadding="8" width="90%" |
| + | | <math>\text{Term Development : Contextual Definition} \rightsquigarrow \text{Combinator Construction}</math> |
| + | |} |
| | | |
| + | <pre> |
| o-----------------------------------------------------------o | | o-----------------------------------------------------------o |
| | | | | | | |