Introduction

Let’s say we have a little language for programs that emit characters. We can run those programs and collect traces, such as "ab" or "ac". What do those traces tell us about the programs? What have we lost by only keeping the characters?

It turns out that two rather different programs can leave exactly the same logs. We’ll start by seeing what extra information would let us tell them apart. Then we’ll try cutting an execution into pieces and putting it back together. What needs to survive the cut?

Those two experiments give us a way into presheaves and sheaves. We’ll introduce the mathematics as we need it, with enough Haskell to keep us honest, and work our way up to a site and a topos. The snippets can be collected into one module; no prior category theory is assumed.

Presheaves and execution traces

A tiny language

Some Haskell to get started:

module Traces where

import Data.List (nub)

data Proc
  = Stop
  | Emit Char Proc
  | Choice Proc Proc
  deriving (Eq, Show)

Emit c p emits c, then continues as p. Choice p q can behave as either p or q. We’re describing possible executions, so there are no probabilities to worry about. Stop does nothing further.

Here are two programs:

later, earlier :: Proc
later = Emit 'a' (Choice (Emit 'b' Stop) (Emit 'c' Stop))

earlier = Choice (Emit 'a' (Emit 'b' Stop))
                 (Emit 'a' (Emit 'c' Stop))

The first emits a, then offers a choice between b and c. The second offers two ways to emit a, each with its own continuation.

We can make that precise by listing the possible next steps:

steps :: Proc -> [(Char, Proc)]
steps Stop         = []
steps (Emit c p)   = [(c, p)]
steps (Choice p q) = steps p ++ steps q

There is no separate visible event for making a choice. Choosing a branch means taking one of its steps. In particular, steps earlier contains two different a transitions.

Let’s collect all finite traces, including executions that we stop observing partway through:

traces :: Proc -> [String]
traces p = nub $ "" :
  [ c : rest
  | (c, q) <- steps p
  , rest <- traces q
  ]

-- traces later
-- ["","a","ab","ac"]

-- traces earlier
-- ["","a","ab","ac"]

Same traces! So much for telling these two apart by reading their logs. "a" tells us that an a occurred, but doesn’t tell us which transition produced it. We have forgotten something about the execution.

Our programs are finite trees, so this enumeration terminates. We won’t add loops in this example.

The category of trace prefixes

If we have an execution of "ab", we can stop watching after the a. That simple operation will do most of the work in this section. Let’s first arrange the words so that we can talk about it: a shorter word points to each word of which it is a prefix. This gives us a category \mathcal P.

A category consists of objects, arrows between objects, an identity arrow \mathrm{id}_u : u \to u for each object, and a composition operation that turns f : u \to v and g : v \to w into g \circ f : u \to w. Composition is associative, and composing with an identity changes nothing.

For \mathcal P, the objects are strings. There is exactly one arrow i_{u,v} : u \to v when u is a prefix of v, and no arrow otherwise. For example:

\texttt{""} \longrightarrow \texttt{"a"} \longrightarrow \texttt{"ab"}.

The composite is the prefix inclusion from "" to "ab". Identities exist because every word is its own prefix. Composition exists because the prefix relation is transitive. And the category laws hold because there is at most one arrow between any two objects: there is no choice about what a composite can be.

The objects are all strings, including strings that our program cannot emit. It is the presheaf that will tell us which strings have executions behind them.

A presheaf assigns executions to words

Definition. A set-valued presheaf F on a category \mathcal C assigns:

• a set F(u) to each object u;
• a function F(f) : F(v) \to F(u) to each arrow f : u \to v;

subject to the laws

F(\mathrm{id}_u)=\mathrm{id}_{F(u)}, \qquad F(g\circ f)=F(f)\circ F(g).

The direction of the function is reversed. For our prefix category, an arrow points from a shorter word to a longer one, but the corresponding function will forget the end of an execution. Let’s implement the two parts of the definition.

First, fix a program p and let F_p(w) be the set of its executions emitting exactly w. The word describes what we observed. An execution must additionally record which transitions we took to produce it.

Recall that steps p lists the possible next transitions, each as an emitted character and a continuation. Number those entries starting at zero. At each step, record the number of the entry we selected, then continue with its continuation. The resulting list of numbers is a Run.

For example, steps earlier offers two entries. Entry 0 emits 'a' and leaves Emit 'b' Stop; entry 1 also emits 'a', but leaves Emit 'c' Stop. The log says a either way. The continuation rather cares which one we picked.

To produce "ac", we must select entry 1. We are then running Emit 'c' Stop, whose steps list has just one entry: ('c', Stop), numbered 0. This execution is therefore recorded as [1,0].

The numbering starts again at each step. These numbers are positions in the current list of available transitions, not positions in the source code, and not characters in the trace. In particular, recording 0 is useful even when there is only one available transition: we want one entry per emitted character, so truncating the record will truncate the execution.

Now executions p word will enumerate all such records that produce word. It takes a program and a requested trace, and returns a list of runs:

type Run = [Int]

executions :: Proc -> String -> [Run]
executions _ "" = [[]]
executions p (c : cs) =
  [ i : rest
  | (i, (label, q)) <- zip [0..] (steps p)
  , label == c
  , rest <- executions q cs
  ]

Read the comprehension as a small search. zip [0..] (steps p) numbers the available transitions. label == c keeps only transitions emitting the next requested character. The recursive call finds all ways for the continuation q to emit the remaining characters cs. Prepending i records the transition we just took.

If no characters remain to be matched, there is exactly one way to finish this search: take no more transitions. Hence executions _ "" = [[]]. This does not assert that the program has terminated; we are allowed to stop observing it. If no transition matches the next character, the comprehension returns [].

There are two list levels: the outer list enumerates possible executions, and each inner list records the transitions of one execution. For example, [[0],[1]] means two different one-step executions, whereas [[0,1]] means one two-step execution.

That’s our assignment w \mapsto F_p(w): give it a word, get back the ways of producing it. The Haskell list enumerates a finite set; the order in which we list its members doesn’t matter.

