Archive for January, 2007

Bart Jacobs’ question (FP lunch 19/1/07)

Sunday, January 21st, 2007 by Thorsten

Recently, Bart Jacob’s asked me a question about containers: He is looking for a formula for the derivative of a quotient container. I sketched a possible answer (I haven’t yet checked the details) and used this opportunity to give a quick introduction to containers.

A container is given by a set S\in * of shapes and a family P\in S\to * of position, giving rise to a functor
F \in * \to * given by F\,X = \Sigma s\in S.(P\, s)\to X. It’s derivative as a functor is
F'\,X = \Sigma (s,p) \in (\Sigma s\in S.P\,s).(\Sigma q\in P\,s.p \not= q)\to X. A quotient container is specified by additionally
giving a family of subgroups R\,s\subseteq Iso\,(P\,s) of the isomorphism group, it gives rise to a functor
F\,X = \Sigma s\in S.((P\, s)\to X)/\sim where the equivalence relation is generated by f \sim f\circ\phi for
\phi\in R\,s. I believe that it’s derivative is given by extending the previous formula by additionally specifying
R'\,(s,p)\subseteq Iso\,(\Sigma q\in P\,s.p \not= q) where \phi\in R'\,(s,p) iff \phi is given by restricting an isomorphim \psi\in R\,s with the property \psi\,p=p (by restricting I mean that \phi \circ \pi_1 = \pi_1 \circ \psi).

A question about observations

Friday, January 19th, 2007 by Graham

Suppose you are interested in the semantics of effects, such as state, input/output, non-determinism, exceptions, etc. Suppose further that you are interested in small-step operational semantics of effects. Is there a systematic way to determine what the “observations” should be in such semantics, i.e. the actions that label the transitions?