12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Thursday May 02, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 23:54, 6 July 2013
, 23:54, 6 July 2013no edit summary
{{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==
==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.
|
|
<p>A ''deductive system'' is a graph in which to each object <math>A\!</math> there is associated an arrow <math>1_A : A \to A,</math> the ''identity'' arrow, and to each pair of arrows <math>f : A \to B</math> and <math>g : B \to C</math> there is associated an arrow <math>gf : A \to C,</math> the ''composition'' of <math>f\!</math> with <math>g.\!</math> A logician may think of the objects as ''formulas'' and of the arrows as ''deductions'' or ''proofs'', hence of</p>
<p>A ''deductive system'' is a graph in which to each object <math>A\!</math> there is associated an arrow <math>1_A : A \to A,</math> the ''identity'' arrow, and to each pair of arrows <math>f : A \to B</math> and <math>g : B \to C</math> there is associated an arrow <math>gf : A \to C,</math> the ''composition'' of <math>f\!</math> with <math>g.\!</math> A logician may think of the objects as ''formulas'' and of the arrows as ''deductions'' or ''proofs'', hence of</p>
|-
::<p><math>\begin{array}{c}
|
::<p><math>\dfrac{~ f : A \to B \quad g : B \to C ~}{gf : A \to C}</math></p>
|-
gf : A \to C
|
<p>as a ''rule of inference''.</p>
<p>as a ''rule of inference''.</p>
|
|
<p>A ''category'' is a deductive system in which the following equations hold, for all <math>f : A \to B,</math> <math>g : B \to C,</math> and <math>h : C \to D.</math></p>
<p>A ''category'' is a deductive system in which the following equations hold, for all <math>f : A \to B,</math> <math>g : B \to C,</math> and <math>h : C \to D.</math></p>
|-
|
::<p><math>f 1_A = f = 1_B f, \quad (hg)f = h(gf).</math></p>
::<p><math>f 1_A = f = 1_B f, \quad (hg)f = h(gf).</math></p>
|-
<p>(Lambek & Scott, 5).
|
<p>(Lambek & Scott, 5).</p>
|}
|}
|
|
<p>'''Definition 1.3.''' A ''functor'' <math>F : \mathcal{A} \to \mathcal{B}</math> is first of all a morphism of graphs …, that is, it sends objects of <math>\mathcal{A}</math> to objects of <math>\mathcal{B}</math> and arrows of <math>\mathcal{A}</math> to arrows of <math>\mathcal{B}</math> such that, if <math>f : A \to A',</math> then <math>F(f) : F(A) \to F(A').</math> Moreover, a functor preserves identities and composition; thus:</p>
<p>'''Definition 1.3.''' A ''functor'' <math>F : \mathcal{A} \to \mathcal{B}</math> is first of all a morphism of graphs …, that is, it sends objects of <math>\mathcal{A}</math> to objects of <math>\mathcal{B}</math> and arrows of <math>\mathcal{A}</math> to arrows of <math>\mathcal{B}</math> such that, if <math>f : A \to A',</math> then <math>F(f) : F(A) \to F(A').</math> Moreover, a functor preserves identities and composition; thus:</p>
|-
|
::<p><math>F(1_A) = 1_{F(A)}, \quad F(gf) = F(g)F(f).</math></p>
::<p><math>F(1_A) = 1_{F(A)}, \quad F(gf) = F(g)F(f).</math></p>
|-
|
<p>In particular, the identity functor <math>1_\mathcal{A} : \mathcal{A} \to \mathcal{A}</math> leaves objects and arrows unchanged and the composition of functors <math>F : \mathcal{A} \to \mathcal{B}</math> and <math>G : \mathcal{B} \to \mathcal{C}</math> is given by:</p>
<p>In particular, the identity functor <math>1_\mathcal{A} : \mathcal{A} \to \mathcal{A}</math> leaves objects and arrows unchanged and the composition of functors <math>F : \mathcal{A} \to \mathcal{B}</math> and <math>G : \mathcal{B} \to \mathcal{C}</math> is given by:</p>
|-
|
::<p><math>(GF)(A) = G(F(A)), \quad (GF)(f) = G(F(f)),</math></p>
::<p><math>(GF)(A) = G(F(A)), \quad (GF)(f) = G(F(f)),</math></p>
|-
|
<p>for all objects <math>A\!</math> of <math>\mathcal{A}</math> and all arrows <math>f : A \to A'</math> in <math>\mathcal{A}.</math></p>
<p>for all objects <math>A\!</math> of <math>\mathcal{A}</math> and all arrows <math>f : A \to A'</math> in <math>\mathcal{A}.</math></p>
===Natural Transformation===
===Natural Transformation===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>'''Definition 2.1.''' Given functors <math>F, G : \mathcal{A} \rightrightarrows \mathcal{B},</math> a ''natural transformation'' <math>t : F \to G</math> is a family of arrows <math>t(A) : F(A) \to G(A)</math> in <math>\mathcal{B},</math> one arrow for each object <math>A\!</math> of <math>\mathcal{A},</math> such that the following square commutes for all arrows <math>f : A \to B</math> in <math>\mathcal{A}</math>:</p>
</pre>
<pre>
<pre>
t(A)
F(A) o------------------>o G(A)
| |
| |
F(f) | | G(f)
| |
v v
F(B) o------------------>o G(B)
t(B)
</pre>
</pre>
<p>that is to say, such that</p>
|-
<pre>
| arrows and rules of inference:
|
|
<p><math>G(f)t(A) = t(B)F(f).\!</math></p>
| R2. A -----> T,
|-
|
|
<p>{Lambek & Scott, 8).</p>
|}
| C --------> A & B
===Positive Intuitionistic Propositional Calculus===
===Graph 2===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
|
|
</pre>
<p>We recall … that, for categories, a ''graph'' consists of two classes and two mappings between them:</p>
<center><pre>
o--------------o source o--------------o
| An 'intuitionistic propositional calculus' is more than a
| | ----------------> | |
| positive one; it requires also falsehood and disjunction,
| Arrows | | Objects |
| that is, a formula 'F' (= false) and an operation 'v' (= or)
| | ----------------> | |
| on formulas, together with the following additional arrows:
o--------------o target o--------------o
|
| []_A
</pre></center>
<p>In graph theory the arrows are usually called ''oriented edges'' and the objects ''nodes'' or ''vertices'', but in various branches of mathematics other words may be used. Instead of writing</p>
|-
|
|
::<p><math>\operatorname{source}(f) = A, \quad \operatorname{target}(f) = B,</math></p>
| R6a. A --------> A v B,
|-
|
|
<p>one often writes <math>f : A \to B</math> or <math>A \xrightarrow{~f~} B.</math> We shall look at graphs with additional structure which are of interest in logic.</p>
<p>(Lambek & Scott, 47).</p>
|}
</pre>
===Classical Propositional Calculus===
===Deductive System 2===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''deductive system'' is a graph with a specified arrow</p>
|-
| the following equations hold between proofs:
|
|
<p><math>\text{R1a.} \quad A ~\xrightarrow{~1_A~}~ A,</math></p>
|-
|
|
| 1_B f = f,
<p>and a binary operation on arrows (''composition'')
|-
|
|
<p><math>\text{R1b.} \quad \dfrac{~ A ~\xrightarrow{~f~}~ B \quad B ~\xrightarrow{~g~}~ C ~}{A ~\xrightarrow{~gf~}~ C}.</math></p>
|-
|
|
<p>(Lambek & Scott, 47).</p>
</pre>
|}
===Cartesian Category===
===Conjunction Calculus===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''conjunction calculus'' is a deductive system dealing with truth and conjunction. Thus we assume that there is given a formula <math>\operatorname{T}</math> ( = true) and a binary operation <math>\land</math> ( = and) for forming the conjunction <math>A \land B</math> of two given formulas <math>A\!</math> and <math>B.\!</math> Moreover, we specify the following additional arrows and rules of inference:</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{R2.} & A ~\xrightarrow{~\bigcirc_A~}~ \operatorname{T};
\\[8pt]
\text{R3a.} & A \land B ~\xrightarrow{~\pi_{A, B}~}~ A,
\\[8pt]
\text{R3b.} & A \land B ~\xrightarrow{~\pi'_{A, B}~}~ B,
\\[8pt]
</pre>
\text{R3c.} & \dfrac{~ C ~\xrightarrow{~f~}~ A \quad C ~\xrightarrow{~g~}~ B ~}{C ~\xrightarrow{~\langle f, g \rangle~}~ A \land B}.
\end{array}</math></p>
|-
|
<p>(Lambek & Scott, 47–48).</p>
|}
===Cartesian Closed Category===
===Positive Intuitionistic Propositional Calculus===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''positive intuitionistic propositional calculus'' is a conjunction calculus with an additional binary operation <math>\Leftarrow</math> ( = if). Thus, if <math>A\!</math> and <math>B\!</math> are formulas, so are <math>\operatorname{T},</math> <math>A \land B,</math> and <math>A \Leftarrow B.</math> (Yes, most people write <math>B \Rightarrow A</math> instead.) We also specify the following new arrow and rule of inference.</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{R4a.} & (A \Leftarrow B) \land B ~\xrightarrow{~\varepsilon_{A, B}~}~ A,
\\[8pt]
\text{R4b.} & \dfrac{~ C \land B ~\xrightarrow{~h~}~ A ~}{~ C ~\xrightarrow{~h^*~}~ A \Leftarrow B ~}.
\end{array}</math></p>
|-
|
|
| for all h : C & B -> A, k : C -> (A <= B).
<p>(Lambek & Scott, 48–49).</p>
|}
===Intuitionistic Propositional Calculus===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<p>An ''intuitionistic propositional calculus'' is more than a positive one; it requires also falsehood and disjunction, that is, a formula <math>\bot</math> ( = false) and an operation <math>\lor</math> ( = or) on formulas, together with the following additional arrows:</p>
|-
|
<p><math>\begin{array}{ll}
\text{R5.} & \bot ~\xrightarrow{~\Box_A~}~ A;
\\[8pt]
\text{R6a.} & A ~\xrightarrow{~\kappa_{A, B}~}~ A \lor B,
\\[8pt]
\text{R6b.} & B ~\xrightarrow{~\kappa'_{A, B}~}~ A \lor B,
\\[8pt]
\text{R6c.} & (C \Leftarrow A) \land (C \Leftarrow B) ~\xrightarrow{~\zeta^C_{A, B}~}~ C \Leftarrow (A \lor B).
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 49–50).</p>
|}
</pre>
==Document History==
===Classical Propositional Calculus===
===Inquiry List, Series A : Jun–Jul 2004===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<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>
|-
|
<p>(Lambek & Scott, 50).</p>
|}
===Category 2===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<p>A ''category'' is a deductive system in which the following equations hold between proofs:</p>
|-
|
<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>
|-
|
<p>(Lambek & Scott, 52).</p>
|}
===Cartesian Category===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<p>A ''cartesian category'' is both a category and a conjunction calculus satisfying the additional equations:</p>
|-
|
<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>
|-
|
<p>(Lambek & Scott, 52).</p>
|}
===Cartesian Closed Category===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<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>
|-
|
<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>
|-
|
<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>
<p>(Lambek & Scott, 53).</p>
|}
==Document History==
===Inquiry List, Series A : Jun–Jul 2004===
* http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
* http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643
# 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]]
