Quick
index
main
eev
maths
blogme
dednat4
littlelangs
PURO

emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
debian-rj
w32/AIX
politics
personal
heroes
irc
contact

Basic Semantics

Quick index:
1. Categories with finite products
==================================
Categories with finite products (CFPs) are categories
in which we can interpret tuples and projections.
Our archetypal CFP is Set.

An example of the translation:

  a,a',(b,c) |---------------> (c,a'),a'

becomes:

            <<π_3;π_2,π_1>,π_1>
  A×A×(B×C) ------------------> (C×A)×A

How? Let's look at how we construct (c,a'),a' from a,a',(b,c):

  a,a',(b,c)
  ----------π_3
      b,c        a,a',(b,c)
      ---π_2     ----------π_2
       c             a'         a,a',(b,c)
       ----------------<,>      ----------π_2
            c,a'                    a'
            -------------------------<,>
                   (c,a'),a'

Now let's make the contexts explicit
(p := a,a',(b,c), for typographical reasons):

  p|-a,a',(b,c)
  -------------π_3
      p|-b,c        p|-a,a',(b,c)
      ------π_2     -------------π_2
       p|-c              p|-a'         p|-a,a',(b,c)
       -----------------------<,>      -------------π_2
                p|-c,a'                    p|-a'
                -------------------------------<,>
                           p|-(c,a'),a'

Translating:

     id
    ---
    π_3        id
  -------      ---
  π_3;π_2      π_2    id
  ----------------    ---
    <π_3;π_2,π_2>     π_2
    ---------------------
     <<π_3;π_2,π_2>,π_2>

Notation: 1={*} is the 0-ary product.
Example: a,b|->* (``!'') is the only morphism from A×B to 1.
It's not important to differentiate the ``*''s -
for example, *,*' |-> *,*' and *,*' |- *',* are the same
morphism from 1×1 to 1×1 - we can write it just as *,* |-> *,*.

L

2. A ring in a CFP
==================
A ring in a CFP is an object R equipped with five morphisms,

      z        s
  1 ----> R <----- R×R      * |---> 0
  1 ----> R <----- R×R      * |---> 1
      u        m                   a+b <----| a,b
          n                         ab <----| a,b
      R -----> R                a |---> -a

These morphisms must obey certain equations,
one for each ring axiom.
For example,

  ∀a,b,c. a(b+c) = ab+ac

becomes the following equation on morphisms:

  (a,b,c |-> a(b+c)) =
  (a,b,c |->  ab+ac)

        t|-b  t|-c    t|-a  t|-b   t|-a  t|-c
        ----------    ----------   ----------
          t|-b,c        t|-a,b       t|-a,c
          ------        ------       -----
  t|-a    t|-b+c        t|-ab        t|-ac
  --------------        ------------------
    t|-a,(b+c)	             t|-ab,ac
    ----------	             --------
    t|-a(b+c)	   =         t|-ab+ac


          π_1  π_2           π_0  π_1      π_0  π_2
          ---------         ---------     ---------
          <π_1,π_2>         <π_0,π_1>     <π_0,π_2>
         -----------       -----------   -----------
  π_0    <π_1,π_2>;s       <π_0,π_1>;m   <π_0,π_2>;m
  ------------------       -------------------------
   <π_0,<π_1,π_2>;s>       <<π_0,π_1>;m,<π_0,π_2>;m>
  -------------------     ---------------------------
  <π_0,<π_1,π_2>;s>;m  =  <<π_0,π_1>;m,<π_0,π_2>;m>;s

L


3. CCC Diagrams
===============
Note (1): these diagrams function as a
``skeleton'' for the whole proof - we take
the diagram, add layers of meat and skin,
and we reconstruct the whole animal.
As far as I know, the standard proofs for
CCC<->λ1 don't have a ``center'' that is
as clear as we have here.

Note (2): our idea of ``dictionaries'' is
related to the idea of ``internal languages''
in Categorical Semantics. It is common in,
e.g., Topos Theory, to take a set-theoretical
proof, then check that it is well-behaved
enough, and then say that ``this proof works
in any topos''. This corresponds to our
liftings; but internal languages assign
precise meanings to all well-formed
expressions of a certaing language, while our
dictionaries will only attribute meanings to
those expressions that are mentioned,
directly or indirectly, in our proofs.
/Internal languages induce infinite
dictionaries/; and our way of building
dictionaries from proofs will let us deal
with arising ambiguities one by one, in
organic (and ad-hoc) ways...

4. CCCs in half-DNC
===================
This diagram expresses the structure in a CCC:

A CCC is a category plus this "structure":

      --| a |--	      a	  a,b <==== a
     /    -    \      -	   -   	    -
    /     |	\     |	   |  <-->  |
   v      v	 v    v	   v	    v
  b <--| b,c |--> c   *    c ===> b|->c

The product diagram comprises two operations
on morphisms, and the adjunction diagram four:
(we'll forget the terminal for the moment)

  /  a  \     /      a      \
  |  -  |     |    -   -    |
  |  |  | |-> |   /     \   |
  |  v  |     |  v       v  |
  \ b,c /     \ b         c /

  /      a      \     /  a  \
  |    -   -    |     |  -  |
  |   /     \   | |-> |  |  |
  |  v       v  |     |  v  |
  \ b         c /     \ b,c /

          a',b <==== a'
            -        -
            |  <--|  |
            v        v
           a,b <==== a
            -        -
            |  <--|  |
            |  |-->  |
            v        v
            c ===> b|->c
            -        -
            |  |-->  |
            v        v
            c' ==> b|->c'


               a',b <==== a'
	         -        -
 p|-<a(πp),π'p>  |  <--|  |  a'|-a(a')
	         v        v
	        a,b <==== a
	         -        -
  p|-f(πp)(π'p)  |  <--|  |  a|-f(a)
        p|-c(p)  |  |-->  |  a|-λb.c(<a,b>)
	         v        v
	         c ===> b|->c
	         -        -
       c|-c'(c)  |  |-->  |  f|-λb.c'(fb)
	         v        v
	         c' ==> b|->c'

5. From CCCs to λ-calculus: products
====================================
From diagrams to natural deduction: propositional calculus

  /  P  \     /      P      \                        P     P
  |  -  |     |    -   -    |                        :     :
  |  |  | |-> |   /     \   |    P|-Q&R   P|-Q&R    Q&R   Q&R
  |  v  |     |  v       v  |    ======   ======    ---   ---
  \ Q&R /     \ Q         R /     P|-Q     P|-R      Q     R

  /      P      \     /  P  \                        P     P
  |    -   -    |     |  -  |                        :     :
  |   /     \   | |-> |  |  |     P|-Q   P|-R        Q     R
  |  v       v  |     |  v  |     ===========        -------
  \ Q         R /     \ Q&R /       P|-Q&R             Q&R

  /  a  \     /      a      \                        a     a
  |  -  |     |    -   -    |                        :     :
  |  |  | |-> |   /     \   |    a|-b,c   a|-b,c    b,c   b,c
  |  v  |     |  v       v  |    ======   ======    ---   ---
  \ b,c /     \ b         c /     a|-b     a|-c      b     b

  /      a      \     /  a  \                        a     a
  |    -   -    |     |  -  |                        :     :
  |   /     \   | |-> |  |  |     a|-b   a|-c        b     c
  |  v       v  |     |  v  |     ===========        -------
  \ b         c /     \ b,c /       a|-b,c             a,c

In half-DNC:

  /  a   \     /      a      \                           a      a
  |  -   |     |    -   -    |                           :      :
  |  |   | |-> |   /     \   |    a|-p(a)    a|-p(a)    p(a)   p(a)
  |  v   |     |  v       v  |    ========  =========  -----  ------
  \ p(a) /     \πp(a)  π'p(a)/    a|-πp(a)  a|-π'p(a)  πp(a)  π'p(a)

  /      a      \     /     a     \                      a      a
  |    -   -    |     |     -     |                      :      :
  |   /     \   | |-> |     |     |  a|-b(a)   a|-c(a)  b(a)   c(a)
  |  v       v  |     |     v     |  =================  -----------
  \ b(a)   c(a) /     \<b(a),c(a)>/   a|-<b(a),c(a)>    <b(a),c(a)>

6. From CCCs to λ-calculus: equations for products
==================================================
The two arrows (coming from the natural transformations)
are inverses, so their two composites must be identites:

  /  a   \     /      a      \     /      a       \
  |  -   |     |    -   -    |     |      -       |
  |  |   | |-> |   /     \   | |-> |      |       | = id
  |  v   |     |  v       v  |     |      v       |
  \ p(a) /     \πp(a)  π'p(a)/     \<πp(a),π'p(a)>/

  /      a      \     /     a     \     /             a              \
  |    -   -    |     |     -     |     |           -   -            |
  |   /     \   | |-> |     |     | |-> |          /     \           | = id
  |  v       v  |     |     v     |     |         v       v          |
  \ b(a)   c(a) /     \<b(a),c(a)>/     \π<b(a),c(a)>   π'<b(a),c(a)>/

  ∀p:B×C. p=<πp,π'p>

  ∀b:B,c:C. b=π<b,c>
  ∀b:B,c:C. c=π'<b,c>

7. Deleted diagrams
===================
           a,b <==== a
            -        -
            |  <--|  |
            v        v
          a',b <==== a'

  a,b <==== a       a,b <==== a
   -        -  	     -        -
   |  <--|  |  	     |  |-->  |
   v        v  	     v        v
   c ===> b|->c	     c ===> b|->c

            c ===> b|->c
            -        -
            |  |-->  |
            v        v
            c' ==> b|->c'

If we translate these six operations to half-DNC we get:

  /  a 	 \     /        a      	  \
  |  - 	 |     |      -   -	  |
  |  | 	 | |-> |     /     \	  |
  |  v 	 |     |    v       v	  |
  \ p(a) /     \ πp(a)     π'p(a) /

  /        a       \     /      a      \
  |      -   -     |     |      -      |
  |     /     \    | |-> |      |      |
  |    v       v   |     |      v      |
  \ b(a)      c(a) /     \ <b(a),c(a)> /

               p <=========== a
               -              -
               |     <--|     |
               v              v
          <a'(πp),π'p> <=== a'(a)

      p <========= a      p <========== a
      -            -      -             -
      |    <--|    |      |    |-->     |
      v            v      v             v
  f(πp)(π'p) ===> f(a)   c(p) ====> λb.c(<a,b>)

               c ===========> f
               -              -
               |     |-->     |
               v              v
             c'(c) =====> λb.c'(fb)



8. New diagrams
===============

An adjunction has 4 operations on morphisms
===========================================

P'&Q <==== P'
  -        -
  |  <--|  |
  v        v
 P&Q <==== P
  -        -
  |  <--|  |
  |  |-->  |
  v        v
  R ====> Q⊃R
  -        -
  |  |-->  |
  v        v
  R ====> Q⊃R

Translating categorical operations to λ-calculus
================================================

                                            P'&Q
					    ----
           P'&Q <==== P'	  	      P'  P'&Q
	    -        -	       		      :   ----
  P'&Q|-P&Q |  <--|  | P'|-P     P'|-P	      P    Q
	    v        v	       =========      ------
	   P&Q <==== P         P'&Q|-P&Q       P&Q

                                        a',b             p
                                        ----            --
               a',b <==== a'             a'    a',b     πp     p
                 -        -              :       :      :    ---
  p|-<a(πp),π'p> |  <--|  | a'|-a(a')   a(a')    b    a(πp)  π'p
                 v        v             ----------    -----------
                a,b <==== a             <a(a'),b>     <a(πp),π'p>


               a',b <==== a'
                 -        -
  p|-<a(πp),π'p> |  <--|  | a'|-a(a')
                 v        v
                a,b <==== a
                 -        -
  p|-f(πp)(pi'p) |  <--|  | a|-f(a)
         p|-c(p) |  |-->  | a|-λb.p(<a,b>)
                 v        v
                 c ===> b|->c
                 -        -
        c|-c'(c) |  |-->  | f|-λb.c'(fb)
                 v        v
                 c' ==> b|->c'


The product and the terminal
============================

Translating λ-calculus rules to categorical constructions
=========================================================