12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 17:49, 24 March 2009
, 17:49, 24 March 2009→Step 2: markup
<math>\begin{array}{l}
<math>\begin{array}{l}
((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow}
((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow}
\\[10pt]
\\ \\
=
=
\\[10pt]
\\ \\
(x \underset{A}{\Downarrow}
(x \underset{A}{\Downarrow}
~ (y \overset{A}{\underset{B}{\Downarrow}}
~ (y \overset{A}{\underset{B}{\Downarrow}}
\end{array}</math>
\end{array}</math>
|}
|}
Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math>
<pre>
<pre>
Note that the explication of P as a term K((SK)S) of
Note that the explication of P as a term K((SK)S) of
type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof
type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof