Detecting Redundant CSS Rules in HTML5
Applications: A Tree Rewriting Approach
Matthew Hague1 , Anthony Widjaja Lin2 and C.-H. Luke Ong3

arXiv:1412.5143v2 [cs.LO] 21 Jul 2015

1

Royal Holloway, University of London
2
Yale-NUS College
3
University of Oxford

HTML5 applications normally have a large set of CSS (Cascading Style Sheets) rules fordata display. Each CSS rule consists of a node selector and a declaration block (which assigns
values to selected nodes’ display attributes). As web applications evolve, maintaining CSS ﬁlescan easily become problematic. Some CSS rules will be replaced by new ones, but these obsolete(hence redundant) CSS rules often remain in the applications. Not only does this “bloat” theapplications – increasing the bandwidth requirement – but it also signiﬁcantly increases web
browsers’ processing time. Most works on detecting redundant CSS rules in HTML5 applications do not consider the dynamic behaviors of HTML5 (speciﬁed in JavaScript); in fact, theonly proposed method that takes these into account is dynamic analysis, which cannot soundly
prove redundancy of CSS rules. In this paper, we introduce an abstraction of HTML5 applications based on monotonic tree-rewriting and study its “redundancy problem”. We establish theprecise complexity of the problem and various subproblems of practical importance (ranging
from P to EXP). In particular, our algorithm relies on an eﬃcient reduction to an analysis ofsymbolic pushdown systems (for which highly optimised solvers are available), which yields afast method for checking redundancy in practice. We implemented our algorithm and demonstrated its eﬃcacy in detecting redundant CSS rules in HTML5 applications.

1

Introduction

HTML5 is the latest revision of the HTML standard of the World Wide Web Consortium(W3C), which has become a standard markup language of the Internet. HTML5 provides a
uniform framework for designing a web application: (1) data content is given as a standard
HTML tree, (2) rules for data display are given in Cascading Style Sheets (CSS), and (3)dynamic behaviors are speciﬁed through JavaScript.
An HTML5 application normally contains a large set of CSS rules for data display, eachconsisting of a (node) selector given in an XPath-like query language and a declaration block
which assigns values to selected nodes’ display attributes. However, many of these stylingrules are often redundant (in the sense of unreachable code), which “bloat” the application.
As a web application evolves, some rules will be replaced by new rules and developers often
forget to remove obsolete rules. Another cause of redundant styling rules is the common useof HTML5 boilerplate (e.g. WordPress) since they include many rules that the application
will not need. A recent case study [44] shows that in several industrial web applications on
average 60% of the CSS rules are redundant. These bloated applications are not only harder tomaintain, but they also increase the bandwidth requirement of the website and signiﬁcantly
increase web browsers’ processing time. In fact, a recent study [45] reports that when web
browsers are loading popular pages around 30% of the CPU time is spent on CSS selectors(18%) and parsing (11%). [These numbers are calculated without even including the extra 31%
uncategorised operations of the total CPU time, which could include operations from these two
1categories.] This suggests the importance of detecting and removing redundant CSS rules in an
HTML5 application. Indeed, a sound and automatic redundancy checker would allow bloated
CSS stylesheets to be streamlined during development, and generic stylesheets to be minimised
before deployment.
There has been a lot of work on optimising CSS (e.g. [42, 45, 44, 20, 13]), which include
merging “duplicated” CSS rules, refactoring CSS declaration blocks, and simplifying CSS selectors, to name a few. However, most of these works analyse the set of CSS rules in isolation.
In fact, the only available methods (e.g. Cilla [44] and UnCSS [56]) that take into accountthe dynamic nature of HTML5 introduced by JavaScript are based on simple dynamic analysis(a.k.a. testing), which cannot soundly prove redundancy of CSS rules since such techniques
cannot in general test all possible behaviors of the HTML5 application. For example, fromthe benchmarks of Mesbah and Mirshokraie [44] there are some non-redundant CSS rules that
their tool Cilla falsely identiﬁes as redundant, e.g., due to the use of JavaScript to compensate
for browser-speciﬁc behavior under certain HTML5 tags like <input/> (see Section 6 for moredetails). Removing such rules can distort the presentation of HTML5 applications, which isundesirable.
Static Analysis of JavaScript A diﬀerent approach to identifying redundant CSS rules byusing static analysis for HTML5. Since JavaScript is a Turing-complete programming language,
the best one can hope for is approximating the behaviors of HTML5 applications. Static analysis
of JavaScript code is a challenging goal, especially in the presence of libraries like jQuery. The
current state of the art is well surveyed by Andreasen and Møller [8], with the main tools in theﬁeld being WALA [49, 53] and TAJS [8, 27, 26]. These tools (and others) provide traditional
static analysis frameworks encompassing features such as points-to [25, 53] and determinacy
analysis [8, 49], type inference [32, 27] and security properties [22, 23]. The modelling of theHTML DOM is generally treated as part of the heap abstraction [26, 23] and thus the tree
structure is not precisely tracked.
For the purpose of soundly identifying redundant CSS rules, we need a technique for computing a symbolic representation of an overapproximation of the set of all reachable HTMLtrees that is suﬃciently precise for real-world applications. Currently there is no clean abstract
model that captures common dynamics of the HTML (DOM) tree caused by the JavaScript
component of an HTML5 application and at the same time is amenable to algorithmic analysis.
Such a model is not only important from a theoretical viewpoint, but it can also serve as a
useful intermediate language for the analysis of HTML5 applications which among others canbe used to identify redundant CSS rules.
Tree rewriting as an intermediate language. The tree-rewriting paradigm — which iscommonly used in databases (e.g. [38, 15, 6, 19, 18, 7]) and veriﬁcation (e.g. [24, 35, 36, 37,
4, 34]) — oﬀers a clean theoretical framework for modelling the dynamics of tree updates andusually lends itself to fully-algorithmic analysis. This makes tree-rewriting a suitable frameworkin which to model the dynamics of tree updates commonly performed by HTML5 applications.
Surveying real-world HTML5 applications (including Nivo-Slider [47] and real-world examples
from the benchmarks in Mesbah and Mirshokraie [44]), we were surprised to learn that onestep tree updates used in these applications are extremely simple, despite the complexity of
the JavaScript code from the point of view of static analysers. That said, we found that these
updates are not restricted to modifying only certain regions of the HTML tree. As a result,models such as ground tree rewrite systems [36] and their extensions [37, 35, 24, 41, 21] (where
only the bottom part of the tree may be modiﬁed) are not appropriate. However, systems

with rules that may rewrite nodes in any region of a tree are problematic since they render
the simplest problem of reachability undecidable. Recently, owing to the study of active XML,
some restrictions that admit decidability of veriﬁcation (e.g. [6, 18, 19, 7]) have been obtained.
However, these models have very high complexity (ranging from double exponential time tononelementary), which makes practical implementation diﬃcult.
Contributions. The main contribution of the paper is to give a simple and clean treerewriting model which strikes a good balance between: (1) expressivity in capturing the dynamics of tree updates commonly performed in HTML5 applications (esp. insofar as detecting
redundant CSS rules is concerned), and (2) decidability and complexity of rule redundancy
analysis (i.e. whether a given rewrite rule can ever be ﬁred in a reachable tree). We show thatthe complexity of the problem is EXP-complete1 , though under various practical restrictions
the complexity becomes PSPACE or even P. This is substantially better than the complexityof the more powerful tree rewriting models studied in the context of active XML, which is
at least double-exponential time. Moreover, our algorithm relies on an eﬃcient reduction toa reachability analysis in symbolic pushdown systems for which highly optimised solvers (e.g.
Bebop [11], Getaﬁx [31], and Moped [46]) are available.
We have implemented our reduction, together with a proof-of-concept translation tool fromHTML5 to our tree rewriting model. Our translation by no means captures the full feature-setof JavaScript and is simply a means of testing the underlying model and analysis we introduce2 .
We speciﬁcally focus on modelling standard features of jQuery [28] — a simple JavaScript
library that makes HTML document traversal, manipulation, event handling, and animationeasy from a web application developer’s viewpoint. Since its use is so widespread in HTML5
applications nowadays (e.g., used in more than half of the top hundred thousand websites[29]) some authors [32] have advocated a study of jQuery as a language in its own right. Our
experiments demonstrate the eﬃcacy of our techniques in detecting redundant CSS rules in
HTML5 applications. Furthermore, unlike dynamic analysis, our techniques will not falsely
report CSS rules that may be invoked as redundant (at least within the fragment of HTML5
applications that our prototypical implementation can handle). We demonstrate this on anumber of non-trivial examples (including a speciﬁc example from the benchmarks of Mesbahand Mirshokraie [44] and an HTML application using the image slider package Nivo-Slider [47]).
Connection with existing works on static analysis of JavaScript. As surveyed byAndreasen and Møller [8], the static analysis of JavaScript in the presence of the jQuery library— which is essential for analysing HTML5 applications — is currently a formidable task forexisting static analysers. We consider our work to be complementary to these works: ﬁrst, ourtree-rewriting model may form part of a static analysis abstraction, and second, static analysis
will be essential in translating HTML5 applications into our tree rewriting model by extracting
accurate tree update operations. In our implementation, we provide an ad-hoc extraction of tree
update operations that allows us to demonstrate the applicability of our approach. Creating
a robust static analysis that achieves this is an interesting and worthwhile research challenge,
which might beneﬁt from the recent remarkable eﬀort by Bodin et al. [12] of capturing the full
JavaScript semantics and verifying it with Coq.
Organisation. We give a quick overview of HTML5 applications via a simple example in
Section 2. We then introduce our tree rewriting model in Section 3. Since the general model
1 These complexity classes are defined below and we describe the roles they play in our investigation.
2 Handling JavaScript in its full generality is a difficult problem [8], which is beyond the scope of this paper.

is undecidable, we introduce a monotonic abstraction in Section 4. We provide an eﬃcient
reduction from an analysis of the monotonic abstraction to symbolic pushdown systems in
Section 5. Experiments are reported in Section 6. We conclude with future work in Section 7.
Missing proofs and further technical details can be found in the appendix.
Notes on computational complexity. In this paper, we study not only decidability but
also the complexity of computational problems. We believe that pinpointing the precise complexity of veriﬁcation problems is not only of fundamental importance, but also it often suggests
algorithmic techniques that are most suitable for attacking the problem in practice. In this paper, we deal with the following computational complexity classes (see [52] for more details):
P (problems solvable in polynomial-time), PSPACE (problems solvable in polynomial space),and EXP (problems solvable in exponential time). Veriﬁcation problems that have complexity
PSPACE and EXP or beyond — see [51, 30] for a few examples — have substantially beneﬁted
from techniques like symbolic model checking [43]. The redundancy problem that we study inthis paper is another instance of a hard computational problem that can be eﬃciently solved
by BDD-based symbolic techniques in practice.

2

HTML5: a quick overview

In this section, we provide a brief overview of a simple HTML application. We assume basic
familiarity with the static elements of HTML5, i.e., HTML documents (a.k.a. HTML DOM
document objects) and CSS rules (e.g. see [57]). We will discuss their formal models in Section
3. Our example (also available at the URL [2]) is a small modiﬁcation of an example takenfrom an online tutorial [48], which is given in Figure 1. To better understand the application,
we suggest the reader open it with a web browser and interact with it.
In this example the page displays a list of input text boxes contained in a div with class
input_wrap. The user can add more input boxes by clicking the “add ﬁeld” button, and canremove a text box by clicking its neighbouring “remove” button. The script, however, imposesa limit (i.e. 10) on the number of text boxes that can be added. If the user attempts to add
another text box when this limit is reached, the div with ID limit displays the text “Limits
reached” in red.
This dynamic behavior is speciﬁed within the second <script/> tag starting at Line 11(the ﬁrst simply loads the jQuery library). To understand the script, we will provide a quick
overview of jQuery calls (see [28] for more detail). A simple jQuery call may take the form$(selector).action(...);
where ‘$’ denotes that it is a jQuery call, selector is a CSS selector, and action is a rule formodifying the subtree rooted at this node. For example, in Figure 1, Line 29, we have$('#limit').addClass('warn');
The CSS selector #limit identiﬁes the unique node in the tree with ID limit, while theaddClass() call adds the class warn to this node. The CSS rule.warn { color: red }appearing in the head of the document at Line 2 will now match the node, and thus its contents
will be displayed in red.
Another simple example of a jQuery call in Figure 1 is at Line 37

<html><head><style>.warn { color: red }</style></head><body><div class="input_wrap"><button class="button">Add Fields</button><div><input type="text" name="mytext[]"> </div></div><div>Total: </div><div id="counter">1</div><div id="limit">Limits not reached</div><script src="http://ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script><script type="text/javascript">$(document).ready(function() {var x = 1;$('.button').click(function(e){if(x < 10){x++;$('.input_wrap').append('<div>' +'<input type="text" name="mytext[]"/>' +'<a href="#" class="delete">Remove</a>' +'</div>');$('#counter').html(x);}else {$('#limit').html('Limits reached');$('#limit').addClass('warn');}});$('.input_wrap').on('click', '.delete', function(e){$(this).parent('div').remove();x--;$('#counter').html(x);$('.warn').removeClass('warn');$('#limit').html('Limits not reached');})});</script></body></html>Figure 1: A simple HTML5 application (see [2]).

$('.warn').removeClass('warn');
The selector .warn matches all 3 nodes in the tree with class warn. The call to removeClass()
removes the class warn from these nodes. Observe that when this call is invoked, the CSS rule
above will no longer be matched.
Some jQuery calls may contain an event listener. E.g. at Line 16 we have$('.button').click(...);
in Figure 1. This speciﬁes that the function in ‘...’ should ﬁre when a node with class button
is clicked. Similarly at Line 33,$('.input_wrap').on('click', '.delete', ...);
adds a click listener to any node within the input_wrap div that has the class delete.
In general, jQuery calls might form chains. E.g. at Line 34 we have$(this).parent('div').remove();
In this line, the call $(this) selects the node which has been clicked. The call to parent()
and then remove() moves one step up the tree and if it ﬁnds a div element, removes the entire
subtree (which is of the form <div><input/><a></a></div>) from the document.
In addition to the action remove() which erases an entire subtree from the document, Figure
1 also contains other actions that potentially modify the shape of the HTML tree. The ﬁrst
such action is append(string1) (at Line 19), which simply appends string1 at the end of thestring inside the selected node tag. Of course, string1 might represent an HTML tree; in our
example, it is a tree with three nodes. So, in eﬀect append() adds this tree as the right-mostchild of the selected node. The second such action is html(string1) (e.g. at Line 25), whichﬁrst erases the string inside the selected node tag and then appends it with string1. In eﬀect,
this erases all the descendants of the selected node and adds a forest represented by string1.
Remark 1. An example where the CSS rule in Figure 1 becomes redundant is when the limiton the number of boxes is removed from the application (in eﬀect, removing x), but the CSS is
not updated to reﬂect the change (e.g. see [1]).
In general, CSS selectors are non-trivial. For example.a.b .c { color: red }matches all nodes with class c and some ancestor containing both classes a and b (the spaceindicates c appears on a descendant). Thus, detecting redundant CSS rules requires a goodknowledge of the kind of trees constructed by the application. In practice, redundant CSS rules
easily arise when one modiﬁes a suﬃciently complex HTML5 application (the size of the top
1000 websites has recently exceeded 1600K Bytes [9]). Some popular web pages are known tohave an average of 60% redundant CSS rules, as suggested by recent case studies [44].

3

A tree-rewriting approach

In this section, we present our tree-rewriting model. Our design philosophy is to put a special
emphasis on model simplicity and fully-algorithmic analysis with good complexity, while retaining adequate expressivity in modelling common tree updates in HTML5 applications (insofar
as detecting redundant CSS rules is concerned). We will start by giving an informal descriptionof our approach and then proceed to our formal model.
3 Unlike node IDs, a single class might be associated with multiple nodes

3.1

An informal description of the approach

Data representation The data model of HTML5 applications is the standard HTML (DOM)
tree. In designing our tree rewriting model, we will adopt a data representation consisting ofa ﬁnite set K of classes, and an unordered, unranked tree with the set 2K of node labels. An
unordered tree does not have a sibling ordering, and an unranked tree does not ﬁx the numberof children of its nodes. Since jQuery and CSS selectors may reason about adjacent node
siblings, unordered trees are in general only an overapproximation of HTML trees. As we shallsee later, the consequence of this approximation is that some CSS rules that we identify in our
analysis as non-redundant might turn out to be redundant when sibling ordering is accounted
for, though all CSS rules that we identify as redundant will definitely be redundant even withthe sibling ordering (see Remark 2 in Section 4). Although it is possible in theory to extend
our techniques to ordered unranked trees, we choose to use unordered trees in our model forthe purpose of simplicity. Not only do unordered trees give a clean data model, but they turnout to be suﬃcient for analysing redundancy of CSS rules in most HTML5 applications. In
the examples we studied, no false positives were reported as a consequence of the unorderedapproximation. The choice of tree labels is motivated by CSS and HTML5. Nodes in an HTML
document are tagged by HTML elements (e.g. div or a) and associated with a set of classes,
which can be added/removed by HTML5 scripts. Node IDs and data attributes are also often
assigned to speciﬁc nodes, but they tend to remain unmodiﬁed throughout the execution of theapplication and so can conveniently be treated as classes.
An “event-driven” abstraction Our tree-rewriting model is an “event-driven” abstractionof the script component of HTML5 applications. The abstraction consists of a (ﬁnite) set oftree-rewrite rules that can be ﬁred any time in any order (so long as they are enabled). In thisabstraction, one can imagine that each rewrite rule is associated with an external event listener(e.g. listening for a mouse click, hover, etc.). Since these external events cannot be controlled
by the system, it is standard to treat them (e.g. see [39]) as nondeterministic components,
i.e., that they can occur concurrently and in any order4 Incidentally, the case for event-driven
abstractions has been made in the context of transformations of XML data [10].
A tree-rewrite rule σ in our rewrite systems is a tuple (g, χ) consisting of a node selector g(a.k.a. guard ) and a rewrite operation χ.
To get a feel for our approach, we will construct an event-driven abstraction for the script
component of the HTML5 example in Figure 1. For simplicity, we will now use jQuery calls as
tree-rewrite rules. We will formalise them later.
The event-driven abstraction for the example in Figure 1 contains four rewrite rules asfollows:(1) $('#limit').addClass('warn');(2) $('.warn').removeClass('warn');(3) $('.input_wrap').append('<div><input/><a class="delete"></a></div>');(4) $('.input_wrap').find('.delete').
parent('div').remove();
4 Note, although, in our model, each rewrite rule is executed atomically, an event that leads to two or more tree

updates will be modelled by several rewrite rules. Our analysis will be a “path-insensitive” over-approximationin that no ordering or connection is maintained between these individual update rules. Thus, an event leading
to several tree updates is not assumed to be handled atomically. Indeed, the order of the updates is also not
maintained. In our experiments this over-approximation did not lead to false positives in the analysis.

