A most excellent gentleman

www.sillof.com

CUSTOM FIGURES

Victorian Marvels

Gaslight Justice League

Star Wars Re-Visioned

Dune: House Atreides

League of Extraordinary Gentlemen

Daredevil

The Venture Brothers

Historical Legends

Star Wars: McQuarrie

Star Wars Legends

Movies

Television

Passive polarization clock

Here’s a design for a passive polarization clock.

The sky is polarized in concentric circles around the sun. The polarization of the southern sky moves through around 180 degrees during daylight hours. It is polarized vertically in the morning, horizontally at noon, and vertically again in the evening.

Align slices of polarized film such that they are parallel to the contours. Any given ray from the center of the sundial outward always hits the contours at the same angle; the angle changes by 360 degrees as the ray passes through 180 degrees. In other words, the clock goes from 6am to 6pm as the sun moves through the sky.

Combinators as addresses

In linear lambda calculus, you must use each bound variable exactly once in a term. A term with a single bound variable is a full binary tree of applications in which one of the leaves is the bound variable, so it makes sense to ask, “which leaf?”

Three combinators are universal for the free linear lambda calculus on a countable set of types. In the description below, means “ applied to ” Note the position of the term in each case:

• identity
  
  
• cut
  
  
• braid
  
  

A full binary tree of applications is either a leaf or an application of a left subtree to a right subtree. says that this leaf is the variable in question; says that the variable is in the right subtree; and says it’s in the left subtree. So, for example, in the linear lambda term

appears in the left subtree, so applying abstraction elimination once gives

Now is on the right; eliminating again in the bracketed term gives

Now is on the left; eliminating again in the bracketed term gives

And finally, we replace with

to get a term with no bound occurrences of The “I-terminated” list of combinators we added, in this case tells us exactly where in the tree the variable appeared.

In the (nonlinear) lambda calculus, the variable may appear in either branch or not at all. The and combinators are a universal basis for this calculus, and can be interpreted as

• the variable may appear in either subtree, since
• the variable does not appear in this subtree, since
• this leaf is a copy of the variable, since

Yoneda embedding as contrapositive and call-cc as double negation

Consider the problem of how to represent negation of a proposition when we only have implication and falsehood:

Since is true and is false, this does what we want.

The contrapositive says has the same truth value as Using only implication, the contrapositive of is

What if we don’t even have falsehood? Well, we can pick any proposition to represent falsehood and form

The Yoneda embedding takes a category and produces a category :

 

This embedding is better known among computer scientists as the continuation passing style transformation.

In a symmetric monoidal closed category, like lambda calculus, we can move everything “inside:” every morphism has an internal version The internal Yoneda embedding of is

 

Here is the “void” type; notice how the target type is isomorphic under the Curry-Howard isomorphism to the contrapositive. This is a term that maps a continuation and a value to

To get double negation, first do the Yoneda embedding on the identity to get

then uncurry, braid, and recurry to get

or, internally,

This takes a value to a function value

Call-with-current-continuation expects a term that has been converted to CPS style as above, and then hands it the remainder of the computation in

The category GraphUp

The category GraphUp of graphs and Granovetter update rules has

• directed finite graphs as objects
• morphisms generated by Granovetter rules, i.e. the following five operations:
  • add a new node. (creation, refcount=0)
  • given a node add a new node and an edge (creation, refcount=1)
  • given edges and add an edge (introduction, ++refcount)
  • remove an edge. (deletion, --refcount)
  • remove a node and all its outgoing edges if it has no incoming edges. (garbage collection)

It’s a monoidal category where the tensor product is disjoint union. Also, since two disjoint graphs can never become connected, they remain disjoint.

Programs in a capability-secure language get interpreted in GraphUp. A program’s state graph consists of nodes, representing the states of the system, and directed edges, representing the system’s transitions between states upon receiving input. A functor from a program state graph to GraphUp assigns an object reference graph as state to each node and an update generated by Granovetter rules to each edge.

Polyadic asynchronous asymmetric pi calculus

where is either an input channel or an output channel and is taken from a countably infinite set.

Structural congruence:

• [with replacing ] if does not appear in (alpha conversion)
• (parallel processes)
• (association)
• (restriction)
• (replication)
• if is not free in