-- executions later "a"
-- [[0]]

-- executions earlier "a"
-- [[0],[1]]

-- executions later "ab"
-- [[0,0]]

-- executions later "ac"
-- [[0,1]]

-- executions earlier "ab"
-- [[0,0]]

-- executions earlier "ac"
-- [[1,0]]

For later, both completed runs start with transition 0. For earlier, one starts with transition 0 and the other with transition 1. The integers name transition occurrences. They are not additional characters in the observed trace.

In particular, F_p(\epsilon)=\{[]\}: there is one empty execution. This is a singleton set, represented by [[]], not the empty set []. An impossible trace such as "z" gets the empty set instead.

Now for the arrows. To keep just the beginning of a run, we only need take. For a prefix inclusion i_{u,v}, define

F_p(i_{u,v}) : F_p(v) \longrightarrow F_p(u), \qquad F_p(i_{u,v})(e)=\operatorname{take}(|u|,e).

Here |u| is the length of the shorter word. In Haskell:

restrictPrefix :: Int -> Run -> Run
restrictPrefix = take

The type alone is broader than the mathematical function: we apply it with length u, to a member of executions p v, when u is a prefix of v. Under those conditions, its result belongs to executions p u.

For later, restricting either completed run to "a" gives [0]. For earlier, restricting "ab" gives [0], whereas restricting "ac" gives [1]. The set assignment and the arrow assignment both contribute information.

The functor laws are properties of take

We’ve written the functions; now we have to pay our mathematical debts and check the two laws. For an identity arrow, the shorter word is the whole word. Every run e\in F_p(u) has length |u|, so

F_p(\mathrm{id}_u)(e)=\operatorname{take}(|u|,e)=e.

For composition, suppose u is a prefix of v, and v a prefix of w. Then, for e\in F_p(w),

\begin{aligned} \bigl(F_p(i_{u,v})\circ F_p(i_{v,w})\bigr)(e) &=\operatorname{take}(|u|,\operatorname{take}(|v|,e))\\ &=\operatorname{take}(|u|,e)\\ &=F_p(i_{u,w})(e). \end{aligned}

The corresponding diagram has executions at its nodes and restriction functions on its arrows. Both routes from the leftmost set to the rightmost set give the same result:

This diagram commutes: following a path of arrows and composing its functions gives the same function as following any other path with the same endpoints. The words here illustrate the law for any program p; some of these sets may be empty.

These are exactly the familiar Haskell equalities:

-- for a run xs of length n:
-- take n xs == xs

-- for 0 <= k <= m <= length xs:
-- take k (take m xs) == take k xs

Nice: take has paid both debts. The executions and these restriction functions really do form a presheaf.

The usual compact notation is F_p : \mathcal P^{op} \to \mathbf{Set}. \mathbf{Set} is the category of sets and functions, and \mathcal P^{op} is \mathcal P with its arrows reversed. A presheaf is also called a contravariant functor from \mathcal P to \mathbf{Set}.

Haskell’s Functor also has an object assignment, an action on arrows, and identity and composition laws. Here, however, the input objects are words rather than Haskell types, and the arrows are prefix inclusions rather than arbitrary Haskell functions. That is why we haven’t written a Functor instance for Run.

What the extra information buys us

Each node below is one execution. Its Trace is the emitted word, and its Run is the list of transition numbers recording how that word was produced. The green nodes all have trace "a"; the question is whether there is one such execution or two. Each arrow forgets the final transition (take 1 for the completed runs, take 0 for the one-step runs):

In later, the two completed executions restrict to the same execution over a. In earlier, they restrict to different executions over a. Reading the arrows backwards gives the branching execution trees.

Reading such a finite tree back into our language is straightforward. A leaf becomes Stop. Reversing a restriction that forgot a c step gives an edge that emits c, hence Emit c .... Several possible next edges become a Choice between the corresponding programs.

The restriction maps tell us which edges belong under the same node. They are what makes these two trees different, even though the trace strings agree.

But there is an important catch: we computed the presheaf from a program. We did not infer it from an ordinary log. If someone only hands us ["", "a", "ab", "ac"], both trees remain possible, even if that list contains every possible trace. Neither presheaves nor any other notation can recover a distinction that the observations have erased.

The presheaf is a richer model of execution. We might obtain it by instrumenting a program, or propose it as a candidate model. Reading it back gives us an implementation of that model, not a guarantee of recovering the original AST.

Sheaves and execution segments

Cutting an execution in two

We know how to keep the beginning of an execution. Can we also keep its middle, and then put the pieces back together? Let’s stay with earlier and the trace "ac". No new language required; this one still has some mileage in it.

There are three boundaries around those two emitted characters:

The first segment contains the a transition and its two boundary states. The second contains the c transition and its two boundary states. They meet at boundary 1: the state where the first segment ends and the second starts.

Recall the two ways for earlier to emit a:

-- transition 0: earlier --a--> Emit 'b' Stop
-- transition 1: earlier --a--> Emit 'c' Stop

The second segment needs to start in Emit 'c' Stop. Only one of those first segments leaves it in the right place. Concatenating the strings is easy; concatenating their explanations requires a little more care.

That is the question the sheaf condition will answer: when do partial executions fit together, and do they determine exactly one whole execution?

Prefixes alone don’t give us much to assemble. Any family of prefixes accounting for the final transition of a finite trace already contains the whole trace. We need pieces that can start later, with enough information to understand them without their missing prefix.

A category of placed segments

Fix a word w of length n. For most of this section, w=\texttt{"ac"}. We number its boundaries from 0 to n. The character w_i labels the transition from boundary i to boundary i+1.

Write [i,j] for the piece from boundary i through boundary j, including both endpoints and every transition between them. It contains j-i characters and j-i+1 boundaries. In Haskell:

data Piece = Empty | Span Int Int
  deriving (Eq, Show)

For "ac", Span 0 2 keeps the whole execution. Span 0 1 keeps the a step with a state on each side, and Span 1 2 does the same for the c step. So far, just the cuts we drew above.

