### Mike Stay

Shared publicly -1

I've been reading Beowulf aloud to Daniel. The good parts version.

Add a comment...

Start a hangout

Mike Stay

Attends University of Auckland

Lives in Mountain View, CA

1,952 followers|880,013 views

AboutPostsPhotosYouTube

1

I've been reading Beowulf aloud to Daniel. The good parts version.

Add a comment...

These bubbles caught my eye this morning. The colors come both from interference patterns in the light due to the thickness of the soap film---light waves resonate in the film like sound waves do in an organ pipe---and from polarization due to the fact that soap is a liquid crystal.

9

Add a comment...

"Pi calculus" is a very simple programming language created by Milner, Parrow, and Walker in 1992. It's based around the notion of sharing "mailbox addresses"; pi calculus uses lowercase letters like x, y, or z for an address. There are only five different instructions; these instructions form what's called a "process"; pi calculus uses uppercase letters like P or Q for a process:

0 = do nothing.

(new x).P = create a new mailbox and call it x; then do P.

P | Q = do P and Q at the same time.

x!(y1, ..., yn) = put the list of mailbox addresses y1, ..., yn into mailbox x.

x?(z1, ..., zn).P =*wait* for a list of addresses to be put into mailbox x; call them z1, ..., zn, and *then* do P.

The way programs run is encoded in the rule

x!(y1, ..., yn) | x?(z1, ..., zn).P

becomes

P{y1, ..., yn / z1, ..., zn}

where we read the slash as "replaces", so if, for example,

P = z1!(z2)

then

P{y1, y2 / z1, z2} = y1!(y2).

However, it only replaces "free" mailboxes, so if

P = z1?(z2).Q

then

P{y1, y2 / z1, z2} = y1?(z2).Q{y1 / z1},

and if

P = (new z2).Q

then

P{y1, y2 / z1, z2} = (new z2).Q{y1 / z1}.

Pi calculus is just as powerful as lambda calculus, the programming language invented by Alonzo Church in 1934; there's a translation from lambda into pi. However, unlike lambda calculus, pi calculus is also good for modeling "concurrency": if lots of processes put lists in the mailbox x, it's nondeterministic which one gets processed:

x!(y1) | x!(y2) | x?(z).P

becomes either

P {y1/z} | x!(y2)

or

P {y2/z} | x!(y1).

The "x?" term combines with*only one* of the "x!"s. You can think of the "x!"s as a deposit and a withdrawal racing to see which gets to the bank account "x?" first; it can matter quite a lot in what order the messages arrive. Similarly, pi calculus can model contention for resources.

x!(y) | x?(z1).P | x?(z2).Q

becomes either

P {y/z1} | x?(z2).Q

or

Q {y/z2} | x?(z1).P.

The "x!" term combines with*only one* of the "x?"s. You can think of the "x!" as a Google search that gets handled by only one server "x?", leaving the other free to handle a different request.

There has been a lot of good exposition of concurrency in terms of linear logic. However, the instruction "x?" has, in the past, caused trouble for attempts to model pi calculus with category theory. It seems obvious to try using an object for mailboxes, an object for processes, 1-morphisms for the instructions above, and a 2-morphism for the rewrite rule. The problem is that done naively, the rewrites don't wait: if some process P rewrites to P', then

x?(y).P

can be rewritten to

x?(y).P'

without waiting for a message to be received in the mailbox x.

+Lucius Meredith and I found a way around that problem by using a "catalyst" morphism COMM. If we modify the rewrite rule so that

x!(y1, ..., yn) | x?(z1, ..., zn).P | COMM

becomes

P{y1, ..., yn / z1, ..., zn} | COMM

and then we only include a COMM at the top level, then the terms that ought to wait are simply*shaped wrong* to be rewritten. Bisimulation carries over directly.

The result is a higher-categorical semantics for the pi calculus that's consistent with the Curry-Howard isomorphism---1-morphisms are typed terms---but also exactly captures the operational semantics of pi calculus.

