12,140
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 13:00, 23 March 2009
, 13:00, 23 March 2009descriptive headings
{{DISPLAYTITLE:Propositions As Types}}
{{DISPLAYTITLE:Propositions As Types}}
==Note 1==
==Identity, or the Identifier==
===Step 1===
<pre>
<pre>
Given a syntactic specification (or paraphrastic definition):
Given a syntactic specification (or paraphrastic definition):
and so K(KS) constitutes a syntactic algorithm for I.
and so K(KS) constitutes a syntactic algorithm for I.
</pre>
Step 2.
===Step 2===
<pre>
Assign types in the specification:
Assign types in the specification:
whose type, read as a proposition, is a theorem of
whose type, read as a proposition, is a theorem of
intuitionistic propositional calculus.
intuitionistic propositional calculus.
</pre>
Step 3 (optional).
===Step 3 (Optional)===
<pre>
Check that A => A is a theorem of classical propositional calculus.
Check that A => A is a theorem of classical propositional calculus.
</pre>
</pre>
==Note 2==
===Step 4===
<pre>
<pre>
If we start from the parse tree of the term I in terms of
If we start from the parse tree of the term I in terms of
the primitive combinators K and S, that is, the articulation
the primitive combinators K and S, that is, the articulation
and to carry along the type information as we go, ending up with
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.
a typed parse tree for I, tantamount to a proof tree for A => A.
Term Development: Contextual Definition ~~~> Combinator Construction
Term Development: Contextual Definition ~~~> Combinator Construction
</pre>
</pre>
==Note 4==
===Step 5===
<pre>
<pre>
| causing me to leave out a few steps.
| causing me to leave out a few steps.
Existential Graph Format, Application Triples with Structure Sharing.
Existential Graph Format,
Application Triples with
Structure Sharing.
Same development in Existential Graph notation.
Same development in Existential Graph notation.
</pre>
</pre>
==Note 5==
==Composition, or the Composer==
===Step 1.===
<pre>
<pre>
Given a specification of the "composition combinator",
Given a specification of the "composition combinator",
or the "composer" P, that has the following effects:
or the "composer" P, that has the following effects:
</pre>
</pre>
==Note 6==
===Step 2===
<pre>
<pre>
Assign types in the specification:
Assign types in the specification:
</pre>
</pre>
==Note 7==
===Step 3 (Optional)===
<pre>
<pre>
Check that the propositional type of the composer P is a theorem
Check that the propositional type of the composer P is a theorem
of classical propositional calculus, which is logically necessary
of classical propositional calculus, which is logically necessary
</pre>
</pre>
==Note 8==
===Step 4===
<pre>
<pre>
Repeat the development in Step 1,
Repeat the development in Step 1,
but this time articulating the
but this time articulating the
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
The foregoing development has taken us from the
The foregoing development has taken us from the
</pre>
</pre>
==Note 10==
===Step 5===
<pre>
<pre>
Rewrite the final proof tree in existential graph format:
Rewrite the final proof tree in existential graph format:
</pre>
</pre>
==Note 11==
==Self-Documentation : Developmental Data Structures==
<pre>
<pre>
Observation. Notice the "self-documenting" property
Observation. Notice the "self-documenting" property
of proof developments in the existential graph format,
of proof developments in the existential graph format,
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
Redo the entire development of the Composer in existential graph format:
Redo the entire development of the Composer in existential graph format:
</pre>
</pre>
==Note 13==
==Triadic Analogy : Analogy Between Two Triadic Relations==
<pre>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
</pre>
</pre>
==Note 14==
==Transposition, or the Transposer==
<pre>
<pre>
x(y(zT)) = y(xz)
x(y(zT)) = y(xz)
specification of how the operator is required to act
specification of how the operator is required to act
on other symbols.
on other symbols.
</pre>
Step 1.
===Step 1===
Find a "pure interpretant" for T, that is, an equivalent term
Find a "pure interpretant" for T, that is, an equivalent term
as a sequence of manipulations on formal identifiers, or on
as a sequence of manipulations on formal identifiers, or on
symbols taken as objects in themselves.
symbols taken as objects in themselves.
x(y(zT)) = y(xz)
x(y(zT)) = y(xz)
Observe that y(xz) matches (xy)(xz) on the right,
Observe that y(xz) matches (xy)(xz) on the right,
</pre>
</pre>
==Note 16==
===Step 2===
<pre>
<pre>
Using the contextual definition of the transposer T,
Using the contextual definition of the transposer T,
</pre>
</pre>
==Note 17==
===Step 3 (Optional)===
<pre>
<pre>
At this juncture we might want to verify that the proposition corresponding
At this juncture we might want to verify that the proposition corresponding
to the type of T is actually a theorem of classical propositional calculus.
to the type of T is actually a theorem of classical propositional calculus.
</pre>
</pre>
==Note 18==
===Step 4===
<pre>
<pre>
The construction of the term T of the appropriate type in terms of the
The construction of the term T of the appropriate type in terms of the
primitive typed combinators of the forms K and S is analogous to the
primitive typed combinators of the forms K and S is analogous to the
denote whatever it is, the supposed object, that
denote whatever it is, the supposed object, that
"(F((SK)S))", the occurrent sign, denotes.
"(F((SK)S))", the occurrent sign, denotes.
Consider the following data:
Consider the following data:
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
If this strategy is successful it suggests that the proof tree can
If this strategy is successful it suggests that the proof tree can
to reconstruct the true embryology or living physiology
to reconstruct the true embryology or living physiology
of discovery involved.
of discovery involved.
Repeat the development in Step 1,
Repeat the development in Step 1,
</pre>
</pre>
==Note 22==
===Step 5===
<pre>
<pre>
Rewrite the final proof tree in existential graph format,
Rewrite the final proof tree in existential graph format,
implementing structure sharing among application triples
implementing structure sharing among application triples
</pre>
</pre>
==Note 23==
===Step 5 (Extended)===
<pre>
<pre>
Redo the development of the proof tree in existential graph format.
Redo the development of the proof tree in existential graph format.