What about Span 1 1? We have brought the scissors together at boundary 1. No transition remains, but there is still a state there: the program left after a, ready to emit c. That is useful information! Empty, on the other hand, keeps nothing, not even a boundary. We’ll need both kinds of piece.

These pieces form our next category, \mathcal I_w. Its objects are Empty and the intervals [i,j] with 0\leq i\leq j\leq n. An arrow U\to V says that U is included in V; there is exactly one such arrow when that inclusion holds, and none otherwise. Empty is included in every piece.

For nonempty intervals, [i,j]\subseteq[k,l] means k\leq i\leq j\leq l. Identities and composition are inclusion into oneself and inclusion in stages. As with the prefix category, the category laws follow from transitivity and the fact that there is at most one arrow between any two objects.

The positions are part of the object. In the word "aa", [0,1] and [1,2] contain the same character but are different pieces. Their intersection is the single boundary [1,1], not a shared a transition.

Our intervals are pieces of a labelled path: boundaries and transitions. They are not merely sets of integer indices. This distinction will matter when we decide whether some pieces cover a whole one.

Sections carry their starting state

Earlier, a Run was enough because we always knew the starting program. Once we detach a segment, we must also retain the state from which its transitions run. We’ll make every boundary state explicit:

data Section
  = NoData
  | Section
      { offset      :: Int
      , states      :: [Proc]
      , transitions :: Run
      }
  deriving (Eq, Show)

offset is the first boundary’s position. A section over [i,j] has j-i+1 states and j-i transition numbers. The numbers still index steps at the current state, just as they did before.

For example, the execution of earlier producing "ac" is:

acSection :: Section
acSection = Section 0
  [earlier, Emit 'c' Stop, Stop]
  [1, 0]

There is a state on each side of each transition. Cutting at boundary 1 will keep Emit 'c' Stop in both pieces. No guessing what the other piece meant.

Which states should a detached piece be allowed to start from? Let’s use the programs we can actually reach from p, by following any of its transitions. These are its residual programs, and we’ll call their finite set Q_p. It includes p itself:

residuals :: Proc -> [Proc]
residuals p = nub $
  p : [r | (_, q) <- steps p, r <- residuals q]

A residual program is just the code left to run. We identify equal Proc values as the same state, but still distinguish different entries in their steps lists. This keeps separate transition occurrences, even when they happen to have the same label and destination.

We can now say precisely what belongs to S_{p,w}([i,j]). A section over [i,j] consists of states q_i,\ldots,q_j\in Q_p and transition numbers r_i,\ldots,r_{j-1} such that

\operatorname{steps}(q_k)[r_k]=(w_k,q_{k+1}) \qquad(i\leq k<j).

If i=0, we additionally require q_0=p. At the beginning of the trace, we know which program we started. The empty piece has the singleton set S_{p,w}(\varnothing)=\{\texttt{NoData}\}.

An internal piece does not know its missing prefix. Its starting state may be any member of Q_p that supports the selected transitions. We do not require it to extend to an execution of the whole word: whether it fits with other pieces is precisely what we want to check later.

In particular, a section over [1,1] is a state in Q_p, with no transitions. A section over [0,0] must instead contain the particular state p. One boundary, two different amounts of information depending on where it sits.

We can enumerate the sections with a small extension of executions:

walks :: Proc -> String -> [([Proc], Run)]
walks q "" = [([q], [])]
walks q (c : cs) =
  [ (q : qs, r : rs)
  | (r, (label, next)) <- zip [0..] (steps q)
  , label == c
  , (qs, rs) <- walks next cs
  ]

sections :: Proc -> String -> Piece -> [Section]
sections _ _ Empty = [NoData]
sections p w (Span i j)
  | 0 <= i && i <= j && j <= length w =
      [ Section i qs rs
      | q <- if i == 0 then [p] else residuals p
      , (qs, rs) <- walks q (take (j - i) (drop i w))
      ]
  | otherwise = []

walks records the state before taking each transition, as well as its number. sections chooses the allowed starting states and the substring to match. As before, lists enumerate finite sets; their order has no mathematical meaning. The Haskell types allow malformed values, so our mathematical claims concern valid pieces and sections such as those produced by sections.

Let’s name the sets of sections for our running example:

firstPieces, secondPieces, boundaryPieces :: [Section]
firstPieces    = sections earlier "ac" (Span 0 1)
secondPieces   = sections earlier "ac" (Span 1 2)
boundaryPieces = sections earlier "ac" (Span 1 1)

-- map transitions firstPieces
-- [[0],[1]]

-- secondPieces
-- [Section {offset = 1, states = [Emit 'c' Stop,Stop],
--           transitions = [0]}]

-- sections earlier "ac" (Span 0 2) == [acSection]
-- True

We haven’t lost our original executions along the way. If the piece starts at zero, we already know its first state is p; following the transition numbers recovers all the others. In other words,

S_{p,w}([0,k])\cong F_p(\operatorname{take}(k,w)).

The left side writes the intermediate states down; the right side reconstructs them by following the run. They carry the same information.

Restriction selects a segment

An inclusion U\subseteq V should give a restriction function S(V)\to S(U). From now on, write S for S_{p,w} with p and w fixed.

Restriction keeps the requested states and transitions, adjusting the starting position. The one extra state is easy to overlook: two transitions need three boundaries.

restrictTo :: Piece -> Section -> Maybe Section
restrictTo Empty _ = Just NoData
restrictTo (Span i j) (Section k qs rs)
  | k <= i && i <= j && j <= k + length rs =
      Just $ Section i
        (take (j - i + 1) (drop (i - k) qs))
        (take (j - i)     (drop (i - k) rs))
restrictTo _ _ = Nothing

-- restrictTo (Span 1 2) acSection
-- Just (Section {offset = 1, states = [Emit 'c' Stop,Stop],
--                transitions = [0]})

-- restrictTo (Span 1 1) acSection
-- Just (Section {offset = 1, states = [Emit 'c' Stop],
--                transitions = []})

