reperiendi

Faces of War

Posted in Perception by Mike Stay on 2007 February 15

The WWI mask shops took over where the rudimentary plastic surgery left off:
“Thanks to you, I will have a home,” one soldier had written her. “…The woman I love no longer finds me repulsive, as she had a right to do.”

http://www.smithsonianmag.com/issues/2007/february/mask.php

MILL, BMCCs, and dinatural transformations

Posted in Category theory, Math, Quantum by Mike Stay on 2007 February 3

I’m looking at multiplicative intuitionistic linear logic (MILL) right now and figuring out how it’s related to braided monoidal closed categories (BMCCs).

The top and bottom lines in the inference rules of MILL are functors that you get from the definition of BMCCs, so they exist in every BMCC. Given a braided monoidal category C, the turnstile symbol

\displaystyle \vdash:C^{\rm{op}} \times C \to \mathbf{Set}

is the external hom functor (that is, x \vdash y is the set of morphisms from x to y). Inference rules are natural or dinatural transformations.

Let D be a category; then a natural transformation \alpha between two functors

\displaystyle F,G:C\to D

can be seen as a functor from the category (A \times C), where A is the category with two objects labelled F and G and one nontrivial arrow between them, labelled \alpha:

\displaystyle F\xrightarrow{\alpha}G

For every morphism f: x \to y in C we get a commuting square in (A \times C):

