12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 23:08, 22 March 2009
, 23:08, 22 March 2009segment
{{DISPLAYTITLE:Propositions As Types}}
{{DISPLAYTITLE:Propositions As Types}}
==Note 1==
<pre>
Identity, or the Identifier
Identity, or the Identifier
Check.
Check.
</pre>
==Note 2==
<pre>
Identity, or the Identifier (cont.)
Identity, or the Identifier (cont.)
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.
</pre>
==Note 3==
<pre>
Identity, or the Identifier (cont.)
Identity, or the Identifier (cont.)
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
==Note 4==
<pre>
| NB. I am working from rough notes that
| NB. I am working from rough notes that
| I wrote out in the Fall of 1996, and it
| I wrote out in the Fall of 1996, and it
Therefore, the type of the application K(KS) is A=>A.
Therefore, the type of the application K(KS) is A=>A.
</pre>
==Note 5==
<pre>
Composition, or the Composer
Composition, or the Composer
P = (K((SK)S))
P = (K((SK)S))
</pre>
==Note 6==
<pre>
Composition, or the Composer (cont.)
Composition, or the Composer (cont.)
propositional calculus, based on the combinator axioms,
propositional calculus, based on the combinator axioms,
K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).
K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).
</pre>
==Note 7==
<pre>
Composition, or the Composer (cont.)
Composition, or the Composer (cont.)
QED.
QED.
</pre>
==Note 8==
<pre>
Composition, or the Composer (cont.)
Composition, or the Composer (cont.)
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
==Note 9==
<pre>
Composition, or the Composer (cont.)
Composition, or the Composer (cont.)
P = (K((SK)S)) : (B=>C)=>((A=>B)=>(A=>C))
P = (K((SK)S)) : (B=>C)=>((A=>B)=>(A=>C))
</pre>
==Note 10==
<pre>
Composition, or the Composer (concl.)
Composition, or the Composer (concl.)
amounting in effect to "Facts" being recycled as "Cases".
amounting in effect to "Facts" being recycled as "Cases".
Square brackets are also used to mark the intended result.
Square brackets are also used to mark the intended result.
</pre>
==Note 11==
<pre>
Self-Documentation
Self-Documentation
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
==Note 12==
<pre>
Self-Documentation, Developmental Data Structures (cont.)
Self-Documentation, Developmental Data Structures (cont.)
That's the sketch as best I can reconstruct it from my notes.
That's the sketch as best I can reconstruct it from my notes.
</pre>
==Note 13==
<pre>
Triadic Analogy: Analogy Between a Couple of Three-Place Relations
Triadic Analogy: Analogy Between a Couple of Three-Place Relations
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
==Note 14==
<pre>
Transposition, or the Transposer
Transposition, or the Transposer
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.
</pre>
==Note 15==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
T = (KK)(((S((KK)S))((SK)S))S)
T = (KK)(((S((KK)S))((SK)S))S)
</pre>
==Note 16==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
read as a proposition, is a theorem of intuitionistic
read as a proposition, is a theorem of intuitionistic
propositional calculus.
propositional calculus.
</pre>
==Note 17==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
==Note 18==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
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.
</pre>
==Note 19==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
==Note 20==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
to reconstruct the true embryology or living physiology
to reconstruct the true embryology or living physiology
of discovery involved.
of discovery involved.
</pre>
==Note 21==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
==Note 22==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
| |
| |
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
</pre>
==Note 23==
<pre>
Transposition, or the Transposer (cont.)
Transposition, or the Transposer (cont.)
o---------------------------------------------------------------------o
o---------------------------------------------------------------------o
<pre>
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o