-- restrictTo Empty acSection
-- Just NoData

The Maybe rejects attempts to select outside the supplied section. For a valid inclusion and a valid section, restriction always succeeds. Every retained step still has the same source, label and destination, so it remains a valid step. If the selected piece contains boundary 0, its state there is still p.

The presheaf laws are again properties of list slicing. Restricting to the original piece changes nothing. For U\subseteq V\subseteq W, selecting V and then U gives the same states and transitions as selecting U directly:

-- for valid nested pieces u, v and a section x of the outer piece:
-- (restrictTo v x >>= restrictTo u) == restrictTo u x

So we have another presheaf, S:\mathcal I_w^{op}\to\mathbf{Set}, with segments in place of prefixes. Taking pieces works. Let’s try putting them back together.

Covering a trace, including its steps

Let’s cut "ac" where we intended to: the first piece U=[0,1] contains the a step, and the second piece V=[1,2] contains the c step. Between them, they contain everything in H=[0,2]. We call this a cover of H.

There is a small trap here. Suppose we kept [0,1] and the final boundary [2,2] instead. All three boundary numbers would still be present. But the c transition would have gone missing! Knowing the state before a step and the state after it isn’t the same as knowing which step connected them.

The dashed arrow shows what the second collection fails to retain. This is why we have been treating intervals as pieces of a path, with both boundaries and transitions, rather than just sets of boundary numbers.

Here is the rule we’ll use: a family of inclusions \{U_a\to H\} is a cover if every boundary and every transition of H belongs to at least one U_a. A piece can cover itself, of course. Keeping only the three boundaries of "ac" won’t do: that loses both steps. At the other extreme, Empty needs no pieces at all, so we allow its empty cover.

We can turn that rule into a small check. First, inclusion of pieces:

included :: Piece -> Piece -> Bool
included Empty _ = True
included _ Empty = False
included (Span i j) (Span k l) = k <= i && j <= l

As with our earlier functions, we use valid pieces of the fixed word: the endpoints of Span i j satisfy 0 <= i <= j <= length w. The type doesn’t enforce this for us.

To check a cover, look for each individual boundary and each individual step in at least one proposed piece. We also check that those pieces belong to the region we’re covering:

covers :: Piece -> [Piece] -> Bool
covers h pieces =
  all (`included` h) pieces &&
  all (\cell -> any (cell `included`) pieces) (cells h)
  where
    cells Empty = []
    cells (Span i j) =
      [Span k k       | k <- [i..j]] ++
      [Span k (k + 1) | k <- [i..j - 1]]

acCover :: [Piece]
acCover = [Span 0 1, Span 1 2]

-- covers (Span 0 2) acCover
-- True

-- covers (Span 0 2) [Span 0 1, Span 2 2]
-- False

-- covers Empty []
-- True

The two lists in cells are the important bit. The first checks the circles in our diagram; the second checks the arrows. Checking only the circles would accept the broken cover we just drew.

The shared boundary, and what a pullback means

Go back to our good cover. What did we keep twice? The first piece ends at boundary 1, and the second starts there. Their overlap is therefore B=[1,1]. It contains no transition, but it still has something to tell us: which state the execution was in between a and c.

There are two inclusions of B to keep track of. Into U, it picks out the last boundary; into V, it picks out the first. Both refer to the same position in H:

These are arrows between pieces, not restriction functions between sets of executions. Both routes from B to H include exactly the same boundary, so the square commutes.

There is more to an intersection than making this square commute. Empty could sit at the left and give a commuting square too, but it would forget our shared boundary. We want the whole common part: anything included in both U and V must also be included in B. Here the only possibilities are [1,1] and Empty, and both fit into B in exactly one way.

This is an example of a pullback. In a general category, start with arrows f:U\to H and g:V\to H. A pullback consists of an object B and arrows \pi_U:B\to U, \pi_V:B\to V satisfying

f\circ\pi_U=g\circ\pi_V,

with the following property: whenever an object X has arrows a:X\to U and b:X\to V satisfying f\circ a=g\circ b, there is a unique arrow h:X\to B such that

\pi_U\circ h=a,\qquad \pi_V\circ h=b.

So any other way of mapping into both sides, consistently over H, goes through the pullback in exactly one way. That’s what makes it the common part we were looking for. The notation is U\times_H V; the subscript says which object the two pieces are being compared inside.

For inclusions of our segments, this definition reduces to intersection. There is no new calculation to perform:

[i,j]\times_H[k,l]=[\max(i,k),\min(j,l)]

provided the left endpoint is no larger than the right; otherwise the result is Empty. If the endpoints are equal, we keep that single boundary. Thus [0,1]\times_H[1,2]=[1,1], while [0,0]\times_H[2,2] is empty.

Here is that intersection calculation on Piece:

intersectPieces :: Piece -> Piece -> Piece
intersectPieces (Span i j) (Span k l)
  | max i k <= min j l = Span (max i k) (min j l)
intersectPieces _ _ = Empty

-- intersectPieces (Span 0 1) (Span 1 2)
-- Span 1 1

-- intersectPieces (Span 0 0) (Span 2 2)
-- Empty

The <= matters: meeting at a boundary still counts as meeting. We can even express the pullback property using included:

-- for valid pieces x, u and v inside the same h:
-- included x (intersectPieces u v)
--   == (included x u && included x v)

This says that x fits into the overlap exactly when it fits into both pieces. There is no separate choice of inclusion to record: in our category, any such arrow is unique.

We’ll meet pullbacks again shortly, this time for functions between sets of executions. Having a definition that works beyond inclusions is going to earn its keep.

What happens when we zoom in?

A covering rule should survive taking smaller pieces. Let’s check ours before we give it a grander name.

Suppose we only want to inspect the first segment U=[0,1]. Intersect each member of our cover with U. The first piece stays [0,1]; the second shrinks to [1,1], since its c step lies outside the region we’re keeping. Together, these still cover U: we kept its a step and both its boundaries.

Let’s do that zoom with the functions we just wrote:

