arXiv:1408.1675v3 [] 12 Aug 2014

Database Queries that Explain their Work
James Cheney

Amal Ahmed

Umut A. Acar

University of Edinburgh
jcheney@inf.ed.ac.uk

Northeastern University
amal@ccs.neu.edu

Carnegie Mellon University &
INRIA-Rocquencourt
umut@cs.cmu.edu

Abstract

promising results have been identified, a scientist may want to
extract just that information that is needed to explain the result,
without showing all of the intermediate search steps or uninteresting results. Conversely, if the results are counterintuitive, the
scientist may want to identify the underlying data that contributed
to the anomalous result. Missier et al. [24] introduced the idea of
a “golden trail”, or a subset of the provenance trace that explains,
or allows reproduction of, a high-value part of the output. They
proposed techniques for extracting “golden trails” using recursive
Datalog queries over provenance graphs; however, they did not
propose definitions of correctness or reproducibility.
It is a natural question to ask how we know when a proposed
solution, such as Missier et al.’s “golden trail” queries, correctly
explains or can be used to correctly reproduce the behavior of the
original computation. It seems to have been taken for granted that
simple graph traversals suffice to at least overapproximate the desired subset of the graph. As far as we know, it is still an open
question how to define and prove such correctness properties for
most provenance techniques. In fact, these properties might be defined and formalized in a number of ways, reflecting different modeling choices or requirements. In any case, in the absence of clear
statements and proofs of correctness, claims that different forms
of provenance “explain” or allow “reproducibility” are difficult to
evaluate objectively.
The main contribution of this paper is to formalize and prove the
correctness of an approach to fine-grained provenance for database
queries. We build on our approach developed in prior work, which
we briefly recapitulate. Our approach is based on analogies between the goals of provenance tracking for databases and workflows, and those of classical techniques for program comprehension and analysis, particularly program slicing [31] and information flow [28]. Both program slicing and information flow rely critically on notions of dependence, such as the familiar control-flow
and data-flow dependences in programming languages.
We previously introduced a provenance model for NRC (including difference and aggregation operations) called dependency
provenance [12], and showed how it can be used to compute data
slices, that is, subsets of the input to the query that include all of
the information relevant to a selected part of the output. Some other
forms of provenance for database query languages, such as howprovenance [20], satisfy similar formal guarantees that can be used
to predict how the output would change under certain classes of input changes, specifically those expressible by semiring homomorphisms. For example, Amsterdamer et al.’s system [3] is based on
the semiring provenance model, so the effects of deletions on parts
of the output can be predicted by inspecting their provenance, but
other kinds of changes are not supported.
More recently, we proposed an approach to provenance called
self-explaining computation [11] and explored it in the context
of a general-purpose functional programming language [1, 27].
In this approach, detailed execution traces are used as a form of

Provenance for database queries or scientific workflows is often
motivated as providing explanation, increasing understanding of
the underlying data sources and processes used to compute the
query, and reproducibility, the capability to recompute the results
on different inputs, possibly specialized to a part of the output.
Many provenance systems claim to provide such capabilities; however, most lack formal definitions or guarantees of these properties, while others provide formal guarantees only for relatively limited classes of changes. Building on recent work on provenance
traces and slicing for functional programming languages, we introduce a detailed tracing model of provenance for multiset-valued
Nested Relational Calculus, define trace slicing algorithms that extract subtraces needed to explain or recompute specific parts of the
output, and define query slicing and differencing techniques that
support explanation. We state and prove correctness properties for
these techniques and present a proof-of-concept implementation in
Haskell.
Keywords

provenance, database queries, slicing

1. Introduction
Over the past decade, the use of complex computer systems in science has increased dramatically: databases, scientific workflow systems, clusters, and cloud computing based on frameworks such as
MapReduce [16] or PigLatin [26] are now routinely used for scientific data analysis. With this shift to computational science based
on (often) unreliable components and noisy data comes decreased
transparency, and an increased need to understand the results of
complex computations by auditing the underlying processes.
This need has motivated work on provenance in databases, scientific workflow systems, and many other settings [7, 25]. There is
now a great deal of research on extending such systems with rich
provenance-tracking features. Generally, these systems aim to provide high-level explanations intended to aid the user in understanding how a computation was performed, by recording and presenting
additional “trace” information.
Over time, two distinct approaches to provenance have emerged:
(1) the use of annotations propagated through database queries to
illustrate where-provenance linking results to source data [7], lineage or why-provenance linking result records to sets of witnessing input records [15], or how-provenance describing how results
were produced via algebraic expressions [20], and (2) the use of
graphical provenance traces to illustrate how workflow computations construct final results from inputs and configuration parameters [5, 21, 29]. However, to date few systems formally specify the
semantics of provenance or give formal guarantees characterizing
how provenance “explains” results.
For example, scientists often conduct parameter sweeps to
search for interesting results. The provenance trace of such a computation may be large and difficult to navigate. Once the most

1

In general, we use sequences of natural numbers [i1 , . . . , in ] ∈ N∗
as indices, and we maintain a stronger invariant: the set of indexes
used in a multiset must form a prefix code. We define a semantics
for NRC expressions over such collections that is fully deterministic and does not resort to generation of fresh intermediate labels;
in particular, the union operation adjusts the labels to maintain distinctness.
The second technical challenge involves extending patterns for
partial collections. In our previous work, any subexpression of a
value can be replaced by a hole. This works well in a conventional functional language, where typical values (such as lists and
trees) are essentially initial algebras built up by structural induction.
However, when we consider unordered collections such as bags,
our previous approach becomes awkward.
For example, if we want to use a pattern to focus on only the
B field of the second record in query result Q(R), we can only
do this by deleting the other record values, and the smallest such
pattern is {[1, r1 ].✷, [2, r2 ].hA:✷, B:3, C:✷i, [2, r3 ].✷}. This is
tolerable if there are only a few elements, but if there are hundreds
or millions of elements and we are only interested in one, this is
a significant overhead. Therefore, we introduce enriched patterns
that allow us to replace entire subsets with holes, for example,
p′ = {[2, r2 ].hB:3; ✷i} ∪˙ ✷. Enriched patterns are not just a
convenience; we show experimentally that they allow traces and
slices to be smaller (and computed faster) by an order of magnitude
or more.

provenance. Traces explain results in the sense that they can be
replayed to recompute the results, and they can be sliced to obtain
smaller traces that provide more concise explanations of parts of
the output. Trace slicing also produces a slice of the input showing
what was needed by the trace to compute the output. Moreover,
other forms of provenance can be extracted from traces (or slices),
and we also showed that traces can be used to compute program
slices efficiently through lazy evaluation. Finally, we showed how
traces support differential slicing techniques that can highlight the
differences between program runs in order to explain and precisely
localize bugs in the program or errors in the input data.
Our long-term vision is to develop self-explaining computation
techniques covering all components used in day-to-day scientific
practice. Databases are probably the single most important such
component. Since our previous work already applies to a generalpurpose programming language, one way to proceed would be to
simply implement an interpreter for NRC in this language, and inherit the slicing behavior from that. However, without some further
inlining or optimization, this naive strategy would yield traces that
record both the behavior of the NRC query and its interpreter, along
with internal data structures and representation choices whose details are (intuitively) irrelevant to understanding the high-level behavior of the query.
1.1 Technical overview
In this paper, we develop a tracing semantics and trace slicing techniques tailored to NRC (over a multiset semantics). This semantics evaluates a query Q over an input database (i.e. environment γ
mapping relation names to table values), yielding the usual result
value v as well as a trace T . Traces are typically large and difficult
to decipher, so we consider a scenario where a user has run Q, inspected the results v, and requests an explanation for a part of the
result, such as a field value of a single record. As in our previous
work for functional programs, we use partial values with “holes” ✷
to describe parts of the output that are to be explained. For example, if the result of a program is just a pair (1, 2) then the pattern
(1, ✷) can be used to request an explanation for just the first component. Given a partial value p matching the output, our approach
computes a “slice” consisting of a partial trace and a partial input
environment, where components not necessary for recomputing the
explained output part p have been deleted.
The main technical contribution of this paper over our previous
work [1, 27] is its treatment of tracing and slicing for collections.
There are two underlying technical challenges; we illustrate both
(and our solutions) via a simple example query Q = σA<B (R) ∪
ρA7→B,B7→A (σA≥B (R)) over a table R with attributes A, B. Here,
σφ is relational selection of all tuples satisfying a predicate φ
and ρA7→B,B7→A is renaming. Thus, Q simply swaps the fields of
records where A ≥ B, and leaves other records alone.
The first challenge is how to address elements of multisets
reliably across different executions and support propagation of
addresses in the output backwards towards the input. Our solution
is to use a mildly enriched semantics in which multiset elements
carry explicit labels; that is, we view multisets of elements from X
as functions I → X from some index set to X. For example, if R
is labeled as follows and we use this enriched semantics to evaluate
the above query Q on R, we get a result:
id
[r1 ]
R=
[r2 ]
[r3 ]

A
1
2
4

B
2
3
3

C
7
8
9

id
[1, r1 ]
Q(R) =
[1, r2 ]
[2, r3 ]

A
1
2
3

B
2
3
4

1.2 Outline
The rest of this paper is structured as follows. Section 2 reviews the
(multiset-valued) Nested Relational Calculus and presents our tracing semantics and deterministic labeling scheme. Section 3 presents
trace slicing, including a simple form of patterns. Section 4 shows
how to enrich our pattern language to allow for partial record and
partial set patterns, which considerably increase the expressiveness
of the pattern language, leading to smaller slices. Section 5 presents
the query slicing algorithm and shows how to compute differential
slices. Section 6 presents additional examples and discussion. Section 7 presents our implementation demonstrating the benefits of
laziness and enriched patterns for trace slicing. Section 8 discusses
related and future work and Section 9 concludes.
Due to space limitations, and in order to make room for examples and high-level discussion, some (mostly routine) formal details
and proofs are relegated to the appendix.

2. Traced Evaluation for NRC
The nested relational calculus [9] is a simply-typed core language
with collection types that can express queries on nested data similar
to those of SQL on flat relations, but has simpler syntax and cleaner
semantics. In this section, we show how to extend the ideas and
machinery developed in our previous work on traces and slicing for
functional languages [27] to NRC. Developing formal foundations
for tracking provenance in the presence of unordered collections
presents a number of challenges not encountered in the functional
programming setting, as we will explain.
2.1 Syntax and Dynamic Semantics
Figure 1 presents the abstract syntax of NRC expressions, values,
and traces. The expression ∅ denotes the empty collection, {e} constructs a singleton collection, and e1 ∪ e2 takes the (multiset) union
of two collections. The operation sum e computes the sum of a collection of integers, while the predicate empty e tests whether the
collection denoted by e is empty. Additional aggregation operations
such as count, maximum and average can
S easily be accommodated.
Finally, the comprehension operation {e′ | x ∈ e} iterates over

C
7
8
9

where in each case the id column contains a distinct index ri . In
Q(R), the first ‘1’ or ‘2’ in each index indicates whether the row
was generated by the left or right subexpression in the union (’∪’).

2

γ, e ⇓ v, T
γ, c ⇓ c, c

γ, e1 ⇓ c1 , T1

···

γ, en ⇓ cn , Tn

γ, f(e1 , . . . , en ) ⇓ f̂(c1 , . . . , cn ), f(T1 , . . . , Tn )
γ, e1 ⇓ v1 , T1

···

γ, x ⇓ γ(x), x

γ, e ⇓ hA1 :v1 , . . . , An :vn i, T

γ, en ⇓ vn , Tn

γ, hA1 :e1 , . . . , An :en i ⇓ hA1 :v1 , . . . , An :vn i, hA1 :T1 , . . . , An :Tn i
γ, e ⇓ true, T
γ, e1 ⇓ v1 , T1
γ, if(e, e1 , e2 ) ⇓ v1 , if(T, e1 , e2 ) ⊲true T1
γ, e1 ⇓ v1 , T1
γ, e2 ⇓ v2 , T2
γ, e1 ∪ e2 ⇓ 1 · v1 ⊎ 2 · v2 , T1 ∪ T2

