12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 17:37, 25 March 2009
, 17:37, 25 March 2009→Step 4: markup
Incidentally, note the inobtrusive appearance of renaming strategies in the progress of this work. Renaming is the natural operation that substitution is the reverse of. With these humble beginnings we have reached a birthplace, a native ground, of the [[sign relation]], an irreducible three-place relationship among what is indicated, what happens to indicate it, and all of the equivalent or associated indications we may find or create in reference to it.
Incidentally, note the inobtrusive appearance of renaming strategies in the progress of this work. Renaming is the natural operation that substitution is the reverse of. With these humble beginnings we have reached a birthplace, a native ground, of the [[sign relation]], an irreducible three-place relationship among what is indicated, what happens to indicate it, and all of the equivalent or associated indications we may find or create in reference to it.
For example, let <math>^{\backprime\backprime} \operatorname{G} ^{\prime\prime},</math> the interposed interpretant, denote whatever it is, the supposed object, that <math>^{\backprime\backprime} (\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) ^{\prime\prime},</math> the occurrent sign, denotes.
For example, let the interposed interpretant <math>^{\backprime\backprime} \operatorname{G} ^{\prime\prime}</math> denote the supposed object, namely, whatever it is that the occurrent sign <math>^{\backprime\backprime} (\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) ^{\prime\prime}</math> denotes.
Consider the following data:
Consider the following data:
:* The parse tree for the term <math>\operatorname{T} = ((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))</math>
:* The type marker of the term <math>\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C))</math>
<pre>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
Can proofs be developed by tracing the stepwise articulation or
Can proofs be developed by tracing the stepwise articulation or explication of the untyped proof hint, typing each term as we go?
explication of the untyped proof hint, typing each term as we go?
For example, we might begin as follows:
For example, we might begin as follows:
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| |
| |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
If this strategy is successful it suggests that the proof tree can
If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term.
be grown in a stepwise equational fashion from a seed term of the
appropriate species, in other words, from a contextual, embedded,
or paraphrastic specification of the desired term.
Thus, these developments culminate in the rather striking and
Thus, these developments culminate in the rather striking and possibly disconcerting consequence that the apparent flow of information or reasoning in the proof tree is something of a put-up job, a snapshot likeness or a likely story that calls to mind the anatomy of a justification, but fails to reconstruct the true embryology or living physiology of discovery involved.
possibly disconcerting consequence that the apparent flow of
information or reasoning in the proof tree is something of
a put-up job, a snapshot likeness or a likely story that
calls to mind the anatomy of a justification, but fails
to reconstruct the true embryology or living physiology
of discovery involved.
Repeat the development in Step 1,
Repeat the development in Step 1, but this time articulating the type information as we go.
but this time articulating the
type information as we go.
<pre>
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
| |
| |