pullBackCover :: Piece -> [Piece] -> [Piece]
pullBackCover region = map (`intersectPieces` region)

-- pullBackCover (Span 0 1) acCover
-- [Span 0 1, Span 1 1]

-- covers (Span 0 1) (pullBackCover (Span 0 1) acCover)
-- True

pullBackCover just intersects each piece with the region. It doesn’t assume that its input covers anything; the claim we’re about to make is that it preserves covers when the region lies inside the original whole.

The same reasoning works for any smaller piece W. Every boundary or step of W belonged to some covering piece before we zoomed in. It still belongs to that piece’s intersection with W. In symbols, whenever \{U_a\to H\} covers H and W\to H is an inclusion, the family

\{U_a\times_H W\to W\}

covers W. This is called stability under pullback. In this example it says exactly what we just checked: intersecting all the covering pieces with the region we want to keep leaves that region covered.

We also want to be able to cut our pieces again. If a family covers H, and we cover each member by smaller pieces, those smaller pieces still cover H. Every boundary and transition was in some original piece, and survives in at least one of its replacements. This is composition of covers.

Together with the fact that a piece covers itself, these are the three rules for a pretopology: identity covers, stability under pullback, and composition. The word packages the checks we have just done.

From covers to a Grothendieck topology

There are several ways to list essentially the same cover. For example, adding [1,1] to our pair [0,1],[1,2] contributes nothing new: that boundary is already inside both pieces. We can avoid worrying about such extra entries by including all subpieces from the start.

For our cover of "ac", this means taking the two one-step segments, all three individual boundaries, and Empty. It does not mean adding [0,2]: neither of the two covering pieces contains the whole path.

A collection of pieces inside H closed under taking smaller pieces is called a sieve on H. In categorical language, it is a collection of arrows into H closed under precomposition: if U\to H is in it, so is the composite W\to U\to H. Here that simply says, “if we have this piece, we have its subpieces too.”

For our finite intervals, closing a family under subpieces is easy to compute:

subpieces :: Piece -> [Piece]
subpieces Empty = [Empty]
subpieces (Span i j) =
  Empty : [Span k l | k <- [i..j], l <- [k..j]]

generatedSieve :: [Piece] -> [Piece]
generatedSieve = nub . concatMap subpieces

-- generatedSieve acCover
-- [Empty, Span 0 0, Span 0 1, Span 1 1, Span 1 2, Span 2 2]

-- Span 0 2 `elem` generatedSieve acCover
-- False

-- covers (Span 0 2) (generatedSieve acCover)
-- True

concatMap subpieces adds everything we can select inside each chosen piece; nub removes duplicates such as the shared boundary. Nothing here joins the two segments into a larger one. That is why the whole Span 0 2 stays out.

We declare a sieve covering when it contains a covering family. Our sieve containing both one-step segments qualifies. The sieve of just boundaries and Empty doesn’t, because neither transition is in it. The covering sieves obtained this way form a Grothendieck topology J; the three rules above ensure the required topology axioms hold.

A category equipped with a Grothendieck topology is a site. Ours is (\mathcal I_w,J). The category tells us which pieces we can select; the topology tells us when we have selected enough of them. Quite a lot of terminology for cutting up "ac", but we now have a precise version of “check the pieces and their overlaps” that works in other categories too.

The word topology doesn’t mean we have silently turned these segments into open subsets of the real line. Their covers are the ones we chose and checked. Now let’s put executions on them and see whether they agree.

When local executions match

Keep p = earlier, w = "ac", and the cover by U=[0,1] and V=[1,2]. A section over U explains the first transition. A section over V explains the second. They form a matching pair when their restrictions to the shared boundary B=[1,1] are equal.

Let’s try our two first segments. Taking transition 0 produces the a, but leaves Emit 'b' Stop. Our second segment needs Emit 'c' Stop. We have a perfectly good a and a perfectly good c; unfortunately, they aren’t on speaking terms.

Taking transition 1 instead leaves Emit 'c' Stop, exactly where the second segment begins. This pair matches. Both candidates spell "ac" if we just concatenate their characters; comparing the boundary states is what tells them apart.

We can test agreement by applying the restriction functions we already wrote:

matchingPairs :: Piece -> [Section] -> [Section]
              -> [(Section, Section)]
matchingPairs overlap xs ys =
  [ (x, y)
  | x <- xs
  , y <- ys
  , Just sx <- [restrictTo overlap x]
  , Just sy <- [restrictTo overlap y]
  , sx == sy
  ]

matchingAC :: [(Section, Section)]
matchingAC = matchingPairs (Span 1 1) firstPieces secondPieces

-- map (\(x, y) -> (transitions x, transitions y)) matchingAC
-- [([1],[0])]

The overlap argument must be the intersection of the two pieces under consideration. For longer overlapping segments, this compares every shared state and transition, not merely the endpoints. For an empty overlap, both restrictions are NoData, so there is no shared information to disagree about.

For more than two pieces, we make the same check on every overlap. Formally, a family of sections x_a\in S(U_a) over a cover \{U_a\to H\} is a matching family when

S(\pi_a)(x_a)=S(\pi_b)(x_b) \quad\text{in }S(U_a\times_H U_b) \qquad\text{for every }a,b.

Here \pi_a and \pi_b include the overlap into the two pieces. Applying S reverses the arrows: S(\pi_a) and S(\pi_b) restrict the local executions to their common part.

Matching pairs form a fibre product

Start with the ordinary product S(U)\times S(V): all pairs of local executions. We just tried its two members: one failed the boundary check, and one passed. We write the set of pairs that pass as

S(U)\times_{S(B)}S(V).

Read it as “pairs of executions over U and V agreeing over B”. The subscript tells us where to compare their restrictions.

In this example, the comparison maps take the last state of the first segment and the first state of the second. Over the boundary state Emit 'c' Stop, each map has one relevant section in its fibre. These two sections give our matching pair. Over Emit 'b' Stop, the first map has a section, but the second has none, so there is no pair to form.

