Changes

MyWikiBiz, Author Your Legacy — Wednesday May 01, 2024
Jump to navigationJump to search

Directory:Jon Awbrey/Papers/Propositions As Types (view source)

Revision as of 23:54, 6 July 2013

1,534 bytes added ,  23:54, 6 July 2013
no edit summary
Line 1: Line 1:  
{{DISPLAYTITLE:Propositions As Types}}
 
{{DISPLAYTITLE:Propositions As Types}}
 +
 +
'''NB.''' In this discussion, combinators are being applied on the right of their arguments.  The resulting formulas will look backwards to people who are accustomed to applying combinators on the left.
    
==Identity, or the Identifier==
 
==Identity, or the Identifier==
Line 2,223: Line 2,225:  
==Bibliography==
 
==Bibliography==
   −
Here are a three references on combinatory logic and lambda calculus, given in order of difficulty from introductory to advanced, that are especially pertinent to the use of combinators in computer science:
+
Here are three references on combinatory logic and lambda calculus, given in order of difficulty from introductory to advanced, that are especially pertinent to the use of combinators in computer science:
    
# Smullyan, R. (1985), ''To Mock a Mockingbird, And Other Logic Puzzles, Including an Amazing Adventure in Combinatory Logic'', Alfred A. Knopf, New York, NY.
 
# Smullyan, R. (1985), ''To Mock a Mockingbird, And Other Logic Puzzles, Including an Amazing Adventure in Combinatory Logic'', Alfred A. Knopf, New York, NY.
Line 2,292: Line 2,294:  
|-
 
|-
 
|
 
|
−
<p>(Lambek & Scott, 5).
+
<p>(Lambek & Scott, 5).</p>
 
|}
 
|}
   Line 2,420: Line 2,422:  
|
 
|
 
<p><math>\begin{array}{ll}
 
<p><math>\begin{array}{ll}
−
\text{R4a.} & (A \Leftarrow B) \land B \xrightarrow{~\varepsilon_{A, B}~} A,
+
\text{R4a.} & (A \Leftarrow B) \land B ~\xrightarrow{~\varepsilon_{A, B}~}~ A,
 
\\[8pt]
 
\\[8pt]
−
\text{R4b.} & \dfrac{C \land B \xrightarrow{~h~} A}{C \xrightarrow{~h^*~} A \Leftarrow B}.
+
\text{R4b.} & \dfrac{~ C \land B ~\xrightarrow{~h~}~ A ~}{~ C ~\xrightarrow{~h^*~}~ A \Leftarrow B ~}.
 
\end{array}</math></p>
 
\end{array}</math></p>
 
|-
 
|-
Line 2,447: Line 2,449:  
|-
 
|-
 
|
 
|
−
<p>(Lambek & Scott, 49&ndash;50).
+
<p>(Lambek & Scott, 49&ndash;50).</p>
 
|}
 
|}
    
===Classical Propositional Calculus===
 
===Classical Propositional Calculus===
   −
<pre>
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| If we want 'classical' propositional logic, we must also require:
+
|
 +
<p>If we want ''classical'' propositional logic, we must also require:
 +
|-
 +
|
 +
<p><math>\begin{array}{ll}
 +
\text{R7.} & (\bot \Leftarrow (\bot \Leftarrow A)) \to A.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| R7.  F <= (F <= A) -> A.
+
<p>(Lambek & Scott, 50).</p>
−
</pre>
+
|}
    
===Category 2===
 
===Category 2===
   −
<pre>
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| A 'category' is a deductive system in which
  −
| the following equations hold between proofs:
   
|
 
|
−
| E1.  f 1_A  =  f,
+
<p>A ''category'' is a deductive system in which the following equations hold between proofs:</p>
 +
|-
 
|
 
|
−
|      1_B f = f,
+
<p><math>\begin{array}{ll}
 +
\text{E1.} & f 1_A = f, \qquad 1_B f = f, \qquad (hg)f = h(gf),
 +
\\[8pt]
 +
& \text{for all}~ f : A \to B, \quad g : B \to C, \quad h : C \to D.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
|      (hg)f  =  h(gf),
+
<p>(Lambek & Scott, 52).</p>
−
|
+
|}
−
| for all f : A -> B, g : B -> C, h : C -> D.
  −
</pre>
      
===Cartesian Category===
 
===Cartesian Category===
   −
