Profile

Cover photo
Mike Stay
Attends University of Auckland
Lives in Mountain View, CA
1,952 followers|880,013 views
AboutPostsPhotosYouTube

Stream

Mike Stay

Shared publicly  - 
1
Douglas Summers-Stay's profile photo
 
I've been reading Beowulf aloud to Daniel. The good parts version.
Add a comment...

Mike Stay

Shared publicly  - 
 
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...

Mike Stay

Shared publicly  - 
 
"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
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
Philip Thrift's profile photoBorislav Iordanov's profile photoHilmar Hoffmann's profile photoIvan Pierre's profile photo
15 comments
 
+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.
Add a comment...

Mike Stay

Shared publicly  - 
 
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
 
Elegant reason-poems (AKA "proofs")

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

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

This is a kind of trailer for his book Measurement:

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  
10 comments on original post
11
7
Omar Shareef's profile photoRob Jongschaap's profile photoMark Phelan's profile photoChris Monson's profile photo
Add a comment...

Mike Stay

Shared publicly  - 
 
Total internal reflection from the transparent plastic Braille dots.
4
Add a comment...

Mike Stay

Shared publicly  - 
 
TIL
4
Stephen Paul King's profile photoJohn Cook's profile photo
2 comments
 
+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...
Have him in circles
1,952 people
Alexander Wilce's profile photo
ivis arriojas's profile photo
Deanna McWilliams's profile photo
Kyuhwa Lee's profile photo
Esminee Rase's profile photo
PARAMESWAR RAO BANDARU's profile photo
Olivia Jasmine's profile photo
Aashu Bhardwaj's profile photo
Kris Kowal's profile photo
 
This is great!
 
Trailer for the original, 1951 version of Raiders of the Lost Ark.  I never knew this existed!
View original post
2
Rebecca Stay's profile photo
 
That is hilarious.
Add a comment...
 
William wanted to make his Pinewood Derby car look like an enderman from Minecraft.
13
David Stay's profile photoMike Stay's profile photo
2 comments
 
Add a comment...

Mike Stay

Shared publicly  - 
 
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...

Mike Stay

Shared publicly  - 
 
Apparently this is a thing.
10
2
David Stay's profile photoRebecca Stay's profile photoSamuel Holmes's profile photoiPan Darius's profile photo
6 comments
 
They didn't actually change the tires...
Add a comment...

Mike Stay

Shared publicly  - 
 
Autobots, roll out!
12
1
Mike Stay's profile photocolby larsen's profile photoRebecca Stay's profile photoDanielle “Dani” Trail's profile photo
3 comments
 
love it
Add a comment...

Mike Stay

Shared publicly  - 
 
"could" from Old English cuðe past tense of cunnan "to know how, be able"; c.f. "can", "uncouth", "ken", "know"
3
John Baez's profile photo
 
In Singapore they have a nice expression that goes like this:

"Could you please fax this for me?"

"Can!"
Add a comment...
People
Have him in circles
1,952 people
Alexander Wilce's profile photo
ivis arriojas's profile photo
Deanna McWilliams's profile photo
Kyuhwa Lee's profile photo
Esminee Rase's profile photo
PARAMESWAR RAO BANDARU's profile photo
Olivia Jasmine's profile photo
Aashu Bhardwaj's profile photo
Kris Kowal's profile photo
Work
Occupation
Partner, Biosimilarity, LLC
Skills
Category theory, computer programming, theoretical physics
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
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
Links
YouTube
Other profiles
Story
Introduction
Whenever I'm asked to describe myself, I immediately think of Gödel numbering and quines.
Education
  • University of Auckland
    Computer Science, 2007 - present
    PhD
  • University of Auckland
    Computer Science, 2004 - 2005
    MSc
  • Brigham Young University
    Physics, 1992 - 1997
    BSc
Basic Information
Gender
Male
Other names
Michael Stay