More generally, for functions f:A\to C and g:B\to C, their fibre product is the set

A\times_C B=\{(a,b)\in A\times B\mid f(a)=g(b)\}.

It is a pullback in the category of sets. Its projections send (a,b) to a and b. Any two functions from the same set into A and B that agree after mapping to C factor uniquely through this set, by pairing their outputs. This is the same pullback property as before, now applied to sets and functions rather than inclusions of segments.

For our sections, the square of restriction functions looks like this:

Both routes through the square extract the state at boundary 1. The square commutes by the presheaf laws, so restricting a whole execution always gives a matching pair. The next question goes backwards: can every matching pair be assembled into a whole execution?

The sheaf condition is unique gluing

Our matching pair looks ready to concatenate. A sheaf is a presheaf for which this always works, and works uniquely: every matching family on every cover has exactly one gluing. To spell out the condition, given matching sections x_a\in S(U_a) on a cover \{f_a:U_a\to H\}, there must be exactly one x\in S(H) such that

S(f_a)(x)=x_a\qquad\text{for every }a.

For two adjacent segments, gluing concatenates their transition records and joins their state lists, keeping only one copy of the common boundary state:

glueAdjacent :: Section -> Section -> Maybe Section
glueAdjacent (Section i qs rs) (Section j (q : ps) ts)
  | not (null qs)
  , j == i + length rs
  , last qs == q =
      Just (Section i (qs ++ ps) (rs ++ ts))
glueAdjacent _ _ = Nothing

-- [glueAdjacent x y | (x, y) <- matchingAC] == [Just acSection]
-- True

The position check makes the pieces adjacent. The state check makes them compatible. For valid sections, these checks are enough: the last transition of the first piece and the first transition of the second already use the shared state. Their concatenation is a valid execution.

In our example, the two possible attempts are:

-- [glueAdjacent x y | x <- firstPieces, y <- secondPieces]
--   == [Nothing, Just acSection]
-- True

-- [z | (x, y) <- matchingAC, Just z <- [glueAdjacent x y]]
--   == sections earlier "ac" (Span 0 2)
-- True

The whole word and the placements are already fixed when we ask for a gluing. They tell us which transition occupies each position. We are assembling explanations of that word, not inferring an event order from an unordered bag of log entries.

Why does this prove the sheaf condition for our two-piece cover? First, existence: because the pieces agree at the join, concatenating their transition records gives a valid execution. Cutting it again recovers the pieces we started with.

And uniqueness? Every state and transition of a possible gluing is already specified by one of the pieces. There is nowhere left to make a different choice. Our concatenation is the only candidate.

Consequently, restriction and gluing are inverse functions:

S([0,2])\cong S([0,1])\times_{S([1,1])}S([1,2]).

This makes the restriction square above a pullback square of sets.

The argument works for every cover, including covers with longer overlaps. Choose the state and transition at each position from any covering piece. Agreement on overlaps makes this independent of the choice. Every transition is valid because some piece contains it and both its endpoints. If boundary 0 is present, its state is p. All the data are covered, so the result is unique.

For the empty piece, there is one gluing, NoData, including for its empty cover. For a one-boundary piece, the cover must contain that boundary, so its state is determined too. These cases complete the proof: S_{p,w} is a sheaf.

Nothing in the proof depended on choosing earlier. For later, the matching boundary is instead Choice (Emit 'b' Stop) (Emit 'c' Stop). Its only first a step can be followed by either continuation. The sheaf keeps exactly the branching distinction we saw in the execution presheaf.

What happens when we forget the boundary states

Let’s give the sheaf condition something to complain about. Erase the states from each local execution, retaining only its transition-number record:

forgetStates :: Section -> Run
forgetStates NoData = []
forgetStates (Section _ _ rs) = rs

visibleRuns :: Proc -> String -> Piece -> [Run]
visibleRuns p w piece = nub $ map forgetStates (sections p w piece)

This still defines a presheaf. Restriction slices the transition record using the positions of the source and target pieces; restriction to Empty gives []. It is well-defined because two sections with the same record produce the same sliced record. A restriction of an actual local execution is still an actual local execution, and list slicing satisfies the functor laws.

Now change the requested word to "aa". Our program can emit a, but cannot emit it twice in a row:

-- visibleRuns earlier "aa" (Span 0 1)
-- [[0],[1]]

-- visibleRuns earlier "aa" (Span 1 2)
-- [[0],[1]]

-- visibleRuns earlier "aa" (Span 1 1)
-- [[]]

-- visibleRuns earlier "aa" (Span 0 2)
-- []

Why does the second segment have local executions? It can start in earlier, which belongs to Q_p, and take one of its a transitions. As stipulated when we defined sections, a detached segment does not know the missing prefix.

Choose record [0] in each piece. Both restrict to [] at their overlap, so they match after erasure. Yet there is no whole execution of "aa" to glue them into. The sheaf condition fails.

Before erasure, the mismatch was plain: the first segment ended in Emit 'b' Stop, while the second started in earlier. Removing the states didn’t make those programs equal. It merely removed our way of noticing that they weren’t.

So the overlap wasn’t just bookkeeping. What we retain there determines what compatibility can check. In this example, the boundary states let us compose executions; bare transition numbers let two incompatible pieces slip past the check.

What if we let the word vary?

We’ve spent quite a while inspecting "ac". But a program has more than one possible trace, and we started this article by comparing them. Can we put those words back in the same picture? Yes; we just need to let our pieces carry their characters as well as their positions.

Instead of choosing w first and writing [i,j], write (i,u) for a segment starting at boundary i and spelling the word u. It ends at boundary i+|u|. For example, the first piece of both "ab" and "ac" is now the same object (0,\texttt{"a"}). Their second pieces are (1,\texttt{"b"}) and (1,\texttt{"c"}), respectively.

An inclusion must respect both the positions and the characters. Thus (0,\texttt{"a"}) includes into both (0,\texttt{"ab"}) and (0,\texttt{"ac"}), but (1,\texttt{"b"}) only includes into the first. The two occurrences of a in "aa" are still different pieces: (0,\texttt{"a"}) and (1,\texttt{"a"}). We haven’t thrown their positions away.

