January | 2009 | reperiendi

Syntactic string diagrams

Posted in Category theory, Math, Programming by Mike Stay on 2009 January 24

I hit on the idea of making lambda a node in a string diagram, where its inputs are an antivariable and a term in which the variable is free, and its output is the same term, but in which the variable is bound. This allows a string diagram notation for lambda calculus that is much closer to the syntactical description than the stuff in our Rosetta Stone paper. Doing it this way makes it easy to also do pi calculus and blue calculus.

There are two types, V (for variable) and T (for term). I’ve done untyped lambda calculus, but it’s straightforward to add subscripts to the types V and T to do typed lambda calculus.

There are six function symbols:

$\lambda:V^* \times T \to T.$ Lambda takes an antivariable and a term that may use the corresponding variable.
$\cap:1 \to V^* \times T.$ This turns an antivariable “x” introduced by lambda into the term “x”.
$A:T \times T \to T.$ (Application) This takes $f$ and $x$ and produces $f(x)$ .
${\rm swap}:T \times T \to T \times T$
$!:T \to 1$
$\Delta:T \to T \times T.$ These two mean we can duplicate and delete terms.

The $\beta-\eta$ rule is the real meat of the computation. The “P” is an arbitrary subdiagram. The effect is replacing the “A” application node with the “P” subdiagram, modulo some wiring.

I label the upwards arrows out of lambdas with a variable name in parentheses; this is just to assist in matching up the syntactical representation with the string diagram.

In the example, I surround part of the diagram with a dashed line; this is the part to which the $\beta-\eta$ rule applies. Within that, I surround part with a dash-dot line; this is the subdiagram P in the rule.

When I do blue calculus this way, there are a few more function symbols and the relations aren’t confluent, but the flavor is very much the same.

String diagrams for untyped lambda calculus

An example calculation

1 comment

Imaginary time

Posted in General physics by Mike Stay on 2009 January 9

Statics (geometric = no time):
$\displaystyle x$	[x]	x coordinate
$\displaystyle y(x)$	[y]	y coordinate
$\displaystyle k$	[k]	proportionality constant
$\displaystyle y'(x) = \frac{dy(x)}{dx}$	[y/x]	slope
$\displaystyle s(x) = ky'(x)$	[k y/x]	proportional to slope
$\displaystyle T(x) = \frac{1}{2} ky'(x)^2$	[k y^2/x^2]	distortion
$\displaystyle V(y(x))$	[k y^2/x^2]	original shape
$\displaystyle S(y) = \int (T + V\circ y)(x) dx$ $\displaystyle = \int \left[ \frac{k}{2} \left(\frac{dy(x)}{dx}\right)^2 + V(y(x)) \right] dx$	[k y^2/x]	least S at equilibrium
Statics (with energy):
$\displaystyle x$	[x]	parameterization of curve
$\displaystyle y(x)$	[y]	y coordinate
$\displaystyle k$	[kg x/s^2]	spring constant at x
$\displaystyle v(x) = \frac{dy(x)}{dx}$	[y/x]	slope
$\displaystyle F(x) = kv(x)$	[kg y/s^2]	force due to stretching
$\displaystyle T(x) = \frac{1}{2} kv(x)^2$	[kg y^2/s^2 x = J/x]	stretching energy density
$\displaystyle V(y(x))$	[kg y^2/s^2 x= J/x]	gravitational energy density
$\displaystyle E(y) = \int (T + V\circ y)(x) dx$ $\displaystyle = \int \left[ \frac{k}{2} \left(\frac{dy(x)}{dx}\right)^2 + V(y(x)) \right] dx$	[kg y^2/s^2 = J]	energy (least energy at equilibrium)
Statics (unitless distance):
$\displaystyle x$	[1]	parameterization of curve
$\displaystyle y(x)$	[m]	y coordinate
$\displaystyle k$	[kg/s^2]	spring constant
$\displaystyle v(x) = \frac{dy(x)}{dx}$	[m]	relative displacement
$\displaystyle F(x) = kv(x)$	[kg m/s^2 = N]	force at x due to stretching
$\displaystyle T(x) = \frac{1}{2} kv(x)^2$	[kg m^2 / s^2 = J]	stretching energy at x
$\displaystyle V(y(x))$	[kg m^2 / s^2 = J]	gravitational energy at x
$\displaystyle E(y) = \int (T + V\circ y)(x) dx$ $\displaystyle = \int \left[ \frac{k}{2} \left(\frac{dy(x)}{dx}\right)^2 + V(y(x)) \right] dx$	[kg m^2 / s^2 = J]	energy (least energy at equilibrium)
Dynamics ( $\displaystyle \underline{\lambda x.y(x) \mapsto \lambda t.y(it)}$ ):
$\displaystyle t$	[s]	time
$\displaystyle y(it)$	[m]	y coordinate
$\displaystyle m$	[kg]	mass
$\displaystyle v(t) = \frac{dy(it)}{dt} = i\frac{dy(it)}{dit}$	[m/s]	velocity
$\displaystyle p(t) = m v(t)$	[kg m/s]	momentum
$\displaystyle T(t) = \frac{1}{2}m\;v(t)^2 = -\frac{m}{2}\left(\frac{dy(it)}{dit}\right)^2$	[-kg m^2/s^2 = -J]	-kinetic energy
$\displaystyle V(y(it))$	[kg m^2 / s^2 = J]	potential energy
$\displaystyle iS(y) = \int (T + V\circ y \circ i)(t) dt$ $\displaystyle = \int \left[ -\frac{m}{2}\left(\frac{dy(it)}{dit}\right)^2 + V(y(it)) \right] dt$ $\displaystyle = i \int \left[ \frac{m}{2}\left(\frac{dy(it)}{dit}\right)^2 - V(y(it)) \right] d it$	[kg m^2/s]	i * action