This was a thoroughly collaborative effort, and a pleasure to write.

http://arxiv.org/abs/1504.04311

0 = do nothing.

(new x).P = create a new mailbox and call it x; then do P.

P | Q = do P and Q at the same time.

x!(y1, ..., yn) = put the list of mailbox addresses y1, ..., yn into mailbox x.

x?(z1, ..., zn).P =

The way programs run is encoded in the rule

x!(y1, ..., yn) | x?(z1, ..., zn).P

becomes

P{y1, ..., yn / z1, ..., zn}

where we read the slash as "replaces", so if, for example,

P = z1!(z2)

then

P{y1, y2 / z1, z2} = y1!(y2).

However, it only replaces "free" mailboxes, so if

P = z1?(z2).Q

then

P{y1, y2 / z1, z2} = y1?(z2).Q{y1 / z1},

and if

P = (new z2).Q

then

P{y1, y2 / z1, z2} = (new z2).Q{y1 / z1}.

Pi calculus is just as powerful as lambda calculus, the programming language invented by Alonzo Church in 1934; there's a translation from lambda into pi. However, unlike lambda calculus, pi calculus is also good for modeling "concurrency": if lots of processes put lists in the mailbox x, it's nondeterministic which one gets processed:

x!(y1) | x!(y2) | x?(z).P

becomes either

P {y1/z} | x!(y2)

or

P {y2/z} | x!(y1).

The "x?" term combines with

x!(y) | x?(z1).P | x?(z2).Q

becomes either

P {y/z1} | x?(z2).Q

or

Q {y/z2} | x?(z1).P.

The "x!" term combines with

There has been a lot of good exposition of concurrency in terms of linear logic. However, the instruction "x?" has, in the past, caused trouble for attempts to model pi calculus with category theory. It seems obvious to try using an object for mailboxes, an object for processes, 1-morphisms for the instructions above, and a 2-morphism for the rewrite rule. The problem is that done naively, the rewrites don't wait: if some process P rewrites to P', then

x?(y).P

can be rewritten to

x?(y).P'

without waiting for a message to be received in the mailbox x.

+Lucius Meredith and I found a way around that problem by using a "catalyst" morphism COMM. If we modify the rewrite rule so that

x!(y1, ..., yn) | x?(z1, ..., zn).P | COMM

becomes

P{y1, ..., yn / z1, ..., zn} | COMM

and then we only include a COMM at the top level, then the terms that ought to wait are simply

The result is a higher-categorical semantics for the pi calculus that's consistent with the Curry-Howard isomorphism---1-morphisms are typed terms---but also exactly captures the operational semantics of pi calculus.

This was a thoroughly collaborative effort, and a pleasure to write.

http://arxiv.org/abs/1504.04311

Abstract: We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an ...

30

6

15 comments

Mike Stay

+

1

2

1

2

1

+J H-P There are lots of uses for COMM, and we intend to follow up on those in another paper. In this paper, all we really needed was a unary morphism for marking the "top" scope---i.e. the only scope where we're not waiting for anything before we can process the term---and we built it out of a binary morphism and a nullary one.

If we have more than one COMM at the top scope, then we can do reductions in parallel, so the number of COMMs in that setting captures the number of processors you have working concurrently.

We can explicitly exempt terms of the form x?(y).Q from having to wait for a message to be delivered to x by saying x?(y).(COMM | Q).

If we modify the comm_n rule so that it consumes the COMM instead of having the COMM behave like a catalyst, then we can use COMM for tracking exactly how many messages get delivered.

So COMM is useful for marking scopes, counting processors, altering the evaluation strategy, and managing resources, and probably more that we haven't thought of yet.

If we have more than one COMM at the top scope, then we can do reductions in parallel, so the number of COMMs in that setting captures the number of processors you have working concurrently.