Formally, take the category \mathcal L whose objects are (i,u) for i\geq0 and finite words u, together with Empty. There is one arrow (i,u)\to(j,v) exactly when

j\leq i,\qquad i+|u|\leq j+|v|,\qquad u=\operatorname{take}\bigl(|u|,\operatorname{drop}(i-j,v)\bigr).

That last equality checks that the letters agree where the smaller piece sits. Empty includes into everything, as before. The object (i,\texttt{""}) still has its single boundary at i, so it isn’t Empty.

Use the same covering rule: account for every boundary and every transition. All our intersection and gluing arguments still work inside a given segment. Our old category \mathcal I_w is exactly the category of subpieces of (0,w) in this larger site: the interval [i,j] corresponds to (i,\operatorname{take}(j-i,\operatorname{drop}(i,w))).

Now fix just the program p. Define \mathcal S_p(i,u) to contain executions of u starting at position i, with their states and transition numbers. As before, the starting state must be p if i=0, and may be any member of Q_p if i>0. Restriction cuts out the selected segment. This gives a single sheaf \mathcal S_p over the larger site. Restricting it to the subpieces of (0,w) gives precisely the sheaf S_{p,w} we have been studying.

The code barely changes. walks already knows how to execute a word from a state; we only need to choose the allowed starting states and record the offset:

segmentSections :: Proc -> (Int, String) -> [Section]
segmentSections p (i, word)
  | i < 0 = []
  | otherwise =
      [ Section i qs rs
      | q <- if i == 0 then [p] else residuals p
      , (qs, rs) <- walks q word
      ]

-- segmentSections earlier (0, "ac") == [acSection]
-- True

-- segmentSections earlier (1, "c") == secondPieces
-- True

The pair is our object (i,u): the word is now part of the piece we ask for, not a larger trace chosen elsewhere. Empty still has its sole section NoData; this function handles the nonempty pieces, including a single boundary when word is "".

To recover our old fixed-word function, just select the corresponding substring:

-- for 0 <= i <= j <= length w:
-- segmentSections p (i, take (j - i) (drop i w))
--   == sections p w (Span i j)

And at position zero, keeping just the transition numbers gives back our original executions:

-- for any finite program p and word w:
-- map transitions (segmentSections p (0, w)) == executions p w

-- map transitions (segmentSections earlier (0, "a"))
-- [[0],[1]]

-- map transitions (segmentSections later (0, "a"))
-- [[0]]

That is the concrete correspondence behind

\mathcal S_p(0,w)\cong F_p(w).

At position zero the initial state is known, so the transition record once again determines all the states. A prefix inclusion u\to v gives the inclusion (0,u)\to(0,v); its restriction function is our old take. Thus the initial segments recover the execution presheaf from the first half, while the other segments let us cut and glue inside those executions.

We can check the arrows too. Start with our execution of "ac", cut it down to its first step, then keep its transition numbers:

-- fmap transitions (restrictTo (Span 0 1) acSection)
-- Just [1]

-- Just (restrictPrefix 1 (transitions acSection))
-- Just [1]

Same answer, whether we cut the section first or forget the states first. More generally, for s in segmentSections p (0, w) and 0 <= k <= length w, the square commutes as a Haskell equality:

-- fmap transitions (restrictTo (Span 0 k) s)
--   == Just (restrictPrefix k (transitions s))

The resulting run belongs to executions p (take k w). The Just comes from our defensive restrictTo interface; a valid prefix restriction always succeeds. So we’re recovering both parts of the presheaf: its execution sets and the functions between them.

Here are those two views together. Above, the initial "a" piece includes into both longer words. Below, applying the sheaf reverses those arrows; under the displayed identifications with F_p, both restrictions are take 1.

The shared green node below is a set of executions of "a", not a claim that every longer execution has the same first step. That distinction is exactly what our original presheaf recorded.

Let’s actually follow those two arrows. This function enumerates the executions of a word, restricts each to its first k steps, and reads off the resulting run:

prefixRuns :: Proc -> Int -> String -> [Run]
prefixRuns p k word =
  [ transitions prefix
  | whole <- segmentSections p (0, word)
  , Just prefix <- [restrictTo (Span 0 k) whole]
  ]

-- prefixRuns earlier 1 "ab"
-- [[0]]

-- prefixRuns earlier 1 "ac"
-- [[1]]

-- prefixRuns later 1 "ab"
-- [[0]]

-- prefixRuns later 1 "ac"
-- [[0]]

There it is: earlier reaches different executions of the shared "a" piece, whereas later reaches the same one. The function lists the prefixes of the executions we supplied; it doesn’t search for every possible execution of the shorter word.

And we can perform exactly the same calculation using only the original presheaf:

-- for 0 <= k <= length word:
-- prefixRuns p k word == map (restrictPrefix k) (executions p word)

The branching distinction is still there. Fixing "ac" was a way to concentrate on one gluing problem, not a requirement that every word live in an unrelated model.

From this sheaf to a topos

So far we’ve changed the program, and now we’ve allowed the word to vary too. There’s one more useful change of viewpoint: consider all the sheaves on a site together. For the moment, return to our small site (\mathcal I_w,J). It specifies a word and its pieces, but no program. Different programs can supply different sheaves on it, and so can other kinds of local data.

A map \eta:S\to T of sheaves is a function \eta_U:S(U)\to T(U) for each piece U, compatible with every restriction. For an inclusion f:U\to V,

T(f)\circ\eta_V=\eta_U\circ S(f).

In words: transform a whole section and then restrict, or restrict first and transform the smaller section; the result must be the same. This is a natural transformation. Such maps let us express a change of description that respects taking pieces.

For a concrete example, imagine a very modest execution monitor. At each boundary, it records just whether the program has any next step available. It doesn’t care which character that step emits:

data Activity
  = NoActivity
  | Activity Int [Bool]
  deriving (Eq, Show)