Note that we removed irrelevant attributes (e.g. href) and text contents since they do notaﬀect our analysis of redundant CSS rules. Rules (1)–(3) were extracted directly from thescript. However, the extraction of Rule (4) is more involved. First, the calls to parent() andremove() come directly from the script. Second, the other calls — which select all elements withclass delete that are descendants of a node with class input_wrap — derive from the semantics
of on(). The connection of the two parts arrives because the jQuery selection is passed to theevent handler via the this variable. This connection may be inferred by a data-ﬂow analysis
that is sensitive to the behaviour of jQuery.
Detecting CSS Redundancy It can be shown that the set S1 of all reachable HTML trees
in the example in Figure 1 is a subset of the set S2 of all HTML trees that can be reached byapplying Rules (1)–(4) to the initial HTML document. We may detect whether.warn { color: red }is redundant by checking whether its selector may match some part of a tree in S2 . If not, thensince S1 ⊆ S2 we can conclude that the rule is definitely redundant. In contrast, if the rule canbe matched in S2 , we cannot conclude that the rule is redundant in the original application.
Let us test our abstraction. First, by applying Rule (1) to the initial HTML tree, we conﬁrm
that warn can appear in a tree in S2 and hence the CSS rule may be ﬁred. We now revisit the
scenario in Remark 1 in Section 2 where the limit on the number of boxes is removed, but
the CSS is not updated. In this case, the new event-driven abstraction for the modiﬁed script
will not contain Rule (1) and the CSS rule can be seen to be redundant in S2 . This necessarily
implies that the rule is definitely redundant in S1 .
Thus, we guarantee that redundancies will not be falsely identiﬁed, but may fail to identify
some redundancies in the original application.

3.2

Notations for trees

Before deﬁning our formal model, we brieﬂy ﬁx our notations for describing trees. In this paper
we use unordered, unranked trees. A tree domain is a nonempty ﬁnite subset D of N∗ (i.e. theset of all strings over the alphabet N = {0, 1, · · · }) satisfying preﬁx-closure, i.e., w · i ∈ D withi ∈ N implies w ∈ D.
A (labeled) tree over the nonempty ﬁnite set (a.k.a. alphabet) Σ is a tuple T = (D, λ) where
D is a tree domain and λ is a mapping (a.k.a. node labeling) from D to Σ. We use standard
terminologies for trees, e.g., parents, children, ancestors, descendants, and siblings. The levelof a node v ∈ D in T is |v|. Likewise, the height of the tree T is max{|v| : v ∈ D}. Let Tree(Σ)
denote the set of trees over Σ. For every k ∈ N, we deﬁne Treek (Σ) to be the set of trees ofheight k.
If T = (D, λ) and v ∈ D, the subtree of T rooted at v is the tree T|v = (D′ , λ′ ), where′D := {w ∈ N∗ : vw ∈ D} and λ′ (w) := λ(vw).
We remark, for example, that in our deﬁnitions, the trees T1 = ({ε, 1} , λ1 ) and T2 ({ε, 2} , λ2 )with λ1 (ε) = λ(ε) and λ1 (1) = λ(2) deﬁne distinct trees, although both trees contain a root
node with a single child with the same labels. It is easy to see that our guards discussed in
the following sections cannot distinguish trees up to isomorphism. In Section 4 we discussmorphisms between trees in the context of a monotonicity property.

3.3

The formal model

We now formally deﬁne our tree-rewriting model Trs for HTML5 tree updates. A rewrite
system R in Trs is a (ﬁnite) set of rewrite rules. Each rule σ is a tuple (g, χ) of a guard g anda (rewrite) operation χ. Let us deﬁne the notion of guards and rewrite operations in turn.
Our language for guards is simply modal logic with special types of modalities. It is a subset
of Tree Temporal Logic, which is a formal model of the query language XPath for XML data
[50, 40, 33]. More formally, a guard over the node labeling Σ = 2K with K = {c1 , · · · , cn } canbe deﬁned by the following grammar:
g ::= ⊤ | c | g ∧ g | g ∨ g | ¬g | hdig
where c ranges over K and d ranges over {↑, ↑+ , ↓, ↓+ }, standing for parent, ancestor, child,and descendant respectively. The guard g is said to be positive if there is no occurrence of ¬ in
g. Given a tree T = (D, λ) and a node v ∈ D, we deﬁne whether v matches a guard g (writtenv, T |= g) below. Intuitively, we interpret v, T |= c (for a class c ∈ K) as c ∈ λ(v), and each
modality hdi (where d ∈ {↑, ↑+ , ↓, ↓+}) in accordance with the arrow orientation (possibly witha transitive closure 5 ).
Given a tree T = (D, λ) and a node v ∈ D, we deﬁne whether v of T matches a guard g(written v, T |= g) by induction over the following rules:• v, T |= ⊤.
• v, T |= c if c ∈ λ(v).
• v, T |= g ∧ g ′ if v, T |= g and v, T |= g ′ .
• v, T |= g ∨ g ′ if v, T |= g or v, T |= g ′ .
• v, T |= ¬g if it is not the case that v, T |= g.
• v, T |= h↑ig if v = w.i (for some i ∈ N), and w, T |= g.
• v, T |= h↑+ ig if v = w.w′ (for some w′ ∈ N+ ), and w, T |= g.
• v, T |= h↓ig if there exists a node v.i ∈ D (for some i ∈ N) such that v.i, T |= g.
• v, T |= h↓+ ig if there exists a node v.w ∈ D (for some w ∈ N+ ) such that v.w, T |= g.
See the section below on encoding jQuery rules for some examples.
We say that g is matched in T if v, T |= g for some node v in T . Likewise, we say that g ismatched in a set S of Σ-trees if it is matched in some T ∈ S. In the sequel, we sometimes omit
mention of the tree T from v, T |= g whenever there is no possibility of confusion.
Having deﬁned the notion of guards, we now deﬁne our rewrite operations, which canbe one of the following: (1) AddChild(X), (2) AddClass(X), (3) RemoveClass(X), and (4)RemoveNode, where X ⊆ K. Intuitively, the semantics of Operations (2)–(4) coincides with thesemantics of the jQuery actions addClass(.), removeClass(.), and remove(), respectively.
Similarly, the semantics of AddChild(X) coincides with the semantics of the jQuery action
append(str) in the case when str represents a single node associated with classes X. By
5 If desired, we can include extra transitive-reflexive closure modalities h↓∗ i and h↑∗ i while retaining all upperand lower bound complexity. We can also define, e.g., h↓∗ ig as h↓ig ∨ h↓+ ig although this would cause an
exponential blow up in the size of the formulas.

