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==
|}
|}
In this scheme of inference, the notations <math>^{\backprime\backprime} x \, ^{\prime\prime},</math> <math>^{\backprime\backprime} f \, ^{\prime\prime},</math> and <math>^{\backprime\backprime} f(x) \, ^{\prime\prime}</math> are referred to as ''terms'' and interpreted as names of formal objects.
In this scheme of inference, the notations <math>{}^{\backprime\backprime} x {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} f {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} f(x) {}^{\prime\prime}</math> are referred to as ''terms'' and interpreted as names of formal objects.
In the same context, the notations <math>^{\backprime\backprime} X \, ^{\prime\prime},</math> <math>^{\backprime\backprime} X \to Y \, ^{\prime\prime},</math> and <math>^{\backprime\backprime} Y \, ^{\prime\prime}</math> give us information, or indicate formal constraints, that we may think of as denoting the ''types'' of the formal objects under consideration. By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.
In the same context, the notations <math>{}^{\backprime\backprime} X {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} X \to Y {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} Y {}^{\prime\prime}</math> give us information, or indicate formal constraints, that we may think of as denoting the ''types'' of the formal objects under consideration. By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.
If a moment's spell of double vision leads us to see the functional arrow <math>^{\backprime\backprime} \to \, ^{\prime\prime}</math> as the logical arrow <math>^{\backprime\backprime} \Rightarrow \, ^{\prime\prime}</math> then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called ''modus ponens''. And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of ''modus ponens''.
If a moment's spell of double vision leads us to see the functional arrow <math>{}^{\backprime\backprime} \to {}^{\prime\prime}</math> as the logical arrow <math>{}^{\backprime\backprime} \Rightarrow {}^{\prime\prime}</math> then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called ''modus ponens''. And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of ''modus ponens''.
===Commentary Note 2===
===Commentary Note 2===
Notice that I am carrying out combinator applications "on the right", so the formulas might read backwards from what many people are used to.
==Bibliography==
Here are a three references on combinatory logic and lambda calculus,
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:
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.
# Hindley, J.R. and Seldin, J.P. (1986), ''Introduction to Combinators and <math>\lambda</math>-Calculus'', London Mathematical Society Student Texts No. 1, Cambridge University Press, Cambridge, UK.
# Lambek, J. and Scott, P.J. (1986), ''Introduction To Higher Order Categorical Logic'', Cambridge University Press, Cambridge, UK.
==Basic Concepts from Lambek and Scott (1986)==
Notes on basic concepts from Lambek and Scott (1986), ''Introduction To Higher Order Categorical Logic'', Cambridge University Press, Cambridge, UK. [http://suo.ieee.org/ontology/thrd42.html#03373 Excerpts and discussion on the Ontology List].
Here is a synopsis, exhibiting just the layering of axioms — notice the technique of starting over at the initial point several times and building up both more richness of detail and more generality of perspective with each passing time:
===Concrete Category===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
<p>'''Definition 1.1.''' A ''concrete category'' is a collection of two kinds of entities, called ''objects'' and ''morphisms''. The former are sets which are endowed with some kind of structure, and the latter are mappings, that is, functions from one object to another, in some sense preserving that structure. Among the morphisms, there is attached to each object <math>A\!</math> the ''identity mapping'' <math>1_A : A \to A</math> such that <math>1_A(a) = a\!</math> for all <math>a \in A.\!</math> Moreover, morphisms <math>f : A \to B</math> and <math>g : B \to C</math> may be ''composed'' to produce a morphism <math>gf : A \to C</math> such that <math>(gf)(a) = g(f(a))\!</math> for all <math>a \in A.\!</math></p>
<p>We shall now progress from concrete categories to abstract ones, in three easy stages.</p>
<p>(Lambek & Scott, 4–5).</p>
|}
===Graph===
| We shall now progress from concrete categories
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
| to abstract ones, in three easy stages.
|
<p>'''Definition 1.2.''' A ''graph'' (usually called a ''directed graph'') consists of two classes: the class of ''arrows'' (or ''oriented edges'') and the class of ''objects'' (usually called ''nodes'' or ''vertices'') and two mappings from the class of arrows to the class of objects, called ''source'' and ''target'' (often also ''domain'' and ''codomain'').</p>
<center><pre>
o--------------o source o--------------o
| | ----------------> | |
| Arrows | | Objects |
| | ----------------> | |
o--------------o target o--------------o
</pre></center>
<p>One writes <math>^{\backprime\backprime} f : A \to B \, ^{\prime\prime}</math> for <math>^{\backprime\backprime} \operatorname{source}\ f = A ~\operatorname{and}~ \operatorname{target}\ f = B \, ^{\prime\prime}.</math> A graph is said to be ''small'' if the classes of objects and arrows are sets.</p>
<p>(Lambek & Scott, 5).</p>
|}
| (hg)f = h(gf).
===Deductive System===
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<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>
|-
|
|
| F(gf) = F(g)F(f).
::<p><math>\dfrac{~ f : A \to B \quad g : B \to C ~}{gf : A \to C}</math></p>
|-
|
|
<p>as a ''rule of inference''.</p>
<p>(Lambek & Scott, 5).</p>
|}
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
===Category===
| Definition 2.1. Given functors F, G : $A$ -> $B$,
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<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>
|-
| t(B)
|
|
| that is to say, such that
::<p><math>f 1_A = f = 1_B f, \quad (hg)f = h(gf).</math></p>
|-
|
|
<p>(Lambek & Scott, 5).</p>
|}
===Functor===
| We recall (Part 0, Definition 1.2) that, for categories,
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
| between them:
<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>
|-
| o--------------o target o--------------o
|
|
<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>
|-
| of mathematics other words may be used. Instead of writing
|
|
::<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>(Lambek & Scott, 6).</p>
| look at graphs with additional structure which are
|}
===Natural Transformation===
| A 'deductive system' is a graph with a specified arrow
{| 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>
t(A)
F(A) o------------------>o G(A)
| |
| |
F(f) | | G(f)
| |
v v
F(B) o------------------>o G(B)
t(B)
</pre>
<p>that is to say, such that</p>
|-
| specify the following new arrow and rule of inference:
|
|
<p><math>G(f)t(A) = t(B)F(f).\!</math></p>
|-
| R4b. ----------------.
|
|
<p>{Lambek & Scott, 8).</p>
|}
===Graph 2===
| An 'intuitionistic propositional calculus' is more than a
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>We recall … that, for categories, a ''graph'' consists of two classes and two mappings between them:</p>
<center><pre>
| If we want 'classical' propositional logic, we must also require:
o--------------o source o--------------o
|
| | ----------------> | |
| R7. F <= (F <= A) -> A.
| Arrows | | Objects |
| | ----------------> | |
o--------------o target o--------------o
</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>
| the following equations hold between proofs:
|-
|
|
::<p><math>\operatorname{source}(f) = A, \quad \operatorname{target}(f) = B,</math></p>
|-
|
|
<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>
|
|}
===Deductive System 2===
| A 'cartesian category' is both a category
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| E2. f = O_A, for all f : A -> T.
<p>A ''deductive system'' is a graph with a specified arrow</p>
|-
|
|
<p><math>\text{R1a.} \quad A ~\xrightarrow{~1_A~}~ A,</math></p>
|-
|
|
<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>
|}
===Conjunction Calculus===
| A 'cartesian closed category' is a cartesian category $A$ with
{| 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]
\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>
|-
|
|
| for all h : C & B -> A, k : C -> (A <= B).
<p>(Lambek & Scott, 47–48).</p>
|}
===Positive Intuitionistic Propositional Calculus===
{| 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>
|-
|
<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>
|}
===Classical Propositional Calculus===
{| 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>
|-
|
|
| Thus, a cartesian closed category is
<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]
</pre>
\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==
==Document History==
# 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]]