We can explicitly exempt terms of the form x?(y).Q from having to wait for a message to be delivered to x by saying x?(y).(COMM | Q).

If we modify the comm_n rule so that it consumes the COMM instead of having the COMM behave like a catalyst, then we can use COMM for tracking exactly how many messages get delivered.

So COMM is useful for marking scopes, counting processors, altering the evaluation strategy, and managing resources, and probably more that we haven't thought of yet.

Add a comment...

I first heard of Lockhart from his influential essay "A Mathematician's Lament" wherin he contemplates an alternate dystopian universe in which art is taught in the same way that mathematics is:

*A musician wakes from a terrible nightmare. In his dream he finds himself in a society where music education has been made mandatory. “We are helping our students become more competitive in an increasingly sound-filled world.” Educators, school systems, and the state are put in charge of this vital project. Studies are commissioned, committees are formed, and decisions are made—all without the advice or participation of a single working musician or composer.*

*Since musicians are known to set down their ideas in the form of sheet music, these curious black dots and lines must constitute the “language of music.” It is imperative that students become fluent in this language if they are to attain any degree of musical competence; indeed, it would be ludicrous to expect a child to sing a song or play an instrument without having a thorough grounding in music notation and theory. Playing and listening to music, let alone composing an original piece, are considered very advanced topics and are generally put off until college, and more often graduate school.*

https://www.maa.org/external_archive/devlin/LockhartsLament.pdf

https://www.maa.org/external_archive/devlin/LockhartsLament.pdf

Paul Lockhart waxing lyrical about mathematics. In a way, this video captures, for me,

https://www.youtube.com/watch?v=V1gT2f3Fe44

This is a kind of trailer for his book

http://www.hup.harvard.edu/catalog.php?isbn=9780674057555

Don't miss the wonderful excerpts at

http://www.brainpickings.org/index.php/2012/09/25/measurement-paul-lockhart/

+David Butler , you should love this!

#mathematics

11

7

It is kind of like this post I wrote recently.http://llamasandmystegosaurus.blogspot.com/2015/01/arts-and-sciences.html

Add a comment...

Total internal reflection from the transparent plastic Braille dots.

4

Add a comment...

4

2 comments

John Cook

+

1

2

1

2

1

+Stephen Paul King The internet would run out of things to post photos of, though presumably the policy would be discontinued before we were in danger of a shortage of photographic subjects.

Add a comment...

In his circles

128 people

This is great!

Trailer for the original, 1951 version of *Raiders of the Lost Ark*. I never knew this existed!

2

That is hilarious.

Add a comment...

William wanted to make his Pinewood Derby car look like an enderman from Minecraft.

13

2 comments

Add a comment...

Some wonderful cat armor by Jeff de Boer. His website's here: http://jeffdeboer.com/Home/tabid/36/Default.aspx

When I started this blog I knew I had to have at least one post about cats. Problem is; cats are very rarely connected to roleplaying games unless they're a familiar or... a monster. However, these...

1

Add a comment...

Apparently this is a thing.

10

2

6 comments

They didn't actually change the tires...

Add a comment...

People

In his circles

128 people

Work

Occupation

Partner, Biosimilarity, LLC

Skills

Category theory, computer programming, theoretical physics

Places

Currently

Mountain View, CA

Previously

Lindon, UT - Redford, MI - Amherst, OH - Provo, UT - Puerto San Jose, Guatemala - Jocotenango, Guatemala - Villa Nueva, Guatemala - Villa Hermosa, Guatemala - Colorado Springs, CO - Epsom, New Zealand - Riverside, CA

Story

Introduction

Whenever I'm asked to describe myself, I immediately think of Gödel numbering and quines.

Education

- University of AucklandComputer Science, 2007 - presentPhD
- University of AucklandComputer Science, 2004 - 2005MSc
- Brigham Young UniversityPhysics, 1992 - 1997BSc

Basic Information

Gender

Male

Other names

Michael Stay