adding extra classes, appending a larger subtree can be easily simulated by several steps of
AddChild(X) operations. This is demonstrated in the next section.
We now formally deﬁne the semantics of these rewrite operations. Given two trees T =(D, λ) and T ′ = (D′ , λ′ ), we say that T rewrites to T ′ via σ = (g, χ) (written T →σ T ′ ) if
there exists a node v ∈ D such that v |= g and• if χ = AddClass(X) then D′ = D and λ′ := λ[v 7→ X ∪ λ(v)]. 6• if χ = AddChild(X) then D′ = D ∪ {v.i} and λ′ := λ[v.i 7→ X] and v.i ∈/D• if χ = RemoveClass(X) then D′ = D and λ′ := λ[v 7→ λ(v) \ X]
• if χ = RemoveNode and v is not the root node, D′ := D \ {v.w : w ∈ N∗ } and λ′ is the
restriction of λ to D′ .
Note that the system cannot execute a RemoveNode operation on the root node of a tree.
I.e. there is no transition T →σ T ′ if σ would erase the root node of T .
Given a rewrite system R over Σ-trees, we deﬁne →R to be the union of →σ , for all σ ∈ R.
For every k ∈ N, we deﬁne →R,k to be the restriction of →R to Treek (Σ). Given a set Cof Σ-trees, we write post∗R (C) (resp. post∗R,k (C)) to be the set of trees T ′ satisfying T →∗R T ′(resp. T →∗R,k T ′ ) for some tree T ∈ C.
Encoding jQuery Rewrite Rules Let us translate the four “jQuery rewrite rules” forthe application in Figure 1 into our formalism. The ﬁrst rule translates directly to the rule(#limit, AddClass({.warn})), while the second rule translates to (.warn, RemoveClass({.warn})).
The fourth rule identiﬁes div nodes that have some child with class delete that in turn has
some ancestor with class input_wrap. Thus, it translates to(div ∧ h↓i(.delete ∧ h↑+ i.input_wrap), RemoveNode).
Finally, the third rule requires the construction of a new sub-tree. We achieve this throughseveral rules and a new class tmp. We ﬁrst add the new div element as a child node, and use
the class tmp to mark this new node:(.input_wrap, AddChild({div, tmp})) .
Then, we add the children of the div node with the two rules
and(tmp, AddChild({input}))(tmp, AddChild({a, .delete})) .

We show in the appendix. how to encode a large number of jQuery tree traversals into ourguard language. In general, some of these traversals have to be approximated. For example the.next() operation can be approximated by the modalities h↑ih↓i which select a sibling of thecurrent node.
6 Given a map f : A → B, a′ ∈ A and b′ ∈ B, we write f [a′ 7→ b′ ] to mean the map (f \{(a′ , f (a′ ))})∪{(a′ , b′ )}The redundancy problem The redundancy problem for Trs is the problem that, given a
rewrite system R over Σ-trees, a ﬁnite nonempty set S of guards over Σ, and an initial Σlabeled tree T0 , compute the subset S ′ ⊆ S of guards that are not matched in post∗R (T0 ). The
decision version of the redundancy problem for Trs is simply to check if the aforementioned set
S ′ is empty. Similarly, for each k ∈ N, we deﬁne the k-redundancy problem for Trs to be therestriction of the redundancy problem for Trs to trees of height k (i.e. we use post∗R,k insteadof post∗R ).
The problem of identifying redundant CSS node selectors in a CSS ﬁle can be reduced tothe problem of the redundancy problem for Trs. This is because CSS node selectors can easily
be translated into our guard language (e.g. using the translation given in [20]). Observe thatthe converse is false. E.g., h↓ia ∧ h↓ib cannot be expressed as a CSS selector since a and b
may appear on diﬀerent children of the matched node. The guard in the fourth rule of ourrunning example is also not expressible as a CSS selector. However, this increased expressivity
is required to model tree traversals in jQuery. Note that the redundancy problem for Trs
could also have potential applications beyond detecting redundant CSS rules, e.g., detecting
redundant jQuery calls in HTML5, which could .
Despite the simplicity of our rewrite rules, it turns out that the redundancy problem is in
general undecidable (even restricted to trees of height at most two); see the appendix.
Proposition 1. The 1-redundancy problem for R is undecidable.

4

A monotonic abstraction

The undecidability proof of Proposition 1 in fact relies fundamentally on the power of negationin the guards. A natural question, therefore, is what happens in the case of positive guards. Not
only is this an interesting theoretical question, such a restriction often suﬃces in practice. Thisis partly because the use of negations in CSS and jQuery selectors (i.e. :not(...)) is rather
limited in practice. In particular, there was no use of negations in CSS selectors found in thebenchmark in [44] containing 15 live web applications. In practice, negations are almost always
limited to negating atomic formulas, i.e., ¬c (for a class c ∈ K) which can be overapproximatedby ⊤ often without losing too much precision.
W
Note, in general it is not possible to express ¬c via the formula c′ ∈K\{c} c′ since nodes may
be labelled by multiple classes. That is, labelling a node by c′ does not prevent the node also
being labelled by c. However, when c is an HTML tag name (e.g. div or img), we can assert ¬cby checking whether the node is labelled by some other tag name, since a node can only have
one tag (e.g. a node cannot be both a div and an img).
A main result of the paper is that the “monotonic” abstraction that is obtained by restricting
to positive guards gives us decidability with a good complexity. In this section, we prove theresulting tree rewriting class is “monotonic” in a technical sense of the word, and summarise
the main technical results of the paper.
Notation. Let us denote by Trs0 the set of rewrite systems with positive guards. The guard
databases in the input to redundancy and k-redudancy problems for Trs0 will only containpositive guards as well. In the sequel, unless otherwise stated, a “guard” is understood to mean
a positive guard.

4.1

Formalising and proving “monotonicity”

Recall that a binary relation R ⊆ S × S is a preorder if it is transitive, i.e., if (x, y) ∈ R and(y, z) ∈ R, then (x, z) ∈ R. We start with a deﬁnition of a preorder  over Tree(Σ), whereΣ = 2K . Given two Σ-trees T = (D, λ) and T ′ = (D′ , λ′ ), we write T  T ′ if there exists anembedding from T ′ to T , i.e., a function f : D → D′ such that:(H1) f (ǫ) = ǫ(H2) For each v ∈ D, λ(v) ⊆ λ′ (f (v))(H3) For each v.a ∈ D where v ∈ N∗ and a ∈ N, we have f (v.a) = f (v).b for some b ∈ N.
Note that this is equivalent to the standard notion of homomorphisms from database theory(e.g. see [5]) when each class c ∈ K is treated as a unary relation. The following is a basic
property of , whose proof is easy and is left to the reader.
Fact.  is a preorder on Tree(Σ).
The following lemma shows that embeddings preserve positive guards.
Lemma 1. Given trees T = (D, λ) and T ′ = (D′ , λ′ ) ∈ Tree(Σ) satisfying T  T ′ witha witnessing embedding f : D → D′ , and a positive guard g over Σ, then if v, T |= g thenf (v), T ′ |= g.
We relegate to the appendix the proof of Lemma 1, which is similar to (part of) the proof ofthe homomorphism theorem for conjunctive queries (e.g. see [5, Theorem 6.2.3]). This lemmayields the following monotonicity property of Trs0 .
Lemma 2 (Monotonicity). For each σ ∈ R, if T1  T2 and T1 →σ T1′ , then either T1′  T2 or
T2 →σ T2′ for some T2′ satisfying T1′  T2′ .
Intuitively, the property states that any rewriting step of the “smaller” tree either does not
expand the tree beyond the “bigger tree”, or, the step can be simulated by the “bigger” tree
while still preserving the embedding relation. The proof of the lemma is easy (by considering
all four possible rewrite operations), and is relegated to the appendix.
One consequence of this monotonicity property is that, when dealing with the redundancy
problem, we can safely ignore rewrite rules that use one of the rewrite operations RemoveNodeor RemoveClass(X). This is formalised in the following lemma, whose proof is given in the
appendix.
Lemma 3. Given a rewrite system R over Σ-trees, a guard database S, and an initial tree T0 ,let R− be the set of R-rules less those that use either RemoveNode or RemoveClass(X). Then,for each g ∈ S, g is matched in post∗R (T0 ) iff g is matched in post∗R− (T0 ).
Convention. In the sequel, we assume that there are only two possible rewrite operations,
namely, AddChild(X), and AddClass(X).
Remark 2. When choosing unordered trees for our CSS redundancy analysis in Section 3 (i.e.
instead of ordered trees), we remarked that we have added a layer of sound approximation to
our analysis. We will now explain why this is a sound approximation. We could consider theextension of our guard language with the left-sibling and right-sibling operators h←i and h→i(which would still be contained in Tree Temporal Logic, which as we already mentioned is aformal model of XPath [50, 40, 33]). The semantics of formulas of the form h←ig and h→ig

(with respect ordered trees) can be deﬁned in the same way as our guard language. Given anordered tree T , let T ′ be the unordered version of T obtained by ignoring the sibling orderingfrom T . Given a formula g with left/right sibling operators, we could deﬁne its “unorderedapproximation” g ′ by replacing every occurrence of h←i and h→i by h↑ih↓i. For positive guards
g, it is easy to show by induction on g that v, T |= g implies v, T ′ |= g ′ . By the same token,
we could also consider an extension of our tree rewriting to ordered trees that allows adding
an immediate left/right sibling, e.g., by the operators AddLeftKin(X) and AddRightKin(X)(these are akin to the .before() and .after() jQuery methods). Given a tree rewriting R
in this extended rewrite system, we could construct an approximated rewriting R′ in Trs0
as follows: (1) for every rewrite rule of the form (g, AddLeftKin(X)) or (g, AddRightKin(X))
in this extended tree rewriting, add the rewrite rule (h↓ig ′ , AddChild(X)) in R′ , and (2) for
every other rewrite rule (g, χ) in R, add the rewrite rule (g ′ , χ) in R. A consequence of thisapproximation is that a guard g can be matched in a reachable tree post∗R (T0 ) implies that theunordered approximation g ′ can be matched in a reachable tree post∗R′ (T0′ ). That is, if g ′ isredundant in R′ , then g is redundant in R, i.e., that g can be safely removed.

4.2

Summary of technical results

We have completely identiﬁed the computational complexity of the redundancy and k-redundancy
problem for Trs0 . Our ﬁrst result is:
Theorem 3. The redundancy problem for Trs0 is EXP-complete.
Our upper bound was obtained via an eﬃcient reduction to an analysis of symbolic pushdown
systems (see Section 5), for which there are highly optimised tools (e.g. Bebop [11], Getaﬁx[31], and Moped [46]). We have implemented our reduction and demonstrate its viability indetecting redundant CSS rules in HTML5 applications (see Section 6). The proof of the lower
bound in Theorem 3 is provided in the appendix. In the case of k-redundancy problem, a better
complexity can be obtained.
Theorem 4. The k-redundancy problem Trs0 is:(i) PSPACE-complete if k is part of the input in unary.
(ii) solvable in P-time — nO(k) — for each fixed parameter k, but is W[1]-hard.
Recall that PSPACE ⊆ EXP. The second item of Theorem 4 contains the complexity class
W[1] from parameterised complexity theory (e.g. see [17]), which provides a theory for answering
whether a computational problem with multiple input parameters is efficiently solvable whencertain parameters are fixed. In the case of the k-redundancy problem for Trs0 a problem
instance contains k ∈ N and R ∈ Trs0 as the input parameters. The problem can be solvedin time nO(k) , where n is the size of R. We would like to know whether the parameter k canbe removed from the exponent of n in the time-complexity. That is, whether the problem issolvable in time f (k)nc for some computable function f : N → N and a constant c ∈ N (a.k.a.
fixed-parameter-tractable (FPT) algorithms). Observe that, asymptotically, f (k)nc is smaller
than nO(k) for every ﬁxed value of k. By showing that the problem is W[1]-hard, we havein eﬀect shown that the parameter k cannot be removed from the exponent of n, i.e., that
our nO(k) -time algorithm is, in a sense, optimal. For space reasons, we relegate the proofs ofTheorem 4 to the appendix.

Remark 5. Decidability for the k-redundancy problem for Trs0 is immediate from the theoryof well-structured transition systems (e.g. see [3, 16]). We have shown in Lemma 2 that thetree embedding relation  is monotonic. It can be shown that  is also well-founded on trees ofheight k (e.g. see [18]), i.e., there is no inﬁnite descending chain T1 ≻ T2 ≻ · · · for trees T1 , . . .
of height k. The theory of well-structured transition systems (e.g. see [3, 16]) would imply
decidability for the k-redundancy problem. Unfortunately, this only gives a nonelementary
upper bound complexity (i.e. an unbounded tower of exponential) for the k-redundancy anddoes yield decidability for the general redundancy problem.

5

The algorithm

In this section, we provide an eﬃcient reduction to an analysis of symbolic pushdown systems,
which will give an algorithm with an exponential-time (resp. polynomial-space) worst-case
upper bound for the redundancy (resp. k-redundancy) problem for Trs0 . To this end, we
ﬁrst provide a preliminary background on symbolic pushdown systems. We will then provide
a roadmap of our reduction to symbolic pushdown systems, which will consist of a sequence of
three polynomial-time reductions described in the last three subsections.

5.1

Pushdown systems: a preliminary

Before describing our reduction, we will ﬁrst provide a preliminary background on pushdown
systems and their extensions to symbolic pushdown systems.
Pushdown systems are standard (nondeterministic) pushdown automata without input labels. Input labels are irrelevant since one mostly asks about their transition graphs (in ourcase, reachability). More formally, a pushdown system (PDS) is a tuple
P = (Q, Γ, ∆)where• Q is a ﬁnite set of control states,• Γ is a ﬁnite set of stack symbols, and• ∆ is a ﬁnite subset of (Q × Γ) × (Q × Γ∗ ) such that if ((q, a), (q ′ , w)) ∈ ∆ then |w| ≤ 2.
This PDS generates a transition relation →P ⊆ (Q × Γ∗ ) × (Q × Γ∗ ) as follows: (q, v) →P (q ′ , v ′ )if there exists a rule ((q, a), (q ′ , w)) ∈ ∆ such that v = ua and v ′ = uw for some word u ∈ Γ∗ .
Symbolic pushdown systems are pushdown systems that are succinctly represented by boolean
formulas. They are equivalent to (recursive) boolean programs. More precisely, a symbolic pushdown system (sPDS) is a tuple(V, W, ∆)where• V = {x1 , . . . , xn } and W = {y1 , . . . , ym } are two disjoint sets of boolean variables, and• ∆ is a ﬁnite set of pairs (i, ϕ) of number i ∈ {0, 1, 2} and boolean formula ϕ over the setof variables V ∪ W ∪ V ′ ∪ W ′ , where– V ′ := {x′1 , . . . , x′n }, and– W ′ :=Sijj
j=1 Wj with Wj := {y1 , . . . , ym }.

This sPDS generates a (exponentially bigger) pushdown system P = (Q, Γ, ∆′ ), where Q ={0, 1}n, Γ = {0, 1}m, and ((q, a), (q ′ , w)) ∈ ∆′ iﬀ there exists a pair (i, ϕ) ∈ ∆ satisfying
i = |w|, and ϕ is satisﬁed by the assignment that assigns7 q to V, a to W, q ′ to V ′ , and w toW ′ (i.e. assigning the jth letter of w to Wj ).
The bit-toggling problem for sPDS is a simple reachability problem over symbolic pushdown
systems. Intuitively, we want to decide if we can toggle on the variable yi from the initial
conﬁguration. More precisely, given an sPDS P = (V, W, ∆) with V = {x1 , . . . , xn } and W ={y1 , . . . , ym }, a variable yi ∈ W, and an initial conﬁguration I0 = ((b1 , . . . , bn ), (b′1 , . . . , b′m )) ∈{0, 1}n × {0, 1}m, decide if I0 →∗P (q, a) for some q ∈ {0, 1}n and a = (b′′1 , . . . , b′′m ) ∈ {0, 1}mwith b′′i = 1.
The bounded bit-toggling problem is the same as the bit-toggling problem but the stack heightof the pushdown system cannot exceed some given input parameter h ∈ N (given in unary).
Proposition 2. The bit-toggling (resp. bounded bit-toggling) problem for sPDS is solvable in
EXP (resp. PSPACE).
The proof of this is standard (e.g. see [51]), which for completeness we provide in the
appendix.
Despite the relatively high complexity mentioned in Proposition 2, nowadays there arehighly optimised sPDS and boolean program solvers (e.g. Moped [51, 46], Getaﬁx [31], andBebop [11]) that can solve sPDS bit-toggling problem eﬃciently using BDD (Binary Decision
Diagram) representation of boolean formulas. In fact, the boolean formulas that we produce inour polynomial-time reductions below have straightforward small representations as BDDs.

5.2

Intuition/Roadmap of the reduction

The following theorem formalises our reduction claim.
Theorem 6. The redundancy (resp. k-redundancy) problem for Trs0 is polynomial-time reducible to the bit-toggling (resp. bounded bit-toggling) problem for sPDS.
Together with Proposition 2, Theorem 6 implies an EXP (resp. PSPACE) upper boundfor the redundancy (resp. k-redundancy) problem for sPDS. Moreover, as discussed in the
appendix, it is straightforward to construct from our reduction a counterexample path in therewrite system witnessing the non-redundancy of a given guard.
The actual reduction in Theorem 6 involves several intermediate polynomial-time reductions.
Here is a roadmap.
• We ﬁrst show that it suﬃces to consider “simple” rewrite systems. These systems are
simple in the sense that guards only test direct parents or children of the nodes. Furthermore, these systems have the property that we only need to check redundancy at the root
node. This is given in Section 5.3.
• We then show that the simpliﬁed problem can be solved by a “saturation” algorithm thatuses a subroutine to check whether a given class can be added to a given node via asequence of rewrite rules. This subroutine solves what we call the “class-adding problem”:
a simple reachability problem that checks whether a class can be added to a given node
via a series of rewrite rules that do not change any other existing nodes in the tree (but
7 Meaning that if q = (q1 , . . . , qn ), then qi is assigned to xi

root

team

P1

P2

team

team

success

P1

Figure 2: A reachable conﬁguration
may add new nodes). That is, the node is considered as the only node in a single nodetree, possibly with some contextual (immutable) information about its parent. This isgiven in Section 5.4.
• Finally, we show that the class-adding problem is eﬃciently reducible to the bit-toggling
problem for sPDS. This is given in Section 5.5.
The case of k-redundancy for Trs0 is similar but each intermediate problem is relativised to
the version with bounded height.
The reason we need to simplify the system is because, in the simpliﬁed system, we can test
redundancy only by inspection of the root node, and all guards only refer to direct neighboursof each node. The latter simpliﬁcation makes the reduction to sPDS possible. As explainedin Section 5.5, the constructed sPDS performs a kind of depth-ﬁrst search over the constructed
trees. Since an sPDS can only see the top of its stack, it is important that it only needs
to maintain local information about the node being inspected by the depth-ﬁrst search. The
former simpliﬁcation justiﬁes us only maintaining labelling information about the nodes in theoriginal tree (in particular, the root node) without having to (explicitly) add new nodes.
Running Example. We provide a running example for our sequence of reductions. Imagine atennis double tournament web page which can be used to keep track of a list of teams (containing
exactly two players). The page allows a user to create a team, and add players to a team. The
page will also indicate a success next to the team details after both players have been added.
An overapproximation of the behavior of the page could be abstracted as a rewrite system R
as follows:• The initial tree is the single-node tree with label root.
• The set of node labels is {root, team, P1, P2, success}.
• A team can be added to the tournament, i.e., there is a rule (root, AddChild(team)) ∈ R.
• Player 1 can be added to a team, i.e., there is a rule (team, AddChild(P1)) ∈ R• Player 2 can be added to a team, i.e., there is a rule (team, AddChild(P2)) ∈ R• Success after both of the required players Player 1 & Player 2 are added, i.e., there is arule (h↓iP1 ∧ h↓iP2, AddChild(success)) ∈ R

The set S of guards that we want to check for redundancy is {success}. A snapshot of areachable conﬁguration is provided in Figure 2.

5.3

Simplifying the rewrite system

We will make the following two simpliﬁcations: (1) restricting the problem to only checking
redundancy at the root node, (2) restrict the guards to be used.
To achieve simpliﬁcation (1), one can simply deﬁne a new set of guards from S as {g ∨ h↓+ig : g ∈ S}. Then, for each tree T = (D, λ) ∈ Tree(Σ) and guard g, it is the case that(∃v ∈ D : v, T |= g) iﬀ ǫ, T |= g ∨ h↓+ ig.
We now proceed to simpliﬁcation (2). A guard over the node labeling Σ = 2K is said to be
simple if it is of one of the following two forms
m
^

ci

or

hdi

i=1

m
^

ci

i=1

for some m ∈ N, where each ci ranges over K and d ranges over {↑, ↓}. [Note: if m = 0, thenVm
For notational
convenience, if X = {c1 , . . . , cm }, we shall write X (resp. hdiX)
i=1 ci ≡V⊤.]Vmm
to mean i=1 cm (resp. hdi i=1 cm ). A rewrite system R ∈ Trs0 is said to be simple if (i) all
guards occurring in R are simple, and (ii) if (hdiX, χ) ∈ R, then χ is of the form AddClass(Y ).
We deﬁne Trs′0 ⊆ Trs0 to be the set of simple rewrite systems. The redundancy (resp.
k-redundancy) problem for Trs′0 is deﬁned in the same way as for Trs0 except that all theguards in the set of guards are restricted to be a subset of K.
The following lemma shows that the redundancy (resp. k-redundancy) problem for Trs0
can be reduced in polynomial time to the redundancy (resp. k-redundancy) problem for Trs′0 .
Essentially, the reduction works by introducing new classes representing (non-simple) subformulas of the guards. New rewrite rules are introduced that inductively calculate which subformulas
are true. That is, if a subformula g is true at v, then the labelling of v will include a classrepresenting g.
Note, in the lemma below, S ′ is a set of atomic guards. That is, each guard in S ′ is of theform c for some c ∈ K′ .
Lemma 4. Given a R ∈ Trs0 over Σ = 2K and a set S of guards over Σ, there exists′
R′ ∈ Trs′0 over Σ′ = 2K (where K ⊆ K′ ) and a set S ′ of atomic guards such that:(P1) For each k ∈ N, S is k-redundant for R iff S ′ is k-redundant for R′ .
(P2) S is redundant for R iff S ′ is redundant for R′ .
Moreover, we can compute R′ and S ′ in polynomial time.
We show how to compute R′ . The set K′ is deﬁned as the union of K with the set G of
all non-atomic subformulas (i.e. occurring in the parse tree) of guard formulas in S and R. In
the sequel, to avoid potential confusion, we will often underline members of G in K′ , e.g., writeh↓ic instead of h↓ic. Note that c = c for all c ∈ K.
We now deﬁne the simple rewrite system R′ . Initially, we will deﬁne a rewrite system R1that allows the operators h↑+ i and h↓+ i; later we will show how to remove them. We ﬁrst add
the following “intermediate” rules to R1 :1. ({g, g ′ }, AddClass(g ∧ g ′ )), for each (g ∧ g ′ ) ∈ G.

2. (g, AddClass(g ∨ g ′ )) and (g ′ , AddClass(g ∨ g ′ )), for each (g ∨ g ′ ) ∈ G.
3. (hdig, AddClass(hdig)), for each hdig ∈ G.
4. (g, χ), for each (g, χ) ∈ R.
′

Note that in Rule (3) the guard hdig is understood to mean a non-atomic guard over 2K – thatis, g is an atomic guard. Finally, we deﬁne S ′ := {g : g ∈ S}. Notice that each guard in S ′ isatomic. The aforementioned algorithm computes R1 and S ′ in linear time.
We now show how to remove the operators h↑+ i and h↓+ i (i.e. rules of type (3)). To dothis we will introduce new rules R2 that essentially compute the required transitive closuresusing the ↑ and ↓ operators. Our ﬁnal rewrite system R′ will be R1 ∪ R2 . We deﬁne R2 to be
the set containing the following rules for each rule (hd+ ig, χ) ∈ R1 where d ∈ {↑, ↓}:(a) (hdig, AddClass(hd+ ig)).
(b) (hdihd+ ig, AddClass(hd+ ig)).
Note that from Rule (4) R1 contains the rule (hd+ ig, χ), where hd+ ig is understood to mean′an atomic guard over 2K . Intuitively, this simpliﬁcation can be done because v, T |= hd+ ig iﬀ
at least one of the following cases holds: (i) v, T |= hdig, (ii) there exists a node w in T suchthat w, T |= hd+ ig and w can be reached from v by following the direction d for one step. The
aforementioned computation step again can be done in linear time. The proof of correctness(i.e. (P1) and (P2)) is provided in the appendix. In particular, for all g ∈ S, it is the casethat g is redundant in R iﬀ g is redundant in R′ .
Running Example. In our example, initially, S is changed into {success ∨ h↓+ isuccess}after the ﬁrst simpliﬁcation. To perform the second, we ﬁrst obtain the rewrite system R1
containing the following rules (recall we equate c and c for each class):• (success, AddClass(success ∨ h↓+ isuccess))• (h↓+ isuccess, AddClass(success ∨ h↓+ isuccess))• ({h↓iP1, h↓iP2}, AddClass(h↓iP1 ∧ h↓iP2))• (h↓iP , AddClass(h↓iP )) for each P ∈ {P1, P2}
and from Rule (4) we also have in R1 .
• (root, AddChild(team)),• (team, AddChild(P1)),• (team, AddChild(P2)),• (h↓iP1 ∧ h↓iP2, AddChild(success)).
Now, R2 contains the following rules:• (h↓isuccess, AddClass(h↓+ isuccess))• (h↓ih↓+ isuccess, AddClass(h↓+ isuccess))noFinally, we deﬁne S ′ to be success ∨ h↓+ isuccess .

5.4

Redundancy → class-adding

We will show that redundancy for Trs′0 can be solved in polynomial time assuming an oracle
to the “class adding problem” for Trs′0 . The class-adding problem is a reachability problem for
Trs′0 involving only single-node input trees possibly with a parent node that only provides a“context” (i.e. cannot be modiﬁed). As we will see in the following subsection, the class-adding
problem for Trs′0 lends itself to a fast reduction to the bit-toggling problem for sPDS. Similarly,
k-redundancy can be solved via the same routine, where intermediate problems are restricted
to their bounded height equivalents.
High-level idea. We ﬁrst provide the high-level idea the reduction. After simplifying therewrite system in the previous step, we only need to check redundancy at the root node of
the tree. Our approach is a “saturation” algorithm that exploits the monotonicity property:
we begin with an initial tree and then repeatedly apply a “saturation step” to build the tree
where each node is labelled by all classes that may label the node during any execution. The
saturation step examines the tree built so far and the rules of the rewrite system. If it ﬁnds
that it is possible to apply a sequence of rewrite rules to the tree to add a class c to some nodev, it updates the tree by adding c to the label of v. In this way, larger and larger trees arebuilt. Once it is no longer possible to add any new classes to the existing nodes of the tree,
the algorithm terminates. In particular, we have all classes that could label the root node, andthus we can detect which classes are redundant by inspecting the labelling of the root.
Given a rewrite system R ∈ Trs0 , an initial tree T = (D, λ) ∈ Tree(Σ) with Σ = 2K , anda set S of guards, we try to “saturate” each node v ∈ D with the classes that may be added
to v. Our saturation step is able to reason about the addition of nodes when determining if aclass c can be added to v, but does not need to remember which new nodes needed to be added
to T to add c to v. This is due to monotonicity: since each saturation step begins with a larger
tree than the previous step, additional nodes can be regenerated on-the-ﬂy if needed.
Each saturation step proceeds as follows. Let T1 = (D, λ1 ) be the tree before the saturation
step, and T2 = (D, λ2 ) be the tree after applying then saturation step. The tree domain does
not change and there exists a node v ∈ D such that λ1 (v) ⊂ λ2 (v) (i.e. some classes are added
to λ1 (v)). In particular, we have T1 ≺ T2 .
There are two saturation rules that are repeatedly applied until we reach a ﬁxpoint.
• The ﬁrst saturation rule corresponds to the application of a rewrite rule (g, AddClass(X)) ∈R at v. We simply set λ2 (v) = λ1 (v) ∪ X. Note, in this case we do not need to reason
about the addition of nodes to the tree.
• The second saturation rule is a call to the class-adding subroutine and asks whether someclass c can be added to node v. This step incorporates the behaviour of rewrite rules ofthe form (g, AddChild(X)). In this case we need to reason about whether the node addedby these rules could lead to the addition of c to v. To do this, we construct a pushdown
system P that explores the possible impact of these new nodes. This is discussed in thenext section. If it is found that c could be added to v, we set λ2 (v) = λ1 (v) ∪ {c}.
In sum, our “reduction” is in fact an algorithm for the (k-) redundancy problem for Trs0 thatruns in polynomial-time with an oracle to the bit-toggling (resp. for bounded stack height) forsPDS.
The formal reduction. Before formally deﬁning the class-adding problem, we ﬁrst need thedeﬁnition of an “assumption function”, which plays the role of the possible parent context nodebut is treated as a separate entity from the input tree. As we shall see, this leads to a morenatural formulation of the computational problem. More precisely, an assumption function
f over the alphabet Σ = 2K is a function mapping each element of {root} ∪ K to {0, 1}.
The boolean value of f (root) is used to indicate whether the input single-node tree is a root
node8 .
Given a tree T = (D, λ) ∈ Tree(Σ), a node v ∈ D, and a simple guard g overΣ, we write v, T |=f g if one of the following three cases holds: (i) v 6= ǫ and v, T |= g, (ii)v = ǫ, g is not of the form h↑iX, and v, T |= g, and (iii) v = ǫ, g = h↑iX, f (root) = 0, andX ⊆ {c ∈ K : f (c) = 1}. In other words, v, T |=f g checks whether g is satisﬁed at node v
assuming the assumption function f (in particular, if f (root) = 0, then any guard referring to
the parent of the root node of T is checked against f ).
Given a simple rewrite system R ∈ Trs′0 over Σ and an assumption function f , we may
deﬁne the rewriting relation →R,f ⊆ Tree(Σ) × Tree(Σ) in the same way as we deﬁne →R ,except that |=f is used to check guard satisfaction. The class-adding (reachability) problem
is deﬁned as follows: given a single-node tree T0 = ({ǫ}, λ0 ) ∈ Tree(Σ) with Σ = 2K , anassumption function f : ({root} ∪ K) → {0, 1}, a class c ∈ K, and a simple rewrite system
R, decide if there exists a tree T = (D, λ) such that T0 →∗R,f T and c ∈ λ(ǫ). Similarly, thek-class-adding problem is deﬁned in the same way as the class-adding problem except that thereachable trees are restricted to height k (k is part of the input).
Lemma 5. The redundancy (resp. k-redundancy) problem for simple rewrite systems is P-timesolvable assuming oracle calls to the class-adding (resp. k-class-adding) problem.
Given a tree is T0 = (D0 , λ0 ) ∈ Tree(Σ) with Σ = 2K , a simple rewrite system R overΣ, and a set S ⊆ K, the task is to decide whether S is redundant (or k-redundant). We shallgive the algorithm for the redundancy problem; the k-redundancy problem can be obtained bysimply replacing oracle calls to the class-adding problem by the k-class-adding problem.
The algorithm is a ﬁxpoint computation. Let T = (D, λ):= T0 . At each step, we can apply any of the following “saturation rules”:• if (g, AddClass(B)) is applicable at a node v ∈ D0 in T , then λ(v) := λ(v) ∪ B.
• If the class-adding problem has a positive answer on input hTv , f, c, Ri, then λ(v) :=λ(v) ∪ {c}, where v ∈ D, c ∈ K \ λ(v), and Tv := (ǫ, λv ) with λv (ǫ) = λ(v), where wedeﬁne f : ({root} ∪ K) → {0, 1} with f (root) = 1 ⇔ v = ǫ and, if f (root) = 0 and u isthe parent of v, then f (a) = 1 ⇔ a ∈ λ(u).
Observe that saturation rules can be applied at most K × |D| times. Therefore, when they
can be applied no further, we check whether S ∩ λ(ǫ) 6= ∅ and terminate. Assuming constanttime oracle calls to the class-adding problem, the algorithm easily runs in polynomial time.
Furthermore, since each saturation rule only adds new classes to a node label, the correctnessof the algorithm can be easily proven using Lemma 1 and Lemma 2; see the appendix.
Running Example The application of the saturation algorithm to our running example isquite simple. Since the only node in the initial tree is the root node, we can solve the redundancy
problem with a single call to the class-adding problem. That is, is it possible to add the classsuccess ∨ h↓+ isuccess to the root node?
8 Note that the guard h↑i⊤ evaluates to false on the root node

5.5Class-adding → bit-toggling

We now show how to solve the class-adding problem for a given node v and class c. Let λ(v)be the labelling of node v. We reduce the class-adding problem to the bit-toggling problem asfollows. The pushdown system performs a kind of “depth-ﬁrst search” of the trees that could
be built from the new node and the rewrite rules. It starts with an initial stack of height 1
containing the node being inspected. More precisely, the single item on this stack is the set
λ(v) (possibly with some extra “context” information). It then “simulates” each possible branchthat is spawned from v by pushing items onto the stack when a new node is created (i.e. at
each given moment, the stack contains a single branch in a reachable conﬁguration). It pops
these nodes from the stack when it wishes to backtrack and search other potential branches of
the tree.
The pushdown system is an sPDS that keeps one boolean variable for each class c ∈ K.
If P reaches a single item stack (i.e. corresponding to the node v) where the item contains cthen the answer to the class adding problem is positive. That is, the sPDS has explored theapplication of the rewrite rules to the possible children of v and determined that the label of v
can be expanded to include c.
The reason why it suﬃces to only keep track of the labelling of v (instead of the entire
subtree rooted at v that P explored) is monotonicity of Trs0 (cf. Lemma 2), i.e., that thelabelling of v contains suﬃcient information to “regrow” the destroyed subtree.
Lemma 6. The class-adding (resp. k-class-adding) problem for Trs′0 is polynomial-time reducible to the bit-toggling (resp. bounded bit-toggling) problem for sPDS.
We prove the lemma above. Fix a simple rewrite system R over the node labeling Σ = 2K ,an assumption function f : ({root} ∪ K) → {0, 1}, a single node tree T0 = ({ǫ}, λ0 ) ∈ Tree(Σ),
and a class α ∈ K.
We construct an sPDS P = (V, W, ∆). Intuitively, the sPDS P will simulate R by exploring
all branches in all trees reachable from T0 while accumulating the classes that are satisﬁed
at the root node. Deﬁne V := {xc : c ∈ K} ∪ {pop}, and W := {yc , zc : c ∈ K} ∪ {root}.
Roughly speaking, we will use the variable yc (resp. zc ) to remember whether the class c issatisﬁed at the current (resp. parent of the current) node being explored. The variable xc isneeded to remember whether the class c is satisﬁed at a child of the current node (i.e. after a
pop operation). The variable root signiﬁes whether the current node is a root node, while thevariable pop indicates whether the last operation that changed the stack height is a pop. We
next deﬁne ∆:• For each (A, AddClass(B)) ∈ R, add the rule (1, ϕ), where ϕ asserts
V(a) a∈A ya (A satisﬁed), andV(b) b∈B yb1 (B set to true), and(c) V
all other variables V
remain unchanged, thatpop ↔ pop′ , root ↔ root1 ,V is we assert′
11c∈K (xc ↔ xc ).
c∈K (zc ↔ zc ), andc∈K\B (yc ↔ yc ),• For each (h↑iA, AddClass(B)) ∈ R, add the rule (1, ϕ) where ϕ asserts
V(a) a∈A za (A satisﬁed in the parent), andV(b) b∈B yb1 (B set to true), and(c) all otherunchanged, that is pop ↔ pop′ , root ↔ root1 ,V variables1remain V′
xc ), c∈K (zc ↔ zc ), and c∈K\B (yc ↔ yc1 ).

