[msp-interest] [MSP101] Conor Mc Bride: Leftovers, Rightunders: Typechecking Thinnings Compositionally (1pm Mon 22/9, LT1310)

[Fredrik Nordvall Forsberg]

Comrades,

We kick off a new semester of the MSP101 seminar with a talk by Conor. 
The regular time for the coming semester is Mondays at 1pm.

Hope to see you there!

Cheers,
Fred


Date, time and place:
   Monday 22 September, 13:00, Livingstone Tower room LT1310

Speaker:
   Conor Mc Bride (MSP)

Title:
   Leftovers, Rightunders: Typechecking Thinnings Compositionally

Abstract:
   In the interests of sharing MSP lore, I came up with a way to talk 
about both
   the "Input Subject Output" approach to typechecking and the Category of
   Thinnings in the same talk, making the latter an interesting example 
of the
   former.

   The Input Subject Output approach, like most bidirectional approaches 
to problem
   decomposition, tracks whether signals go from parent to child or vice 
versa,
   but it also acknowledges a signal has a guarantor as well as a sender,
   responsible for the meaningfulness of the signal. Meanwhile, 
thinnings are
   order-preserving embeddings between ordered sequences, or dually, 
selections
   of elements from sequences (their resemblance to binomial coffecients 
is no
   accident), and are thus a fine example of a monoidal category.

   I won't assume that any of you know know any of this: many of us do; 
more of
   us should. And I'll try to tell the story with pictures, drawn on a 
whiteboard,
   rather than jargon.

   I often use thinnings to talk about embeddings between scopes, the 
latter seen
   as sequences which grow on the right (because of prejudices about 
time). A
   compositional way to typecheck a thinning is to start with the 
available stuff
   "over" the thinning, together with a thinning that will start 
choosing from
   the newest stuff on the right. If all is well, we shall learn which 
"leftovers"
   have not yet been considered, and which "rightunders" have been not only
   considered but also selected. There is a healthy story about both the
   monoidal/parallel/spatial/tensor structure of thinnings and their
   categorical/sequential/temporal/composition structure, yielding an 
algorithm
   which never has to guess where to chop sequences in two.

MSP101 Feeds:
   Web: http://msp.cis.strath.ac.uk/msp101.html
   RSS: http://msp.cis.strath.ac.uk/msp101.rss
   iCal: http://msp.cis.strath.ac.uk/msp101.ics