\left( X^{X^X} \right\downarrow

\displaystyle \begin{array}{ccc}(F,x) & \xrightarrow{(1_F, f)} & (F,y) \\ \left. (\alpha, 1_x)\right\downarrow & & \left\downarrow (\alpha,1_y)\right. \\ (G,x) & \xrightarrow{(1_G, f)} & (G,y)\end{array}

that maps to a commuting square in D.

\displaystyle \begin{array}{ccc}Fx & \xrightarrow{Ff} & Fy \\ \left. \alpha_x\right\downarrow & & \left\downarrow \alpha_y \right. \\ Gx & \xrightarrow{Gf} & Gy \end{array}

In other words, it assigns to each object x in C a morphism α_x in D such that the square above commutes.

Now consider the case where we want a natural transformation α between two functors

         op    F,G: C   × C -> D.

Given f:x->y, g:s->t, we get a commuting cube in (A × C^op × C) that maps to a commuting cube in D.

                                G(1_t,f)
                        Gtx -------------------> Gty
                        7|                       7|
                       / |                      / |
                 α_tx /  |G(g,1_x)        α_ty /  |
                     /   |                    /   | G(g,1_y)
                    /    |                   /    |
                   /     V      G(1_s,f)    /     V
                  /     Gsx -------------- /---> Gsy
                 /      7                 /      7
                /      /                 /      /
               /      /                 /      /
              /      /  F(1_t,f)       /      / α_sy
            Ftx -------------------> Fty     /
             |     /                  |     /
             |    /                   |    /
F(g,1_x)   |   / α_sx               | F(g,1_y)
             |  /                     |  /
             | /                      | /
             V/         F(1_s,f)      V/
            Fsx -------------------> Fsy

This is bigger, but still straightforward.

To get a dinatural transformation, we set g:=f and then choose a specific route around the cube so that both of the indices are the same on α.

                         ....................... Gyy
                        ..                       7|
                       . .                      / |
                      .  .                α_yy /  |
                     .   .                    /   | G(f,1_y)
                    .    .                   /    |
                   .     .      G(1_x,f)    /     V
                  .     Gxx -------------- /---> Gxy
                 .      7                 /      .
                .      /                 /      .
               .      /                 /      .
              .      /  F(1_y,f)       /      .
            Fyx -------------------> Fyy     .
             |     /                  .     .
             |    /                   .    .
  F(f,1_x)   |   / α_xx               .   .
             |  /                     .  .
             | /                      . .
             V/                       ..
            Fxx .......................

In other words, a dinatural transformation α: F -> G assigns to each object x a morphism α_xx such that the diagram above commutes.

Dinatural transformations come up when you’re considering two of MILL’s inference rules, namely

                               x ⊢ y   y ⊢ z
   ------- (Identity)   and   --------------- (Cut)
    x ⊢ x                          x ⊢ z

These two have the same symbol appearing on both sides of the turnstile, x in the Identity rule and y in the Cut rule. Setting

   Fxy = * ∈ Set,

where * is the one-element set, and

   Gxy = x ⊢ y ∈ Set,

the Identity rule specifies that given f:x->y we have that f o 1_x = 1_y o f:

                         .......................y ⊢ y
                        ..                       7|
                       . .                      / |
                      .  .                α_yy /  |
                     .   .                    /   | 1_y o f
                    .    .                   /    |
                   .     .      f o 1_x     /     V
                  .    x ⊢ x ------------- /--> x ⊢ y
                 .      7                 /      .
                .      /                 /      .
               .      /                 /      .
              .      /     1           /      .
             * ---------------------> *      .
             |     /                  .     .
             |    /                   .    .
          1  |   / α_xx               .   .
             |  /                     .  .
             | /                      . .
             V/                       ..
             * ........................

where

   α_xx:*  -> x ⊢ x        * |-> 1_x

picks out the identity morphism on x.

In the Cut rule, we let j:x->s, k:t->z, and f:s->t,

   F(t,s) = (x ⊢ s, t ⊢ z)

                j      f         k
   F(1,f) = (x ---> s ---> t, t ---> z)

                j         f      k
   F(f,1) = (x ---> s, s ---> t ---> z)

   G(s,t) = x ⊢ z

and consider the diagram for a morphism f:s->t in C.

                         .......................x ⊢ z
                        ..                       7|
                       . .                      / |
                      .  .         composition /  |
                     .   .                    /   | 1
                    .    .                   /    |
                   .     .          1       /     V
                  .    x ⊢ z ------------- /--> x ⊢ z
                 .      7                 /      .
                .      /                 /      .
               .      /                 /      .
              .      / F(f,1)          /      .
       (x ⊢ s, t ⊢ z) -------> (x ⊢ s, s ⊢ z)
             |     /                  .     .
             |    /                   .    .
             |   / composition        .   .
     F(1,f)  |  /                     .  .
             | /                      . .
             V/                       ..
       (x ⊢ t, t ⊢ z) .................

which says that composition of morphisms is associative.

Job, Isaiah, Percy, Sting

Posted in Poetry by Mike Stay on 2007 February 3

Job 30: 29
29 I am a brother to dragons, and a companion to owls.

Isa 13:19-22
19 And Babylon, the glory of kingdoms, the beauty of the Chaldees’ excellency, shall be as when God overthrew Sodom and Gomorrah.
20 It shall never be inhabited, neither shall it be dwelt in from generation to generation: neither shall the Arabian pitch tent there; neither shall the shepherds make their fold there.
21 But wild beasts of the desert shall lie there; and their houses shall be full of doleful creatures; and owls shall dwell there, and satyrs shall dance there.
22 And the wild beasts of the islands shall cry in their desolate houses, and dragons in their pleasant palaces: and her time is near to come, and her days shall not be prolonged.

Isa. 34: 11-15
11 ¶ But the cormorant and the bittern shall possess it; the owl also and the raven shall dwell in it: and he shall stretch out upon it the line of confusion, and the stones of emptiness.
12 They shall call the nobles thereof to the kingdom, but none shall be there, and all her princes shall be nothing.
13 And thorns shall come up in her palaces, nettles and brambles in the fortresses thereof: and it shall be an habitation of dragons, and a court for owls.
14 The wild beasts of the desert shall also meet with the wild beasts of the island, and the satyr shall cry to his fellow; the screech owl also shall rest there, and find for herself a place of rest.
15 There shall the great owl make her nest, and lay, and hatch, and gather under her shadow: there shall the vultures also be gathered, every one with her mate.

Ozymandias

I met a traveller from an antique land
Who said:–Two vast and trunkless legs of stone
Stand in the desert. Near them on the sand,
Half sunk, a shatter’d visage lies, whose frown
And wrinkled lip and sneer of cold command
Tell that its sculptor well those passions read
Which yet survive, stamp’d on these lifeless things,
The hand that mock’d them and the heart that fed.
And on the pedestal these words appear:
“My name is Ozymandias, king of kings:
Look on my works, ye mighty, and despair!”
Nothing beside remains: round the decay
Of that colossal wreck, boundless and bare,
The lone and level sands stretch far away.

— Percy Bysshe Shelley

Mad about you

A stone’s throw from Jerusalem
I walked a lonely mile in the moonlight
And though a million stars were shining
My heart was lost on a distant planet
That whirls around the April moon
Whirling in an arc of sadness
I’m lost without you, I’m lost without you

Though all my kingdoms turn to sand and fall into the sea
I’m mad about you, I’m mad about you

And from the dark secluded valleys
I heard the ancient songs of sadness
But every step I thought of you
Every footstep only you
Every star a grain of sand
The leavings of a dried up ocean
Tell me, how much longer,
How much longer?

They say a city in the desert lies
The vanity of an ancient king
But the city lies in broken pieces
Where the wind howls and the vultures sing
These are the works of man
This is the sum of our ambition
It would make a prison of my life
If you became another’s wife

With every prison blown to dust, my enemies walk free
I’m mad about you, I’m mad about you

And I have never in my life
Felt more alone than I do now
Although I claim dominions over all I see
It means nothing to me
There are no victories
In all our histories
Without love

A stone’s throw from Jerusalem
I walked a lonely mile in the moonlight
And though a million stars were shining
My heart was lost on a distant planet
That whirls around the April moon
Whirling in an arc of sadness
I’m lost without you, I’m lost without you

And though you hold the keys to ruin of everything I see
With every prison blown to dust, my enemies walk free
Though all my kingdoms turn to sand and fall into the sea
I’m mad about you, I’m mad about you.

— Gordon Matthew ‘Sting’ Sumner

stay@google.com

Posted in Journal by Mike Stay on 2007 February 3

I’ve accepted a job at Google in their Applied Security team. We’ll be moving at the end of March, when the quarter is over. I don’t know if my first choice of email address above will be the one I get, but I can’t imagine someone else has it. My second and third choices were quantum@google.com and functor@google.com .

Cris checked out U. Auckland’s policy on off-site students for me. They’re currently waiving international student fees for doctoral students, and I wouldn’t have to take any more classes or exams, just write a thesis. The guideline for what constitutes a thesis is apparently three publications’ worth of material, and I have that much in the queue already:

  1. Most Programs Stop Quickly or Never Halt,”
  2. “Four perspectives on braided monoidal closed categories,” and
  3. “Weakly-universal machines and the algorithmic uncertainty principle.”

I’ll need to have a co-advisor, so I’m hoping John will agree to it. It would be really cool if I could get a Ph.D. while at Google. It would be cooler still if they still give me that scholarship they offered me when I graduated.