<pre>
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| A 'cartesian category' is both a category
  −
| and a conjunction calculus satisfying the
  −
| additional equations:
   
|
 
|
−
| E2.  f  =  O_A,  for all f : A -> T.
+
<p>A ''cartesian category'' is both a category and a conjunction calculus satisfying the additional equations:</p>
 +
|-
 
|
 
|
−
| E3a. p1_A,B <f, g>  = f,
+
<p><math>\begin{array}{ll}
 +
\text{E2.}  & f = \bigcirc_A, \quad \text{for all}~ f : A \to \operatorname{T};
 +
\\[8pt]
 +
\text{E3a.} & \pi^{}_{A,B} \langle f, g \rangle = f,
 +
\\[8pt]
 +
\text{E3b.} & \pi^\prime_{A,B} \langle f, g \rangle = g,
 +
\\[8pt]
 +
\text{E3c.} & \langle \pi^{}_{A,B} h, \pi^\prime_{A,B} h \rangle = h,
 +
\\[8pt]
 +
& \text{for all}~ f : C \to A, \quad g : C \to B, \quad h : C \to A \land B.
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| E3b.  p2_A,B <f, g> =  g,
+
<p>(Lambek & Scott, 52).</p>
−
|
+
|}
−
| E3c. <p1_A,B h, p2_A,B h> =  h,
  −
|
  −
| for all f : C -> A, g : C -> B, h : C -> A & B.
  −
</pre>
      
===Cartesian Closed Category===
 
===Cartesian Closed Category===
   −
<pre>
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
−
| A 'cartesian closed category' is a cartesian category $A$ with
  −
| additional structure R4 satisfying the additional equations:
   
|
 
|
−
| E4a.  !e!_A,B <h* p1_C,B, p2_C,B>   =  h,
+
<p>A ''cartesian closed category'' is a cartesian category <math>\mathcal{A}</math> with additional structure <math>\text{R4}\!</math> satisfying the additional equations:</p>
 +
|-
 
|
 
|
−
| E4b. (!e!_A,B <k p1_C,B, p2_C,B>)* = k,
+
<p><math>\begin{array}{ll}
 +
\text{E4a.} & \varepsilon^{}_{A,B} \langle h^* \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle = h,
 +
\\[8pt]
 +
\text{E4b.} & (\varepsilon^{}_{A,B} \langle k \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle)^* = k,
 +
\\[8pt]
 +
& \text{for all}~ h : C \land B \to A \quad \text{and} \quad k : C \to (A \Leftarrow B).
 +
\end{array}</math></p>
 +
|-
 
|
 
|
−
| for all h : C & B -> A,  k : C -> (A <= B).
+
<p>Thus, a cartesian closed category is a positive intuitionistic propositional calculus satisfying the equations <math>\text{E1}\!</math> to <math>\text{E4}.\!</math>  This illustrates the general principle that one may obtain interesting categories from deductive systems by imposing an appropriate equivalence relation on proofs.</p>
−
|
+
 
−
| Thus, a cartesian closed category is
+
<p>(Lambek & Scott, 53).</p>
−
| a positive intuitionistic propositional
+
|}
−
| calculus satisfying the equations E1 to E4.
  −
| This illustrates the general principle that
  −
| one may obtain interesting categories from
  −
| deductive systems by imposing an appropriate
  −
| equivalence relation on proofs.
  −
</pre>
      
==Document History==
 
==Document History==
Line 2,593: Line 2,609:  
# http://stderr.org/pipermail/inquiry/2005-July/002895.html
 
# http://stderr.org/pipermail/inquiry/2005-July/002895.html
 
# http://stderr.org/pipermail/inquiry/2005-July/002896.html
 
# http://stderr.org/pipermail/inquiry/2005-July/002896.html
 +
 +
[[Category:Combinator Calculus]]
 +
[[Category:Combinatory Logic]]
 +
[[Category:Computer Science]]
 +
[[Category:Graph Theory]]
 +
[[Category:Lambda Calculus]]
 +
[[Category:Logic]]
 +
[[Category:Logical Graphs]]
 +
[[Category:Mathematics]]
 +
[[Category:Programming Languages]]
 +
[[Category:Type Theory]]
Jon Awbrey
12,080

edits

Retrieved from "https://mywikibiz.com/Special:MobileDiff/83240...195743"

Navigation menu