γ, e ⇓ false, T
γ, e2 ⇓ v2 , T2
γ, if(e, e1 , e2 ) ⇓ v2 , if(T, e1 , e2 ) ⊲false T2
γ, e ⇓ v, T
γ, x ∈ v, e′ ⇓∗ v′ , Θ
[
[
γ, {e′ | x ∈ e} ⇓ v′ , {e′ | x ∈ T } ⊲ Θ

γ, e ⇓ v, T
v=∅
γ, empty e ⇓ true, empty T

γ, x ∈ v, e ⇓∗ v, Θ
∗

γ, x ∈ ∅, e ⇓ ∅, ∅

γ, e1 ⇓ v1 , T1
γ[x 7→ v1 ], e2 ⇓ v2 , T2
γ, let x = e1 in e2 ⇓ v2 , let x = T1 in T2

γ, e.Ai ⇓ vi , T.Ai

γ, ∅ ⇓ ∅, ∅

γ, e ⇓ v, T
γ, {e} ⇓ {ǫ.v}, {T }

γ, e ⇓ {ℓ1 .v1 , . . . , ℓn .vn }, T
γ, sum e ⇓ v1 +̂ . . . +̂vn , sum T

γ, e ⇓ v, T
v 6= ∅
γ, empty e ⇓ false, empty T

γ, x ∈ v1 , e ⇓∗ v1′ , Θ1
γ, x ∈ v2 , e ⇓∗ v2′ , Θ2
∗ ′
γ, x ∈ v1 ⊎ v2 , e ⇓ v1 ⊎ v2′ , Θ1 ⊎ Θ2

γ[x 7→ v], e ⇓ v′ , T
γ, x ∈ {ℓ.v}, e ⇓∗ ℓ · v′ , {ℓ.T }

Figure 2. Traced evaluation.
Other operations on labels and labeled collections will be introduced in due course.
The labels on the elements of a collection provide us with a persistent address for a particular element of the collection. This capability is essential when asking and answering provenance queries
about parts of the source or output data, and when tracking finegrained dependencies.
Both expressions and traces are subject to a type system. NRC
types include collection types {τ } which are often taken to be sets,
bags (multisets), or lists, though in this paper, we consider multiset
collections only. However, types do not play a significant role in
this paper so the typing rules are omitted. For expressions, the
typing judgment Γ ⊢ e : τ is standard and the typing rules for
trace well-formedness Γ ⊢ T : τ are presented in Appendix A.

f ::= + | − | ∗ | / | = | < | ≤ | · · ·
e ::= c | f(e1 , . . . , en ) | x | let e = x in e′
| hA1 : e1 , . . . , An : en i | e.A | if(e, e′ , e′′ )
S
| ∅ | {e} | e1 ∪ e2 | {e′ | x ∈ e}
| empty e | sum e | · · ·
Labels
ℓ ::= ℓ.ℓ′ | ǫ | n
Values
v ::= c | hA1 : v1 , . . . An : vn i
| ∅ | {ℓ1 .v1 , . . . , ℓn .vn }
Environments γ ::= [x1 7→ v1 , . . . , xn 7→ vn ]
Traces
T ::= · · · | if(T, e′ , e′′ ) ⊲true T | if(T, e′ , e′′ ) ⊲false T
S
|
{e | x ∈ T } ⊲ Θ
Trace Sets
Θ ::= {ℓ1 .T1 , . . . , ℓn .Tn }
Types
τ ::= int | bool | hA1 : τ1 , . . . , An : τn i | {τ }
Type Contexts Γ ::= x1 : τ1 , . . . , xn : τn

Operations
Expressions

Traced evaluation NRC traces include a trace form corresponding to each of the expressions described above. The structure of the
traces is best understood by inspecting the typing rules (Figure 12)
and the traced evaluation rules (Figure 2), which define a judgment
γ, e ⇓ v, T indicating that evaluating an expression e in environment γ yields a value v and a trace T . We assume an environment
Σ associating constants and function symbols with their types, and
write f̂ or +̂ for the semantic operations corresponding to f or +,
and so on. In most cases, the trace form is similar to the expression
form; for example the trace of a constant or variable is a constant
trace c, the trace of a primitive operation f(e1 , . . . , en ) is a primitive operation trace f(T1 , . . . , Tn ) applied to the traces Ti of the
arguments ei , the trace of a record expression is a trace record constructor hA1 : T1 , . . . , An : Tn i, and the trace of a field projection
e.A is a trace T.A. Also, the trace of a let-binding is a let-binding
trace let x = T1 in T2 , where x is bound in T2 . In these cases,
the traces mimic the expression structure.
The traced evaluation rules for conditionals illustrate that traces
differ from expressions in recording control flow decisions. The
trace of a conditional is a conditional trace if(T, e1 , e2 ) ⊲b T ′
where T is the trace of the conditional test, b is the Boolean
value of the test e1 , and T ′ is the trace of the taken branch. The
expressions e1 and e2 are not strictly necessary but retained to
preserve structural similarity to the original expression.
The trace of ∅ is a constant trace ∅. To evaluate a singletoncollection constructor {e}, we evaluate e to obtain a value v and
return the singleton {ǫ.v} with empty label ǫ. We return the sin-

Figure 1. NRC expressions, values, traces, and types.

the collection obtained by evaluating e, evaluating e′ (x) with x
bound to each element of the collection in turn, and returning a
collection containing the union of all of the results. We sometimes
consider pairs (e1 , e2 ), a special case of records h#1 : e1 , #2 : e2 i
using two designated field names #1 and #2 . Many trace forms are
similar to those for expressions; only the differences are shown.
Labels are sequences ℓ = [ii , . . . , in ] ∈ N∗ , possibly empty.
The empty sequence is written ǫ, and labels can be concatenated
ℓ · ℓ′ ; concatenation is associative. Record field names are written
A, B, A1 , A2 , . . ..
Values in NRC include constants c, which we assume include at least booleans and integers. Record values are essentially partial functions from field names to values, written hA1 :
v1 , . . . , An : vn i. Collection values are essentially partial, finitedomain functions from labels in N∗ to values, which we write
{ℓ1 .v1 , . . . , ℓn .vn }. Since they denote functions, collections and
records are identified up to reordering of their elements, and their
field names or labels are always distinct. We write ℓ · v for the
operation that prepends ℓ to each of the labels in a set v, that is,
ℓ · {ℓ1 .v1 , . . . , ℓn .vn } = {ℓ · ℓ1 .v1 , . . . , ℓ · ℓn .vn } .

3

gleton trace {T } recording the trace for the evaluation of the element. To evaluate the union of two expressions, we evaluate each
one and take the semantic union (written ⊎) of the resulting collections, with a ‘1’ or ‘2’ concatenated onto the beginning of each
label to reflect whether each element came from the first or second
part of the union; the union trace T1 ∪ T2 records the traces for the
evaluation of the two subexpressions. For sum e, evaluating e yields
a collection of numbers whose sum we return, together with a sum
trace sum T recording the trace for evaluation of e. Evaluation of
emptiness tests empty e is analogous,
S yielding a trace empty T .
To evaluate a comprehension {e′ | x ∈ e}, we first evaluate e,
which yields a collection v and trace T , and then (using auxiliary
judgment γ, x ∈ v, e′ ⇓∗ v ′ , Θ) evaluate e′ repeatedly with
x bound to each element vi of the collection v to get resulting
values vi′ and corresponding traces Ti′ . We return a new collection
v ′ = {ℓ1 · v1′ , . . . , ℓn · vn′ }; similarly we return a labeled set of
traces Θ = {ℓ1 .T1 , . . . , ℓn .Tn }. (Analogously to values, trace sets
are essentially finite partial functions from labels to traces). For
each of these collections, we prepend the appropriate label ℓi of the
corresponding input element.
A technical point of note is that the resulting trace Ti may contain free occurrences of x. As in our trace semantics for functional
programs, these variables serve as markers in Ti that will be critical
for the trace replaySsemantics. The comprehension trace records,
using the notation {e′ | x ∈ T } ⊲ {ℓ1 .T1 , . . . , ℓn .Tn }, that the
trace T was used to compute a multiset v, and x was bound to
each element ℓi .vi in v in turn, with trace Ti showing how the corresponding subset of the result was computed. The comprehension
trace also records the expression e′ and bound variable x, which are
again not strictly necessary but preserve the structural similarity to
the original expression.
At this point it is useful to provide some informal motivation
for the labeling semantics, compared for example to other semantics that use annotations or labels as a form of provenance. We do
not view the labels themselves as provenance; instead, they provide a useful infrastructure for traces, which do capture a form of
provenance. Moreover, by calculating the label of each part of an
intermediate or final result deterministically (given the labels on
the input), we provide a way to reliably refer to parts of the output,
which otherwise may be unaddressable in a multiset-valued semantics. This is essential for supporting compositional slicing for operations such as let-binding or comprehension, where the output of
one subexpression becomes a part of the input for another.
A central point of our semantics is that evaluation preserves the
property that labels uniquely identify the elements of each multiset.
This naturally assumes that the labels on the input collections
are distinct. In fact, a stronger property is required: evaluation
preserves the property that set labels form a prefix code. In the
following, we write x ≤ y to indicate that sequence x is a prefix of
sequence y.

γ, T y v
···

γ, T1 y c1
γ, c y c

γ, Tn y cn

γ, f(T1 , . . . , Tn ) y f̂(c1 , . . . , cn )
γ, T1 y v1

γ, x y γ(x)

γ[x 7→ v1 ], T2 y v2

γ, let x = T1 in T2 y v2

γ, T1 y v1
···
γ, Tn y vn
γ, hA1 :T1 , . . . , An :Tn i y hA1 :v1 , . . . , An :vn i
γ, T y hA1 :v1 , . . . , An :vn i
γ, T.Ai y vi
γ, T y false

γ, T y true
γ, T1 y v1
γ, if(T, e1 , e2 ) ⊲true T1 y v1
γ, T y v

γ, T2 y v2

γ, if(T, e1 , e2 ) ⊲false T2 y v2
γ, T1 y v1
γ, T2 y v2
γ, T1 ∪ T2 y 1 · v1 ⊎ 2 · v2
γ, T y v
v=∅
γ, empty T y true

γ, ∅ y ∅

γ, {T } y {ǫ.v}

γ, T y {ℓ1 .v1 , . . . , ℓn .vn }
γ, sum T y v1 +̂ . . . +̂ vn
γ, T y v
v 6= ∅
γ, empty T y false

γ, T y v
γ, x ∈ v, Θ y∗ v′
[
γ, {e | x ∈ T } ⊲ Θ y v′

γ, x ∈ v, Θ y∗ v ′
∗

γ, x ∈ ∅, Θ y ∅

γ, x ∈ v1 , Θ y∗ v1′
γ, x ∈ v2 , Θ y∗ v2′
γ, x ∈ v1 ⊎ v2 , Θ y∗ v1′ ⊎ v2′

ℓi ∈ dom(Θ)

γ[x 7→ vi ], Θ(ℓi ) y vi′

γ, x ∈ {ℓi .vi }, Θ y∗ ℓi · vi′

Figure 3. Trace replay.
Theorem 2.2. If γ is prefix-labeled and γ, e ⇓ v, T then v and
T are both prefix-labeled. Moreover, if γ and v are prefix-labeled
and γ, x ∈ v, e ⇓∗ v ′ , Θ then v ′ and Θ are prefix-labeled, and in
addition dom(Θ) = dom(v) ≤ dom(v ′ ).
Proof. By induction on derivations. The key cases are those for
union, which is straightforward, and for comprehensions. For the
latter case we need the second part, to show that whenever γ and
v are prefix-labeled, if γ, x ∈ v, e ⇓∗ v ′ , Θ then v ′ and Θ are
prefix-labeled, and in addition dom(Θ) = dom(v) and dom(v) is
a sub-prefix code of dom(v ′ ).
The prefix code property is needed later in the slicing algorithms, when we will need it to match elements of collections produced by comprehensions with corresponding elements of the trace
set Θ. From now on, we assume that all values, environments, and
traces are prefix-labeled, so any labeled set is assumed to have the
prefix code property.
We will use the following query as a running example.
[
Q = {if(x.B = 3, {hA:x.A, B:x.Ci}, {}) | x ∈ R}

Definition 2.1. A prefix code over Σ is a set of sequences L ⊆ Σ∗
such that for every x, y ∈ L, if x ≤ y then x = y. A sub-prefix
code of a prefix code L is a prefix code L′ such that for all x ∈ L
there exists y ∈ L′ such that y ≤ x. We write L′ ≤ L to indicate
that L′ is a sub-prefix code of L. We say that L and L′ are prefixdisjoint when no element of L is a prefix of an element of L′ and
vice versa.

This is a simple selection query; it identifies records in R that have
B-value of 3, and returns record hA:x.A, B:x.Ci containing x’s A
value and its C value renamed to B. The result of Q on the input R
in the introduction is Q(R) = {[r2 ].hA:2, B:8i, [r3 ].hA:4, B:9i},
and the trace is:
S
T = { | x ∈ R} ⊲ { [r1 ].if(x.B = 3, , ) ⊲false {},
[r2 ].if(x.B = 3, , ) ⊲true { },
[r3 ].if(x.B = 3, , ) ⊲true { } }

Let v be a collection v = {ℓ1 .v1 , . . . , ℓn .vn }. We define the
domain of v to be dom(v) = {ℓ1 , . . . , ℓn }. . We say that a value
or value environment is prefix-labeled if for every collection v
occurring in it, the labels ℓ1 , . . . , ℓn are distinct and dom(v) is a
prefix code. Similarly, we say that a trace is prefix-labeled if every
labeled trace set Θ = {ℓ1 .T1 , . . . , ℓn .Tn } is prefix-labeled.

4

where indicates omitted (easily inferrable) subexpressions.

Proposition 2.6 (Consistency). If γ, e ⇓ v, T then γ, T y v.

Replay We introduce a judgment γ, T y v for replaying a
trace on a (possibly different) environment γ. The rules for replaying NRC traces are presented in Figure 3. Many of the rules are
straightforward or analogous to the corresponding evaluation rules.
Here we only discuss the replay rules for conditional and comprehension traces.
For the conditional rules, the basic idea is as follows. If replaying the trace T of the test yields the same boolean value b as
recorded in the trace, we replay the trace of the taken branch. If the
test yields a different value, then replay fails.
S
To replay a comprehension trace {e | x ∈ T } ⊲ Θ, rule
RC OMP first replays trace T to update the set of elements v
over which we will iterate. We define a separate judgment γ, x ∈
v, Θ y∗ v ′ to iterate over set v and replay traces on the corresponding elements. For elements ℓi ∈ dom(Θ), we replay the
corresponding trace Θ(ℓi ). Replay fails if v contains any labels not
present in Θ.
Replaying a trace can fail if either the branch taken in a conditional test differs from that recorded in the trace, or the intermediate
set obtained from rerunning a comprehension trace includes values
whose labels are not present in the trace. This means, in particular,
that changes to the input can be replayed if they only change base
values or delete set elements, but changes leading to additions of
new labels to sets involved in comprehensions typically cannot be
replayed.
Returning to the running example, suppose we change field B
of row r1 of R from 2 to 5. This change has no effect on the
control flow choice taken in Q, and replaying the trace T succeeds.
Likewise, changing the A or C field of any column of R has no
effect, since these values do not affect the control flow choices in
T . However, changing the B field of a row to 3 (or changing it from
3 to something else) means that replay will fail.

Finally, trace replay is faithful to ordinary evaluation in the following sense: if T is generated by running e in γ and we successfully replay T on γ ′ then we obtain the same value (and same trace)
as if we had rerun e from scratch in γ ′ , and vice versa:
Proposition 2.7 (Fidelity). If γ, e ⇓ v, T , then for any γ ′ , v ′ we
have γ ′ , e ⇓ v ′ , T if and only if γ ′ , T y v ′ .
Observe that consistency is a special case of fidelity (with γ ′ =
γ, v ′ = v. Moreover, the “if” direction of fidelity holds even though
replay can fail, because we require that γ ′ , e ⇓ v ′ , T holds for the
same trace T . If γ ′ , e ⇓ v ′ , T ′ is derivable but only for a different
trace T ′ , then replay fails.

3. Trace Slicing
The goal of the trace slicing algorithm we consider is to remove
information from a trace and input that is not needed to recompute a part of the output. To accommodate these requirements, we
introduce traces and values with holes and more generally, we consider patterns that represent relations on values capturing possible
changes. In this section, we limit attention to pairs, and consider
slicing for a class of simple patterns. We consider records and more
expressive enriched patterns in the next section.
We extend traces with holes ✷
T

::=

··· | ✷

and define a subtrace relation ⊑ that is essentially a syntactic
precongruence on traces and trace sets such that ✷ ⊑ T holds
and Θ ⊆ Θ′ implies Θ ⊑ Θ′ . (The definition of ⊑ is shown in
full in the companion technical report.) Intuitively, holes denote
parts of traces we do not care about, and we can think of a trace
T with holes as standing for a set of possible complete traces
{T ′ | T ⊑ T ′ } representing different ways of filling in the holes.
The syntax of simple patterns p, set patterns sp, and pattern
environments ρ is:

2.2 Key properties
Before moving on to consider trace slicing, we identify some properties that formalize the intuition that traces are consistent with and
faithfully record execution.
Evaluation and traced evaluation are deterministic:

p
sp
ρ

Proposition 2.3 (Determinacy). If γ, e ⇓ v, T and γ, e ⇓ v ′ , T ′
then v = v ′ and T = T ′ . If γ, T y v and γ, T y v ′ then v = v ′ .

::=
::=
::=

✷ | ✸ | c | (p1 , p2 ) | sp
∅ | {ℓ1 .p1 , . . . , ℓn .pn }
[x1 7→ p1 , . . . , xn 7→ pn ]

Essentially, a pattern is a value with holes in some positions. The
meaning of each pattern is defined through a relation hp that says
when two values are equivalent with respect to a pattern. This relation is defined in Figure 5. A hole ✷ indicates that the part of
the value is unimportant, that is, for slicing purposes we don’t care
about that part of the result. Its associated relation h✷ relates any
two values. An identity pattern ✸ is similar to a hole: it says that
the value is important but its exact value is not specified, and its
associated relation h✸ is the identity relation on values. Complete
set patterns {ℓ1 .p1 , . . . , ℓn .pn } specify the labels and patterns for
all of the elements of a set; that is, such a pattern relates only sets
that have exactly the labeled elements specified and whose corresponding values match according to the corresponding patterns.
We define the union of two set patterns as {ℓi .pi } ⊎ {ℓ′i .p′i } =
{ℓi .pi , ℓ′i .p′i } provided their domains ℓ~i and ℓ~′i are prefix-disjoint.
We define a (partial) least upper bound operation on patterns p ⊔ p′
such that for any v, v ′ we have v hp⊔p′ v ′ if and only if v hp v ′
and v hp′ v ′ ; the full definition is shown in Figure 4. We define
the partial ordering p ⊑ p′ as p ⊔ p′ = p′ . We say that a value v
matches pattern p if p ⊑ v. Observe that this implies v hp v. We
extend the ⊔ and ⊑ operations to pattern environments ρ pointwise,
that is, (ρ ⊔ ρ′ )(x) = ρ(x) ⊔ ρ(x′ ).
We define several additional operations on patterns that are
needed for the slicing algorithm. Consider the following singleton

When the trace is irrelevant, we write γ, e ⇓ v to indicate that
γ, e ⇓ v, T for some T .
Traced evaluation is type-safe and produces well-typed traces,
and trace replay is also type-safe.
Theorem 2.4. If γ : Γ and Γ ⊢ e : τ and γ, e ⇓ v, T then v : τ
and Γ ⊢ T : τ . If γ : Γ and Γ ⊢ T : τ and γ, T y v then v : τ .
Traces can be represented using pointers to share common
subexpressions; using this DAG representation, traces can be stored
in space polynomial in the input. (This sharing happens automatically in our implementation in Haskell.)
Proposition 2.5. For a fixed e, if γ, e ⇓ v, T then the sizes of v
and of the DAG representation of T are at most polynomial in |γ|.
Proof. Most cases are straightforward. The only non-trivial case is
for comprehensions, where we need a stronger induction hypothesis: if γ, x ∈ v, e ⇓∗ v ′ , Θ then the sizes of v ′ and of the DAG
representation of Θ are at most polynomial in |γ|.
Furthermore, traced evaluation produces a trace that replays
to the same value as the original expression run on the original
environment. We call this property consistency.

5

✷⊔p=p⊔✷
✸⊔p=p⊔✸
c⊔c
(p1 , p2 ) ⊔ (p′1 , p′2 )
{ℓi .pi } ⊔ {ℓi .p′i }

=
=
=
=
=

p
p[✸/✷]
c
(p1 ⊔ p′1 , p2 ⊔ p′2 )
{ℓi .pi ⊔ p′i }

✸[✸/✷] = ✷[✸/✷]
c[✸/✷]
(p1 , p2 )[✸/✷]
{ℓi .pi }[✸/✷]

=
=
=
=

✸
c
(p1 [✸/✷], p2 [✸/✷])
{ℓi .pi [✸/✷]}

patterns describing the subsets obtained from the first and second
subtraces in the union pattern, respectively.
The rule SC OMP uses a similar idea to let-binding. We slice the
trace set Θ using an auxiliary judgment p, x.Θ ց∗ ρ, Θ0 , p0 , obtaining a sliced input environment, sliced trace set Θ0 , and pattern
p0 describing the set of values to which x was bound. We then use
p0 to slice backwards through the subtrace T that constructed the
set. The auxiliary slicing judgment for trace sets has three rules:
a trivial rule SE MPTY∗ when the set is empty, rule SS NG∗ that
uses label projection p[ℓ] to handle a singleton trace set, and a rule
SU NION∗ handling larger trace sets by decomposing them into subsets. This is essentially a structural recursion over the trace set, and
is deterministic even though the rules can be used to decompose the
trace sets in many different ways, because ⊎ is associative. Rule
SU NION∗ also requires that we restrict the set pattern to match the
domains of the corresponding trace patterns.
The slicing rules SS UM and SE MPTY P follow the same idea as
for primitive operations at base type: we require that the whole set
value be preserved exactly. As discussed by Perera et al. [27] with
primitive operations, this is a potential source of overapproximation, since (for example) for an emptiness test, all we really need is
to preserve the number of elements in the set, not their values. The
last rule shows how to slice pair patterns when the pattern is ✸: we
slice both of the subtraces by ✸ and combine the results.
It is straightforward to show that the slicing algorithm is welldefined for consistent traces. That is, if γ, T y v and p ⊑ v then
there exists ρ, S such that p, T ց ρ, S holds, where ρ ⊑ γ and
S ⊑ T . We defer the correctness theorem for slicing using simple
patterns to the end of the next section, since it is a special case of
correctness for slicing using enriched patterns.
Continuing our running example, consider the pattern p =
{[r2 ].hA:✷, B:8i, [r3 ].✷}. The slice of T with respect to this pattern is of the form:
S
T ′ = { | x ∈ R} ⊲ { [r1 ].✷,
[r2 ].if(x.B = 3, , ) ⊲true { },
[r3 ].✷ }

where:

Figure 4. Least upper bound for simple patterns
v hp v ′
v h✷ v

′

v h✸ v

v1 hp2 v2′
v1 hp1 v1′
(v1 , v2 ) h(p1 ,p2 ) (v1′ , v2′ )

c hc c

vi hpi vi′ (i ∈ {1, . . . , n})
′
{ℓ1 .v1 , . . . , ℓn .vn } h{ℓ1 .p1 ,...,ℓn .pn } {ℓ1 .v1′ , . . . , ℓn .vn
}

γ hρ γ ′ ⇐⇒ ∀x ∈ dom(ρ). γ(x) hρ(x) γ ′ (x)
Figure 5. Simple pattern equivalence.
extraction operation p.ǫ and label projection operation p[ℓ]:
({ǫ.p}).ǫ
sp[ℓ]

=
=

p
{ℓ′ .v | ℓ.ℓ′ .v ∈ sp}

✷.ǫ = ✷ ✸.ǫ = ✸
✷[ℓ] = ✷ ✸[ℓ] = ✸

These operations are only used for the above cases; they have no
effect on constant or pair patterns. For sets, p[ℓ] extracts the subset
of p whose labels start with ℓ, truncating the initial prefix ℓ, while if
p is ✷ or ✸ then again p[ℓ] returns the same kind of hole. Moreover,
dom(p[ℓ]) is a prefix code if dom(p) is.
Suppose L is a prefix code. We define restriction of a set pattern
p to L as follows:
sp|L = {ℓ.ℓ′ .p ∈ sp | ℓ ∈ L}

✷|L = ✷

and the slice of R is R′ = {[r1 ].✷, [r2 ].hA:✷, B:3, C:8i, [r3 ].✷}.
(That is, R′ is the value of ρ(R), where ρ is the pattern environment produced by slicing T with respect to p.) Observe that the
value of A is not needed but the value of B must remain 3 in order to preserve the control flow behavior of the trace on r2 . The
holes indicate that changes to r1 and r3 in the input cannot affect r2 . However, a trace matching T ′ cannot be replayed if any
of r1 , r2 , r3 are deleted from the input or if the A field is removed
from an input record, because the replay rules require all of the labels mentioned in collections or records in T ′ to be present. We
now turn our attention to enriched patterns, which mitigate these
drawbacks.

✸|L = ✸

It is easy to see that dom(p|L ) ⊆ dom(p) so dom(p|L ) is a prefix
code if dom(p) is, so this operation is well-defined on collections:
Lemma 3.1. If sp is prefix-labeled and L is a prefix code then
sp[ℓ] and sp|L are prefix-labeled.
We show other properties of patterns in Appendix B.
Backward Slicing The rules for backward slicing are given in
Figure 6. The judgment p, T ց ρ, T ′ slices trace T with respect
to a pattern p to yield the slice T ′ and sliced input environment
ρ. The sliced input environment records what parts of the input
are needed to produce p; this is needed for slicing operations such
as let-binding or comprehensions. The main new ideas are in the
rules for collection operations, particularly comprehensions. The
slicing rules SC ONST, SP RIM, SVAR, SL ET, SPAIR, SP ROJi , and
SI F follow essentially the same idea as in our previous work [1, 27].
We focus discussion on the new cases, but we review the key ideas
for these operations here in order to make the presentation selfcontained.
The rules for collections use labels and set pattern operations to
effectively undo the evaluation of the set pattern. The rule SE MPTY
is essentially the same as the constant rule. The rule SS NG uses
the singleton extraction operation p.ǫ to obtain a pattern describing the single element of a singleton set value matching p. The
rule SU NION uses the two projections p[1] and p[2] to obtain the

4. Enriched Patterns
So far we have considered only complete set patterns of the form
{ℓ1 .p1 , . . . , ℓn .pn }. These patterns relate pairs of values that have
exactly n elements labeled ℓ1 , . . . , ℓn , each of which matches
p1 , . . . , pn respectively.
This is awkward, as we already can observe in our running example above: to obtain a slice describing how one record was computed, we need to use a set pattern that lists all of the indexes in the
output. Moreover, the slice with respect to such a pattern may also
include labeled subtraces explaining why the other elements exist
in the output (and no others). This information seems intuitively
irrelevant to the value at ℓ1 , and can be a major overhead if the collection is large. We also have considered only binary pairs; it would
be more convenient to support record patterns directly.

6

p, T ց ρ, S
✷, T ց [], ✷

SH OLE

p, c ց [], c

SC ONST

✸, T1 ց ρ1 , S1

p2 , T2 ց ρ2 [x 7→ p1 ], S2
p1 , T1 ց ρ1 , S1
SL ET
p2 , let x = T1 in T2 ց ρ1 ⊔ ρ2 , let x = S1 in S2

✸, Tn ց ρn , Sn

p[1], T1 ց ρ1 , S1

p[2], T2 ց ρ2 , S2

p, T1 ∪ T2 ց ρ1 ⊔ ρ2 , S1 ∪ S2
✸, T ց ρ, S
SE MPTY P
p, sum T ց ρ, sum S

SU NION

p,

[

p, x ց [x 7→ p], x

p, ∅ ց [], ∅

SVAR

(p, ✷), T ց ρ, S
SP ROJ 1
p, T.#1 ց ρ, S.#1
p.ǫ, T ց ρ, S
SS NG
p, {T } ց ρ, {S}

SE MPTY

p, x.Θ ց∗ ρ′ , Θ′ , p′

p′ , T ց ρ, S
[
SC OMP
{e | x ∈ T } ⊲ Θ ց ρ ⊔ ρ′ , {e | x ∈ S} ⊲ Θ′

✸, T ց ρ, S
SS UM
p, empty T ց ρ, empty S

∅, x.∅ ց∗ [], ∅, ∅

SP RIM

p1 , T1 ց ρ1 , S1
p2 , T2 ց ρ2 , S2
SPAIR
(p1 , p2 ), (T1 , T2 ) ց ρ1 ⊔ ρ2 , (S1 , S2 )

p, T ′ ց ρ′ , S ′
b, T ց ρ, S
SI F
p, if(T, e1 , e2 ) ⊲b T ′ ց ρ′ ⊔ ρ, if(S, e1 , e2 ) ⊲b S ′

(✷, p), T ց ρ, S
SP ROJ 2
p, T.#2 ց ρ, S.#2

p, x.Θ ց∗ ρ, Θ0 , p0

···

p, f(T1 , . . . , Tn ) ց ρ1 ⊔ · · · ⊔ ρn , f(S1 , . . . , Sn )

✸, T1 ց ρ1 , S1
✸, T2 ց ρ2 , S2
SD IAMOND
✸, (T1 , T2 ) ց ρ1 ⊔ ρ2 , (S1 , S2 )

p[ℓ], T ց ρ[x 7→ p0 ], S
SS NG∗
p, x.{ℓ.T } ց∗ ρ, {ℓ.S}, {ℓ.p0 }

SE MPTY∗

p|dom(Θ1 ) , x.Θ1 ց∗ ρ1 , Θ′1 , p1

p|dom(Θ2 ) , x.Θ2 ց∗ ρ2 , Θ′2 , p2

∗

p, x.Θ1 ⊎ Θ2 ց ρ1 ⊔ ρ2 , Θ′1 ⊎ Θ′2 , p1 ⊎ p2

SU NION∗

Figure 6. Backward trace slicing.
In this section we sketch how to enrich the language of patterns
to allow for partial set and partial record patterns, as follows:
p

::=

✸⊎✷ =✷⊎✸ =✷⊎✷
✸⊎✸
sp ⊎ ∅ = ∅ ⊎ sp
{ℓi .pi } ⊎ ✷ = ✷ ⊎ {ℓi .pi }
{ℓi .pi } ⊎ ✸ = ✸ ⊎ {ℓi .pi }
{ℓi .pi } ⊎ ({ℓ′j .p′j } ∪˙ ✷)
˙ ✸)
{ℓi .pi } ⊎ ({ℓ′j .p′j } ∪
({ℓi .pi } ∪˙ ✷) ⊎ ({ℓ′j .p′j } ∪˙ ✷)
˙ ✸) ⊎ ({ℓ′j .p′j } ∪˙ ✷)
({ℓi .pi } ∪
˙ ✷) ⊎ ({ℓ′j .p′j } ∪
˙ ✸)
({ℓi .pi } ∪
˙ ✸)
({ℓi .pi } ∪˙ ✸) ⊎ ({ℓ′j .p′j } ∪

✷ | ✸ | c | sp | rp

rp

::=

hi | hAi : pi i | hAi : pi ; ✷i | hAi : pi ; ✸i

sp

::=

∅ | {ℓi .pi } | {ℓi .pi } ∪˙ ✷ | {ℓi .pi } ∪˙ ✸

Record patterns are of the form hAi : pi i, listing the fields and the
patterns they must match, possibly followed by ✷ or ✸, which the
remainder of the record must match. The pattern {ℓi .pi } ∪˙ ✷ stands
for a set with labeled elements matching patterns p1 , . . . , pn , plus
some additional elements whose values we don’t care about. For
example, we can use the pattern {ℓ1 .p1 } ∪˙ ✷ to express interest
in why element ℓ1 matches p1 , when we don’t care about the rest
of the set. The second partial pattern, {ℓi .pi } ∪˙ ✸, has similar
behavior, but it says that the rest of the sets being considered must
be equal. For example, {ℓ.✷} ∪˙ ✸ says that the two sets are equal
except possibly at label ℓ. This pattern is needed mainly in order to
ensure that we can define a least upper bound on enriched patterns,
since we cannot express ({ℓ1 .v1 , . . . , ℓn .pn } ∪˙ ✷) ⊔ ✸ otherwise.
We define dom({ℓi .pi } ∪˙ ✷) = dom({ℓi .pi } ∪˙ ✸) =
{ℓ1 , . . . , ℓn }. Disjoint union of enriched patterns sp ⊎ sp′ is defined only if the domains are prefix-disjoint, so that the labels of the
result still form a prefix code; this operation is defined in Figure 7.
We now extend the definitions of p[✸/✷] and ⊔ to account for
extended patterns. We extend the [✸/✷] substitution operation as
follows:
hAi : pi i[✸/✷]
hAi : pi ; ✷i[✸/✷]
hAi : pi ; ✸i[✸/✷]
({ℓi .pi } ∪˙ ✷)[✸/✷]
˙ ✸)[✸/✷]
({ℓi .pi } ∪

=
=
=
=
=

=
=
=
=
=
=
=
=
=
=
=

✷
✸
sp
˙ ✷
{ℓi .pi } ∪
˙ ✸
{ℓi .pi } ∪
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✷
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✸
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✷
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✷
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✷
({ℓi .pi } ⊎ {ℓ′j .p′j }) ∪˙ ✸

Figure 7. Enriched pattern union
We extend the singleton extraction p.ǫ, label projection p[ℓ], and
restriction p|L operations on set patterns as follows:
˙ ✸).ǫ = ({ǫ.p} ∪
˙ ✷).ǫ
({ǫ.p} ∪
˙ ✷)
ℓ · ({ℓi .pi } ∪
ℓ · ({ℓi .pi } ∪˙ ✸)
˙ ✷)[ℓ]
({ℓi .pi } ∪
({ℓi .pi } ∪˙ ✸)[ℓ]
˙ ✷)|L
({ℓi .pi } ∪
({ℓi .pi } ∪˙ ✸)|L

=
=
=
=
=
=
=

p
(ℓ · {ℓi .pi }) ⊎ ✷
(ℓ · {ℓi .pi }) ⊎ ✸
({ℓi .pi }[ℓ]) ⊎ ✷
({ℓi .pi }[ℓ]) ⊎ ✸
({ℓi .pi }|L ) ⊎ ✷
({ℓi .pi }|L ) ⊎ ✸

Note that in many cases, we use the disjoint union operation ⊎
on the right-hand side; this ensures, for example, that we never
produce results of the form ∅ ∪˙ ✷ or ∅ ∪˙ ✸; these are normalized to
✷ and ✸ respectively, and this normalization reduces the number
of corner cases in the slicing algorithm.
We define a record pattern projection operation p.A as follows:

hAi : pi [✸/✷]i
hAi : pi [✸/✷];✸i
hAi : pi [✸/✷]; ✸i
{ℓi .pi [✸/✷]} ∪˙ ✸
{ℓi .pi [✸/✷]} ∪˙ ✸

hA1 :p1 , . . . , An :pn i.Ai
hA1 :p1 , . . . , An :pn ; i.Ai
hA1 :p1 , . . . , An :pn ; ✷i.B
hA1 :p1 , . . . , An :pn ; ✸i.B

We handle the additional cases of the ⊔ operation in Figure 8,
and extend the hp relation as shown in Figure 9. Note that taking
the least upper bound of a partial pattern with a complete pattern
yields a complete pattern, while taking the least upper bound of
partial patterns involving ✸ again relies on the [✸/✷] substitution
operation.

=
=
=
=

pi
✷.A = ✷
pi
✸.A = ✸
✷ (B ∈
/ {A1 , . . . , An })
✸ (B ∈
/ {A1 , . . . , An })

We extend the slicing judgment to accommodate these new
patterns in Figure 10. The rules SR EC and SP ROJA are similar to
those for pairs, except that we use the field projection operation
in the case for a record trace, and we use partial record patterns

7

{ℓi .pi , ℓ′j .qj } ⊔ ({ℓi .p′i } ∪˙ ✷)

=

{ℓi .pi ⊔ p′i , ℓ′j .qj }

˙ ✸)
{ℓi .pi , ℓ′j .qj } ⊔ ({ℓi .p′i } ∪

=

{ℓi .pi ⊔ p′i , ℓ′j .qj [✸/✷]}

˙
({ℓi .pi , ℓ′j .qj } ∪˙ ✷) ⊔ ({ℓi .p′i , ℓ′′
k .rk } ∪ ✷)

=

˙
{ℓi .pi ⊔ p′i , ℓ′j .qj , ℓ′′
k .rk } ∪ ✷

˙
({ℓi .pi , ℓ′j .qj } ∪˙ ✷) ⊔ ({ℓi .p′i , ℓ′′
k .rk } ∪ ✸)

=

˙
{ℓi .pi ⊔ p′i , ℓ′j .qj [✸/✷], ℓ′′
k .rk } ∪ ✸

˙
({ℓi .pi , ℓ′j .qj } ∪˙ ✸) ⊔ ({ℓi .p′i , ℓ′′
k .rk } ∪ ✸)

=

˙
{ℓi .pi ⊔ p′i , ℓ′j .qj [✸/✷], ℓ′′
k .rk [✸/✷]} ∪ ✸

hAi : pi , Bj : qj i ⊔ (hAi : p′i ; ✷i)

=

hAi : pi ⊔ p′i , Bj : qj i

p′i ; ✸i)

=

hAi : pi ⊔ p′i , Bj : qj [✸/✷]i

(hAi : pi , Bj : qj ; ✷i) ⊔ (hAi : p′i , Ck : rk ; ✷i)

=

hAi : pi ⊔ p′i , Bj : qj , Ck : rk ; ✷i

(hAi : pi , Bj : qj ; ✷i) ⊔ (hAi : p′i , Ck : rk ; ✸i)

=

hAi : pi ⊔ p′i , Bj : qj [✸/✷], Ck : rk ; ✸i

=

hAi : pi ⊔ p′i , Bj : qj [✸/✷], Ck : rk [✸/✷]; ✸i

hAi : pi , Bj : qj i ⊔ (hAi :

(hAi : pi , Bj : qj ; ✸i) ⊔ (hAi :

p′i , Ck

: rk ; ✸i)

Figure 8. Least upper bound for enriched patterns (excluding some symmetric cases).

v1 hp1 v1′

hAi : vi i hhA

i :pi i

v1 hp1 v1′

hAi : vi′ i
′
vn hpn vn

···

hAi : vi , Bj :wj i hhA

i :pi ;✷i

v1 hp1 v1′

hAi : vi , Bj :wj i hhA

i :pi ;✸i

{ℓi .vi } ⊎ v h{ℓ
v1 hp1 v1′
{ℓi .vi } ⊎ v

hAi : vi′ , Ck :wk′ i

Lemma 4.2 (Projection and ⊑).

′
vn hpn vn

···

v1 hp1 v1′

1. If p1 ⊑ v1 and p2 ⊑ v2 and v1 hp1 v1′ and v2 hp2 v2′ then
v1 ⊎ v2 hp1 ⊎p2 v1′ ⊎ v2′ , provided all of these disjoint unions
are defined.
2. If p ⊑ v1 ⊎ v2 and L1 ≤ dom(v1 ) and L2 ≤ dom(v2 ) and
L1 , L2 are prefix-disjoint, then p|L1 ⊑ v1 and p|L2 ⊑ v2 .

′
vn hpn vn

···

1.
2.
3.
4.

hAi : vi′ , Bj :wj i

···

′
vn hpn vn

˙
i .pi }∪✷

{ℓi .vi′ } ⊎ v′

Lemma 4.3 (Projection and hp ).
1. If p ⊑ {ǫ.v} and v hp.ǫ v ′ then {ǫ.v} hp {ǫ.v ′ }.
2. If p ⊑ 1 · v1 ⊎ 2 · v2 and v1 hp[1] v1′ and v2 hp[2] v2′ then
1 · v1 ⊎ 2 · v2 hp 1 · v1′ ⊎ 2 · v2′ .
3. If p ⊑ ℓ · v and v hp[ℓ] v ′ then ℓ · v hp ℓ · v ′ .
4. If p ⊑ hAi : vi i and v1 hp.A1 v1′ , . . . , vn hp.An vn′ then
hAi : vi i hp hAi : vi′ i.

′
···
vn hpn vn
{ℓi .vi′ } ⊎ v
h{ℓ .p }∪✸
i i ˙

Figure 9. Enriched pattern equivalence

p, T ց ρ, S

Proofs are collected in Appendix B.
We now state the key correctness property for slicing. Intuitively, it says that if we slice T with respect to output pattern p,
obtaining a slice ρ and S, then p will be reproduced on recomputation under any change to the input and trace that is consistent with
the slice — formally, that means that the changed trace T ′ must
match the sliced trace S, and the changed input γ ′ must match γ
modulo ρ.

hA:p; ✷i, T ց ρ, S
SR EC
p, T.A ց ρ, S.A

p.A1 , T1 ց ρ1 , S1

···

p.An , Tn ց ρn , Sn

p, hA1 :T1 , . . . , An :Tn i ց ρ1 ⊔ · · · ⊔ ρn , hA1 :S1 , . . . , An :Sn i

SP ROJ A

p, x.Θ ց∗ ρ, Θ′ , p0
✷, x.Θ ց∗ [], ∅, ✷

SH OLE∗

✸, x.∅ ց∗ [], ∅, ∅

If p ⊑ {ǫ.v} then p.ǫ ⊑ v.
If p ⊑ 1 · v1 ⊎ 2 · v2 then p[1] ⊑ v1 and p[2] ⊑ v2 .
If p ⊑ ℓ · v then p[ℓ] ⊑ v.
If p ⊑ hAi : vi i then p.Ai ⊑ vi .

Theorem 4.4 (Correctness of Slicing).

SD IAMOND∗

1. Suppose γ, T y v and p ⊑ v and p, T ց ρ, S. Then for all
γ ′ hρ γ and T ′ ⊒ S such that γ ′ , T ′ y v ′ we have v ′ hp v.
2. Suppose γ, x ∈ v0 , Θ y∗ v and p ⊑ v and p, x.Θ0 ց
ρ, Θ′0 , p0 , where Θ0 ⊆ Θ. Then for all γ ′ hρ γ and v0′ hp0 v0
and Θ′ ⊒ Θ′0 such that γ ′ , x ∈ v0 , Θ′ y∗ v ′ we have v ′ hp v.

Figure 10. Backward trace slicing over enriched patterns.

hA : p; ✷i in the case for a field projection trace. The added
rules SH OLE∗ and SD IAMOND∗ handle the possibility that a partial
pattern reduces to ✷ or ✸ through projection; we did not need to
handle this case earlier because a simple set pattern is either a hole
(which could be handled by the rule ✷, T ց [], ✷) or a complete
set pattern showing all of the labels of the result.
Both simple and extended patterns satisfy a number of lemmas
that are required to prove the correctness of trace slicing.

Returning to our running example, we can use the enriched
pattern p′ = {[r2 ].hB:8; ✷i} ∪˙ ✷ to indicate interest in the B field
of r2 , without naming the other fields of the row or the other row
indexes. Slicing with respect to this pattern yields the following
slice:
[
T ′′ = { | x ∈ R} ⊲ {[r2 ].if(x.B = 3, , ) ⊲true { }}
˙ This indicates
and the slice of R is R′′ = {[r2 ].hB:3, C:8; ✷i}∪✷.
that (as before) the values of r1 and r3 and of the A field of r2

Lemma 4.1 (Properties of union and restriction).

8

are irrelevant to r2 in the result; unlike T ′ , however, we can also
potentially replay if r1 and r3 have been deleted from R. Likewise,
we can replay if the A field has been removed from a record, or if
some other field such as D is added. This illustrates that enriched
patterns allow for smaller slices than simple patterns, with greater
flexibility concerning possible updates to the input.
A natural question is whether slicing computes the (or a) smallest possible answer. Because our definition of correct slices is based
on recomputation, minimal slices are not computable, by a straightforward reduction from the undecidability of minimizing dependency provenance [1, 12].

p, T ց
ց ρ, e
✷, T ց
ց [], ✷

p, c ց
ց [], c

✸, T1 ց
ց ρ1 , e1

···

✸, Tn ց
ց ρn , en

p, f(T1 , . . . , Tn ) ց
ց ρ1 ⊔ · · · ⊔ ρn , f(e1 , . . . , en )

p, x ց
ց [x 7→ p], x
p2 , T2 ց
ց ρ2 [x 7→ p1 ], e2
p1 , T1 ց
ց ρ1 , e1
p2 , let x = T1 in T2 ց
ց ρ1 ⊔ ρ2 , let x = e1 in e2

5. Query and Differential Slicing

p1 , T1 ց
ց ρ1 , e1

We now adapt slicing techniques to provide explanations in terms
of query expressions, and show how to use differences between
slices to provide precise explanations for parts of the output.

···

pn , Tn ց
ց ρn , en

hA1 :p1 , . . . , An :pn i, hA1 :T1 , . . . , An :Tn i ց
ց ρ1 ⊔ · · · ⊔ ρn , hA1 :e1 , . . . , An :en i
p.A, T ց
ց ρ, S
p, T.A ց
ց ρ, S.A

5.1 Query slicing

p1 , T1 ց
ց ρ1 , e′1
true, T ց
ց ρ, e′
p1 , if(T, e1 , e2 ) ⊲true T1 ց
ց ρ1 ⊔ ρ, if(e′ , e′1 , ✷)

Our previous work [27] gave an algorithm for extracting a program
slice from a trace. We now adapt this idea to queries. A trace slice
shows the parts of the trace that need to be replayed in order to compute the desired part of the output; similarly, a query slice shows the
part of the query expression that is needed in order to ensure that the
desired part of the output is recomputed. As with traces, we allow
holes ✷ in programs to allow deleting subexpressions, and define
⊑ as a syntactic precongruence such that ✷ ⊑ e. We also define a
least upper bound operation e ⊔ e′ on partial query expressions in
the obvious way, so that ✷ ⊔ e = e.
We define a judgment p, T ց
ց ρ, e that traverses T and “unevaluates” p, yielding a partial input environment ρ and partial program e. The rules are illustrated in Figure 11. Many of the rules are
similar to those for trace slicing; the main differences arise in the
cases for conditionals and comprehensions, where we collapse the
sliced expressions back into expressions, possibly inserting holes or
merging sliced expressions obtained by running the same code in
different ways (as in a comprehension that contains a conditional).
Again, it is straightforward to show that if γ, e ⇓ v, T and
p ⊑ v then there exist ρ, e′ such that p, T ց
ց ρ, e′ , where ρ ⊑ γ
and e′ ⊑ e. The essential correctness property for query slices is
similar to that for trace slices: again, we require that rerunning any
sufficiently similar query on a sufficiently similar input produces a
result that matches p. The proof of this result is in Appendix D.

p2 , T2 ց
ց ρ2 , e′2
false, T ց
ց ρ, e′
p2 , if(T, e1 , e2 ) ⊲false T2 ց
ց ρ2 ⊔ ρ, if(e′ , ✷, e′2 )

∅, ∅ ց
ց [], ∅

p[1], T1 ց
ց ρ1 , e1
p[2], T2 ց
ց ρ2 , e2
p, T1 ∪ T2 ց
ց ρ1 ⊔ ρ2 , e1 ∪ e2

p[ǫ], T ց
ց ρ, e
p, {T } ց
ց ρ, {e}

✸, T ց
ց ρ, e
p, empty T ց
ց ρ, empty e

✸, T ց
ց ρ, e
p, sum T ց
ց ρ, sum e

p, x.Θ ց
ց∗ ρ′ , e′ , p0
p0 , T ց
ց ρ, e′0
[
[
′
p, {e | x ∈ T } ⊲ Θ ց
ց ρ ⊔ ρ , {e′ | x ∈ e′0 }
✸, T1 ց
ց ρ1 , e1
···
✸, Tn ց
ց ρn , en
✸, hA1 : T1 , . . . , An : Tn i ց
ց ρ1 ⊔ · · · ⊔ ρn , hA1 : e1 , . . . , An : en i

✸, ∅ ց
ց [], ∅

p, x.Θ ց
ց ρ, e, p′
✷, x.Θ ց
ց∗ [], ✷, ✷

Theorem 5.1 (Correctness of Query Slicing).

∅, x.∅ ց
ց∗ [], ✷, ∅

✸, x.∅ ց
ց∗ [], ✷, ∅

p[ℓ], T ց
ց ρ[x 7→ p0 ], e
p, x.{ℓ.T } ց
ց∗ ρ, e, {ℓ.p0 }

1. Suppose γ, T y v and p ⊑ v and p, T ց
ց ρ, e. Then for all
γ ′ hρ γ and e′ ⊒ e such that γ ′ , e′ ⇓ v ′ we have v ′ hp v.
2. Suppose γ, x ∈ v0 , Θ y∗ v and p ⊑ v and p, Θ ց
ց ρ, e0 , p0 .
Then for all γ ′ hρ γ and v0′ hp0 v0 and e′0 ⊒ e0 such that
γ ′ , x ∈ v0′ , e′0 ⇓∗ v ′ we have v ′ hp v.

p|dom(Θ1 ) , x.Θ1 ց
ց∗ ρ1 , e1 , p1

p|dom(Θ2 ) , x.Θ2 ց
ց∗ ρ2 , e2 , p2

p, x.Θ1 ⊎ Θ2 ց
ց∗ ρ1 ⊔ ρ2 , e1 ⊔ e2 , p1 ⊎ p2

Combining with the consistency property (Proposition 2.6), we
have:

Figure 11. Unevaluation (selected rules).

Corollary 5.2. Suppose γ, e ⇓ v, T and p ⊑ v and p, T ց
ց ρ, e′ .
Then for all γ ′ hρ γ and e′′ ⊒ e′ such that γ ′ , e′′ ⇓ v ′ , we have
v hp v ′ .

5.2 Differential slicing
We consider a pattern difference to be a pair of patterns (p, p′ )
where p ⊑ p′ . Intuitively, a pattern difference selects the part of a
value present in the outer component p′ and not in the inner component p. For example, the pattern difference (hB:✷; ✷i, hB:8; ✷i)
selects the value 8 located in the B component of a record. We can
also write this difference as hB: 8 ; ✷i, using ? to highlight the
boundary between the inner and outer pattern. Trace and query pattern differences are defined analogously.

Continuing our running example, the query slice for the pattern
p′ considered above is
[
Q′ = {if(x.B = 3, {hA:✷, B:x.Ci}, {}) | x ∈ R}
since only the computation of the A field in the output is irrelevant
to p′ .

9

It is straightforward to show by induction that slicing is monotonic in both arguments:

A related point: one may wonder whether it makes sense to select a particular copy of hB:3i in the output, since in a conventional multiset, multiple copies of the same value are indistinguishable. We believe it is important to be able to distinguish different
copies of a value, which may have different explanations. Treating
n copies of a value as a single value with multiplicity n would obscure this distinction and force us to compute the slices of all of the
copies even if only a single explanation is required. This is why we
have chosen to work with indexed sets, rather than pure multisets.

Lemma 5.3 (Monotonicity). If p ⊑ p′ and T ⊑ T ′ and p′ , T ′ ց
ρ′ , S ′ then there exist ρ, S such that p, T ց ρ, S and ρ ⊑ ρ′ and
S ⊑ S ′ . In addition, p, S ′ ց ρ, S.
This implies that given a pattern difference and a trace, we can
compute a trace difference using the following rule:
p 2 , T ց ρ 2 , S2
p 1 , S2 ց ρ 1 , S1
(p1 , p2 ), T ց (ρ1 , ρ2 ), (S1 , S2 )

Joins So far all examples have involved a single table R. Consider a simple join query

It follows from monotonicity that ρ1 ⊑ ρ2 and S1 ⊑ S2 , thus,
pattern differences yield trace differences. Furthermore, the second
part of monotonicity implies that we can compute the smaller slice
S1 from the larger slice S2 , rather than re-traverse T . It is also
possible to define a simultaneous differential slicing judgment, as
an optimization to ensure we only traverse the trace once.
Query slicing is also monotone, so differential query slices can
be obtained in exactly the same way. Revisiting our running example one last time, consider the differential pattern {[r2 ].hB: 8 ; ✷i}∪˙
✷. The differential query slice for the pattern p′ considered above
is
[
Q′′ = {if(x.B = 3, {hA:✷, B: x.C i}, {}) | x ∈ R}

Q3 = {hA:x.A, B:y.Ci | x ∈ R, y ∈ S, x.B = y.B}
and consider the following table S, and the result Q3 (R, S).
id
[s1 ]
S=
[s2 ]
[s3 ]

B
2
3
4

C
4
4
5

id
[r1 , s1 ]
Q3 (R, S) =
[r2 , s2 ]
[r3 , s2 ]

A
1
2
4

B
4
4
5

The full trace of this query execution is as follows:
S
T3 = S
{ | x ∈ R} ⊲ {
[r1 ]. { | y ∈ S} ⊲ {

6. Examples and Discussion

[r2 ].

S

{ | y ∈ S} ⊲ {

In this section we present some more complex examples to illustrate key points.

[r3 ].

S

{ | y ∈ S} ⊲ {

Renaming Recall the swapping query from the introduction,
written in NRC as
[
Q1 = {{if(x.A > x.B, hA:x.B, B:x.Ai, hxi)} | x ∈ R}

[s1 ].if(x.B
[s2 ].if(x.B
[s3 ].if(x.B
[s1 ].if(x.B
[s2 ].if(x.B
[s3 ].if(x.B
[s1 ].if(x.B
[s2 ].if(x.B
[s3 ].if(x.B

=
=
=
=
=
=
=
=
=

y.B,
y.B,
y.B,
y.B,
y.B,
y.B,
y.B,
y.B,
y.B,

,
,
,
,
,
,
,
,
,

) ⊲true { },
) ⊲false {},
) ⊲false {}},
) ⊲false {},
) ⊲true { },
) ⊲false {}},
) ⊲false {},
) ⊲true { },
) ⊲false {}}}

Slicing with respect to {[r1 , s1 ].hA:1; ✷i, [r2 , s2 ].hB:4; ✷i} ∪˙ ✷
yields trace slice

This query illustrates a key difference between our approach and
the how-provenance model of Green et al. [20]. As discussed in
[13], renaming operations are ignored by how-provenance, so the
how-provenance annotations of the results of Q1 are the same as for
a query that simply returns R. In other words, the choice to swap
the fields when A > B is not reflected in the how-provenance,
which shows that it is impossible to extract where-provenance (or
traces) from how-provenance. Extracting where-provenance from
traces appears straightforward, extending our previous work [1].
This example also illustrates how traces and slices can be used
for partial recomputation. The slice for output pattern {[1, r1 ].hB:2i}∪˙
✷, for example, will show that this record was produced because
the A component of hA:1, B:2, C:7i at index [r1 ] in the input was
less than or equal to the B component. Thus, we can replay after
any change that preserves this ordering information.
Union Consider query
[
Q2 = {{hB:x.Bi} | x ∈ R} ∪ {hB:3i}
that projects the B fields of elements of R and adds another copy
of hB:3i to the result. This yields
Q2 (R) = {[1, r1 ].hB:2i, [1, r2 ].hB:3i, [1, r3 ].hB:3i, [2].hB:3i}
This illustrates that the indexes may not all have the same length,
but still form a prefix code. If we slice with respect to {[1, r2 ].hB:3i}∪˙
✷ then the query slice is:
[
Q′2 = {{hB:x.Bi} | x ∈ R} ∪ ✷
and R′ = {[r2 ].hB:3; ✷i} ∪˙ ✷ whereas if we slice with respect to
{[2].hB:3i} ∪˙ ✷ then the query slice is Q′′2 = ✷ ∪ {hB:3i} and
R′′ = ✷, indicating that this part of the result has no dependence
on the input.

10

S
T3′ = S
{ | x ∈ R} ⊲ {
[r1 ]. S{ | y ∈ S} ⊲ {
[r2 ]. { | y ∈ S} ⊲ {

[s1 ].if(x.B = y.B, , ) ⊲true { },
[s2 ].if(x.B = y.B, , ) ⊲true { }}

and input slice R3′ = {[r1 ].hA:1, B:2; ✷i, [r2 ].hB:3; ✷i} and
S3′ = {[s1 ].hB:2; ✷i, [s2 ].hB:3; C:4i}.
Workflows NRC expressions can be used to represent workflows, if primitive operations are added representing the workflow
steps [2, 21]. To illustrate query slicing and differential slicing for a
workflow-style query, consider the following more complex query:
Q4 = {f (x, y) | x ∈ T, y ∈ T, z ∈ U, p(x, y), q(x, y, z)}
where f computes some function of x and y and p and q are selection criteria. Here, we assume T and U are collections of data files
and f, p, q are additional primitive operations on them. This query
exercises most of the distinctive features of our approach; we can
of course translate it to the NRC core calculus used in the rest of the
paper. If dom(T ) = {t1 , . . . , t10 } and dom(U ) = {u1 , . . . , u10 }
then we might obtain result {[t3 , t4 , u5 ].v1 , [t6 , t8 , u10 ].v2 }. If we
focus on the value v1 using the pattern {[t3 , t4 , u5 ].v1 } ∪˙ ✷, then
the program slice we obtain is Q4 itself, while the data slice might
be T ′ = {[t3 ].✸, [t4 ].✸} ∪˙ ✷, U ′ = {[u5 ].✸} ∪˙ ✷, indicating that
if the values at t3 , t4 , u5 are held fixed then the end result will still
be v1 . The trace slice is similar, and shows that v1 was computed
by applying f with x bound to the value at t3 in T , y bound to t4 ,
and z bound to u5 , and that p(x, y) and q(x, y, z) succeeded for
these values.
If we consider a differential slice using pattern difference
{[t3 , t4 , u5 ]. v1 } ∪˙ ✷ then we obtain the following program difference:
[
Qδ4 = { f (x, y) | x ∈ T, y ∈ T, z ∈ U, p(x, y), q(x, y, z)}

This shows that most of the query is needed to ensure that the
result at [t3 , t4 , u5 ] is produced, but the subterm f (x, y) is only
needed to compute the value v1 . This can be viewed as a querybased explanation for this part of the result.

tracing, making it feasible for in-memory execution of workflows
represented in NRC.

8. Related and future work
Program slicing has been studied extensively [17, 30, 31], as has the
use of execution traces, for example in dynamic slicing. Our work
contrasts with much of this work in that we regard the trace and
underlying data as being of interest, not just the program. Some
of our previous work [12] identified analogies between program
slicing and provenance, but to our knowledge, there is no other
prior work on slicing in databases.
Lineage and why-provenance were motivated semantically in
terms of identifying witnesses, or parts of the input needed to ensure that a given part of the output is produced by a query. Early
work on lineage in relational algebra [15] associates each output
record with a witness. Buneman et al. studied a more general notion called why-provenance that maps an output part to a collection of witnesses [7, 8]. This idea was generalized further to the
how-provenance or semiring model [18, 20], based on using algebraic expressions as annotations; this approach has been extended
to handle some forms of negation and aggregation [4, 19]. Semiring
homomorphisms commute with query evaluation; thus, homomorphic changes to the input can be performed directly on the output
without re-running the query. However, this approach only applies
to changes describable as semiring homomorphisms, such as deletion.
Where-provenance was also introduced by Buneman et al. [7,
8]. Although the idea of tracking where input data was copied
from is natural, it is nontrivial to characterize semantically, because
where-provenance does not always respect semantic equivalence.
In later work, Buneman et al. [6] studied where-provenance for
the pure NRC and characterized its expressiveness for queries and
updates. It would be interesting to see whether their notion of
expressive completeness for where-provenance could be extended
to richer provenance models, such as traces, possibly leading to an
implementation strategy via translation to plain NRC.
Provenance has been studied extensively for scientific workflow
systems [5, 29], but there has been little formal work on the semantics of workflow provenance. The closest work to ours is that of
Hidders et al. [21], who model workflows by extending the NRC
with nondeterministic, external function calls. They sketch an operational semantics that records runs that contain essentially all of
the information in a derivation tree, represented as a set of triples.
They also suggest ways of extracting subruns from runs, but their
treatment is partial and lacks strong formal guarantees analogous
to our results.
There have been some attempts to reconcile the database and
workflow views of provenance; Hidders et al. [21] argued for the
use of Nested Relational Calculus (NRC) as a unifying formalism for both workflow and database operations, and subsequently
Kwasnikowska and Van den Bussche [22] showed how to map this
model to the Open Provenance Model. Acar et al. [2] later formalized a graph model of provenance for NRC. The most advanced
work in this direction appears to be that of Amsterdamer et al. [3],
who combined workflow and database styles of provenance in the
context of the PigLatin system (a MapReduce variant based on
nested relational queries). Lipstick allows analyzing the impact of
restricted hypothetical changes (such as deletion) on parts of the
output, but to our knowledge no previous work provides a formal
guarantee about the impact of changes other than deletion.
In our previous work [12], we introduced dependency provenance, which conservatively over-approximates the changes that
can take place in the output if the input is changed. We developed definitions and techniques for dependency provenance in full
NRC including nonmonotone operations (empty, sum) and primi-

7. Implementation
To validate our design and experiment with larger examples, we
extended our Haskell implementation Slicer of program slicing for
functional programs [27] with the traces and slicing techniques
presented in this paper. We call the resulting system NRCSlicer;
it supports a free combination of NRC and general-purpose functional programming features. NRCSlicer interprets expressions inmemory without optimization. As reported previously for Slicer,
we have experimented with several alternative tracing and slicing
strategies, which use Haskell’s lazy evaluation strategy in different
ways. The alternatives we consider here are:
• eager: the trace is fully computed during evaluation.
• lazy: the value is computed eagerly, but the trace is computed

lazily using Haskell’s default lazy evaluation strategy.
To evaluate the effectiveness of enriched patterns, we measured the
time needed for the eager and lazy techniques to trace and slice
the workflow example Q4 in the previous section. We considered a
instantiation of the workflow where the data values are simply integers and with input tables T, U = {1, . . . , 50}, and defined the
operations f (x, y) as x ∗ y, p(x, y) as x < y, and q(x, y, z) as
x2 + y 2 = z 2 . This is not a realistic workflow, and we expect that
the time to evaluate the basic operations of a realistic workflow following this pattern would be much larger. However, the overheads
of tracing and slicing do not depend on the execution time of primitive operations, so we can still draw some conclusions from this
simplistic example.
The comprehension iterates over 503 = 125,000 triples, producing 20 results. We considered simple and enriched patterns selecting a single element of the result. We measured evaluation time,
and the overhead of tracing, trace slicing, and query slicing. The
experiments were conducted on a MacBook Pro with 2GB RAM
and a 2.8GHz Intel Core Duo, using GHC version 7.4.
eager-simple
eager-enriched
lazy-simple
lazy-enriched

eval
0.5
0.5
0.5
0.5

trace
1.5
1.5
0.7
0.7

slice
2.5
<0.1
1.3
<0.1

qslice
1.6
<0.1
1.7
<0.1

The times are in seconds. The “eval” column shows the time needed
to compute the result without tracing. The “trace”, “slice”, and “qslice” columns show the added time needed to trace and compute
slices. The full traces in each of these runs have over 2.1 million
nodes; the simple pattern slices are almost as large, while the enriched pattern slices are only 95 nodes. For this example, slicing is
over an order of magnitude faster using enriched patterns. The lazy
tracing approach required less total time both for tracing and slicing (particularly for simple patterns). Thus, Haskell’s built-in lazy
evaluation strategy offers advantages by avoiding explicitly constructing the full trace in memory when it is not needed; however,
there is still room for improvement. Again, however, for an actual
workflow involving images or large data files, the evaluation time
would be much larger, dwarfing the time for tracing or slicing.
Our implementation is a proof-of-concept that evaluates queries
in-memory via interpretation, rather than compilation; further work
would be needed to adapt our approach to support fine-grained
provenance for conventional database systems. Nevertheless, our
experimental results do suggest that the lazy tracing strategy and
use of enriched patterns can effectively decrease the overhead of

11

tive functions. Dependency provenance cannot predict exactly how
the output will be affected by a general modification to the source,
but it can guarantee that some parts of the output will not change if
certain parts of the input are fixed. Our notion of equivalence modulo a pattern is a generalization of the equal-except-at relation used
in that work. Motivated by dependency provenance, an earlier technical report [10] presented a model of traced evaluation for NRC
and proved elementary properties such as fidelity. However, it did
not investigate slicing techniques, and used nondeterministic label
generation instead of our deterministic scheme; our deterministic
approach greatly simplifies several aspects of the system, particularly for slicing.
There are several intriguing directions for future work, including developing more efficient techniques for traced evaluation and
slicing that build upon existing database query optimization capabilities. It appears possible to translate multiset queries so as to
make the labels explicit, since a fixed given query increases the
label depth by at most a constant. Thus, it may be possible to evaluate queries with label information but without tracing first, then
gradually build the trace by slicing backwards through the query,
re-evaluating subexpressions as necessary. Other interesting directions include the use of slicing techniques for security, to hide confidential input information while disclosing enough about the trace to
permit recomputation, and the possibility of extracting other forms
of provenance from traces, as explored in the context of functional
programs in prior work [1].

ciety University Research Fellowship, by the EU FP7 DIACHRON
project, and EPSRC grant EP/K020218/1. Acar is partially supported by an EU ERC grant (2012-StG 308246—DeepSea) and an
NSF grant (CCF-1320563).

References
[1] U. A. Acar, A. Ahmed, J. Cheney, and R. Perera. A core calculus for
provenance. Journal of Computer Security, 21:919–969, 2013. Full
version of a POST 2012 paper.
[2] U. A. Acar, P. Buneman, J. Cheney, N. Kwasnikowska,
J. Van den Bussche, and S. Vansummeren. A graph model of
data and workflow provenance. In TAPP, 2010.
[3] Y. Amsterdamer, S. B. Davidson, D. Deutch, T. Milo, J. Stoyanovich,
and V. Tannen. Putting lipstick on pig: Enabling database-style workflow provenance. PVLDB, 5(4):346–357, 2011.
[4] Y. Amsterdamer, D. Deutch, and V. Tannen. Provenance for aggregate
queries. In PODS, pages 153–164. ACM, 2011.
[5] R. Bose and J. Frew. Lineage retrieval for scientific data processing: a
survey. ACM Comput. Surv., 37(1):1–28, 2005.
[6] P. Buneman, J. Cheney, and S. Vansummeren. On the expressiveness
of implicit provenance in query and update languages. ACM Transactions on Database Systems, 33(4):28, November 2008.
[7] P. Buneman, S. Khanna, and W. Tan. Why and where: A characterization of data provenance. In ICDT, number 1973 in LNCS, pages
316–330. Springer, 2001.
[8] P. Buneman, S. Khanna, and W. Tan. On propagation of deletions and
annotations through views. In PODS, pages 150–158, 2002.

9. Conclusion

[9] P. Buneman, S. A. Naqvi, V. Tannen, and L. Wong. Principles of programming with complex objects and collection types. Theor. Comp.
Sci., 149(1):3–48, 1995.

The importance of provenance for transparency and reproducibility
is widely recognized, yet there has been little explicit discussion
of correctness properties formalizing intuitions about how provenance is to provide reproducibility. In self-explaining computation,
traces are considered to be explanations of a computation in the
sense that the trace can be used to recompute (parts of) the output
under hypothetical changes to the input. This paper develops the
foundations of self-explaining computation for database queries,
by defining a tracing semantics for NRC, proposing a formal definition of correctness for tracing (fidelity) and slicing, and defining
a correct (though potentially overapproximate) algorithm for trace
slicing. Trace slicing can be used to obtain smaller “golden trail”
traces that explain only a part of the input or output, and explore the
impact of changes in hypothetical scenarios similar to the original
run. At a technical level, the main contributions are the careful use
of prefix codes to label multiset elements, and the development of
enriched patterns that allow more precise slices. Our design is validated by a proof-of-concept implementation that shows that laziness and enriched patterns can significantly improve performance
for small (in-memory) examples.
In the near term, we plan to combine our work on selfexplaining functional programs [27] and database queries (this
paper) to obtain slicing and provenance models for programming
languages with query primitives, such as F# [14] or Links [23].
Ultimately, our aim is to extend self-explaining computation to
programs that combine several execution models, including workflows, databases, conventional programming languages, Web interaction, or cloud computing.

[10] J. Cheney, U. A. Acar, and A. Ahmed. Provenance traces. CoRR,
arXiv.org/abs/0812.0564, 2008.
[11] J. Cheney, U. A. Acar, and R. Perera. Toward a theory of selfexplaining computation. In In search of elegance in the theory and
practice of computation: a Festschrift in honour of Peter Buneman,
number 8000 in LNCS, pages 193–216. Springer, 2013.
[12] J. Cheney, A. Ahmed, and U. A. Acar. Provenance as dependency
analysis. Mathematical Structures in Computer Science, 21(6):1301–
1337, 2011.
[13] J. Cheney, L. Chiticariu, and W. C. Tan. Provenance in databases:
Why, how, and where. Foundations and Trends in Databases,
1(4):379–474, 2009.
[14] J. Cheney, S. Lindley, and P. Wadler. A practical theory of languageintegrated query. In ICFP, pages 403–416, New York, NY, USA, 2013.
ACM.
[15] Y. Cui, J. Widom, and J. L. Wiener. Tracing the lineage of view data in
a warehousing environment. ACM Trans. Database Syst., 25(2):179–
227, 2000.
[16] J. Dean and S. Ghemawat. MapReduce: simplified data processing on
large clusters. Commun. ACM, 51(1):107–113, 2008.
[17] J. Field and F. Tip. Dynamic dependence in term rewriting systems
and its application to program slicing. Information and Software
Technology, 40(11–12):609–636, 1998.
[18] J. N. Foster, T. J. Green, and V. Tannen. Annotated XML: queries and
provenance. In PODS, pages 271–280, 2008.
[19] F. Geerts and A. Poggi. On database query languages for K-relations.
J. Applied Logic, 8(2):173–185, 2010.

Acknowledgments We are grateful to Peter Buneman, Jan Van
den Bussche, and Roly Perera for comments on this work and to
the anonymous reviewers for detailed suggestions. Effort sponsored
by the Air Force Office of Scientific Research, Air Force Material
Command, USAF, under grant number FA8655-13-1-3006. The
U.S. Government and University of Edinburgh are authorized to reproduce and distribute reprints for their purposes notwithstanding
any copyright notation thereon. Cheney is supported by a Royal So-

[20] T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings.
In PODS, pages 31–40, 2007.
[21] J. Hidders, N. Kwasnikowska, J. Sroka, J. Tyszkiewicz, and J. Van den
Bussche. A formal model of dataflow repositories. In DILS, 2007.
[22] N. Kwasnikowska and J. Van den Bussche. Mapping the NRC
dataflow model to the open provenance model. In IPAW, pages 3–16,
2008.

12

[23] S. Lindley and J. Cheney. Row-based effect types for database integration. In TLDI, pages 91–102. ACM Press, 2012.
[24] P. Missier, B. Ludäscher, S. Dey, M. Wang, T. McPhillips, S. Bowers,
M. Agun, and I. Altintas. Golden trail: Retrieving the data history that
matters from a comprehensive provenance repository. International
Journal of Digital Curation, 7(1):139–150, 2011.
[25] L. Moreau. The foundations for provenance on the web. Foundations
and Trends in Web Science, 2(2–3), 2010.
[26] C. Olston, B. Reed, U. Srivastava, R. Kumar, and A. Tomkins. Pig
latin: a not-so-foreign language for data processing. In SIGMOD,
pages 1099–1110. ACM, 2008.
[27] R. Perera, U. A. Acar, J. Cheney, and P. B. Levy. Functional programs
that explain their work. In ICFP, pages 365–376. ACM, 2012.
[28] A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5–19,
2003.
[29] Y. Simmhan, B. Plale, and D. Gannon. A survey of data provenance
in e-science. SIGMOD Record, 34(3):31–36, 2005.
[30] F. Tip. A survey of program slicing techniques. J. Prog. Lang., 3(3),
1995.
[31] M. Weiser. Program slicing. In ICSE, pages 439–449. IEEE Press,
1981.

13

Γ⊢T :τ
b ∈ {true, false}
Γ ⊢ b : bool

n∈N
Γ ⊢ n : int

f : (b1 , . . . , bn ) → b ∈ Σ
Γ ⊢ T1 : b1
···
Γ ⊢ f(T1 , . . . , Tn ) : b

Γ ⊢ T1 : τ1
Γ, x : τ1 ⊢ T2 : τ2
Γ ⊢ let x = T1 in T2 : τ2
b ∈ {true, false}

Γ ⊢ T : {τ }

Γ ⊢ T1 : τ1
···
Γ ⊢ Tn : τn
Γ ⊢ hA1 : T1 , . . . , An : Tn i : hA1 : τ1 , . . . , An : τn i

Γ ⊢ T ∪ T ′ : {τ }

Γ, x : τ ⊢ e : {τ ′ }

Γ ⊢ T : {τ }

Γ ⊢ sum T : int

Γ ⊢ empty T : bool

Γ ⊢ T : {τ }
Γ, x ∈ {τ } ⊢ Θ : {τ ′ }
[
Γ ⊢ {e | x ∈ T } ⊲ Θ : {τ ′ }

Γ, x : τ ⊢ T : {τ ′ }
Γ, x ∈ {τ } ⊢ {ℓ.T } : {τ ′ }

′

Γ, x ∈ {τ } ⊢ ∅ : {τ }

Γ⊢T :τ
Γ ⊢ {T } : {τ }

Γ ⊢ ∅ : {τ }

Γ ⊢ T : {int}

Γ, x ∈ {τ } ⊢ Θ : {τ ′ }

x:τ ∈Γ
Γ⊢x:τ

Γ ⊢ T : hA1 : τ1 , . . . , An : τn i
Γ ⊢ T.Ai : τi

Γ ⊢ T′ : τ

Γ ⊢ T : bool
Γ ⊢ e1 : τ
Γ ⊢ e2 : τ
Γ ⊢ if(T, e1 , e2 ) ⊲b T ′ : τ

Γ ⊢ T ′ : {τ }

Γ ⊢ Tn : bn

Γ, x ∈ {τ } ⊢ Θ1 : {τ ′ }
Γ, x ∈ {τ } ⊢ Θ2 : {τ ′ }
Γ, x ∈ {τ } ⊢ Θ1 ∪ Θ2 : {τ ′ }

Figure 12. Well-typed traces.
T′ ⊑ T

T ′′ ⊑ T ′

✷⊑T

hA1 :

T ⊑T
T1′ ⊑ T1
′
T1 , . . . , An :

T′ ⊑ T
{T ′ } ⊑ {T }

T

′′

T′ ⊑ T

T1′ ⊑ T1
T2′ ⊑ T2
′
′
T1 ∪ T2 ⊑ T1 ∪ T2

···

f(T1′ , . . . , Tn′ )

⊑T

···
Tn′ ⊑ Tn
⊑ hA1 : T1 , . . . , An : Tn i

Tn′ i

T1′ ⊑ T1
T′ ⊑ T
T .A ⊑ T.A
′

T′ ⊑ T
sum T ′ ⊑ sum T

T1′ ⊑ T1

Tn′ ⊑ Tn

⊑ f(T1 , . . . , Tn )

let x =

T0′ ⊑ T0
′
if(T0 , e1 , e2 ) ⊲b T ′

T′ ⊑ T
empty T ′ ⊑ empty T

T1′

in

T2′

T2′ ⊑ T2
⊑ let x = T1 in T2

T′ ⊑ T
⊑ if(T0 , e1 , e2 ) ⊲b T

∅⊑∅

T′ ⊑ T
Θ′ ⊑ Θ
[
[
′
′
{e | x ∈ T } ⊲ Θ ⊑ {e | x ∈ T } ⊲ Θ

Θ′ ⊑ Θ ⇐⇒ ∀ℓ ∈ dom(Θ′ ).Θ′ (ℓ) ⊑ Θ(ℓ)
Figure 13. Subtrace relation.

A. Auxiliary definitions
Figure 12 summarizes the typing rules for traces. Figure 13 defines the subtrace relation.

B. Proofs of pattern properties
We prove the required properties for enriched patterns. The corresponding properties for the sublanguage of simple patterns follow
immediately since simple patterns are closed under the relevant operations.
Lemma B.1. If p, p′ ⊑ v then p ⊔ p′ exists and is the least upper bound of p and p′ .
Proof. If both p and p′ match some pattern q, then it is straightforward to show by induction on q that p ⊔ p′ is defined and p ⊔ p′ ⊑ q.
Specifically, if p or p′ is ✷ or ✸ then we are done; if p and p′ are both constants then we are done; otherwise, in each case, the toplevel
structure of p and p′ must match q, so that we can apply one of the rules for ⊔ on smaller terms that match part of q. When q = v, the desired
result follows. The second part (that ⊔ is a least upper bound) also follows directly since clearly, p, p′ ⊑ p ⊔ p′ and if p, p′ ⊑ q then a similar
argument shows that p ⊔ p′ ⊑ q.
Lemma B.2. For any v, v ′ , p, v hp[✸/✷] v ′ holds if and only if v hp v ′ holds and v = v ′ .
Proof. Straightforward induction on the derivation of v hp[✸/✷] v ′ .
Lemma B.3. For any v, v ′ , p, p′ , we have v hp⊔p′ v ′ if and only if v hp v ′ and v hp′ v ′ . Moreover, p ⊑ p′ if and only if for all v, v ′ , we
have v hp′ v ′ implies v hp v ′ .
Proof. For the first part, we proceed by induction on the total size of p, p′ . The cases where one of p, p′ is ✷ or ✸ are straightforward; for ✸
we also need Lemma B.2. The cases involving constants, pairs, or complete set and record patterns are also straightforward.
There are several similar cases involving partial set or record patterns. We illustrate two representative cases:
1. If p = {ℓi .pi , ℓ′i .qi } and p′ = {ℓi .p′i } ∪˙ ✷ then p ⊔ p′ = {ℓi .pi ⊔ p′i , ℓ′i .qi }. First, suppose v hp⊔p′ v ′ . This means v = {ℓi .vi , ℓ′i .wi }
and v ′ = {ℓi .vi′ , ℓ′i .wi′ }, where vi hpi ⊔p′i vi′ and wi hqi wi′ . Therefore, by induction, vi hpi vi′ and vi hp′i vi′ , so we can conclude that
{ℓi .vi , ℓ′i .wi } hp {ℓi .vi′ , ℓ′i .wi′ } and {ℓi .vi , ℓ′i .wi } hp′ {ℓi .vi′ , ℓ′i .wi′ }, as required.
14

Conversely, if we assume v hp v ′ and v hp′ v ′ , then we must have v = {ℓi .vi , ℓ′i .wi } and v ′ = {ℓi .vi′ , ℓ′i .wi′ }, where vi hpi vi′ and
vi hp′i vi′ and wi hqi wi′ . Thus, by induction we have vi hpi ⊔p′i vi′ so we can conclude {ℓi .vi , ℓ′i .wi } hp⊔p′ {ℓi .vi′ , ℓ′i .wi′ }.
2. If p = {ℓi .pi , ℓ′i .qi } ∪˙ ✷ and p′ = {ℓi .p′i , ℓ′′i .ri } ∪˙ ✸ then p ⊔ p′ = {ℓi .pi ⊔ p′i , ℓ′i .qi [✸/✷], ℓ′′i .ri } ∪˙ ✸. First, suppose v hp⊔p′ v ′ .
This means v = {ℓi .vi , ℓ′i .wi , ℓ′′i .ui } ⊎ w0 and v ′ = {ℓi .vi′ , ℓ′i .wi′ , ℓ′′i .u′i } ⊎ w0 , where vi hpi ⊔p′i vi′ and wi hqi [✸/✷] wi′ and
ui hri u′i . Therefore, by induction, vi hpi vi′ and vi hp′i vi′ , and we also have wi hqi wi′ and wi = wi′ , so we can conclude that
{ℓi .vi , ℓ′i .wi , ℓ′′i .ui } ⊎ w0 hp {ℓi .vi′ , ℓ′i .wi′ , ℓ′′i .u′i } ⊎ w0 and {ℓi .vi′ , ℓ′i .wi , ℓ′′i .ui } ⊎ w0 hp′ {ℓi .vi′ , ℓ′i .wi′ , ℓ′′i .u′i } ⊎ w0 , as required.
Conversely, if we assume v hp v ′ and v hp′ v ′ , then we must have v = {ℓi .vi , ℓ′i .wi , ℓ′′i .ui } ⊎ v0 and v ′ = {ℓi .vi′ , ℓ′i .wi′ , ℓ′′i .u′i } ⊎ v0′
where vi hpi vi′ and vi hp′i vi′ and wi hqi wi′ and ui hri u′i . In addition, we must have that wi = wi′ and v0 = v0′ since v and v ′
must be equal at all labels not in ℓi , ℓ′′i . Thus, by induction we have vi hpi ⊔p′i vi′ and (using Lemma B.2) we can also easily show that
wi hqi [✸/✷] wi , so we can conclude that {ℓi .vi , ℓ′i .wi , ℓ′′i .u′i } ⊎ v0 hp⊔p′ {ℓi .vi′ , ℓ′i .wi , ℓ′′i .ui } ⊎ v0 .
The second part follows immediately from the definition of p ⊑ p′ as p ⊔ p′ = p′ .
Lemma B.4 (Properties of union and restriction).
1. If p1 ⊑ v1 and p2 ⊑ v2 and v1 hp1 v1′ and v2 hp2 v2′ then v1 ⊎ v2 hp1 ⊎p2 v1′ ⊎ v2′ , provided all of these disjoint unions are defined.
2. If p ⊑ v1 ⊎ v2 and L1 ≤ dom(v1 ) and L2 ≤ dom(v2 ) and L1 , L2 are prefix-disjoint, then p|L1 ⊑ v1 and p|L2 ⊑ v2 .
Proof. For part 1, assume p1 ⊑ v1 , p2 ⊑ v2 , v1 hp1 v1′ and v2 hp2 v2′ , and assume that the domains of p1 and p2 , v1 and v2 , and v1′ and v2′
are prefix-disjoint respectively, so that the unions exist. There are several cases. If p1 or p2 is ✷ then the conclusion is immediate. If both are
✸ then v1 = v1′ and v2 = v2′ so v1 ⊎ v2 = v1′ ⊎ v2′ .
Most of the remaining cases are straightforward; we illustrate with the case p1 = {ℓi .pi } ∪˙ ✷ and p2 = {ℓ′i .qi } ∪˙ ✸. In this case,
v1

=

{ℓi .vi1 } ⊎ v01

v2

=

{ℓ′i .vi2 } ⊎ v02

v1′
v2′

=

{ℓi .wi1 } ⊎ w01

=

{ℓ′i .wi2 } ⊎ w02

and we also know that vi1 hpi wi1 and vi2 hqi wi2 for each i. Therefore,
{ℓi .vi1 } ⊎ v01 ⊎ {ℓ′i .vi2 } ⊎ v02

=
h{ℓ

′
˙
i .pi ,ℓi .qi }∪✷

=

{ℓi .vi1 , ℓ′i .vi2 } ⊎ v01 ⊎ v02
{ℓi .wi1 , ℓ′i .wi2 } ⊎ w01 ⊎ w02
{ℓi .wi1 } ⊎ w01 ⊎ {ℓ′i .wi1 } ⊎ w02

For part 2, assume p ⊑ v1 ⊎ v2 and Li ≤ dom(vi ) for i ∈ {1, 2}. We proceed by case analysis on p. The cases p = ✷ and p = ✸ are
immediate since ✷|L = ✷ and ✸|L = ✸. If p = {ℓi .pi } is a complete set pattern, then p|L1 selects just those elements of p that have a prefix
in Li , and since every element of vq has its label’s prefix in L1 we must have that v1 = {ℓ′i .vi′ } where pi ⊑ vi′ for each i and p|L1 = {ℓ′i .p′i },
which is what we need to show. The cases for p = {ℓi .pi } ∪˙ ✷ and p = {ℓi .pi } ∪˙ ✸ are similar.
A symmetric argument suffices to show p|L2 ⊑ v2 .
Lemma B.5 (Projection and ⊑).
1.
2.
3.
4.

If p ⊑ {ǫ.v} then p.ǫ ⊑ v.
If p ⊑ 1 · v1 ⊎ 2 · v2 then p[1] ⊑ v1 and p[2] ⊑ v2 .
If p ⊑ ℓ · v then p[ℓ] ⊑ v.
If p ⊑ hAi : vi i then p.Ai ⊑ vi .

Proof. For part (1), suppose p ⊑ {ǫ.v}. We proceed by case analysis on p. The cases for ✷ and ✸ are trivial. If p = {ǫ.p′ } then p.ǫ = p′ so
the conclusion follows. The cases for p = {ǫ.p′ } ∪˙ ✷ or p = {ǫ.p′ } ∪˙ ✸ are similar.
For part (2), suppose p ⊑ 1 · v1 ⊎ 2 · v2 . Suppose v1 = {ℓi .vi } and v2 = {ℓ′i .vi′ }. If p is a complete set pattern, then it must be of the
form {1.ℓi .pi , 2.ℓ′i .qi } , where pi ⊑ vi and qi ⊑ vi′ . The desired conclusion follows since p[1] = {ℓi .pi }, and a symmetric argument shows
that p[2] ⊑ v2 . The cases for partial set patterns are similar, since the ✷ or ✸ is preserved by the projection operation.
For part (3), suppose p ⊑ ℓ · v. The proof is analogous to the previous case.
For part (4), suppose p ⊑ hAi : vi i. If p = ✸ or ✷, the result is immediate; otherwise, p is a record pattern. If it is a total record pattern
hAi : pi i then clearly p.Ai = pi ⊑ vi . Otherwise, it is a partial pattern, in which case either p.Ai is a pattern pi mentioned in p, in which
case we are done, or p.Ai = ✸ or p.Ai = ✷, and the conclusion follows immediately.
Lemma B.6 (Projection and hp ).
1.
2.
3.
4.

If p ⊑ {ǫ.v} and v hp.ǫ v ′ then {ǫ.v} hp {ǫ.v ′ }.
If p ⊑ 1 · v1 ⊎ 2 · v2 and v1 hp[1] v1′ and v2 hp[2] v2′ then 1 · v1 ⊎ 2 · v2 hp 1 · v1′ ⊎ 2 · v2′ .
If p ⊑ ℓ · v and v hp[ℓ] v ′ then ℓ · v hp ℓ · v ′ .
If p ⊑ hAi : vi i and v1 hp.A1 v1′ , . . . , vn hp.An vn′ then hAi : vi i hp hAi : vi′ i.
15

Proof. For part (1), suppose p ⊑ {ǫ.v} and v hp.ǫ v ′ . If p = ✷ or ✸ then the result is immediate (this is the case for all three parts of the
lemma). If p = {ǫ.p′ }, p = {ǫ.p′ } ∪˙ ✷, or p = {ǫ.p′ } ∪˙ ✸ then p.ǫ = p′ so v hp′ v ′ . We can conclude {ǫ.v} hp {ǫ.v ′ }.
For part (2), suppose p ⊑ 1 · v1 ⊎ 2 · v2 and v1 hp[1] v1′ and v2 hp[2] v2′ . As usual, the cases p = ✷ and p = ✸ are trivial. Suppose
v1 = {ℓi .vi′ } and v2 = {ℓ′i .vi′′ }. If p is a complete set pattern it must be of the form {1.ℓi .pi , 2.ℓ′i .qi }, and v1 h{ℓi .pi } v1′ and v2 h{ℓ′ .qi } v2′ .
i
It is straightforward to show that 1·v1 h{1·ℓi .pi } 1·v1′ and 2·v2 h{2·ℓ′ .q } 2·v2′ , so by previous results we have 1·v1 ⊎2·v2 hp 1·v1′ ⊎2·v2′ .
i i
The cases for partial patterns follow the same reasoning, making use of the fact that projection preserves the partial pattern.
For part (3), suppose p ⊑ ℓ · v. The argument is similar to the previous case.
For part (4) suppose p ⊑ hAi : vi i and vi hp.Ai vi′ for each i. If p is ✷, ✸, or a complete record pattern then the conclusion is immediate.
Otherwise, if p = hBi : qi i ∪˙ ✷, the conclusion is immediate since each component of the records hAi : vi i and hAi : vi′ i either match the
appropriate qi or need not match because of the hole. Finally, if p = hBi : qi i ∪˙ ✸, the conclusion follows since each pair of corresponding
components of the records hAi : vi i and hAi : vi′ i either match the appropriate qi or are equal because p.Ai = ✸ if Ai is not among the
Bj .

C. Proof of correctness of trace slicing
Lemma C.1. If γ, x ∈ v1 , Θ y∗ v2 and v1′ ⊆ v1 then there exists v2′ ⊆ v2 such that γ, x ∈ v1′ , Θ y∗ v2′ .
Proof. The proof is straightforward by induction on derivations. The cases for v1 = ∅ and v1 = {ℓ.v} are immediate; if v1 = w1 ⊎ w2 then
we proceed by induction using the subsets w1′ = w1 ∩ v1′ and w2′ = w2 ∩ v1′ .
We prove correctness of the full trace slicing algorithm, with enriched patterns, since the correctness for simple patterns follows as a
special case.
Theorem C.2 (Correctness of Slicing).
1. Suppose γ, T y v and p ⊑ v and p, T ց ρ, S. Then for all γ ′ hρ γ and T ′ ⊒ S such that γ ′ , T ′ y v ′ we have v ′ hp v.
2. Suppose γ, x ∈ v0 , Θ y∗ v and p ⊑ v and p, x.Θ0 ց∗ ρ, Θ′0 , p0 , where Θ0 ⊆ Θ. Then for all γ ′ hρ γ and v0′ hp0 v0 and Θ′ ⊒ Θ′0
such that γ ′ , x ∈ v0′ , Θ′ y∗ v ′ we have v ′ hp v.
Proof. For part (1), the proof is by induction on the structure of slicing derivations, using inversion to extract information from other
derivations. The cases for variables, constants, primitive operations, and let-binding are exactly as in previous work [1]. The cases for
conditionals are similar to the those for variant types and case constructs in previous work.
We show the cases for records and set operations, which are new to this paper (records are handled similarly to pairs in our previous work,
so the cases for pairs are omitted).
• Field projection. If the last step in the slicing derivation is

hAi :p; ✷i, T ց ρ, S
p, T.Ai ց ρ, S.Ai
then the evaluation derivation must be of the form
γ, T y hA1 :v1 , . . . , An :vn i
γ, T.Ai y vi
Let γ ′ hρ γ and T ′ ⊒ S.Ai be given, where γ ′ , T ′ y v ′ . Then T ′ must have the form T ′′ .Ai for some T ′′ ⊒ S so the replay derivation
is of the form
γ ′ , T ′′ y hA1 :v1′ , . . . , An :vn′ i
γ ′ , T ′′ .Ai y vi′
The induction hypothesis applies since it is easy to show that hAi : p; ✷i ⊑ hA1 :v1 , . . . , An :vn i. Therefore
hA1 :v1′ , . . . , An :vn′ i hhAi :p;✷i hA1 :v1 , . . . , An :vn i .
From this it is obvious that vi′ hp vi .
• Record. If the last step in the slicing derivation is
p.A1 , T1 ց ρ1 , S1
···
p.An , Tn ց ρn , Sn
p, hA1 :T1 , . . . , An :Tn i ց ρ1 ⊔ · · · ⊔ ρn , hA1 :S1 , . . . , An :Sn i
then the evaluation derivation must be of the form
γ, T1 y v1
···
γ, Tn y vn
γ, hA1 :T1 , . . . , An :Tn i y hA1 :v1 , . . . , An :vn i
Let γ ′ hρ1 ⊔···⊔ρn γ and T ′ ⊒ hA1 :S1 , . . . , An :Sn i be given, where γ ′ , T ′ y v ′ . Then T ′ must have the form hA1 :T1′ , . . . , An :Tn′ i,
where Ti′ ⊒ Si for each i, so the replay derivation is of the form
γ ′ , T1′ y v1′
···
γ ′ , Tn′ y vn′
′
′
γ , hA1 :T1 , . . . , An :Tn i y hA1 :v1′ , . . . , An :vn′ i
′

16

By Lemma B.5 we know p.Ai ⊑ vi for each i, and γ ′ hρi γ for each i, so by induction vi′ hp.Ai vi for each i. Using Lemma B.6 we
can conclude that hA1 :v1′ , . . . , An :vn′ i hp hA1 :v1 , . . . , An :vn i.
• Empty set. This case is trivial, similar to the usual case for constants.
• Singleton. This case follows immediately from the relevant properties of p.ǫ, using similar reasoning to the record projection case.
• Union. If the last step in the slicing derivation is
p[1], T1 ց ρ1 , S1
p[2], T2 ց ρ2 , S2
p, T1 ∪ T2 ց ρ1 ⊔ ρ2 , S1 ∪ S2
then the evaluation derivation must be of the form
γ, T1 y v1
γ, T2 y v2
γ, T1 ∪ T2 y 1 · v1 ⊎ 2 · v2
Let γ ′ hρ1 ⊔ρ2 γ and T ′ ⊒ T1 ∪ T2 be given, where γ ′ , T ′ y v ′ . Then T ′ must have the form T1′ ∪ T2′ where Ti′ ⊒ Si so the replay
derivation is of the form
γ ′ , T1′ y v1′
γ ′ , T2′ y v2′
γ ′ , T1′ ∪ T2′ y 1 · v1′ ⊎ 2 · v2′
By Lemma B.5 we know p[1] ⊑ v1 and p[2] ⊑ v2 , and γ ′ hρi γ, so by induction we have v1′ hp[1] v1 and v2′ hp[2] v2 , and therefore by
Lemma B.6 we can conclude 1 · v1′ ⊎ 2 · v2′ hp 1 · v1 ⊎ 2 · v2 .
• Sum and emptiness. In both cases, since the slice ensures that the whole argument to the sum or emptiness test is preserved, the argument
is straightforward. For example, for emptiness suppose the derivation is of the form:
✸, T ց ρ, S
p, empty T ց ρ, empty S
Then there are two cases. If replay derivation is of the form
γ, T y ∅
γ, empty T y true
Suppose γ ′ hρ γ and T ′ ⊒ empty S with γ ′ , T ′ y v ′ . Then T ′ is of the form empty T ′′ with T ′′ ⊒ S, so the replay derivation must be
of the form:
γ ′ , T ′′ y v ′′
′
γ , empty T ′′ y v ′
By induction, v ′′ h✸ ∅, which implies v ′′ = ∅ so v ′ = true hp true (since p ⊑ true). The cases where the argument to empty T
evaluates to a nonempty set, and for sum T , are similar.
• Comprehension. If the derivation is of the form
p, x.Θ ց∗ ρ′ , Θ0 , p0
p0 , T ց ρ, S
[
[
p, {e | x ∈ T } ⊲ Θ ց ρ ⊔ ρ′ , {e | x ∈ S} ⊲ Θ0
then the replay derivation must be of the form
γ, T y v0
γ, x ∈ v0 Θ y∗ v
[
γ, {e | x ∈ T } ⊲ Θ y v

S
S
Suppose γ ′ hρ⊔ρ′ γ and T ′ ⊒ {e | x ∈ S} ⊲ Θ0 with γ ′ , T ′ y v ′ . Then T ′ must be of the form {e | x ∈ T ′′ } ⊲ Θ′ for some T ′′ ⊒ S
′
and Θ ⊒ Θ0 so the replay derivation must be of the form
γ ′ , T ′′ y v0′
γ ′ , x ∈ v0′ , Θ′ y∗ v ′
[
γ ′ , {e | x ∈ T ′′ } ⊲ Θ′ y v ′
Since p0 ⊑ v0 and γ ′ hρ γ and γ ′ hρ′ γ we have v0′ hp0 v0 by induction. Thus, by the second induction hypothesis, since p ⊑ v and
γ ′ hρ′ γ and v0′ hp0 v0 we have v ′ hp v.
For part (2), the proof is again by induction on the structure of derivations.
• If the slicing derivation is of the form

∅, x.∅ ց∗ [], ∅, ∅
then the conclusion is immediate, since rerunning an empty trace set always yields the empty set.
• If the slicing derivation is of the form
✸, x.∅ ց∗ [], ∅, ∅
then the conclusion is immediate as before, since rerunning an empty trace set always yields the empty set.

17

• If the slicing derivation is of the form

✷, x.Θ ց∗ [], ∅, ✷
then the conclusion is immediate, since any two values match according to ✷.
• If the slicing derivation is of the form
p[ℓ], T ց ρ[x 7→ p0 ], S
p, x.{ℓ.T } ց∗ ρ, {ℓ.S}, {ℓ.p0 }
then observe that Θ ⊇ {ℓ.T } by assumption, so Θ(ℓ) = T . So, the replay derivation must have the form
ℓ ∈ dom(Θ)
γ[x 7→ v0 ], T y v
γ, x ∈ {ℓ.v0 }, Θ y∗ ℓ · v
Now suppose that γ ′ hρ γ and v0′ h{ℓ.p0 } {ℓ.v0 } and Θ′ ⊒ {ℓ.S} are given where γ ′ , x ∈ v0′ , Θ′ y∗ v ′ . It follows that v0′ = {ℓ.v0′′ }
and v0′′ hp0 v0 , so γ ′ [x 7→ v0′′ ] hρ[x7→p0 ] γ[x 7→ v0 ]. Moreover, by inversion the derivation must have the form:
ℓ ∈ dom(Θ′ )
γ ′ [x 7→ v0′′ ], Θ′ (ℓ) y v ′
′
γ , x ∈ {ℓ.v0′′ }, Θ′ y∗ ℓ · v ′
Since by Lemma B.5 p[ℓ] ⊑ v and Θ′ (ℓ) ⊒ S (which holds because Θ′ ⊒ {ℓ.S}), we have by induction that v ′ hp[ℓ] v, and using
Lemma B.6 we can conclude that ℓ · v ′ hp ℓ · v, as desired.
• Suppose the slicing derivation is of the form:
p|dom(Θ1 ) , x.Θ1 ց∗ ρ1 , Θ′1 , p1
p|dom(Θ2 ) , x.Θ2 ց∗ ρ2 , Θ′2 , p2
p, x.Θ1 ⊎ Θ2 ց∗ ρ1 ⊔ ρ2 , Θ′1 ⊎ Θ′2 , p1 ⊎ p2
and suppose that γ, x ∈ v0 , Θ y∗ v where Θ ⊇ Θ1 ⊎ Θ2 . Suppose that γ ′ hρ1 ⊔ρ2 γ and v0′ hp1 ⊎p2 v0 and Θ′ ⊒ Θ′1 ⊎ Θ′2 are given,
where γ ′ , x ∈ v0′ , Θ′ y∗ v ′ . We need to show that v ′ hp v.
Since v0′ hp1 ⊎p2 v0 , it is straightforward to show that there must exist v1 , v2 , v1′ , v2′ such that v1 ⊎ v2 = v0 , v1′ ⊎ v2′ = v0′ , v1 hp1 v1
and v2′ hp2 v2 . Furthermore, by Lemma C.1 we know that γ, x ∈ vi , Θ y∗ wi and γ ′ , x ∈ vi′ , Θ′ y∗ wi′ for some w1 , w2 , w1′ , w2′ .
Therefore, we can conclude that:
γ ′ , x ∈ v1′ , Θ′ y∗ w1′
γ ′ , x ∈ v2′ , Θ′ y∗ w2′
′
′
′
′
γ , x ∈ v1 ⊎ v2 , Θ y∗ w1′ ⊎ w2′

γ, x ∈ v1 , Θ y∗ w1
γ, x ∈ v2 , Θ y∗ w2
γ, x ∈ v1 ⊎ v2 , Θ y∗ w1 ⊎ w2

Furthermore, since v1 ⊎ v2 = v0 , by determinacy we know that w1 ⊎ w2 = v and similarly w1′ ⊎ w2 = v ′ . By induction since pi ⊑ vi
and Θi ⊆ Θ, we know that wi′ hp|dom(Θ ) wi , so we know that
i

v ′ = w1′ ⊎ w2′ hp|dom(Θ

i)

⊎p|dom(Θ )
2

w 1 ⊎ w2 = v .

To conclude, since p ⊑ w1 ⊎ w2 and dom(Θ1 ) ≤ w1 and dom(Θ2 ) ≤ w2 , it follows that p = p|dom(Θ1 ) ⊎ p|dom(Θ2 ) , so we can
conclude w1 ⊎ w2 hp w1′ ⊎ w2′ as desired.
This exhausts all cases and completes the proof.

D. Proof of correctness of query slicing
Lemma D.1. If γ, x ∈ v1 , e ⇓∗ v2 and v1′ ⊆ v1 then there exists v2′ ⊆ v2 such that γ, x ∈ v1′ , e ⇓∗ v2′ .
Proof. The proof is straightforward by induction on derivations. The cases for v1 = ∅ and v1 = {ℓ.v} are immediate; if v1 = w1 ⊎ w2 then
we proceed by induction using the subsets w1′ = w1 ∩ v1′ and w2′ = w2 ∩ v1′ .
We prove Theorem 5.1 by strengthening the induction hypothesis as follows:
Theorem D.2 (Correctness of Query Slicing).
1. Suppose γ, T y v and p ⊑ v and p, T ց
ց ρ, e. Then for all γ ′ hρ γ and e′ ⊒ e such that γ ′ , e′ ⇓ v ′ we have v ′ hp v.
2. Suppose γ, x ∈ v0 , Θ y∗ v and p ⊑ v and p, Θ0 ց
ց∗ ρ, e0 , p0 , where Θ0 ⊆ Θ. Then for all γ ′ hρ γ and v0′ hp0 v0 and e′0 ⊒ e0 such
′
′
′
∗ ′
′
that γ , x ∈ v0 , e0 ⇓ v we have v hp v.
Proof. The proof is by induction on the structure of query slicing derivations. Many of the cases are essentially the same as for trace slicing.
The cases for conditionals are straightforward, since in either case the sliced trace and environment retain enough information to force the
same branch to be taken on recomputation. We show the details of the cases involving conditionals and comprehensions.
For part (1), we consider a conditional and comprehension rule:
• If the slicing derivation is of the form:

p 1 , T1 ց
ց ρ1 , e′1
true, T ց
ց ρ, e′
p1 , if(T, e1 , e2 ) ⊲true T1 ց
ց ρ1 ⊔ ρ, if(e′ , e′1 , ✷)
18

then the replay derivation must be of the form:
γ, T y true
γ, T1 y v1
γ, if(T, e1 , e2 ) ⊲true T1 y v1
Suppose γ ′ hρ1 ⊔ρ γ and e′′ ⊒ if(e′ , e′1 , ✷) are given where γ ′ , e′ ⇓ v ′ . Then e′′ = if(e′′0 , e′′1 , e′′2 ), where e′′0 ⊒ e′ and e′′1 ⊒ e′1 , so
there are two cases for the evaluation derivation. If it has the form
γ ′ , e′0 ⇓ false
γ ′ , e′2 ⇓ v2′
γ ′ , if(e′0 , e′1 , e′2 ) ⇓ v2′
then since γ ′ hρ γ and γ ′ hρ1 γ, by induction we would have that false htrue true, which is absurd. So this case cannot arise.
Otherwise, the derivation must have the form:
γ ′ , e′0 ⇓ true
γ ′ , e′1 ⇓ v1′
′
′
′
′
γ , if(e0 , e1 , e2 ) ⇓ v1′
Since γ ′ hρ γ and γ ′ hρ1 γ, by induction we have that v1′ hp1 v1 as desired.
• Comprehension. If the derivation is of the form
p0 , T ց
ց ρ, e′0
p, x.Θ ց
ց∗ ρ′ , e′1 , p0
[
[
p, {e | x ∈ T } ⊲ Θ ց
ց ρ ⊔ ρ′ , {e′1 | x ∈ e′0 }
then the replay derivation must be of the form
γ, T y v0
γ, x ∈ v0 , Θ y∗ v
[
γ, {e | x ∈ T } ⊲ Θ y v

S
S
Suppose γ ′ hρ⊔ρ′ γ and e′′ ⊒ {e′1 | x ∈ e′0 } with γ ′ , e′′ ⇓ v ′ . Then e′′ must be of the form {e′′1 | x ∈ e′′0 } for some e′′1 ⊒ e′1 and
′′
′
e0 ⊒ e0 , so the evaluation derivation must be of the form
γ ′ , e′′0 ⇓ v0′
γ ′ , x ∈ v0′ , e′′1 ⇓∗ v ′
[
γ ′ , {e′′1 | x ∈ e′′0 } ⇓ v ′
Since p0 ⊑ v0 and γ ′ hρ γ and γ ′ hρ′ γ we have v0′ hp0 v0 by induction. Thus, by the second induction hypothesis, since p ⊑ v and
γ ′ hρ′ γ and v0′ hp0 v0 we have v hp v ′ .
For part (2), we consider the singleton and union rules:
• If the slicing derivation is of the form

p[ℓ], T ց
ց ρ[x 7→ p0 ], e′
p, x.{ℓ.T } ց
ց∗ ρ, e′ , {ℓ.p0 }
then recall that by assumption, Θ(ℓ) ⊇ {ℓ.T }, so Θ(ℓ) = T , so the replay derivation must have the form
ℓ ∈ dom(Θ)
γ[x 7→ v0 ], T y v
γ, x ∈ {ℓ.v0 }, Θ y∗ ℓ · v
Now suppose that γ ′ hρ γ and v0′ h{ℓ.p0 } {ℓ.v0 } and e′′ ⊒ e′ are given where γ ′ , x ∈ v0′ , e′′ ⇓∗ v ′ . It follows that v0′ = {ℓ.v0′′ } and
v0′′ hp0 v0 , so γ ′ [x 7→ v0′′ ] hρ[x7→p0 ] γ[x 7→ v0 ]. Moreover, by inversion the derivation must have the form:
γ ′ [x 7→ v0′′ ], e′′ ⇓ v ′
γ , x ∈ {ℓ.v0′′ }, e′′ ⇓∗ ℓ · v ′
′

Since by Lemma B.5 p[ℓ] ⊑ v we have by induction that v ′ hp[ℓ] v, and using Lemma B.6 we can conclude that ℓ · v ′ hp ℓ · v, as desired.
• Suppose the slicing derivation is of the form:
p|dom(Θ1 ) , x.Θ1 ց
ց∗ ρ1 , e′1 , p1
p|dom(Θ2 ) , x.Θ2 ց
ց∗ ρ2 , e′2 , p2
∗
′
p, x.Θ1 ⊎ Θ2 ց
ց ρ 1 ⊔ ρ 2 , e0 , p 1 ⊎ p 2
and suppose that γ, x ∈ v0 , Θ y∗ v where Θ ⊇ Θ1 ⊎ Θ2 . Suppose that γ ′ hρ1 ⊔ρ2 γ and v0′ hp1 ⊎p2 v0 and e′0 ⊒ e0 are given, where
γ ′ , x ∈ v0′ , e′0 ⇓∗ v ′ . We need to show that v ′ hp v.
Since v0′ hp1 ⊎p2 v0 , it is straightforward to show that there must exist v1 , v2 , v1′ , v2′ such that v1 ⊎ v2 = v0 , v1′ ⊎ v2′ = v0′ , v1 hp1 v1 and
v2′ hp2 v2 . Furthermore, by Lemmas C.1 and D.1 we know that γ, x ∈ vi , Θ y∗ wi and γ ′ , x ∈ vi′ , e′0 ⇓∗ wi′ for some w1 , w2 , w1′ , w2′ .
Therefore, we can conclude that:
γ ′ , x ∈ v1′ , e′0 ⇓∗ w1′
γ ′ , x ∈ v2′ , e′0 ⇓∗ w2′
γ, x ∈ v1 , Θ y∗ w1
γ, x ∈ v2 , Θ y∗ w2
∗
′
′
′
′
γ, x ∈ v1 ⊎ v2 , Θ y w1 ⊎ w2
γ , x ∈ v1 ⊎ v2 , e0 ⇓∗ w1′ ⊎ w2′
Furthermore, since v1 ⊎ v2 = v0 , by determinacy we know that w1 ⊎ w2 = v and similarly w1′ ⊎ w2 = v ′ . By induction since pi ⊑ vi
and Θi ⊆ Θ, we know that wi′ hp|dom(Θ ) wi , so we know that
i

v ′ = w1′ ⊎ w2′ hp|dom(Θ

i)

19

⊎p|dom(Θ )
2

w 1 ⊎ w2 = v .

To conclude, since p ⊑ w1 ⊎ w2 and dom(Θ1 ) ≤ w1 and dom(Θ2 ) ≤ w2 , it follows that p = p|dom(Θ1 ) ⊎ p|dom(Θ2 ) , so we can
conclude w1 ⊎ w2 hp w1′ ⊎ w2′ as desired.
This exhausts all cases and completes the proof.

20

