Blog » Formal semantics for side effects
Posted on 1234195011|%A: %d %B, %Y|agohover
Got an idea for formal semantics for operations with side-effects like IO operations, random, etc. It's inspired by Haskell's use of Category Theory as a semantic device and by the Z specification language (the ISO Standard is downloadable; see the small print below the price list. An outdated but still useful manual is here.)
The idea in brief is that we model the world as a category W, whose objects are events and whose sole arrow is a precedence operator ( >- , \succ in LaTeX). What the events represent specifically is irrelevant; we only care about an event "input 'c'" as an abstract event. Think of this as the infinite list of events that contains all possible permutations of real world events.
To provide the semantics of the execution of a program P, we establish an isomorphism between it and W. The isomorphism maps "opaque" terms (e.g. IO terms, random values, etc.) to events. Ordering is preserved by some kind of rule mapping textual precedence in P to event precedence in W. In other words, to model a particular execution of P we incorporate a subset of W into the semantic domain. The static semantics of P are expressed only in the semantic domain, excluding W.
Now the meaning of the program is the text of P, its mapping to a semantic domain (the usual denotational mapping for e.g. '3'), plus the set of all possible isomorphisms between opaque terms and W. The actual exposition is a little more complicated than that, but this conveys the general idea.
This allows us to express program semantics, including dynamic semantics, in a rigorous, formal model that completely excludes any hint of dynamics, contingency, side-effects, etc. The notion of evaluation is also eliminated.
Like this entry?
Leave a comment
If I understand this correctly, we can represent what you're talking about in Haskell by what I informally think about as the 'free data structure' with the right set of operations:
— IO as a functor
data IOElem a where
Fmap :: (a -> b) -> IO a -> IO b
PutChar :: Char -> IO ()
GetChar :: IO Char
— …
— Free monad over IOElem
data IO a where
Roll :: IOElem (IO a) -> IO a
Return :: a -> IO a
instance Functor IO where
fmap f (Roll e) = Roll (Fmap f e)
fmap f (Return a) = Return (f a)
instance Monad IO where
return = Return
Return a »= k = k a
Roll a »= k = Roll (fmap (»=k) m)
putChar c = fmap return (PutChar c)
getChar = fmap return GetChar
— …
I believe this, as a way of assigning semantics to 'opaque' constructs such as IO, is well-known. The problem with this, and with semantics for IO in general, is that, because it's the /free/ data structure with the right properties, it doesn't allow deriving all of the properties which one would desire. Indeed, the difficulty in defining semantics for IO arises not from mechanically stating what it would /mean/ to define such semantics, but in stating which operations are equivalent.
For instance, is putChar 'a' » putChar 'b' equivalent to putStr "ab"? I would argue that the semantics here are unclear — operationally, it depends on whether the former results in one syscall or two (or even one call to any DSO or two), since those behaviours are externally observable. Denotationally, we are torn between wanting as many programs as possible to be considered equivalent, and wanting to avoid claiming programs are equivalent when they will behave differently when implemented (or tying the hands of an implementor to a particular implementation strategy).
Hi lilac and thanks for your thoughtful response,
I'm afraid the "free x" stuff is a little over my head. I grok monoids and various other animals, but I've never managed to acquire an intuition about the "free" in "free monoid" (or free algebra, etc.) Its on my list, and I was hoping to put it off a bit longer, but it looks like I'll have to tackle it. Darn.
Regarding IO semantics. You observe "the difficulty …[is] in stating which operations are equivalent, and then you give an example, "putChar 'a' » putChar 'b'" v. "putStr 'ab'", asking whether they are equivalent from a DS perspective. This is unclear, since we don't know how these calls will be translated into syscalls (and thus observable behavior). My understanding is you mean to point out that a single IO operation may translate into multiple actions: "ab" as output will ordinarily mean two RealWorld events, namely the appearance of 'a' on the terminal (for example), then the appearance of 'b'.
We can abstract this as the question of what to do about event structure. The user may experience the appearance of "ab" on her screen as a single event, if the machine is fast, or as two events if the machine is slow. One event or two?
I think we have a simple answer to this: one-to-one correspondence between opaque terms (or the application of opaque terms to args) and events in category W. The actual apparatus by which such events are experienced in the world is not relevant; from the perspective of the program text, they are single events.
For example, suppose we have a "makeSandwich" operator. Obviously, making a sandwich involves many steps; it is a complex, structured event as far as the human observer is concerned. But for program semantics, it is a single, simplex event. For a given execution (interpretation) of the program, a makeSandwich expression will denote a sandwich /in toto/. There is no need to break it down into constituent components.
That's why I say the details of the actual event are irrelevant; all that matters is that it be an event. The beauty of this (which I didn't grok until I read your message) is that in addition to its intuitive clarity, it happens to fit into the formal semantics of category theory. CT doesn't care about objects; it's all about the arrows. So all we need to do is establish the isomorphism between the program and an event sequence; it doesn't matter what the events represent; since they are objects of our category, we can disregard them.
One other point: the mapping from text expressions to category W passes through stuff like syscalls, as you point out. But that's implementation detail; it does not affect semantics. We don't care how the morphisms are represented (as syscalls, smoke signals, interpretive dance, whatever), so long as they map terms to W values.
You also mention the problem of demonstrating program equivalence. To channel Bill Clinton, that depends on what the meaning of "is" ('equivalence') is. Consider "putChar 'a' »= putChar 'b'". Syntactically, the two IO expressions are equal. They are also equal, or at least equivalent, at the level of 2nd order logic: they use the same function, applied to the same argument. But they do not have equivalent denotations. The reason for this goes to the concept of types and tokens. If a symbol, e.g. '3', occurs twice in an expression, each occurrence is a token of its type. This doesn't generally matter in pure denotational semantics, but it is essential for modeling the real world. In a program text, such symbols denote; if they denote the same value, they are equivalent. But treated as output events, this is not the case, since outputted symbols do not denote. An expression like "print 3" may occur multiple times in a program text, generating the appearance of the symbol '3' multiple times on the output medium. Actually we should not call the output a symbol, since symbols denote; better to call it a figure (or token). In the program text we needn't think of each occurrence as a distinct token, since only their denotations count, which are all the same. Or: each occurence of '3' is a distinct token, but all '3' tokens have the same denotation. But on the output medium we /must/ consider each such occurrence as a distinct token with no denotation. On the output medium they don't denote; they're just forms as tokens. Therefore we cannot collapse them; two different occurrences of the symbol '3' cannot be equivalent, since they are tokens, not denoting symbols. Only denotation allows us to perform substitution.
I hope that's clear and makes sense,
-gregg
Thanks,
gregg
I am so grateful to read this such a wonderful post.
http://www.nikerbo.com
http://www.jordanhut.com
http://www.bestmonclerhut.com
Write very good! Back Up.
Discount Sunglasses http://www.bestsunglassesbrand.com
Moncler Down http://www.frbestmoncler.com
Sunglasses for Glasses http://www.worstsunglassesbrand.com
Discount Nike Sneakers http://www.nikerwo.com
Post preview:
Close preview