Reduction rules:

• [with replacing ]
• If then
• If then
• If and then

Haskell monads for the category theorist

A monad in Haskell is about composing almost-compatible morphisms. Typically you’ve got some morphism and then you think of a reason that you’d rather have where is a functor. In Haskell, though, you don’t define functors right out: you define type constructors, which are like the map of objects in a functor. You have to define the map of morphisms separately.

To define the map of morphisms, we have to define (aka ) and . We define to be the category-theorist’s unit composed with the input. Applying to gives

To compose “half-functored” morphisms like we define like this: given an input and a morphism like bind produces

So a “monad” in Haskell is always the monad for categories, except the lists are of bindable half-functored morphisms like rather than lists of composable morphisms.

A side-effect monad has where is the data type for the environment on which the morphism is to act. The IO monad is a specific instance of a side-effect monad with the environment being the keyboard queue, disk drive, network, etc.

Another piece of the stone

A few days ago, I thought that I had understood pi calculus in terms of category theory, and I did, in a way.

calculus model in Set type set of values term function (deterministic outcome) rewrite rule identity functional

calculus model in Set process set of states reduction rule state update rule (deterministic outcome)

To make lambda calculus into a category, we mod out by the rewrite rules and consider equivalence classes of terms instead of actual terms. A model of this category (i.e. a functor from the category to Set) picks out a set of values for each datatype and a function for each program. Given a value from the input set, we get a single value from the output set.

Similarly, a model of the pi calculus assigns to each process a set of states and to each reduction rule a function that updates the state. A morphism in this way of thinking is a certain number of reductions to perform. The reductions are deterministic in the sense that we can model “A or B” as Given an object’s state at a certain point, we can tell what set of states it can be in after the system reduces n messages.

However, what we really want is to know the set of states it can be in after all the messages have been processed: what is its normal form? This is far more like the rewrite rules in lambda calculus. It suggests that we should be treating the reduction rules like 2-morphisms instead of 1-morphisms. There’s one important difference from lambda calculus, however: the 2-morphisms of pi calculus are not confluent! It matters very much in which order they are evaluated. Thus processes can’t map to anything but trivial functions.

It looks like a better fit for models of the pi calculus is Rel, the category of sets and relations. A morphism in Rel can relate a single input state to multiple output states. This suggests we have a single object * in the pi calculus that gets mapped to a set of possible states for the system, while each process gets mapped to a relation that encodes all its possible reductions.

I’m rather embarrassed that it took me so long to notice this, since my advisor has been talking about replacing Set by Rel for years.

category	lambda calculus	pi calculus
objects	types	only one type *, a system of processes
a morphism	an equivalence class of terms	a structural congruence class of processes
dinatural transformation from the constant functor (mapping to the terminal set and its identity) to a functor generated by hom, products, projections, and exponentials (if they’re there)	combinator: template for programs mapping between isomorphic types (usually)	since there’s only one type, this is trivial
Model of the category in Rel	(usually taken in Set, a subcategory of Rel) a set of values for each data type and a function for each morphism between them	* maps to a set S of states for the system, and each process gets mapped to a relation that relates each element of S to its possible reductions in S

The Yoda embedding

Continuation passing as a reflection

We can write any expression like as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:

Figure 1:

[In the caption of figure 1, the expression is slightly different; when using trees, it's more convenient to curry all the functions---that is, replace every comma "," by back-to-back parens: ")(" .]

The continuation passing transform (Yoneda embedding) first reflects the tree across the vertical axis and then replaces the root and all the left children with their continuized form—a value gets replaced with a function value

Figure 2:

What does this evaluate to? Well,

As we hoped, it’s the continuization (Yoneda embedding) of the original expression. Iterating, we get

Figure 3:

At this point, we get an enormous simplification: we can get rid of overlines whenever the left and right branch both have them. For instance,

Actually working out the whole expression would mean lots of epicycular reductions like this one, but taking the shortcut, we just get rid of all the lines except at the root. That means that we end up with

for our final expression.

However, if this expression is just part of a larger one—if what we’re calling the “root” is really the child of some other node—then the cancellation of lines on siblings applies to our “root” and its sibling, and we really do get back to where we started!