V

c∈K (xc ↔

• For each (h↓iA, AddClass(B)) ∈ R, add the rule (1, ϕ) where ϕ asserts(a) pop (we popped from a child), andV(b) a∈A xa (A satisﬁed in child), andV(c) b∈B yb1 (B set to true), and(d) all otherunchanged, that is pop ↔ pop′ , root ↔ root1 ,V variables1remainV′xc ), c∈K (zc ↔ zc ), and c∈K\B (yc ↔ yc1 ).

V

c∈K (xc ↔

• For each (A, AddChild(B)) ∈ R, add the rule (2, ϕ), where ϕ asserts
V(a) a∈A ya (A satisﬁed), andV(b) b∈B yb2 (B true in new child), andV(c) c∈K\B ¬yc2 (new child has no other classes), andV(d) c∈K (yc ↔ zc2 ) (new child’s parent classes), and(e) ¬root2 (new child is not root), andV(f) ¬pop′ ∧ c∈K ¬x′c (new child does not have a child), andVV(g) the current node is unchanged, that is c∈K (yc ↔ yc1 ), c∈K (zc ↔ zc1 ), and (root ↔
root′ )• Finally, add the rule (0, ϕ), where ϕ asserts(a) ¬root (can return to parent), and(b) pop′ (ﬂag the return), andV(c) c∈K (yc ↔ x′c ) (return classes to parent).
These boolean formulas can easily be represented as BDDs of linear size (see appendix).
Continuing with our translation, the bit that needs to be toggled on is yα . We now construct
the initial conﬁguration for our bit-toggling problem. For each subset X ⊆ K and a function
q : V → {0, 1}, deﬁne the function IX,f,q : (V ∪W) → {0, 1} as follows: IX,f,q (root) := f (root),
IX,f,q (pop) := q(pop), and for each c ∈ K: (i) IX,f,q (xc ) := q(xc ), (ii) IX,f,q (yc ) = 1 iﬀ c ∈ X,
and (iii) IX,f,q (zc ) := f (c). We shall write IX,f to mean IX,f,q with q(x) = 0 for each x ∈ V.
Deﬁne the initial conﬁguration I0 as the function Iλ0 (ǫ),f .
Let us now analyse our translation. The translation is easily seen to run in polynomial time.
In fact, with a more careful analysis, one can show that the output sPDS is of linear size andthat the translation can be implemented in polynomial time. Correctness of our translation
immediately follows from the following technical lemma:
Lemma 7. For each subset X ⊆ K, the following are equivalent:(A1) There exists a tree T = (D, λ) ∈ Tree(Σ) such that T0 →∗R,f T and λ(ǫ) = X.
(A2) There exists q ′ : V → {0, 1} such that Iλ0 (ǫ),f →∗P IX,f,q′ .
This lemma intuitively states that the constructed sPDS performs a “faithful simulation”
of R. Moreover, the direction (A2)⇒(A1) gives soundness of our reduction, while (A1)⇒(A2)
gives completeness of our reduction. The proof is very technical, which we relegate to theappendix.

Running Example We show how the sPDS constructed can determine that the requiredclass success ∨ h↓+ isuccess can be added to the root node of the tree, thus implying that
there are no redundant selectors.
We write conﬁgurations of a symbolic pushdown system using the notation (X, Y1 . . . Ym )where X is the set of classes c such that the variable xc is true, and Y1 . . . Ym is a stack of setsof classes (with the top on the right) such that each Yi is a set of classes c such that yc is true
at stack position i. Note, we do not show the zc variables’ values since they are only needed toevaluate h↑i modalities, which do not appear in our example.
First we apply the rule (root, AddChild(team)) and then (team, AddChild(P1)). Each step
pushes a new item onto the stack. By executing these steps the sPDS is exploring a branchfrom root to P1.
(∅, {root}) →(∅, {root} {team}) →(∅, {root} {team} {P1})
At this point there’s nothing more we can do with the P1 node. Hence, the sPDS backtracks,
remembering in its control state the classes contained in the child it has returned from. Once
this information is remembered in its control state, it knows that a child is labelled P1 andhence (h↓iP1, AddClass(h↓iP1)) can be applied.
(∅, {root} {team} {P1}) →({P1},{root} {team})→ on{P1}, {root} team, h↓iP1
Now the sPDS can repeat the analogous sequence of actions to obtain that h↓iP2 can also label
the team node.
no{P1}, {root} team, h↓iP1
→

n
o

∅, {root} team, h↓iP1 {P2} →on→{P2}, {root} team, h↓iP1no{P2}, {root} team, h↓iP1, h↓iP2
Now we are able to deduce that success can also label the team node.
on→{P2}, {root} team, h↓iP1, h↓iP2on→{P2}, {root} . . . , h↓iP1 ∧ h↓iP2(∅, {root} {. . .} {success})
We are then able to backtrack to the root node, accumulating the information that h↓+ isuccessholds at the root node, and thus (success ∨ h↓+ isuccess) is not redundant.
(∅, {root} {. . .} {success}) →({success}, {root} {. . .}) →({success}, {root} {. . . , h↓+ isuccess}) →+({.
 . . , h↓n isuccess}, {root})o →{. . .}, . . . , h↓+ isuccess→no+{. . .}, . . . , success ∨ h↓ isuccess6

Experiments

We have implemented our approach in a new tool TreePed which is available for download [55].
We tested it on several case studies. Our implementation contains two main components:
a proof-of-concept translation from HTML5 applications using jQuery to our model, and aredundancy checker (with non-redundancy witness generation) for our model. Both tools weredeveloped in Java. The redundancy checker uses jMoped [54] to analyse symbolic pushdown
systems. In the following sections we discuss the redundancy checker, translation from jQuery,and the results of our case studies.

6.1

The Redundancy Checker

The main component of our tool implements the redundancy checking algorithm for proving
Theorem 3. Largely, the algorithm is implemented directly. The most interesting diﬀerences
are in the use of jMoped to perform the analysis of sPDSs to answer class-adding checks. In
the following, assume a tree Tv , rewrite rules R, and a set K of classes.
Optimising the sPDS For each class c ∈ K we construct an sPDS. We can optimise by
restricting the set of rules in R used to build the sPDS. In particular, we can safely ignore allrules in R that cannot appear in a sequence of rules leading to the addition of c. To do this,
we begin with the set of all rules that either directly add the class c or add a child to the tree(since these may lead to new nodes matching other rules). We then add all rules that directly
add a class c′ that appears in the guard of any rules included so far. This is iterated until aﬁxed point is reached. The rules in the ﬁxed point are the rules used to build the sPDS.
Reducing the number of calls. We re-implemented the global backwards reachability analysis (and witness generation) of Moped [51] in jMoped. This means that a single call to jMoped
can allow us to obtain a BDD representation of all initial conﬁgurations of the sPDSs obtained
from class-adding problems hTv , f, c, Ri that have a positive answer to the class-adding problem
for a given class c ∈ K. Thus, we only call jMoped once per class.

6.2

Translation from HTML5

The second component of our tool provides a proof-of-concept prototypical translation fromHTML5 using jQuery to our model. We provide a detailed description in the Appendix andprovide a small example below. There are three main parts to the translation.
• The DOM tree of the HTML document is directly translated to a tree in our model. We
use classes to encode element types (e.g. div or a), IDs and CSS classes.
• We support a subset of CSS covering the most common selectors and all selectors in ourcase studies. Each selector in the CSS stylesheet is translated to a guard to be analysed
for redundancy. For pseudo-selectors such as g:hover and g:before we simply check forthe redundancy of g.
• Dynamic rules are extracted from the JavaScript in the document by identifying jQuerycalls and generating rules as outlined in Section 3.3. Developing a translation tool thatcovers all covers all aspects of such an extremely rich and complex language as JavaScript
is a diﬃcult problem [8]. Our proof-of-concept prototype covers many, but by no means

all, interesting features of the language. The implemented translation is described in moredetail in the appendix.
Sites formed of multiple pages with common CSS ﬁles are supported by automatically collating
the results of independent page analyses and reporting site-wide redundancies.
To give a ﬂavour of the translation of a single line we recall one of the rules from theexample in Figure 1, except we adjust it to a call addClass() instead of remove() (since calls
to remove() are ignored by our abstraction).
$('.input_wrap').find('.delete').parent('div').addClass('deleted');We can translate this rule inductively. From the initial jQuery call $('.input_wrap') we
obtain a guard that is simply .input_wrap that matches any node with the class input_wrap.
We can then extend this guard to handle the find() call. This looks for any child of thecurrently matched node that has the class delete. Thus, we build up the guard to.delete ∧ h↑+ i.input_wrap
Next, because of the call to .parent() we have to extend the guard further to match the parentof the currently selected node, and enforce that the parent node is a div.
div ∧ h↓i(.delete ∧ h↑+ i.input_wrap)
Finally, we encounter the call to addClass() which we translate to an AddClass({deleted})rule.
(div ∧ h↓i(.delete ∧ h↑+ i.input_wrap), AddClass({deleted}))

6.3

Case Studies

We performed several case studies. One is based on the Igloo example from the benchmark
suite of the dynamic CSS analyser Cilla [44], and is described in detail below. Another (andthe largest) is based on the Nivo Slider plugin [47] for animating transitions between a seriesof images. The remaining examples are hand built and use jQuery to make frequent additions
to and removals from the DOM tree. The ﬁrst bikes.html allows a user to select diﬀerent
frames, wheels and groupsets to build a custom bike, comments.html displays a comments
section that is loaded dynamically via an AJAX call, and transactions.html is a ﬁnance page
where previous transactions are loaded via AJAX and new transactions may be added andremoved via a form. The example in Figure 1 is example.html and example-up.html is theversion without the limit on the number of input boxes. These examples are available in thesrc/examples/html directory of the tool distribution [55].
All case studies contained non-trivial CSS selectors whose redundancy depended on the
dynamic behaviour of the system. In each case our tool constructed a rewrite system following
the process outlined above, and identiﬁed all redundant rules correctly. Below we provide theanswers provided by UnCSS [56] and Cilla [14] when they are available9 .
The experiments were run on a Dell Latitude e6320 laptop with 4Gb of RAM and four
2.7GHz Intel i7-2620M cores. We used OpenJDK 7, using the argument “-Xmx” to limit RAM
9 We did not manage to successfully set up Cilla [44] and so only provide the output for the Igloo example
that has been provided by the authors in [14].

Case Study

Ns

Ss

Ls

Rs

Time

bikes.html
comments.html
example.html
example-up.html
igloo/
index.html
engineering.html
Nivo-Slider/demo.html
transactions.html

23
5
11
3

18 (0)
13 (1)1 (0)1 (1)261 (89)

97
43
28
15

37
26
4
3

3.6s
2.9s
.6s
.6s
3.4s

24
24

1
1

501
37

21
6

145
236
15
20

172 (131)
9 (0)

6.3s
1.6s

Table 1: Case study results.
usage to 2.5Gb. The results are shown in Table 1. Ns is the initial number of elements in the
DOM tree, Ss is the number of CSS selectors (with the number of redundant selectors shownin brackets), Ls is the number of Javascript lines reported by cloc, and Rs is the number ofrules in the rewrite system obtained from the JavaScript10 after simpliﬁcation (unsimpliﬁed
rules may have arbitrarily complex guards). The ﬁgures for the Igloo example are reported perﬁle or for the full analysis as appropriate.
We remark that the translation from JavaScript and jQuery is the main limitation of thetool in its application to industrial websites, since we do not support JavaScript and jQuery in
its full generality. However, we also note that the number of rules required to model websites
is often much smaller than the size of the code. For example, the Nivo-Slider example contains
501 lines of JavaScript, but its abstraction only requires 21 rules in our model. It is the numberof these rules and the number of CSS selectors (and the number of classes appearing in theguards) that will have the main eﬀect on the scalability of the tool.
Although we report the number of nodes in the webpages of our examples, checking CSS
matching against these pre-existing nodes is no harder than standard CSS matching. The
dynamic addition of nodes to the webpage is where symbolic pushdown analysis is required,hence the number of rewrite rules gives a better indication of the diﬃculty of an analysis
instance.
Example from Figure 1 TreePed suggests that the selector .warn might be reachable and,
therefore, is not deleted. We have run UnCSS on this example, which incorrectly identiﬁes.warn as unreachable.
The Igloo example The Igloo example is a mock company website with a home page(index.html) and an engineering services page (engineering.html). There are a total of
261 CSS selectors, out of which 89 of them are actually redundant (we have veriﬁed this byhand). UnCSS reports 108 of them are redundant rules.
We mention one interesting selector which both Cilla and UnCSS have identiﬁed as redundant, but is actually reachable. The Igloo main page includes a search bar that contains someplaceholder text which is present only when the search bar is empty and does not have focus.
Placeholder text is supported by most modern browsers, but not all (e.g. IE9), and the page
10 Not including the number of rules required to represent the CSS selectors.

(function($) {function supportsInputPlaceholder() {var el = document.createElement('input');
return 'placeholder' in el;}$(function() {if (!supportsInputPlaceholder()) {var searchInput = $('#searchInput'),
placeholder = searchInput.attr('placeholder');
searchInput.val(placeholder).focus(function() {var $this = $(this);$this.addClass('touched');
...
})
...
});
}
})(jQuery);Figure 3: JavaScript code snippet from Igloo example
contains a small amount of JavaScript to simulate this functionality when it is not provided by
the browser. The relevant code is shown in Figure 3. In particular, the CSS class touched,
and rule#search .touched { color: #333; }are used for this purpose. Both Cilla and UnCSS incorrectly claim that the rule is redundant.
Since we only identify genuinely redundant rules, our tool correctly does not report the rule as
redundant.
In addition, TreePed identiﬁed a further unexpected mistake in Igloo’s CSS. The ruleh2 a:hover, h2 a:active, h2 a:focus
h3 a:hover, h3 a:active, h2 a:focus { ... }is missing a comma from the end of the ﬁrst line. This results in the redundant selector“h2 a:focus h3 a:hover” rather than two separate selectors as was intended. Cilla did notreport this redundancy as it appears to ignore all CSS rules with pseudo-selectors. Finally, we
remark that the second line of the above rule contains a further error: “h2 a:focus” shouldin fact be “h3 a:focus”. This raises the question of selector subsumption, on which there isalready a lot of research work (e.g. see [13, 44]). These algorithms may be incorporated into
our tool to obtain a further size reduction of CSS ﬁles.

The Nivo-Slider example Nivo-Slider [47] is an easy-to-use image slider JavaScript packagethat heavily employs jQuery. In particular, it provides some beautiful transition eﬀects whendisplaying a gallery of images. In this case study, we use a demo ﬁle that displays a seriesof four images. The ﬁle contains a total of 172 CSS selectors, out of which 131 are actually
redundant (we veriﬁed this by hand). UnCSS reports 152 redundant CSS selectors (i.e. about
50% of false positives).

...
<div id="slider" class="nivoSlider">...
<a href="http://dev7studios.com"><img src="images/up.jpg"
data-thumb="images/up.jpg"
alt=""
title="This is an example of a caption"/>
</a>
...
<div>
...

Figure 4: HTML code snippet for Nivo-Slider demo.
var slider = $('#slider');slider.data('nivo:vars', vars).addClass('nivoSlider');// Find our slider children
var kids = slider.children();kids.each(function() {var child = $(this);var link = '';if(!child.is('img')){if(child.is('a')){child.addClass('nivo-imageLink');
link = child;
}
...
}
...
}

Figure 5: JavaScript code snippet for Nivo-Slider demo.
We mention the following interesting rule that UnCSS reports as redundant:.nivoSlider a.nivo-imageLink {...
z-index:6;...
}
Recall that the z-index of an HTML element speciﬁes the vertical stack order; a greater stackorder means that the element is in front of an element with a lower stack order. This CSS rule,among others, sets the z-index of an HTML element that matches the selector to a higher
value. In eﬀect, this allows a hyperlink that overlaps with the second image in the series to beclicked (which takes the user to a diﬀerent web page). Removing this rule disables the hyperlink
from the page. The code snippet in Figure 4 provides the relevant part of the HTML document.
In particular, the class nivo-imageLink will be added by the JavaScript bit of the page tothe the depicted hyperlink element above, as is shown in the JavaScript code snippet in Figure
5. In contrast to UnCSS, TreePed correctly identiﬁes that the above CSS rule may be used.

7

Conclusion and Future WorkAt the moment our translation from HTML5 applications to our tree-rewriting model is prototypical and does not incorporate many features that such a rich and complex language as
JavaScript has, especially in the presence of libraries. Therefore, an important research direction is to develop a more robust translation, perhaps by building on top of existing JavaScript
static analysers like WALA [49, 53] and TAJS [8, 27, 26]. As Andreasen and Møller [8] describe,a static analysis of JavaScript in the presence of jQuery is presently a formidable task for existing static analysers for JavaScript. For this reason, we do not expect the task of building amore robust translation to our tree-rewriting model to be easy.
Our technique should not be seen as competing with dynamic analysis techniques for identifying redundant CSS rules (e.g. UnCSS and Cilla). In fact, they can be combined to obtaina more precise CSS redundancy checker. Our tool TreePed attempts to output the deﬁnitely
redundant rules, while Uncss/Cilla attempts to output those that are deﬁnitely non-redundant.
The complement of the union of these sets is the “donâĂŹt know set”, which can (for example)
be checked manually by the developer. For future work, we would like to combine static anddynamic analysis to build a more precise and robust CSS redundancy checker.
Another direction is to ﬁnd better ways of overapproximating redundancy problems for theundecidable class Trs of rewrite systems using our monotonic abstractions (other than replacing
non-positive guards by ⊤). In particular, for a general guard, can we automatically constructa more precise positive guard that serves as an overapproximation? A more precise abstraction
would be useful in identifying redundant CSS rules with negations in the node selectors, which
can be found in real-world HTML5 applications (though not as common as those rules without
negations).
We may also consider other ways of improving CSS performance using the results of ouranalysis. For example, a descendant selector.a .b { ... }is less eﬃcient than a direct child selector.a > .b { ... }since the descendant selector must search through all descendants of a given node. However,
it is very common for the former to be used in place of the latter. If we can identify that theguard a ∧ h↓ih↓+ ib is never matched, while a ∧ h↓ib is matched, then we can safely replace thedescendant selector with the direct child selector.
Acknowledgments We sincerely thank Max Schaefer for fruitful discussions. Hague is supported by the Engineering and Physical Sciences Research Council [EP/K009907/1]. Lin is
supported by a Yale-NUS Startup Grant. Ong is partially supported by a visiting professorship, National University of Singapore.

References[1] https://bitbucket.org/TreePed/treeped/raw/master/src/examples/html/example-up.html,
March 2015.
[2] https://bitbucket.org/TreePed/treeped/raw/master/src/examples/html/example.html,
March 2015.

[3] Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability
theorems for infinite-state systems. In LICS, pages 313–321, 1996.
[4] Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d’Orso. Regular tree model
checking. In CAV, pages 555–568, 2002.
[5] S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1994.
[6] Serge Abiteboul, Omar Benjelloun, and Tova Milo. Positive active XML. In PODS, pages 35–45,
2004.
[7] Serge Abiteboul, Luc Segoufin, and Victor Vianu. Static analysis of active XML systems. ACM
Trans. Database Syst., 34(4), 2009.
[8] E. Andreasen and A. Møller. Determinacy in static analysis for jquery. In OOPSLA, pages 17–31,
2014.
[9] http://www.websiteoptimization.com/speed/tweak/average-web-page/.
[10] James Bailey, Alexandra Poulovassilis, and Peter T. Wood. An event-condition-action language
for XML. In WWW, pages 486–495, 2002.
[11] Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs.
In SPIN, pages 113–130, 2000.
[12] M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and
G. Smith. A trusted mechanised javasript specification. In POPL, pages 87–100, 2014.
[13] Martí Bosch, Pierre Genevès, and Nabil Layaïda. Automated refactoring for size reduction of CSS
style sheets. In DocEng, pages 13–16, 2014.
[14] https://github.com/saltlab/cilla/.
[15] Wenfei Fan, Floris Geerts, and Frank Neven. Expressiveness and complexity of XML publishingtransducers. ACM Trans. Database Syst., 33(4), 2008.
[16] Alain Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput.
Sci., 256(1-2):63–92, 2001.
[17] J. Flum and M. Grohe. Parameterized Complexity Theory. Springer, 2006.
[18] Blaise Genest, Anca Muscholl, Olivier Serre, and Marc Zeitoun. Tree pattern rewriting systems.
In ATVA, pages 332–346, 2008.
[19] Blaise Genest, Anca Muscholl, and Zhilin Wu. Verifying recursive active documents with positive
data tree rewriting. In FSTTCS, pages 469–480, 2010.
[20] Pierre Geneves, Nabil Layaida, and Vincent Quint. On the Analysis of Cascading Style Sheets. In
WWW, pages 809–818, 2012.
[21] Stefan Göller and Anthony Widjaja Lin. Refining the process rewrite systems hierarchy via groundtree rewrite systems. ACM Trans. Comput. Log., 15(4):26:1–26:28, 2014.
[22] S. Guarnieri and V. B. Livshits. GATEKEEPER: mostly static enforcement of security andreliability policies for javascript code. In USENIX, pages 151–168, 2009.
[23] S. Guarnieri, M. Pistoia, O. Tripp, J. Dolby, S. Teilhet, and R. Berg. Saving the world wide webfrom vulnerable javascript. In ISSTA, pages 177–187, 2011.
[24] Matthew Hague. Senescent ground tree rewrite systems. In CSL-LICS, page 48, 2014.
[25] D. Jang and K. -Moo Choe. Points-to analysis for javascript. In SAC, pages 1930–1937, 2009.
[26] S. H. Jensen, M. Madsen, and A. Møller. Modeling the HTML DOM and browser API in static
analysis of javascript web applications. In SIGSOFT/FSE, pages 59–69, 2011.
[27] S. H. Jensen, A. Møller, and P. Thiemann. Type analysis for javascript. In SAS, pages 238–255,
2009.
[28] http://jquery.com/.
[29] http://trends.builtwith.com/javascript/jQuery.
[30] N. Klarlund, A. Møller, and M. I. Schwartzbach. MONA implementation secrets. Int. J. Found.
Comput. Sci., 13(4):571–586, 2002.

[31] Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. Analyzing recursive programs using a fixed-point calculus. In PLDI, pages 211–222, 2009.
[32] Benjamin S. Lerner, Liam Elberty, Jincheng Li, and Shriram Krishnamurthi. Combining form andfunction: Static types for jquery programs. In ECOOP, pages 79–103, 2013.
[33] Leonid Libkin. Logics for unranked trees: An overview. Logical Methods in Computer Science,2(3), 2006.
[34] Anthony Widjaja Lin. Accelerating tree-automatic relations. In FSTTCS, pages 313–324, 2012.
[35] Anthony Widjaja Lin. Weakly-synchronized ground tree rewriting. In MFCS, pages 630–642,
2012.
[36] Christof Löding. Reachability problems on regular ground tree rewriting graphs. Theory Comput.
Syst., 39(2):347–383, 2006.
[37] Christof Löding and Alex Spelten. Transition graphs of rewriting systems over unranked trees. In
MFCS, pages 67–77, 2007.
[38] Sebastian Maneth, Alexandru Berlea, Thomas Perst, and Helmut Seidl. XML type checking withmacro tree transducers. In PODS, pages 283–294, 2005.
[39] Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.
[40] Maarten Marx. Conditional xpath. ACM Trans. Database Syst., 30(4):929–959, 2005.
[41] Richard Mayr. Process rewrite systems. Inf. Comput., 156(1-2):264–286, 2000.
[42] Davood Mazinanian, Nikolaos Tsantalis, and Ali Mesbah. Discovering refactoring opportunities
in cascading style sheets. In FSE, pages 496–506, 2014.
[43] K. L. McMillan. Symbolic model checking. Kluwer, 1993.
[44] Ali Mesbah and Shabnam Mirshokraie. Automated Analysis of CSS Rules to Support Style Maintenance. In ICSE, pages 408–418, 2012.
[45] Leo A. Meyerovich and Rastislav Bodik. Fast and parallel webpage layout. In WWW, pages
711–720, 2010.
[46] http://www2.informatik.uni-stuttgart.de/fmi/szs/tools/moped/.
[47] https://github.com/gilbitron/Nivo-Slider.
[48] http://www.sanwebe.com/2013/03/addremove-input-fields-dynamically-with-jquery.
[49] M. Schäfer, M. Sridharan, J. Dolby, and F. Tip. Dynamic determinacy analysis. In PLDI, pages
165–174, 2013.
[50] Bernd-Holger Schlingloff. Expressive completeness of temporal logic of trees. Journal of Applied
Non-Classical Logics, 2(2):157–180, 1992.
[51] Stefan Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technischen Universität
München, 2002.
[52] M. Sipser. Introduction to The Theory of Computation. Cengage Learning, 3 edition, 2012.
[53] M. Sridharan, J. Dolby, S. Chandra, M. Schäfer, and F. Tip. Correlation tracking for points-to
analysis of javascript. In ECOOP, pages 435–458, 2012.
[54] Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, and Javier Esparza. jMoped: A test
environment for Java programs. In CAV, pages 164–167, 2007.
[55] https://bitbucket.org/TreePed/treeped.
[56] https://github.com/giakki/uncss.
[57] http://www.w3schools.com/.

A

Proof of Proposition 1

We prove the undecidability of the 1-redundancy problem when negation is allowed in theguards. The proof is by a reduction from the undecidable control-state reachability problem fordeterministic two counter machines (2-CM): given a 2-CM M = (Q, ∆, q0 , qF ) with counters X
and Y , decide whether there exist a path from (q0 , 0, 0) to some conﬁguration in {qF } × N × N.
We will use X and Y to denote the two counters, and Z to range over {X, Y }. The two counter
tests will be = and > and we use  to range over these tests. We may assume that(i) counter tests and counter increments / decrements never take place in the same transition,i.e., rules are of form (q, [Z  0]) → q ′ or q → (q ′ , inc(Z)) or q → (q ′ , dec(Z)), and(ii) there are no self-loops in the counter machine i.e. there is no transition of the form (q, ·) →q.
The initial tree T0 = (D0 , λ0 ) is deﬁned to be D0 = {ǫ} and λ0 (ǫ) = q0 . We now constructa rewrite system R ∈ Trs. The state of the machine is always recorded in the root node.
The values of the two counters X and Y will be encoded by the number of nodes at level 1(i.e. children of the root node) that are associated with class X and Y , respectively. Moreprecisely, for each transition rule σ of the machine, we introduce a class σ. In addition, we use
the following four classes: X, Y , new , and del . The main problem that we have to overcome
in our reduction is to simulate one transition of M by several simpler steps of T0 owing to thesimplicity of rewrite operations that we allow in Trs. This is in fact the reason for adding
the last two classes new and del , which are just “ﬂags” to indicate whether a node (at level1) is “new” or is “scheduled to be deleted”. Our rewrite system R operates over Σ := 2K with
K = Q ∪ ∆ ∪ {X, Y, new, del }. Next we introduce the guards:V (a) g(Z = 0) := ¬h↓iZ, (b)g(Z > 0) := h↓iZ, (c) θ1 := ¬h↓inew ∧ ¬h↓idel , and (d) θ2 := γ∈∆ ¬γ. As we shall see, theguard θ1 ∧ θ2 means that there is no “pending job”. The rewrite rules for R are as follows:• If σ = (q, [Z  0]) → q ′ , then add the following rules:(1) (q ∧ g(Z  0) ∧ θ1 ∧ θ2 , AddClass({σ, q ′ }))(2) (σ, RemoveClass({q, σ}))• If σ = q → (q ′ , inc(Z)), then add:
(1) (q ∧ θ1 ∧ θ2 , AddClass({σ, q ′ })(2) (σ ∧ θ1 , AddChild({Z, new }))(3) (σ ∧ h↓i(Z ∧ new ), RemoveClass({σ, q})).
(4) (new ∧ h↑iθ2 , RemoveClass({new }))• If σ = q → (q ′ , dec(Z)), then add:
(1) (q ∧ θ1 ∧ θ2 , AddClass({σ, q ′ }))(2) (Z ∧ h↑i(σ ∧ ¬h↓idel ), AddClass({del }))(3) (σ ∧ h↓i(Z ∧ del), RemoveClass(σ, q))(4) (del ∧ h↑iθ2 , RemoveClass({Z, del}))Observe that the trees reachable from the initial tree is of height at most 1. Possible labels of
the root are only q ∈ Q and σ ∈ ∆. Possible labels of a leaf node (necessarily a child of theroot) are X, Y, new and del .
It is not diﬃcult to see that R when initialised in T0 performs a faithful simulation of thecounter machine M from the conﬁguration (q, 0, 0). Our rewrite system R is deﬁned in such a
way that each group of rewrite rules introduced in R to simulate a transition σ of M has tobe executed before the next transition of M can be simulated by R. In particular, to simulatea M transition σ from a given state q ∈ Q, our rewrite system R needs to add σ to the root
node, which can only be done if the following properties are satisﬁed: (1) the label of the root
node is {q} for some q ∈ Q, and (2) no child of the root has del or new in the label. This isowing to the conjuncts θ1 ∧ θ2 in the guard. In particular, this means that the root contains at
most one σ. In addition, if σ is a class of the form q → (q ′ , inc(Z)) or q → (q ′ , dec(Z)), then σ
can only be removed only after proper simulation of counter increments/decrements has been
performed.
In summary, we have that M reaches the control state qF iﬀ qF is not redundant in R. Thisconcludes our reduction.

B

Proof of Lemma 1

We prove that if T  T ′ , then T ′ satisﬁes at least the same guards as T at each node v. The
proof is by induction on g. For the base cases, g = ⊤ is trivial, and that v, T |= X implies
f (v), T ′ |= X holds since, by (H2), we have X ⊆ λ(v) ⊆ λ′ (f (v)). We now proceed to the
inductive case. The cases of conjunction and disjunction are obvious.
Assume that v, T |= hdig for some d ∈ {↑, ↓}. We will only show the case when d =↓; theother case can be handled in the same way. This means that v.i, T |= g for some i ∈ N. By
induction, we have f (v.i), T ′ |= g. By (H3), we have that f (v.i) = f (v).j for some j ∈ N.
Altogether, this implies that f (v), T ′ |= h↓ig as desired.
Assume that v, T |= hd+ ig for some d ∈ {↑+ , ↓+ }. We will only show the case when d =↓+ ;the other case can be handled in the same way. The proof is by induction on the length n ofpath from v to a descendant vw (with w 6= ǫ) satisfying vw, T |= g. If n = 1, then by theprevious paragraph we have f (v), T ′ |= h↓ig and so f (v), T ′ |= h↓+ ig as desired. If n > 1 andw = iu′ for some i ∈ N and u′ ∈ N∗ , then vi, T |= h↓+ ig with a witnessing path of length n − 1.
Therefore, by induction, we have f (vi), T ′ |= h↓+ ig. Since f (vi) = f (v).j for some j ∈ N, it
follows that f (v), T ′ |= h↓ih↓+ ig and so f (v), T ′ |= h↓+ ig as desired.

C

Proof of Lemma 2

We prove that, whenever T1  T2 and T1 →σ T1′ , then either T1′  T2 or T2 →σ T2′ with T1′  T2′ .
Suppose T1 →σ T2 where T1 = (D1 , λ1 ), T1′ = (D1′ , λ′1 ) and σ = (g, χ); and T1  T2 =(D2 , λ2 ) is witnessed by an embedding f : D1 → D2 . Assume v, T1  g for some v ∈ D1 . Thenf (v), T2  g by Lemma 1. We consider each of the four cases of χ in turn.
Case: χ = AddClass(X). Then set T2′ = (D2′ , λ′2 ) with D2′ := D2 and λ′2 := λ2 [f (v) 7→
λ2 (f (v)) ∪ X)]. Hence T2 →σ T2′ . Moreover we have T1′  T2′ , as witnessed by f : D1′ → D2′(note that D1′ = D1 and D2′ = D2 ).
Case: χ = AddChild(X). Assume D1′ = D1 ∪ {v.i} and λ′1 = λ1 [v.i 7→ X] where i is thenumber of children of v in T1 . Let i′ be the number of children of f (v) in T2 . Then set
T2′ = (D2′ , λ′2 ) with D2′ := D2 ∪ {f (v).i′ } and λ′2 := λ2 [f (v).i′ 7→ X]. Then T2 →σ T2′ andT1′  T2′ is witnessed by f ′ : D1′ → D2′ such that f ′ := f [v.i 7→ f (v).i′ ].
Case: χ = RemoveClass(X) or χ = RemoveNode. In both cases, the function f (restricted
to D1′ ) is still an embedding from T1′ to T2 and so T1′  T2 .

D

Proof of Lemma 3

We show that, when guards are monotonic, the RemoveClass(B) and RemoveNode operations
do not aﬀect the redundancy of the guards. The ⇐-direction is trivial. For the other direction,
assume T0 →σ0 T1 →σ1 · · · →σn−1 Tn →σn Tn+1 = (D, λ) where each σi = (gi , χi ), and′v, Tn+1  g for some v ∈ D. It suﬃces to construct trees T0′ , · · · , Tn+1
with T0′ = T0 such′′′′that g matches Tn+1 , and for each i ∈ [1..n], Ti  Ti and Ti →σi′ Ti+1 where each σi′ is nota RemoveNode or a RemoveClass(X) operation but may be the identity operation. We shallconstruct such a sequence of trees by induction on i. The base case follows immediately fromthe assumptions. Let i ≥ 0. Suppose Ti′ has been constructed such that Ti  Ti′ . There are two′cases. If χi = RemoveNode or χi = RemoveClass(X) then set Ti+1:= Ti′ and σi′ is the identity′′
operation; otherwise, thanks to Lemma 2, set σi := σi and we can construct Ti+1
such that′′′′
Ti →σi′ Ti+1 and Ti+1  Ti+1 . Finally, since Tn+1  Tn+1 and g matches Tn+1 , we have g also′
matches Tn+1
by Lemma 1 as required.

E

Proof of Proposition 2

To show EXP membership for the bit-toggling problem, we simply compute an exponentialsized PDS from a given sPDS and apply the standard polynomial-time algorithm for solving
control-state reachability for PDS (this is the same as emptiness for pushdown automata overa unary input alphabet {a}).
To show PSPACE membership for the bounded bit-toggling problem, suppose that the input
to the problem is P = (V, W, ∆) and h ∈ N with V = {x1 , . . . , xn } and W = {y1 , . . . , ym }. Eachconﬁguration is a pair (q, w) of q ∈ {0, 1}n and w is a word over the stack alphabet Γ = {0, 1}m.
Since the stack height is always bounded by h, each conﬁguration is of size at most n + (h × m).
Also, checking whether σ = ((q, a), (q ′ , w)) is a transition rule of P — where q, q ′ ∈ {0, 1}n,a ∈ {0, 1}m, and w is a word of length at most 2 over Γ — can be checked in linear time(and therefore polynomial space) by simply evaluating each symbolic rule of the form (|w|, ϕ)with respect to the boolean assignment σ. [Evaluating BDDs, boolean formulas, and boolean
circuits can all be done in linear time.] So, we can obtain a nondeterministic polynomial spacealgorithm (and therefore membership in PSPACE) by guessing the symbolic rule that needs tobe applied at any given moment.

F

Proof of Correctness of Lemma 4

We show correctness of the reduction to simple rewrite systems. To show (P1) and (P2), it
suﬃces to show the following four statements:(P1a) For each k ∈ N, S is k-redundant for R iﬀ S ′ is k-redundant for R1 .
(P1b) For each k ∈ N, S is k-redundant for R1 iﬀ S ′ is k-redundant for R′ .
(P2a) S is redundant for R iﬀ S ′ is redundant for R1 .
(P2a) S is redundant for R iﬀ S1 is redundant for R′ .
We ﬁrst show (P1a) and (P2a). To this end, we say that a tree T = (D, λ) ∈ Tree(Σ′ ) is
consistent if, for each g ∈ G and each node v ∈ D with g ∈ λ(v), it is the case that v, T |= g.
We say that T is maximally consistent if it is consistent and that, for each g ∈ G and each nodev ∈ D, if v, T |= g then g ∈ λ(v). Observe that each tree in Tree(Σ) (in particular, the initialtree) is consistent and that each of the rules (1–3) preserves consistency. Therefore, for alltrees T ∈ Tree(Σ) and T ′ ∈ Tree(Σ′ ), if T →∗R1 T ′ then T ′ is consistent. In addition, for atree T ∈ Tree(Σ′ ), we write T ∩ Σ to denote the the tree that is obtained from T by restricting
to node labels from Σ. Let Θ ⊆ R1 denote the set of intermediate rules added above. Since
the class G is closed under taking subformulas, for each tree T ∈ Tree(Σ), it is the case thatT →∗Θ T ′ for some maximally consistent tree T ′ ∈ Tree(Σ′ ) satisfying T ′ ∩ Σ = T . Now, by asimple induction on the length of paths, it follows that that T1 = (D1 , λ1 ) →∗R T2 = (D2 , λ2 )iﬀ T1 →∗R1 T2′ for some maximally consistent tree T2′ such that T2′ ∩ Σ = T2 . Since S ′ contains
precisely all g for which g ∈ S, (P1a) and (P2a) immediately follow.
We now show (P1b) and (P2b). Observe that both rules (a) and (b) preserve treeconsistency since v, T |= hd+ ig iﬀ at least one of the following cases holds: (i) v, T |= hdig,(ii) there exists a node w in T such that w, T |= hd+ ig and w can be reached from v by following the direction d for one step. As before, by a simple induction on the length of paths, for all
consistent trees T1 , T2 ∈ Tree(Σ′ ), it is the case that T1 →∗R′ T2 iﬀ T1 →∗R1 T2 . This implies
implies (P1b) and (P2b), i.e., the correctness of our entire construction.
Note, in particular, for all g ∈ S, it is the case that g is redundant in R iﬀ g is redundantin R′ .

G

Proof of Algorithm for Lemma 5

We argue the correctness of the ﬁxpoint algorithm in the proof of Lemma 5, which shows thatthe redundancy (resp. k-redundancy) problem is polynomial time solvable assuming oracle calls
to the class-adding (resp. k-class-adding) problem.
Soundness The proof is by induction over the number of applications of the ﬁxpoint rules. Fix
some sequence of rule applications reaching a ﬁxpoint and let Ti = (D0 , λi ) be the tree obtained
after ith application. We prove by induction that we have a tree T such that T0 →∗R T = (D′ , λ′ )and Ti  T and thus our algorithm is sound.
In the base case, when i = 0, T = T0 and the proof is trivial. Hence, assume by induction
we have a tree T such that T0 →∗R,f T and Ti  T . There are two cases.
• When we apply a rule σ = (g, AddClass(B)) at a node v ∈ D0 , then Ti →σ Ti+1 and by
Lemma 2 (Monotonicity) we obtain T ′ satisfying the induction hypothesis.
• When the class-adding problem has a positive answer on input hTv , f, c, Ri and we update
λ(v) := λ(v) ∪ {c}, then there is a sequence of rule applications σ1 , . . . , σn witnessing thepositive solution to the class-adding problems. By n applications of Lemma 2 we easily
obtain T ′ satisfying the induction hypothesis as required.
Completeness Take any sequence of rules σ1 , . . . , σn such that
T0 →σ1 T1 →σ2 · · · →σn Tn
where for each i, Ti = (Di , λi ). Note D0 ⊆ Di for each i. Let TF = (D0 , λ) be the tree obtained
as the conclusion of the ﬁxpoint calculation. We show λi (v) ⊆ λ(v) for all v ∈ D0 and hence
our algorithm is complete.
We induct over i. In the base case i = 0 and the result is trivial. For the induction, if σiwas applied to v ∈/ D0 or σi is an AddChild(B) rule, the result is also trivial. Else σi is of theform σ = (g, AddClass(B)) and applied to v ∈ D0 . There are several cases.

• When g = A let v ′ = v and when g = h↑iA let v ′ be the parent of v. Since v ∈ D0 we also
have v ′ ∈ D0 and thus λi (v ′ ) ⊆ λ(v) and thus σ is applicable at v ′ and the ﬁrst ﬁxpoint
rule applies. Since TF is a ﬁxpoint, we necessarily have B ⊆ λ(v).
• When g = h↓iA there are two cases.
– If the guard was satisﬁed by matching with v ′ ∈ D0 , then we have B ⊆ λ(v) exactly
as above.
– Otherwise, the guard was satisﬁed in the run to T ′ by matching with v ′ ∈/ D0 . Thus
we can pick out the sub-sequence of σ1 , . . . , σn beginning with the AddChild(C) rule(applied at v) that created v ′ and all rules applied at v ′ or a descendant. By Lemma 2(Monotonicity) and the fact that all guards are simple, this sequence is a witness tothe positive solution of the class-adding problem hTv , f, c, Ri for all c ∈ B and thusB ⊆ λ(v) as required.

H

BDD representation in the Proof of Lemma 6

We ﬁrst recall the deﬁnition of BDDs. A binary decision diagram (BDD) is a symbolic representation of boolean functions. A BDD over the variables V = {x1 , . . . , xn } is a rooted directed
acyclic graph G = (V, E) together with a mapping λ : (V ∪ E) → (V ∪ {0, 1}) such that:(i) if v ∈ V is an internal node, then λ(v) ∈ V and it has precisely two outgoing edges e1 , e2labeled by λ(e1 ) = 0 and λ(e2 ) = 1, respectively, and(ii) (ii) if v ∈ V is a leaf node, then it is labeled by λ(v) ∈ {0, 1}.
Given an assignment ν : V → {0, 1}, we can determine the truth value of G under ν as follows:
start at the root node of G; if the current node is v labeled by x ∈ V, follow the outgoing
ν(x)-labeled from v to determine the next node; and if the current node is a leaf, then the truth
value is given by the label of this leaf.
An ordered BDD (oBDD) is a BDD together with an ordering of V (say x1 < · · · < xn ) suchthat if v is a predecessor of u in G where both v and u are internal nodes, then λ(v) < λ(u).
So, no variable x ∈ V occurs more than once in each path from the root to a leaf in an oBDD.
Finally, an oBDD is reduced if (i) it has no two isomorphic subgraphs, and (ii) it has nointernal node whose two children are the same node. In the sequel, we use the term BDD tomean reduced oBDD.
We now demonstrate how to represent boolean formulas in the reduction as BDDs. Observe that each boolean formula in our P-rules is a conjunction of formulas, in which no two
conjuncts share any common variable. This allows an easy conversion to BDD representation.
For example, the BDD G = (V, E, λ) for the formula ϕ in the ﬁrst type of rules in our sPDS
construction in Section 5 can be deﬁned as follows. Each conjunct of the form s ↔ t is turned
into the following BDD
0

t

0

1

t

1

s

1

where a missing edge means that it goes to a 0-labeled leaf (also omitted from diagram).
Similarly, a conjunct of the form s is turned into the following BDD

1
s

1

where, again, a missing edge means that it goes to a 0-labeled leaf. Now, if G1 and G2 are
BDDs for the conjuncts ϕ1 and ϕ2 with diﬀerent sets of variables, then the BDD for ϕ1 ∧ ϕ2 canbe constructed by gluing the 1-labeled leaf in G1 by the root of G2 (using the label of the rootof G2 ). Since no two conjuncts in ϕ share a common variable, the BDD for ϕ can be obtainedby linking these simpler BDDs in this way. The resulting BDD is of size linear in the size of ϕ.

I

Proof of Lemma 7

We ﬁrst prove the direction (A2)⇒(A1). We will prove this by induction on the length of paths.
The problem is that our induction hypothesis is not strong enough to get us oﬀ the ground(since the state component of Iλ0 (ǫ),f is always (0, . . . , 0)). Therefore, we will ﬁrst prove thisby induction with a stronger induction hypothesis:
Lemma 8. Given P-configurations (q, α) and (q ′ , α′ ) with q, q ′ : V → {0, 1} and α, α′ : W →{0, 1} (i.e. stack of height 1), suppose that (q, α) →∗P (q ′ , α′ ). Define T = (D, λ) ∈ Tree(Σ) as(1) D = {ǫ} ∪ {0 : q(pop) = 1}, (2) λ(ǫ) = {c ∈ K : α(yc ) = 1} and λ(0) = {c ∈ K : q(xc ) = 1}.
Define the assumption function fα : (K ∪ {root}) → {0, 1} with fα (c) = α(zc ) for c ∈ K andfα (root) = α(root). Then, there exists T ′ = (D′ , λ′ ) ∈ Tree(Σ) such that λ′ (ǫ) = {c ∈ K :α′ (yc ) = 1} and T →∗R,fα T ′ .
Observe that the direction (A2)⇒(A1) is immediate from this Lemma: simply apply it with(q, α) = Iλ0 (ǫ),f and (q ′ , α′ ) = IX,f,q′ .
Proof. The proof is by induction on the length k of the witnessing path π : (q, α) →∗ (q ′ , α′ ).
When k = 0, we have that (q, α) = (q ′ , α′ ). So, we may set T ′ = T and the statement issatisﬁed.
Let us now consider the case when k > 0. There are two cases to consider depending on thesecond conﬁguration in the path π:(i) π = (q, α) → (q1 , α1 ) →∗ (q ′ , α′ ), for some q1 : V → {0, 1} and α1 : W → {0, 1}.
(ii) π = (q, α) → (q1 , α1 β1 ) →∗ (q ′ , α′ ), where q1 : V → {0, 1} and α1 , β1 : W → {0, 1}.
Note that the case when the ﬁrst action is a pop (i.e. (q, α) → (q1 , ǫ)) is not possible since(q1 , ǫ) is a deadend.
Let us consider Case (i). The conﬁguration (q1 , α1 ) is obtained by applying a rule σ =(1, ϕ) ∈ ∆, which was generated by a rule γ = (g, AddClass(B)) ∈ R. Suppose that g = A ⊆ K;
the other two cases (i.e. when g is of the form (hdiA, AddClass(B))) can be handled in the sameway. Since ϕ has a conjunct of the form ya for each a ∈ A, it is the case that A ⊆ λ(ǫ). Since
yb1 is a conjunct of ϕ for each b ∈ B, The rule σ toggles on the variables yb for each b ∈ B while
preserving the value of all other variables in V ∪ W. So, if T1 := (D, λ1 ) with λ1 (0) := λ(0)and λ1 (ǫ) := λ(ǫ) ∪ B, then T0 →R,fα T1 . We may now apply the induction hypothesis on
the subpath (q1 , α1 ) →∗ (q ′ , α′ ) of π of shorter length and obtain T1 →R,fα T ′ . Concatenating
paths, we obtain a path T →R,fα T ′ as desired.
Let us now consider Case (ii). The conﬁguration (q1 , α1 β1 ) is obtained by applying a ruleσ = (2, ϕ) ∈ ∆, which was generated by a rewrite rule (A, AddChild(B)) ∈ R. Therefore,
it must be the case that (q1 , β1 ) →∗P (q2 , β2 ) →σ2 (q3 , ǫ) and (q3 , α1 ) →∗P (q ′ , α′ ) for someconﬁgurations (q2 , β2 ) and (q3 , ǫ) with stack height 1 and 0, respectively, and some P-rule(0, ϕ′ ). As in the previous case, we have A ⊆ λ(ǫ) and so, applying (A, AddChild(B)) atǫ, we obtain T1 = (D1 , λ1 ) with D1 := D ∪ {1} and λ1 is an extension of λ to D1 withλ1 (1) := B. Let T1′ = ({ǫ}, λ′1 ) be the subtree of T1 rooted at node 1. Applying induction on
the path (q1 , β1 ) →∗P (q2 , β2 ), we obtain a tree T2′ = (D2′ , λ′2 ) such that: (1) ν : T1′ →∗R,f T2′
with assumption function f := fβ1 , and (2) λ′2 (ǫ) = {c ∈ K : β2 (yc ) = 1}. Similarly, if we
let T3 = ({ǫ, 0}, λ3 ) be the tree with λ3 (ǫ) = λ(ǫ) and λ3 (0) = λ′2 (ǫ), we apply induction
hypothesis on the path (q3 , α1 ) →∗P (q ′ , α′ ) and obtain a path µ : T3 →∗R,fα T ′′ (here fα = fα1 )for some tree T ′′ = (D′′ , λ′′ ) with λ′′ (ǫ) = {c ∈ K : α′ (yc ) = 1}. Now let T ′ be the tree
obtained from T ′′ by: (1) removing the node 0 of T ′′ and replacing it by the tree T2′ (note:
T ′′ (0) = T2′ (ǫ)), and (2) adding a node labeled by λ(0) as a child of the root node of T ′′ . We
have T ′ (ǫ) = T ′′ (ǫ) = {c ∈ K : α′ (yc ) = 1}. Finally, we see that T →R,fα T1 →∗R,fα T ′ , where
the path T1 →∗R,fα T ′ is obtained by ﬁrst applying the path ν on the subtree of T1 rooted at 1
and then applying the path µ on the resulting tree (in the second step, we keep the subtree ofT1 rooted at the node 0 unchanged).
We now prove the direction (A1)⇒(A2) of the above claim. The proof is by induction on
the length k of the path π : T0 →∗R,f T . The base case is when k = 0, in which case we set
q ′ (x) := 0 for all x ∈ V and (A2) is satisﬁed since Iλ0 (ǫ),f = IX,f,q′ .
We proceed to the induction case, i.e., when k > 0. We may assume that λ(ǫ) is a strict
superset of λ0 (ǫ); otherwise, we may replace π with an empty path, which reduces us to thebase case. Therefore, some rewrite rule (g, AddClass(B)) with B ∩ λ0 (ǫ) 6= ∅ is applied at ǫ atsome point in π. We have two cases depending on the ﬁrst application of such a rewrite ruleσ = (g, AddClass(B)) at ǫ in π:(Case 1) We have g = A or g = h↑iA for some A ⊆ K. Since λ0 (ǫ) = λ′ (ǫ), the rule σ
can already be applied at ǫ in T0 yielding a tree T1 = ({ǫ}, λ1 ) with λ1 (ǫ) = λ0 (ǫ) ∪ B. Owing
to Lemma 2, we may apply the same sequence of rewrite rules witnessing π but with T1 as an
initial conﬁguration. Furthermore, we may remove any application of σ at ǫ in this sequence(since B is always a subset of the label of ǫ), which gives a path π ′ : T1 →R,f T of length≤ k − 1. Altogether, we obtain another path T0 →σ,f T1 →∗R,f T of length ≤ k. In addition, we
have Iλ0 (ǫ),f →P Iλ1 (ǫ),f by applying the rule (1, ϕ) ∈ ∆ generated from σ in the constructionof P. Now we may apply the induction hypothesis to the path π ′ : T1 →∗R,f T (of length < k)and obtain q ′ : V → {0, 1} such that Iλ1 (ǫ),f →∗P Iλ(ǫ),f,q′ , which gives us a path from Iλ0 (ǫ),fto Iλ(ǫ),f,q′ , as desired.
(Case 2) We have g = h↓iA for some A ⊆ K. In this case, the ﬁrst rule applied in π must
be of the form γ = (C, AddChild(Y )) for some C, Y ⊆ K. That is, we have π : T0 →γ,f T2 →∗R,f
T3 →σ,f T4 →∗R,f T for some trees Ti = (Di , λi ) (i ∈ {2, 3, 4}) such that: (1) λ0 (ǫ) = λi (ǫ)
for all i ∈ {2, 3}, (2) D2 = {ǫ, 0}, (3) At T3 , the rule σ is applied at ǫ, and so D4 = D3 andλ4 (v) = λ3 (v) for v 6= ǫ and λ4 (ǫ) = λ3 (ǫ) ∪ B ⊃ λ3 (ǫ). So, this means that some child i ∈ N of
the root node in T3 satisﬁes λ3 (i) ⊇ A, which enables σ to be executed at the root node. Now
recall that simple guards allow a node to inspect only its immediate neighbours (i.e. parent
or children). For this reason, we may assume without a loss of generality that i = 0, i.e., that
it was the child of ǫ that was spawned by the ﬁrst transition γ. In fact, we may go one stepfurther to assume that 0 is the only child of the root node in the subpath T2 →∗R,f T3 ! This isbecause that without modifying the label of ǫ, simple guards do not allow the node 0 to “detect”
the presence of the other children.
To ﬁnish oﬀ the proof, we will apply induction hypotheses twice on two diﬀerent paths.
Firstly, we apply the induction hypothesis on the shorter path (T2 )|0 →∗R,fǫ (T3 )|0 , where fǫ isan assumption function that captures the node label λ3 (ǫ), i.e., fǫ (root) = 0 and fǫ (c) = 1 iﬀ
c ∈ λ3 (ǫ); note that λ0 (ǫ) = λ2 (ǫ) = λ3 (ǫ). [Recall that (T2 )|0 means the subtree of T2 rooted atthe node 0.] This gives us the path Iλ2 (0),fǫ →∗P Iλ3 (0),fǫ ,q′′ for some q ′′ : V → {0, 1}. Therefore,
we have the path ν1 : Iλ0 (ǫ),f →P (0̄, µǫ µ0 ) →∗P (q ′′ , µǫ µ′0 ) →P (q ′ , µǫ ) → (q ′ , µ′ǫ ), where• µǫ (r) = 1 iﬀ Iλ0 (ǫ),f (r) = 1 for each r ∈ W = {yc , zc : c ∈ K} ∪ {root}.
• µ0 (root) = 0; µ0 (zc ) := µǫ (yc ); and µ0 (yc ) = 1 iﬀ c ∈ B, for each c ∈ K.
• µ′0 (r) = Iλ3 (0),fǫ ,q′′ (r) for each r ∈ W.
• q ′ (pop) = 1 and q ′ (xc ) = µ′0 (yc ) for each c ∈ K.
• µ′ǫ (r) = 1 iﬀ µǫ (r) = 1 or r ∈ B.
Note that (q ′ , µ′ǫ ) is the same as Iλ4 (ǫ),f,q′ . We are now going to apply the induction hypothesis
the second time. To this end, we let T4′ = ({ǫ}, λ′4 ) be the single-node tree deﬁned by restricting
T4 to the root, i.e., λ′4 (ǫ) = λ4 (ǫ) ⊃ λ0 (ǫ). Since T0  T4 , by the proof of Lemma 2, we have
T4′ →∗R,f T by following the actions in the path π, except for the action σ. This gives us apath π ′ whose length is |π| − 1. So, by induction, we have a path ν2 : Iλ4 (ǫ),f →∗P Iλ(ǫ),f,p forsome p : V → {0, 1}. In order to connect ν1 and ν2 , we need to use the following lemma, which
completes the proof of Lemma 7.
Lemma 9. Suppose p, q : V → {0, 1} such that p(x) ≤ q(x) for each x ∈ V. Then, for all
stack content v = α1 · · · αm where each αi : W → {0, 1}, if (p, v) →σ (p′ , w) with σ ∈ ∆, then(q, v) →σ (q ′ , w) for some q ′ : V → {0, 1} such that p′ (x) ≤ q ′ (x) for each x ∈ V.
Proof. Easy to verify by checking each P-rule.

J

A polynomial-time fixed point algorithm for boundedheightWe now provide a simple ﬁxpoint algorithm for the k-redundancy problem that runs in timenO(k) . We assume that we have simpliﬁed our rewrite systems using the simpliﬁcation given in
Section 5. The input to the algorithm is a simple rewrite system R over Tree(Σ) with Σ = 2K ,a guard database S ⊆ K, and an initial Σ-labeled tree T0 = (D0 , λ0 ) ∈ Tree(Σ). The numberk ∈ N is ﬁxed (i.e. not part of the input). Our algorithm will compute a tree TF = (DF , λF )such that TF ∈ post∗R (T0 ) and, for all trees T ∈ post∗R (T0 ), we have T  TF . By Lemma 1, if
a guard g ∈ S is matched in some T ∈ post∗R (T0 ), then g is matched in TF . The converse also
holds since TF ∈ post∗R (T0 ). Furthermore, we shall see that TF is of height at most k, each ofwhose nodes has at most |T0 | + |R| children (and so of size at most O(|T0 | + |R|)O(k) ), and iscomputed in time (|T0 | + |R|)O(k) . Computing the rules in S that are matched in TF can beeasily done in time linear in |S| × |TF |.
The algorithm for computing TF works as follows.
(1) Set T = (D, λ) := T0 ;(2) Set W := ∅;(3) Add each pair (v, σ) to W , where v ∈ D and σ ∈ R is a rule that is applicable at v,
i.e. v, T |= g where σ = (g, χ) for some χ; all pairs in W are initially “unmarked”;(4) Repeat the following for each unmarked pair (v, σ) ∈ W with σ = (g, χ):(a) if χ = AddClass(X), then λ(v) := λ(v) ∪ X;(b) if χ = AddChild(X), |v| ≤ k − 1, and X 6⊆ λ(v.i) for each v.i ∈ D child of v, thenset D := D ∪ {v.(i + 1)} where i := max{j ∈ N : v.j ∈ D} + 1 (by convention,
max ∅ = 0), and λ(v.i) := X;(c) Mark (v, σ);(d) For each (w, γ) ∈ (D × R) \ W that is applicable, add (w, γ) to W unmarked;(5) Output TF := T ;Proof of Correctness. We will show that T  TF for each T ∈ post∗R (T0 ). The proof is by
induction on the length m of path from T0 to T . We write TF = (DF , λF ). The base case iswhen m = 0, in which case T = T0 = (D0 , λ0 ). Since our rewrite rules only add classes to nodes
and add new nodes, it is immediate that D0 ⊆ DF and that λ0 (v) ⊆ λF (v) for each v ∈ D0 .
That is, T0  TF . We now proceed to the inductive step and assume that T = (D, λ)  TF
with a witnessing embedding f : D → DF . Let v ∈ D and σ = (g, χ) be a R-rule that is
applicable on the node v of T . By Lemma 1, it follows that f (v), TF |= g. Let us suppose thatafter applying σ on v, we obtain T ′ := (D′ , λ′ ). We have two cases now:
1. χ = AddClass(X). In this case, D′ = D, λ′ (u) = λ(u) whenever u 6= v, and λ′ (v) =λ(v) ∪ X. Since T  TF , it follows that λ(v) ⊆ λF (f (v)). Since f (v), TF |= g, it follows
that (f (v), (g, AddClass(X))) is marked in W (by the end of the computation of TF ).
This means that X ⊆ λF (f (v)). Altogether, T ′  TF .
2. χ = AddChild(X) and |v| ≤ k − 1. In this case, D′ = D ∪ {v.i} for some i ∈ N with
v.i ∈/ D, λ′ (u) = λ(u) for each u ∈ D, and λ′ (v.i) = X. Since T  TF , the properties(H1) and (H3) of embeddings imply that v and f (v) have the same levels in T and TF
respectively. Also, since v, TF |= g, it follows that (f (v), (g, AddChild(X))) is marked in
W (by the end of the computation of TF ). This means that there exists a child f (v).j in
DF with X ⊆ λF (f (v).j). Hence, the extension of f with f (v.i) := f (v).j is a witness forT ′  TF , as desired.
Running time analysis. We ﬁrst analyse the time complexity of each individual step in theabove algorithm. Checking whether a simple guard g is satisﬁed at a node v can be done byinspecting the node labels of v and its neighbours (i.e. parent and children), which can be
performed in time O(|K| × (number of neighbours of v)). So, since each node in T0 has most|T0 | children, then step (3) can be achieved in time O(|K| × |T0 |2 ). Similarly, modifying a nodelabel can be done in time O(|K|), which is the running time of Step (4a). Since no rewrite rulein R can be applied twice at a node, each node in TF has at most m := |T0 | + |R| children, i.e.,either that child was already in T0 or that it was generated by a rewrite rule in R. Therefore,
Step (4b) takes time O(|K| × m). Since Step (4d) needs to check only (w, γ) where w is aneighbor (i.e. children or parent) of v, then it can be done in time O(|K| × m). Since the tree
TF has height at most k and each node has at most m children, the tree TF has at most O(mk )nodes. So, the entire Step (4) runs in time O(|K| × |T0 |k+1 × |R|k+1 ), which is also a timebound for the running time of the entire algorithm.

K

W[1]-hardness for k-redundancy problem

Before proving our W[1]-hardness, we ﬁrst brieﬂy review some standard concepts from parameterised complexity theory [17]. A parameterized problem C is a computational problem with

input of the form hv; ki, where v ∈ {0, 1}∗ and k ∈ N (represented in unary) is called theparameter. An fpt-algorithm for C runs in time O(f (k).nc ) for some constant c, and somecomputable function f : N → N (both independent of input). Here, n is the size of the input.
So, an algorithm that runs in time O(nk ) is not an fpt-algorithm. The problem C is said to be
fixed-parameter tractable if it can be solved by an fpt-algorithm. There are classes of problems
in parameterized complexity that are widely believed not to be solvable by fpt-algorithms, e.g.,
W[1] (and others in the W-hierarchy). To show that a problem C is W[1]-hard, it suﬃces to give
an fpt-reduction to C from the short acceptance problem of nondeterministic Turing machines(NTM): given a tuple h(M, w); ki, where M is an NTM, w ∈ {0, 1}∗ is an input word, andk is a positive integer represented in unary, decide whether M accepts w in k steps. Amongothers, standard reductions in complexity theory that satisfy the following two conditions are
fpt-reductions: (1) fpt-algorithms, (2) if k is the input parameter, then the output parameteris O(k).
We now show that k-redundancy is W[1]-hard. To this end, we reduce from the short acceptance problem of nondeterministic Turing machines. The input to the problem is hM, w; ki,where M is an NTM, w is an input word for M, and k ∈ N given in unary. Suppose thatM = (Γ, Σ, ⊔, Q, ∆, q0 , qacc ), where Γ = {0, 1} is the input alphabet, Σ = {0, 1, ⊔} is the tapealphabet, ⊔ is the blank symbol, Q is the set of control states, ∆ ⊆ (Q × Σ) × (Q × Σ × {L, R})
is the transition relation (L/R signify go to left/right), q0 ∈ Q is the initial state, and qacc is
the accepting state. Each conﬁguration of M on w of length k can be represented as a word
(0, a0 , c0 )(1, a1 , c1 ) · · · (k, ak , ck )where ai ∈ Σ for each i ∈ [0, k], and for some j ∈ [0, k] we have cj ∈ Q and for all r 6= j it is thecase that cj = ⋆. Note that this is a word (of a certain kind) over Ω := Ωk := [0, k]×Σ×(Q∪{⋆}).
In the sequel, we denote by CONFk the set of all conﬁgurations of M of length k. Suppose thatw = a1 · · · an . If n < k, we append some blank symbols at the end of w and assume that|w| ≥ k. The initial conﬁguration will be I0 (w) := (0, ⊔, q0 )(1, a1 , ⋆) · · · (k, ak , ⋆). [Notice that
if n > k, then some part of the inputs will be irrelevant.] In the following, we will append thesymbol (−1, ⊔, ⋆) (resp. (k + 1, ⊔, ⋆)) before the start (resp. after the end) of M conﬁgurations
to aid our deﬁnitions. Therefore, deﬁne Ωe := Ωk,e := [−1, k + 1] × Σ × (Q ∪ {⋆}).
We now construct a tree-rewrite system P to simulate M. First oﬀ, for each ∆-rule σ,deﬁne a relation Rσ ⊆ Ω4e such that (~v1 , ~v2 , ~v3 , w)
~ ∈ R describes the update by rule σ of cell~v2 to w~ given the neighbouring cells ~v1 and ~v3 . That is, (~v1 , ~v2 , ~v3 , w)
~ ∈ R iﬀ a conﬁguration
C2 = ~u−1 · · · ~uk+1 of M, where ~ui+1 = w~ for some i, can be reached in one step S
using σ fromanother conﬁguration C1 = ~u′−1 · · · ~u′k+1 , where ~u′i ~u′i+1 ~u′i+2 = ~v1~v2~v3 . Let R = σ∈∆ Rσ . In
this case, we say that rule σ is a witness for the tuple (~v1 , ~v2 , ~v3 , w).
~ Notice that, given a rule
σ of P and ~v1 , ~v2 , ~v3 , there exists at most one w~ such that (~v1 , ~v2 , ~v3 , w)
~ ∈ R and is witnessedby σ. In addition, it is easy to see that checking whether (~v1 , ~v2 , ~v3 , w)
~ ∈ R can be done inpolynomial time (independent of k) since this is a simple local check of M rules.
The rewrite system P works over trees of labels Ξ = Ωe ∪ ∆. The initial tree is a tree witha single node labeled by I0 (w). We add the following rules to P:
1. For each σ ∈ ∆, we add (⊤, AddChild(σ)) to P.
2. For each (~vi−1 , ~vi , ~vi+1 , w)
~ ∈ R witnessed by σ ∈ ∆, for i ∈ [0, k], we add(σ ∧ h↑i{~vi−1 , ~vi , ~vi+1 }, AddClass(w))~
to P.

3. For each σ ∈ ∆, we add (σ, AddClass((−1, ⊔, ⋆))) and (σ, AddClass((k + 1, ⊔, ⋆))) to P.
Rule 1 ﬁrst guesses the rule σ to be applied to obtain the next conﬁguration C2 of the NTM
M. This rule is added as a class in the child v of the current node u containing the current
conﬁguration C1 . Rule 3 is then applied to obtain the left and right delimiter. After that,
conﬁguration C2 is written down in node v by applying Rule 2 for k times. In particular, thesystem will look up the rule σ that was guessed before and the content of the parent node u(i.e. C1 ). If we let S = [0, k] × Σ × {qacc }, then S is not k-redundant iﬀ M accepts w withink steps. Notice that this is an fpt-preserving reduction. In particular, it runs in time O(k c nd )for some constant c and d.

L

Proof of PSPACE-hardness in Theorem 4

We reduce to the k-redundancy problem, when k forms part of the input, from membershipof a linear bounded Turing machine. Note, since the runs of a linear bounded Turing machine
may be of exponential length, the encoding in the previous section no longer works.
Suppose the input TM is M = (Γ, Σ, ⊔, Q, ∆, q0 , qacc ), where Γ = {a, b} is an input alphabet,Σ = {a, b, ⊔} is the tape alphabet, ⊔ is the blank symbol, Q is the set of control states,∆ ⊆ (Q × Σ) × (Q × Σ × {L, R}) is the transition function (L/R signify go to left/right), q0 ∈ Q
is the initial state, and qacc is the accepting state. We are only interested in runs of M thatuse N := dn space for some constant d. Each conﬁguration of M on w can be represented as aword of length N + 1 in the alphabet Ω := ΩN , which was deﬁned in the proof of W[1]-hardness.
The initial conﬁguration I0 (w) is deﬁned to be(0, a0 , c0 )(1, a1 , c1 ) · · · (N, aN , cN )where a0 a1 · · · aN = ⊔w⊔(d−1)n , c0 = q0 , and c1 = · · · = cN = ⋆. In the following, we will alsouse extension Ωe := ΩN,e of Ω and the logspace-computability of the 4-ary relation ∆ ⊂ Ω4edeﬁned in that proof.
We now construct our rewrite system R, which works over the alphabet Ξ := {R, 0, 1} ∪ Ωe .
Let M := 2(N + log |Q| + log N ). Firstly, it suﬃces to consider runs of M of at most length
3N × |Q| × N < 2M since exceeding this length there must be a repeat of conﬁgurations by the
pigeonhole principle. Our initial conﬁguration is T0 = (D0 , λ0 ), where D = {ǫ} and λ0 (ǫ) = R.
We start by adding the following rules to R: (g, AddChild(0)) and (g, AddChild(1)), whereg = (h↑i)i R and i ∈ [0, M − 1]. These rules simply build trees of height M , into which thebinary tree of height M can be embedded. The label in any path from the root to a leaf node
gives us a number i in [0, 2M ] written in binary, which will in turn have a child representing
the ith conﬁguration of M from I0 (w) (which is unique since M is deterministic).
We now add the rule (g, AddChild({(−1, ⊔, ⋆), (N + 1, ⊔, ⋆)})), where g = (h↑i)M R. This
rule initialises the content of each conﬁguration (of a given branch).
Notation. For a guard g, a class c, and direction d ∈ {↑, ↓, ↑+, ↓+ }, we write chdig to meanc ∧ hdig.
The following set of rules deﬁnes the ﬁrst conﬁguration I0 (w) in the tree. For each i ∈ [0, N ],we add the rule (g, AddClass((i, ai , ci ))) g = h↑i(0h↑i)M−1 R.
We now add a set of rules for deﬁning subsequent conﬁgurations in the tree. The guard
will inspect a previous conﬁguration of the current conﬁguration. Based on this, it will add anappropriate content of each tape cell. Each of these rules will be of the form (g, AddChild(~v )),where ~v ∈ Ω. For each (~v1 , ~v2 , ~v3 , w)
~ and i ∈ [0, M − 1], we add a rule (g, AddChild(w))~ whereg := ⊤h↑iσi h↓i{~v1 , ~v2 , ~v3 } where σi = (0h↑i)i 1h↑i⊤h↓i0(h↓i1)i . The guard g selects precisely
the nodes containing the jth conﬁguration of M (there can be at most one jth conﬁguration of
M since M is deterministic), where j is a number whose binary representation ends with 10i .
The guard traverses the tree upward trying to ﬁnd the ﬁrst bit that is turned on (i.e. of form
10i ) and then looks at the complement of this bit pattern (i.e. of form 01i ).
Finally, if we set S = {(i, a, qF ) : i ∈ [0, N ], a ∈ Σ}, then S is not (M + 1)-redundant iﬀ
M accepts w. The reduction is easily seen to run in polynomial time. This completes our
reduction.

M

Proof of EXP-hardness in Theorem 3

We show that the redundancy problem for R is EXP-hard. To this end, we reduce membershipfor alternating linear bounded Turing machines, which is EXP-complete. An alternating Turingmachine is a tuple M = (Γ, Σ, ⊔, Q, ∆, q0 , qacc ), where Γ = {0, 1} is the input alphabet, Σ ={0, 1, ⊔} is the tape alphabet, ⊔ is the blank symbol, Q is the set of control states, ∆ ⊆ (Q×Σ)×(Q × Σ × {L, R})2 × {∧, ∨} is the transition relation. Given an M-conﬁguration C, a transition((q, a), (qL , aL , dL ), (qR , aR , dR ), s) spawns two new M-conﬁgurations CL and CR such that CL(resp. CR ) is obtained from C by applying a normal NTM transition ((q, a), (qL , aL , dL )) (resp.
((q, a), (qR , aR , dR ))). In this way, a run π of M is a binary tree, whose nodes are labeled by
M-conﬁgurations and additionally each internal (i.e. non-leaf) node is labeled by a transition
from ∆. To determine whether the run π is accepting, we construct a boolean circuit from π
as follows: (1) each internal node labeled by a transition ((q, a), (qL , aL , dL ), (qR , aR , dR ), s) is
replaced by a boolean operator s, and (2) assign 1 (resp. 0) to a leaf node if the conﬁgurationis (resp. is not) in the state qacc . The run π is accepting iﬀ the output of this circuit is 1.
We are only interested in tape conﬁgurations of size d.n for a constant integer d, where nis the length of the input word w. Therefore, each conﬁguration of M on input w is a word in
CONFN deﬁned in the proof of W[1]-hardness. As before, the initial conﬁguration I0 (w) is(0, a0 , c0 )(1, a1 , c1 ) · · · (N, aN , cN )where a0 a1 · · · aN = ⊔w⊔(d−1)n , c0 = q0 , and c1 = · · · = cN = ⋆. As before, we will also use
extension Ωe := ΩN,e of Ω and put a delimiter at the left/right end of each conﬁguration. For
each σ = ((q, a), (qL , aL , dL ), (qR , aR , dR ), s) ∈ ∆ and t ∈ {L, R}, we deﬁne a relation Rσ,t ⊆ Ω4e
as the log-computable relation Rσ′ deﬁned in the previous W[1]-hardness proof, where σ ′ is theNTM transition rule ((q, a), (qt , at , dt )).
Our rewrite system R will work over the set K := {root, success, L, R} ∪ Ωe ∪ ∆ of classes.
The initial conﬁguration is T0 = (D0 , λ0 ) with D0 = {ǫ} and λ0 (ǫ) = {root, (−1, ⊔, ⋆), (N +1, ⊔, ⋆)} ∪ {(i, ai , ci ) : i ∈ [0, N ]}. Deﬁne g := {root, success}, which is the guard we want tocheck for redundancy. Roughly speaking, our rewrite system R will guess an accepting run π
of M on the input word w. Each accepting conﬁguration (at the leaf) will then be labeled bysuccess. This label success will be propagated to the root of the tree according to the Mtransition that produce a M-conﬁguration in the tree. More precisely, we deﬁne R by adding
the following rewrite rules:
1. For each t ∈ {L, R},
σ = ((q, a), (qL , aL , dL ), (qR , aR , dR ), s) ∈ ∆and i ∈ [0, N ], add the rule((i, a, q), AddChild({σ, t, (−1, ⊔, ⋆), (N + 1, ⊔, ⋆)})

to R.
2. For each σ ∈ ∆, t ∈ {L, R}, and (~v1 , ~v2 , ~v3 , w)
~ ∈ Rσ,t , add the rule({t, σ}h↑i{~v1 , ~v2 , ~v3 }, AddClass(w))~
to R.
3. For each i ∈ [0, N ] and a ∈ Γ, add the rule({(i, a, qacc ), AddClass(success))
to R.
4. For each
σ = ((q, a), (qL , aL , dL ), (qR , aR , dR ), s) ∈ ∆if s = ∨, then add the rule(h↓i{σ, success}, AddClass(success)) .
If s = ∧, then add the rule(g, AddClass(success))where
g = h↓i{σ, success, L} ∧ h↓i{σ, success, R}
The ﬁrst rewrite rule spawns a child labeled by an M-transition σ and a symbol t ∈ {L, R} toindicate whether its a left/right child in the M-path to be guessed. The second rewrite rule
determines the conﬁguration of the current node (because an M-rule σ has been guessed). The
third rewrite rule adds a label success to accepting conﬁgurations. The fourth rewrite rulepropagates the label success upwards.
Our translation runs in polynomial-time. Furthermore, it is easy to see that M accepts w
iﬀ g is not redundant with respect to the rewrite system R and initial tree T0 . This completes
our reduction.

N

Implementation Optimisations

N.1

Limiting the Number of Rules

For each class c ∈ K we construct a symbolic pushdown system that is used to determine whether
the class c can be added at a certain node. We improve the performance of the pushdown
analysis by ﬁrst removing all rules of the rewrite system with rules R that cannot contributetowards the addition of class c at a node. We then perform analysis with the reduced set ofrules R′ . Since a rule is added for each CSS selector, with intermediate rules being introduced
to simplify the guards on the rules, the removal of irrelevant rules to a particular class can givesigniﬁcant gains.
We identify rules which may contribute to the addition of class c by a backwards ﬁxed point
algorithm. We begin by including in R′ all rules that either directly add the class c, or add achild to the tree. The reason we add all AddChild(B) rules is because new nodes may lead to
new guards being satisﬁed, even if the label of the new child does not appear in the guard (e.g.
h↑ia cannot be satisﬁed without a node labelled with a having a child).

Algorithm 1 Restricting R
Require: A class c ∈ K and a set R of rewrite rules.
Ensure: R′ contains all rules relevant to the addition of c.
{ σ ∈ R | σ = (g, AddClass(B)) ∧ c ∈ B } ∪R′ ={ σ ∈ R | σ = (g, AddChild(B)) }repeatfor all σ ∈ R′ and classes c′ appearing in σ do
R′ = R′ ∪ { (g, AddClass(B)) ∈ R | c′ ∈ B }end foruntil R′ reaches a ﬁxed point

We then search for any rules σ = (g, AddClass(B)) ∈ R such that there exists c′ ∈ B withc appearing in the guard of some rule in R′ . We add all such σ to R′ and iterate until a ﬁxed
point is reached. The full algorithm is given in Algorithm 1′

Proposition 3. Given a single-node tree T0 , assumption function f and a class c ∈ K, therewrite system R has a positive solution to the class-adding problem hT0 , f, c, Ri has a positive
answer iff the class-adding problem hT0 , f, c, R′ i has a positive answer.
Proof. The “if” direction is direct since R contains all rules in R′ . The “only-if” direction canbe shown by induction over the length of a sequence of rule applications σ1 , . . . , σn where σnadds class c to the tree. Note, we relax the proposition for the induction hypothesis, allowing
T0 to be any arbitrary tree.
In the base case n = 0 and the proof is immediate. Hence, assume for the tree T1 obtained′by applying σ1 to T0 we have, by induction, a sequence of rule applications σ1′ , . . . , σmwhich isa subsequence of σ1 , . . . , σm , resulting in the addition of class c. We need to show there exists
such a sequence beginning at T0 . There are several cases.
′
When σ1 = (g, AddChild(B)) then σ1 ∈ R′ and the sequence σ1 , σ1′ , . . . , σm
suﬃces.
′When σ1 = (g, AddClass(B)) there are three cases. If c ∈ B then σ1 ∈ R and the sequence′
σ1 suﬃces. If there is some c′ ∈ B used in the matching of some guard g ′ of a rule in σ1′ , . . . , σm
,
′
′
′
′
′
then, since c appears in a rule in R we have also σ1 ∈ R and the sequence σ1 , σ1 , . . . , σm′
suﬃces. Otherwise, no c′ ∈ B is used in the matching of some guard g ′ in σ1′ , . . . , σmand the′′sequence σ1 , . . . , σm suﬃces.

N.2

Limiting the Number of jMoped Calls

By performing global backwards reachability analyses with jMoped we in fact only need toperform one pushdown analysis per class c ∈ K. Given a set of target conﬁgurations, global
backwards reachability analysis constructs a representation of the set of conﬁgurations fromwhich a target conﬁguration may be reached.
Thus, we begin with the set of target conﬁgurations (q, a) where a = (b1 , . . . , bm ) ∈ {0, 1}mwith bi = 1 and bi = 1 indicates the addition of class c to the root node. The global backwards
reachability analysis of this target set then gives us a representation of all conﬁgurations thatcan eventually reach one of the targets, that is, add the class c. In particular, we obtain fromjMoped a BDD representing all hTv , f, c, Ri that have a positive answer to the class-adding
problem. We can then use this BDD to determine whether a given class-adding problem for c
represents a positive instance without having to use jMoped again.

N.3

Matching Guards Anywhere in the Tree

We can check whether a guard g is not matched anywhere in the tree by checking whetherg ∨ h↓+ ig is redundant. However, during the simpliﬁcation step this results in the addition ofa new class for each guard that has to be propagated up the tree.
We avoid this cost by checking directly whether a guard may be matched anywhere in thetree. After simpliﬁcation this amounts to checking whether a given class may be matchedanywhere in the tree. Hence, after we have saturated Tv , we do a ﬁnal check to detect whether
each class c that does not appear in the saturated tree might still be able to appear in a nodecreated by a sequence of AddChild(B) rules. To do this, we perform a similar class adding
check as above, except we test reachability of a conﬁguration of the form (q, w) where the top
character of the stack w is a = (b1 , . . . , bm ) ∈ {0, 1}m with bi = 1. That is, the node where c
was added does not have to be the root node. We obtain a single BDD per class as above, andcheck it against all assumption functions f that can represent nodes in the saturated tree.

O

HTML5 Translation

We informally describe here our process for extracting rules from HTML5 documents that use
jQuery. Note, this translation is for experimental purposes only and does not claim to be a
rigorous, systematic, or sound approach. It is merely to demonstrate the potential for extracting
interesting rewrite rules from real HTML5 and to obtain some representative benchmarks forour implementation. A robust dataﬂow analysis could in principle be built, and remains aninteresting avenue of future work.
We begin by describing how to translate complete jQuery calls that do not depend on theirsurrounding code. E.g.
$('.a').next().append('<div class="b"/>');
does not depend on any other code in the document, whereas$(x).next().append('<div class="b"/>');
depends on the value of the x variable. We will describe in a later section how we track
variables, although we will make mention in when translating jQuery calls section when aparticular variable receives a given value. First we describe the translation of CSS selectors andjQuery calls.

O.1

CSS Selectors

We translate the following subset of CSS selectors.
• Each class, element type, or ID is directly translated to a class in our model with thesame name.
• Conjunctions of guards are translated to sets of classes. E.g. div.selected.item becomes{div, selected, item}.
• Descendant relations are encoded using h↑+ i. That is x y, where x and y are selectors
with translations into guards g and g ′ respectively becomes h↑+ ig ∧ g ′ .
• Child relations are encoded using h↑i. That is x > y, where x and y are selectors withtranslations into guards g and g ′ respectively becomes h↑ig ∧ g ′ .

O.2

jQuery Calls

Given a jQuery call of the form$(s).f(x)....g(y).h(z)where s is a CSS selector string and f(x)....g(y).h(z) is a sequence of jQuery calls, we canextract new rules as follows. We recursively translate the sequence of calls $(s).f(x)....g(y)where $(s) is the base case, and obtain from the recursion a guard reﬂecting the nodes matchedby the calls. Then we generate a rule depending on the eﬀect of h(z).
Note that the call to $(s) returns a jQuery object which contains within it a stack of setsof nodes matched. When s is just a CSS selector this stack will contain a single element thatis the set of nodes matched by s. Each function in the sequence f(x)....g(y).h(z) receives
as its this object the jQuery object and obtains a new set of nodes derived from the nodes on
the top of the stack. This new set is then pushed onto the stack and passed to the next callin the sequence. There is a jQuery function end() that simply pops the top element from thestack and passes the remaining stack to the next call. We model this stack as a stack of guards
during our translation.
We start with the base case $(s). In this case we translate the CSS selector s into a guard
g and return the single-element stack g. Note: this assumes s is a string constant. Otherwise
we set g to be true (i.e. matches any node).
In the recursive case we have a call l.f(x) where l is a sequence of jQuery calls and f(x)is a jQuery call. We obtain a stack σ by recursive translation of l and then do a case split on
f. In each case we obtain a new stack ρ which is returned by the recursive call. In some cases
we also add new rules to our translated model. We describe the currently supported functions
below. In all cases, let σ = σ ′ g. Note, our implementation directly supports h↓∗ iϕ which isequivalent to h↓+ iϕ ∨ ϕ, and similarly for h↑∗ iϕ.
• animate(...): we return ρ = σ.
• addBack(): let σ = σ ′′ g ′ g, we set ρ = σ ′′ (g ∨ g ′ ).
• addClass(c): set ρ = σ and add the rule (g, AddClass({c})) when c is a string constant(otherwise add all classes).
• ajax(...): we attempt to resolve all functions f in the argument to the call to constantfunctions (usually this coded directly in place by the programmer). If we are able to do
this, we translate f with the this variable set to σ. We return ρ = σ. If we cannot resolve
f we ignore it (the body of f will be translated elsewhere with this matching any node).
• append(s): we attempt to obtain a constant string from s. If s is a concatenation ofstrings and variables, we attempt to resolve all variables to strings. If we fail, we make thesimplifying assumption that variables do not contain HTML code (this can be controlled
via the command line) and omit them from the concatenation. If we are able to obtaina constant HTML string in this way we use a sequence of new rules and classes to buildthat tree at the nodes selected by g. E.g. (g, AddChild({x, a})), ({x}, AddChild({b})),({x}, AddChild({c})) where x is a fresh class adds a sub-tree containing a node with class“a” with two children with classes “b” and “c” respectively. In the case where we cannot
ﬁnd a constant string (e.g. if we assume variables may contain HTML strings), we simply
add rules to construct all possible sub-trees.

• bind(..., f): we attempt to resolve f to a constant function (usually this is provided
directly by the programmer). If we are able to do this, we translate f with the thisvariable set to σ. We return ρ = σ. If we cannot resolve f we ignore it (the body of fwill be translated elsewhere with this matching any node)• blur(f): we treat this like a call to bind(..., f).
• children(s): we ﬁrst obtain from the CSS selector s a guard g ′ (or true if s is notconstant), then we set ρ = σ(h↑ig ∧ g ′ ).
• click(f ): same as blur().
• closest(s): we ﬁrst obtain from the CSS selector s a guard g ′ (or true if s is notconstant), then we set ρ = σ(h↓∗ ig ∧ g ′ ).
• data(...): we return ρ = σ.
• each(f ): we attempt to resolve f to a constant, as with click. The function f may take0 or 2 arguments (the second being the matched element). In both cases we translate fwith this set to σ. If it has arguments, then the second argument is also set to σ. We
return ρ = σ.
• eq(...): we return ρ = σg.
• fadeIn(...): we return ρ = σ.
• fadeOut(...): we return ρ = σ.
• focus(f): same as blur().
• end(): we return ρ = σ ′ .
• find(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant), thenwe set ρ = σ(h↑+ ig ∧ g ′ ).
• filter(...): we simply return ρ = σg.
• first(...): we simply return ρ = σg.
• has(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant), thenwe set ρ = σ(h↓+ ig ′ ∧ g).
• hover(f1,f2 ): we attempt to resolve f1 and f2 to constant functions (else we ignore
them to be translated elsewhere with less precise guards). Both f1 and f2 take a single
argument, which is the element being hovered over. We translate both functions with theargument and the this variable set to σ.
• html(s): this is handled like append.
• next(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or not
supplied), then we set ρ = σ(h↑ih↓ig ∧ g ′ ).
• nextAll(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or
not supplied), then we set ρ = σ(h↑ih↓ig ∧ g ′ ).
• not(...): we ignore the negation and simply return ρ = σg.

• on(e,s,f ): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or
not supplied), and we attempt to resolve f to a constant function (like click). We thentranslate f with this set to σ(h↑+ ig ∧ g ′ ). We return with ρ = σ.
• parent(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or
not supplied), then we set ρ = σ(h↓ig ∧ g ′ ).
• parents(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or
not supplied), then we set ρ = σ(h↓+ ig ∧ g ′ ).
• prepend(s): this is handled like append.
• prev(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or not
supplied), then we set ρ = σ(h↑ih↓ig ∧ g ′ ).
• prevAll(s): we obtain from the CSS selector s a guard g ′ (or true if s is not constant or
not supplied), then we set ρ = σ(h↑ih↓ig ∧ g ′ ).
• remove(s): this function is ignored and we return ρ = σ.
• removeClass(s): this function is ignored and we return ρ = σ.
• resize(f): same as blur().
• show(...): we return ρ = σ.
• slideUp(...): we return ρ = σ.
• slideDown(...): we return ρ = σ.
• stop(...): we return ρ = σ.
• val(...): we return ρ = σg.
We also ignore the following functions that do not return a jQuery object or manipulate theDOM tree: extend(), hasClass(), height(), is(), width().

O.3

More Complex JavaScript

In reality, it is rare for jQuery statements to be completely independent of the rest of the code.
We extend our translation by identifying common jQuery programming patterns to enable thegeneration of more precise rules. This is, in eﬀect, a kind of ad-hoc dataﬂow analysis over thesyntax tree of the JavaScript.
We remark that current JavaScript static analysers do not track the kind of informationneeded to build meaningful guards from the jQuery calls. Indeed, implementing a systematic dataﬂow analysis for propagating jQuery guards remains an interesting avenue of future
research.
Often a call will take the form$(x).f(y)for some variable x. In the worst case one can assume any value for guards derived from x byusing the guard ⊤. In other cases it is possible to be more precise.
When translating a call such as

$('.a').each(function () {$(this).addClass('b');));
for example, is it easy to infer that the selection returned by the this variable is all elementswith the class “a”. Hence, when we are translating constant functions such as these, we track
the guards in the this variable as described in the previous section. Similarly, if we wrote$('.a').each(function (i, e) {$(e).addClass('b');));
we pass the stack of guards from the $('a') selector to the e variable, and are thus able tointerpret $(e).
Note, we are also able to translate $(s, x) where x is this or some variable known to holda jQuery object with stack σg by using the guardh↑+ ig ∧ g ′where g ′ is the guard obtained from the selector s. Similarly $(document) can be translated
to the root node of the HTML.
We can further improve the analysis by tracking variables declared in the JavaScript. To
this end, we identify all variables that are assigned outside of a loop or conditional variable(i.e. assigned only once) and remember their value for use in later translations. This capturescommon cases such as
var eles = $('myelements');...
eles.addClass('b');
eles.append('<p>Some test.</p>');Finally, we also provide some support for user-deﬁned jQuery functions. In a preprocessing
step, we look for lines of the form$.fn.f = function (args) { ... };and keep a map from f to the function deﬁnition. Thus, when we ﬁnd elsewhere in the code ajQuery call of the form...f(params)...
we can translate the function body of f with the this variable set to the current jQuery stack,any parameters can be passed to the arguments of the function. Note, if we discover a line off which overwrites a parameter variable, we will forget the value passed from the call and use
a top value instead.