activity :: Section -> Activity
activity NoData = NoActivity
activity (Section i qs _) =
  Activity i [not (null (steps q)) | q <- qs]

-- activity acSection
-- Activity 0 [True, True, False]

Both earlier and its continuation Emit 'c' Stop can take a step. Stop can’t. We have turned an execution into a little strip of indicator lights.

Let’s say precisely which sheaf receives this strip. For a piece [i,j], let T([i,j]) contain all lists of j-i+1 booleans, one per boundary, with offset i. Let T(\varnothing)=\{\texttt{NoActivity}\}. Restriction keeps the selected boundaries:

restrictActivity :: Piece -> Activity -> Maybe Activity
restrictActivity Empty _ = Just NoActivity
restrictActivity (Span i j) (Activity k flags)
  | k <= i && i <= j && j < k + length flags =
      Just (Activity i (take (j - i + 1) (drop (i - k) flags)))
restrictActivity _ _ = Nothing

This T is a sheaf: if the strips agree at shared boundaries, they assemble into exactly one strip on the whole piece. Every boundary is covered, so no light is left unspecified. We allow all strips, including ones that no execution of p produces. Taking only the images of actual executions would require a separate gluing check, as our earlier visibleRuns example warned us.

Now compare the two routes around the naturality square. For the c segment, we can either make the lights first and cut them down, or cut the execution first and then make its lights:

-- restrictActivity (Span 1 2) (activity acSection)
-- Just (Activity 1 [True, False])

-- fmap activity (restrictTo (Span 1 2) acSection)
-- Just (Activity 1 [True, False])

Both routes meet at the same green node:

The lower route uses fmap activity because restrictTo returns a Maybe: we compute the lights inside its successful Just. The upper route computes the whole strip first, then selects boundaries 1 and 2.

The same equality holds for every valid section s and subpiece piece:

-- restrictActivity piece (activity s)
--   == fmap activity (restrictTo piece s)

Why? activity applies the same test independently to every state, and list slicing commutes with that map. At Empty, both routes give Just NoActivity. So activity supplies the functions \eta_U:S(U)\to T(U), restrictTo supplies S(f), and restrictActivity supplies T(f). We’ve written a map of sheaves, not just a function on whole executions.

This also works on the larger site where words vary. For example, map activity (segmentSections earlier (0, "ac")) gives [Activity 0 [True, True, False]]; restricting any of those sections satisfies the same equality. The monitor only needs the states in the selected segment, so choosing a different surrounding word doesn’t change how it works.

The category of set-valued sheaves and these maps is written

\operatorname{Sh}(\mathcal I_w,J).

A category equivalent to the category of sheaves on a small site is called a Grothendieck topos. That’s what we’ve just constructed. The site specifies the pieces and covers; the topos collects the sheaves and the maps between them. Our execution sheaf is one object in it.

The larger site of labelled segments \mathcal L gives a topos too, with one \mathcal S_p describing all the traces of each program p. So we can work either around a particular word or in a setting where the words vary. The choice changes the site, not what “sheaf” means.

Why care about the surrounding category? It lets us construct new models from old ones. Products pair local descriptions. Fibre products pair them subject to agreement on some shared information, just as our boundary-state check did. These constructions are performed piece by piece and remain sheaves. More generally, a topos has function objects and an internal logic for expressing properties of its objects. Those are reasons to study the whole category, rather than just one particularly agreeable execution model.

For this finite example, there is also a reassuringly concrete description. Every segment containing a transition is covered by its one-step segments, with boundaries as their overlaps. Thus a sheaf is determined by its sets at individual boundaries and steps, and the two endpoint restriction functions for each step:

For a general sheaf, these are sets of data, not necessarily program states. Longer sections are obtained by iterated fibre products matching the endpoints. Conversely, any such diagram of sets determines a sheaf by that construction, with a singleton at Empty. So, in this fixed-word example, we can still get our hands on every part of the construction: sets at the steps and boundaries, functions between them, and matching pairs to build longer runs.

Conclusion and bibliography

What we constructed

We began with a slightly disappointing discovery: earlier and later leave the same trace strings. Keeping the executions and their prefix restrictions let us see where their choices differ. That was our presheaf.

Then we tried cutting those executions somewhere other than at the end. A detached piece needed to remember its starting state, and putting two pieces back together meant checking the state at their join. Once we chose covers that account for every step, those matching pieces determined a unique whole execution. That was our sheaf.

The site made our choice of pieces and covers explicit; the topos lets us work with all the sheaves respecting that choice. And by putting positions and characters into the pieces, we could let the word vary and recover our original execution presheaf inside the larger construction.

There is still no way to tell earlier from later using only their trace strings. We got the extra information by following the programs. The useful part of the mathematics is making clear what that information buys us: which runs share a beginning, which pieces can follow each other, and what we lose when we forget the state at a cut.

Further reading

• Presheaf models for CCS-like languages, by Gian Luca Cattani and Glynn Winskel. A broader setting for presheaf models of processes, where branching behaviour matters beyond sets of trace strings.

• Dynamical Systems and Sheaves, by Patrick Schultz, David I. Spivak and Christina Vasilakopoulou. Develops a categorical framework for interconnected systems using sheaves to describe behaviour through time, including discrete and continuous systems.

• Temporal Type Theory: A Topos-Theoretic Approach to Systems and Behavior, by Patrick Schultz and David I. Spivak. Takes the connection between interval sheaves, behaviour and topos logic much further. Its interval site is richer than the finite, fixed-word site used here.

• Sites and Sheaves, in the Stacks Project. A formal reference for presheaves, coverings, sheaves and topoi; useful for following the general definitions beyond this finite example.

• Innocent Strategies are Sheaves over Plays, by Takeshi Tsukada and C.-H. Luke Ong. A different application to higher-order game semantics, with a site of plays and a locality condition describing innocence. Our gluing of consecutive execution segments is not that innocence condition, but it provides a first example of what a sheaf model of behaviour can look like.

Posted: 2026-10-21