Submission received: February 21, 2017; revised submission received: ?;
accepted for publication: ?.

# On the Complexity of CCG Parsing

Marco Kuhlmann Department of Computer and Information Science, Linköping
University, 581 83 Linköping, Sweden. E-mail<EMAIL_ADDRESS>Linköping
University  Giorgio Satta Department of Information Engineering, University of
Padua, via Gradenigo 6/A, 35131 Padova, Italy. E-mail<EMAIL_ADDRESS>University of Padua  Peter Jonsson Department of Computer and Information
Science, Linköping University, 581 83 Linköping, Sweden. E-mail:
<EMAIL_ADDRESS>Linköping University

###### Abstract

We study the parsing complexity of Combinatory Categorial Grammar (CCG) in the
formalism of Vijay-Shanker and Weir (1994). As our main result, we prove that
any parsing algorithm for this formalism will take in the worst case
exponential time when the size of the grammar, and not only the length of the
input sentence, is included in the analysis. This sets the formalism of Vijay-
Shanker and Weir (1994) apart from weakly equivalent formalisms such as Tree-
Adjoining Grammar (TAG), for which parsing can be performed in time polynomial
in the combined size of grammar and input sentence. Our results contribute to
a refined understanding of the class of mildly context-sensitive grammars, and
inform the search for new, mildly context-sensitive versions of CCG.

##  1 Introduction

Combinatory Categorial Grammar (CCG; Steedman and Baldridge, 2011) is a well-
established grammatical framework that has supported a large amount of work
both in linguistic analysis and natural language processing. From the
perspective of linguistics, the two most prominent features of CCG are its
tight coupling of syntactic and semantic information, and its capability to
compactly encode this information entirely within the lexicon. Despite the
strong lexicalization that characterizes CCG, it is able to handle non-local
dependencies in a simple and effective way (Rimell, Clark, and Steedman,
2009). After the release of annotated datasets (Hockenmaier and Steedman,
2007), there has been a surge of interest in CCG within statistical and, more
recently, neural natural language processing. The wide range of applications
for which CCG has been used includes data-driven syntactic parsing (Clark and
Curran, 2007; Zhang and Clark, 2011), natural language generation (White,
Clark, and Moore, 2010; Zhang and Clark, 2015), machine translation (Lewis and
Steedman, 2013), and broad-coverage semantic parsing (Lewis and Steedman,
2014; Lee, Lewis, and Zettlemoyer, 2016).

In this article we study the parsing complexity of CCG. Our point of departure
is the work of Vijay-Shanker and Weir (1990), who presented the first
polynomial-time parsing algorithm for CCG. The runtime complexity of this
algorithm is in ${\cal O}({n^{6}})$, where $n$ is the length of the input
sentence. This matches the runtime complexity of standard parsing algorithms
for Tree-Adjoining Grammar (TAG, Schabes, 1990), which fits nicely with the
celebrated result that CCG and TAG are weakly equivalent (Weir and Joshi,
1988; Vijay-Shanker and Weir, 1994). However, while the runtime of Vijay-
Shanker and Weir’s algorithm is polynomial in the length of the input
sentence, it is _exponential_ in the size of the grammar. This is in contrast
with the situation for TAG, where the runtime is (roughly) quadratic with
respect to grammar size (Schabes, 1990). The only other polynomial-time
parsing algorithms for CCG that we are aware of (Vijay-Shanker and Weir, 1993;
Kuhlmann and Satta, 2014) exhibit the same behaviour. Kuhlmann and Satta
(2014) ask whether parsing may be inherently more complex for CCG than for TAG
when grammar size is taken into account. Our main technical result in this
article is that the answer to this question is positive: We show that _any_
parsing algorithm for CCG in the formalism considered by Vijay-Shanker and
Weir will _necessarily_ take in the worst case exponential time when the size
of the grammar is included in the analysis. Formally, we prove that the
universal recognition problem for this formalism is EXPTIME-complete. The
following paragraphs provide some context to this result.

##### The Mild Context-Sensitivity of Modern CCG

Our interest in the computational properties of CCG is motivated by our desire
to better understand modern incarnations of this framework from a mathematical
point of view. Theoretical work on CCG has always emphasized the importance of
keeping the computational and generative power of the grammar as low as
possible (see for instance Steedman, 2000, p. 23, and Baldridge, 2002, Section
2.5), and in doing so has followed the tradition of the so-called mildly
context-sensitive theories of grammar. The aforementioned polynomial-time
parsing algorithm and the weak equivalence with TAG established the membership
of CCG in this class of grammars even on a formal level. However, recent work
has drawn attention to the fact that the specific formalism for which these
results were obtained, and which we will refer to as VW-CCG (after Vijay-
Shanker and Weir), differs from contemporary versions of CCG in several
important aspects. In particular, it allows to restrict and even ban the use
of combinatory rules on a per-grammar basis, whereas modern CCG postulates one
universal set of rules, controlled by a fully lexicalized mechanism based on
typed slashes, as in other approaches to categorial grammar (Baldridge, 2002;
Steedman and Baldridge, 2011). The difference is important because the weak
equivalence result crucially depends on the availability of grammar-specific
rule restrictions—without this feature, the generative power of VW-CCG is
strictly smaller than that of TAG (Kuhlmann, Koller, and Satta, 2015). At the
same time, modern CCG includes combinatory rules that are absent from VW-CCG,
specifically substitution and type-raising, and there is the possibility that
this can counterbalance the loss of generative power that comes with the
lexicalization of the rule control mechanism. Then again, these new rules are
not supported by existing polynomial-time parsing algorithms. Moreover, the
weak equivalence proof uses another feature of VW-CCG that is not available in
contemporary versions of CCG: the ability to assign lexicon entries to the
empty string. Such “empty categories” are ruled out by one of the fundamental
linguistic principles of CCG, the Principle of Adjacency (Steedman, 2000, p.
54), and it is far from obvious that the weak equivalence proof can be re-
written without them. In summary, the formalism of Vijay-Shanker and Weir is
the only CCG formalism that has been proved to be weakly equivalent to
TAG,111Baldridge and Kruijff (2003) show that the weak generative power of
their formalism for multi-modal CCG is _at most as_ strong as that of TAG, but
they do not show that it is _at least as_ strong. and the only one that has
been shown to be parsable in polynomial time. As such, it is arguably the only
CCG formalism that has been shown to be mildly context-sensitive, which is why
we consider it to be of continued interest from a mathematical point of view.
At the same time, we hope that the insights that we can obtain from the
analysis of VW-CCG will eventually lead to the development of linguistically
more adequate, provably mildly context-sensitive formalisms for CCG.

##### Universal Recognition

The _universal recognition problem_ for a class of grammars $\mathcal{G}$ is
the problem defined as follows: Given as input a grammar $G$ in $\mathcal{G}$
and a string $w$, decide whether $w$ is in $L(G)$, the language generated by
$G$. The computational complexity of this problem is measured as a function of
the combined size of $G$ and $w$. The universal recognition problem should be
contrasted with the _membership problem_ for any specific grammar $G$ in
$\mathcal{G}$, whose complexity is measured as a function solely of the length
of $w$. The complexity of the universal recognition problem is generally
higher than that of the membership problem. For instance, the universal
recognition problem for context-free grammars is PTIME-complete (complete for
decision problems solvable in deterministic polynomial time), whereas the
membership problem for these grammars defines the class LOGCFL (decision
problems reducible in logarithmic space to a context-free language), which is
generally conjectured to be a proper subset of PTIME.

The definitions of the universal recognition problem and the membership
problem often generate some confusion. For instance, in applications such as
parsing or translation, we work with a _fixed_ grammar, so it might seem that
the universal recognition problem is of little practical relevance. However,
it is worth remembering that for these applications, we are primarily
interested in the structural descriptions that the grammar assigns to a
generated sentence, not in the membership of the sentence _per se_. Therefore
the universal recognition problem is a more accurate model of parsing than the
membership problem, as the latter also admits decision procedures where the
grammar is replaced with some other mechanism that may produce no or
completely different descriptions than the ones we are interested in. The
universal recognition problem is also favoured when the ambition is to
characterize parsing time in terms of all relevant inputs—both the length of
the input string and the size and structure of the grammar (Ristad, 1986).
Such an analysis often reveals (and does so even in this article) how specific
features of the grammar contribute to the complexity of the parsing task. More
precisely, when investigating the universal recognition problem one expresses
the computational complexity of parsing in terms of several parameters (other
than the input string length), as for instance the number of nonterminals,
maximum size of rules, or maximum length of unary derivations. This provides a
much more fine-grained picture than the one that we get when analyzing the
membership problem, and discloses the effects that each individual feature of
the grammar has on parsing.

##### Structure of the Article

The remainder of this article is structured as follows. After presenting the
VW-CCG formalism in Section 2, we first study in Section 3 the universal
recognition problem for a restricted class of VW-CCG, where each category is
“lexicalized” in the sense of the Principle of Adjacency. We show that for
this subclass, universal recognition is NP-complete. Under the assumption that
PTIME $\neq$ NP, this already implies our main result that parsing algorithms
for VW-CCG will take in the worst case exponential time in the combined size
of the grammar and the input string. In Section 4 we analyze the general case
and show that the universal recognition problem for unrestricted VW-CCG is
EXPTIME-complete. This is a stronger result than the one in Section 3, as it
does not rely on any assumptions. However, we anticipate that many readers
will be content with the result in Section 3, especially since the proofs of
the more general result are considerably more complex. Finally, Section 5 is
devoted to a general discussion of our results, its ramifications, and its
relevance for current research.

##  2 Preliminaries

In this section we present the VW-CCG formalism. We assume the reader to be
already familiar with the basic notions of categorial grammar, and in
particular with the idea of categories as syntactic types. Like other
categorial formalisms, a VW-CCG grammar has two central components: a lexicon,
which specifies the categories for individual words, and a set of rules, which
specify how to derive the categories of longer phrases from the categories of
their constituent parts.

###  2.1 Lexicon

The VW-CCG lexicon is a set of pairs $\sigma\mathrel{:=}X$, where $\sigma$ is
a word (formalized as a symbol from some finite vocabulary) and $X$ is a
category. Formally, the set of categories over a given set ${\mathcal{A}}$ is
the smallest set $\mathcal{C}({\mathcal{A}})$ such that  (i)
${\mathcal{A}}\subseteq\mathcal{C}({\mathcal{A}})$and  (ii) if
$X\in\mathcal{C}({\mathcal{A}})$ and $Y\in\mathcal{C}({\mathcal{A}})$ then
$X/Y\in\mathcal{C}({\mathcal{A}})$ and
$X\mathord{\reflectbox{$/$}}Y\in\mathcal{C}({\mathcal{A}})$.  Categories of
form (i) are called atomic, those of form (ii) are called complex.

##### Categories as Stacks

Categories are usually viewed as directed versions of the function types in
the simply-typed lambda calculus. Here we follow authors such as Baldridge
(2002, p. 195f.) and view them as _stacks_. We treat slashes as left-
associative operators and omit unncessary parentheses. This lets us to write
every category $X\in\mathcal{C}({\mathcal{A}})$ in the form

$X\;=\;A\mathnormal{|}_{1}X_{1}\cdots\mathnormal{|}_{m}X_{m}$

where $m\geq 0$, $A\in{\mathcal{A}}$ is an atomic category that we call the
target of $X$, and the $\mathnormal{|}_{i}X_{i}$ are slash–category pairs that
we call the arguments of $X$. Based on this notation we view $X$ as a pair
consisting of the target $A$ and a stack whose elements are the arguments of
$X$, with the argument $\mathnormal{|}_{m}X_{m}$ at the top of the stack. Note
that arguments can in general contain complex categories.

$\vphantom{([q^{+}\hat{S}])}\text{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to198.44994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{We}}\vphantom{([q^{+}\hat{S}])}\text{S}\mathord{\reflectbox{$/$}}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to132.29996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{prove}}\vphantom{([q^{+}\hat{S}])}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.14998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}/\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{two}}\@deduce{}[\vbox
to66.14998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{theorems}}$
Figure 1: A sample derivation tree for the sentence “We prove two theorems”.

######  Example 2.1.

In the derivation shown in Figure 1, lexicon assignments are indicated by
dotted lines: The verb _prove_ for example is associated with the complex
category $(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}$. In our
notation, the same category can also be written as
$\text{S}\mathord{\reflectbox{$/$}}\text{NP}/\text{NP}$. The target of this
category is S, and the stack consists of the two arguments
$\mathord{\reflectbox{$/$}}\text{NP}$ and $/\text{NP}$, with $/\text{NP}$ at
the top of the stack. Note that we follow the standard convention in CCG and
draw derivations with the leaves at the top and the root at the bottom.

###  2.2 Rules

$\displaystyle X/Y\quad Y$ $\displaystyle\quad\Rightarrow\quad X$ (forward
application) (1) $\displaystyle Y\quad X\mathord{\reflectbox{$/$}}Y$
$\displaystyle\quad\Rightarrow\quad X$ (backward application) (2)
$\displaystyle X/Y\quad Y/Z$ $\displaystyle\quad\Rightarrow\quad X/Z$ (forward
harmonic composition) (3) $\displaystyle X/Y\quad
Y\mathord{\reflectbox{$/$}}Z$ $\displaystyle\quad\Rightarrow\quad
X\mathord{\reflectbox{$/$}}Z$ (forward crossed composition) (4) $\displaystyle
Y\mathord{\reflectbox{$/$}}Z\quad X\mathord{\reflectbox{$/$}}Y$
$\displaystyle\quad\Rightarrow\quad X\mathord{\reflectbox{$/$}}Z$ (backward
harmonic composition) (5) $\displaystyle Y/Z\quad
X\mathord{\reflectbox{$/$}}Y$ $\displaystyle\quad\Rightarrow\quad X/Z$
(backward crossed composition) (6) Figure 2: The combinatory schemata with
degree $0$ (application; top) and $1$ (composition; bottom).

The rules of VW-CCG are derived from two combinatory schemata,

$\displaystyle{\hbox{\pagecolor{yellow!60}\mathstrut$X/Y$}}\quad
Y\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}$
$\displaystyle\quad\Rightarrow\quad
X\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}$ (forward schema)
$\displaystyle
Y\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}\quad{\hbox{\pagecolor{yellow!60}\mathstrut$X\mathord{\reflectbox{$/$}}Y$}}$
$\displaystyle\quad\Rightarrow\quad
X\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}$ (backward schema)

where $d\geq 0$, the $\mathnormal{|}_{i}$ are slashes (forward or backward),
and $X$, $Y$ and the $Z_{i}$ are variables ranging over categories. Each
schema specifies how to combine a primary input category (highlighted) and a
secondary input category into an output category. The integer $d$ is called
the degree of the schema. Rules derived from the schemata where $d=0$ are
called application rules; the others are called composition rules.

######  Example 2.2.

Figure 2 shows all (six) combinatory schemata with degree at most 1, together
with their conventional names. In the derivation shown in Figure 1, each
branching of the tree is annotated with the schema used in that step.

A combinatory rule over a set of categories $\mathcal{C}({\mathcal{A}})$ is
obtained from a combinatory schema by optionally restricting the ranges of
some of the variables. Two types of restrictions are possible:  (i) We may
require the variable $Y$ or any of the $Z_{i}$ to take the value of some
specific category in $\mathcal{C}({\mathcal{A}})$. For example, we could
derive a restricted version of backward crossed composition that applies only
if $Y=\text{S}\mathord{\reflectbox{$/$}}\text{NP}$:
$(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/Z\quad
X\mathord{\reflectbox{$/$}}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})\quad\Rightarrow\quad
X/Z$ (7) (ii) We may restrict the range of the variable $X$ to categories with
a specific target $A\in{\mathcal{A}}$. For example, we could restrict backward
crossed composition to apply only in situations where the target of $X$ is S,
the category of complete sentences. We denote the resulting rule using the
“$\mathinner{\$}$” notation of Steedman (2000), where the symbol
$\mathinner{\$}$ is used as a variable for the part of the category stack
below the topmost stack element:
$Y/Z\quad\text{S}\mathinner{\$}\mathord{\reflectbox{$/$}}Y\quad\Rightarrow\quad\text{S}\mathinner{\$}/Z$
(8)

$\vphantom{([q^{+}\hat{S}])}\text{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to327.3333pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{Kahn}}\vphantom{([q^{+}\hat{S}])}\text{S}\mathord{\reflectbox{$/$}}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{blocked}}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})\mathord{\reflectbox{$/$}}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})}{\vphantom{([q^{+}\hat{S}])}\text{skillfully}}\vphantom{([q^{+}\hat{S}])}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}/\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{a}}\vphantom{([q^{+}\hat{S}])}\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{N}/\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{powerful}}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{shot}}\vphantom{([q^{+}\hat{S}])}\text{N}\mathord{\reflectbox{$/$}}\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{N}\mathord{\reflectbox{$/$}}\text{N})/\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{by}}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{Rivaldo}}$

$\vphantom{([q^{+}\hat{S}])}\text{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to392.79996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}}{\vphantom{([q^{+}\hat{S}])}\hbox
to0.0pt{\hss*\leavevmode\nobreak\
}\text{Kahn}}\vphantom{([q^{+}\hat{S}])}\text{S}\mathord{\reflectbox{$/$}}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to261.86664pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{blocked}}\@deduce{}[\vbox
to261.86664pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})\mathord{\reflectbox{$/$}}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})}{\vphantom{([q^{+}\hat{S}])}\text{skillfully}}\vphantom{([q^{+}\hat{S}])}\text{NP}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to261.86664pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}/\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{a}}\vphantom{([q^{+}\hat{S}])}\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}\text{N}/\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to130.93332pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{N}/\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{powerful}}\vphantom{([q^{+}\hat{S}])}\text{N}\mathord{\reflectbox{$/$}}\text{N}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}(\text{N}\mathord{\reflectbox{$/$}}\text{N})/\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{by}}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{NP}}{\vphantom{([q^{+}\hat{S}])}\text{Rivaldo}}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\text{N}}{\vphantom{([q^{+}\hat{S}])}\text{shot}}$

Figure 3: Overgeneration caused by unrestricted backward crossed composition.

######  Example 2.3.

Backward crossed composition (6) can be used for the analysis of heavy NP
shift in sentences such as _Kahn blocked skillfully a powerful shot by
Rivaldo_ (example from Baldridge, 2002). A derivation for this sentence is
shown in the upper half of Figure 3. However, the schema cannot be universally
active in English, as this would cause the grammar to also accept strings such
as _*Kahn blocked skillfully a powerful by Rivaldo shot_ , which is witnessed
by the derivation in the lower half of Figure 3 (a dagger $\dagger$ marks the
problematic step). To rule out this derivation, instead of the unrestricted
schema, a VW-CCG grammar of English may select only certain instances of this
schema as rules, in particular instances that combine the two restrictions in
(7) and (8). In this way the unwanted derivation in Figure 3 can be blocked,
while the other derivation is still admissible. Other syntactic phenomena
require other grammar-specific restrictions, including the complete ban of
certain combinatory schemata (cf. Steedman, 2000, Sections 4.2.1–4.2.2).

A ground instance of a combinatory rule over $\mathcal{C}({\mathcal{A}})$ is
obtained by replacing every variable with a concrete category from
$\mathcal{C}({\mathcal{A}})$. We denote ground instances using a triple arrow.
For example, the two instances of backward crossed composition in Figure 3
are:

$(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}\;\;(\text{S}\mathord{\reflectbox{$/$}}\text{NP})\mathord{\reflectbox{$/$}}(\text{S}\mathord{\reflectbox{$/$}}\text{NP})\;\;\Rrightarrow\;\;(\text{S}\mathord{\reflectbox{$/$}}\text{NP})/\text{NP}\qquad\qquad\text{N}/\text{N}\;\;\text{N}\mathord{\reflectbox{$/$}}\text{N}\;\;\Rrightarrow\;\;\text{N}/\text{N}$

Every combinatory rule over $\mathcal{C}({\mathcal{A}})$ has infinitely many
ground instances. In particular, the variable $X$ in such a rule can be
replaced with infinitely many concrete categories.

###  2.3 Grammars

A VW-CCG grammar fixes a finite lexicon and a finite set of combinatory rules.
Formally, a grammar is defined as a structure
$G=(\Sigma,{\mathcal{A}},{\mathrel{:=}},R,S)$ where $\Sigma$ is a finite
vocabulary, ${\mathcal{A}}$ is a finite set of atomic categories,
${\mathrel{:=}}$ is a finite relation between the sets
$\Sigma_{\varepsilon}=\Sigma\cup\\{\varepsilon\\}$ and
$\mathcal{C}({\mathcal{A}})$, $R$ is a finite set of combinatory rules over
$\mathcal{C}({\mathcal{A}})$, and $S\in{\mathcal{A}}$ is a distinguished
atomic category. In what follows, we simply refer to the elements of $R$ as
rules.

##### Derivations

Derivations of $G$ are represented as binary trees whose nodes are labeled
with either lexicon entries (leaves) or categories (inner nodes). In order to
represent such trees by linear terms, we use the following notation. Let $A$
be some unspecified alphabet. For $a\in A$, the term $a$ represents a tree
with a single node labeled by $a$. For tree terms $t_{1},\dots,t_{m}$, $m\geq
1$, the term $a(t_{1},\ldots,t_{m})$ represents the tree whose root node is
labeled by $a$ and has $m$ children, which are the root nodes of the trees
represented by $t_{1},\dots,t_{m}$. With this notation, we define the set of
derivation trees of $G$ and the associated mappings top (which returns the
category at the root node of the tree) and yield (which returns the left-to-
right concatenation of the symbols at the leaves) recursively as follows:

  * •

Every lexicon entry $\sigma\mathrel{:=}X$ forms a (single-node) derivation
tree $\tau$. We define $\text{{top}}(\tau)=X$ and
$\text{{yield}}(\tau)=\sigma$.

  * •

Let $\tau_{L}$ and $\tau_{R}$ be derivation trees with
$\text{{top}}(\tau_{L})=X_{L}$, $\text{{yield}}(\tau_{L})=w_{L}$,
$\text{{top}}(\tau_{R})=X_{R}$, and $\text{{yield}}(\tau_{R})=w_{R}$, and let
$X_{L}\;X_{R}\Rrightarrow X$ be a ground instance of some combinatory rule in
$R$. Then $\tau=X(X_{L},X_{R})$ is a derivation tree. We define
$\text{{top}}(\tau)=X$ and $\text{{yield}}(\tau)=w_{L}w_{R}$, where
juxtaposition denotes string concatenation.

The connection between this formal definition and the graphical notation for
derivation trees that we have used in Figure 1 and Figure 3 should be clear.
The only thing to note is that in a formal derivation tree, leaf nodes
correspond to lexicon entry $\sigma\mathrel{:=}X$, while in our graphical
notation, leaf nodes are split into a parent node with the category $X$ and a
child, leaf node with the symbol $\sigma$.

##### Generated Language

Based on the concept of derivation trees, we can now define the string
language generated by a grammar $G$. The grammar $G$ generates a string $w$ if
there exists a derivation tree whose root node is labeled with the
distinguished category $S$ and whose yield equals $w$. The language generated
by $G$, denoted by $L(G)$, is the set of all strings generated by $G$. As
mentioned before, Weir and Joshi (1988) and Vijay-Shanker and Weir (1994) show
VW-CCG generates the same class of languages as Tree-Adjoining Grammar (TAG;
Joshi and Schabes, 1997).

$\vphantom{([q^{+}\hat{S}])}S\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to392.79996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}A}{\vphantom{([q^{+}\hat{S}])}\mathstrut
a}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to327.3333pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}A}{\vphantom{([q^{+}\hat{S}])}\mathstrut
a}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A\mathord{\reflectbox{$/$}}A\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A\mathord{\reflectbox{$/$}}A/\hat{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A\mathord{\reflectbox{$/$}}A/\hat{S}/B\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A/\hat{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A/\hat{S}/B}{\vphantom{([q^{+}\hat{S}])}\mathstrut\varepsilon}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}B}{\vphantom{([q^{+}\hat{S}])}\mathstrut
b}\@deduce{}[\vbox
to130.93332pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\hat{S}\mathord{\reflectbox{$/$}}A/\hat{S}/B}{\vphantom{([q^{+}\hat{S}])}\mathstrut\varepsilon}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}B}{\vphantom{([q^{+}\hat{S}])}\mathstrut
b}\@deduce{}[\vbox
to261.86664pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\hat{S}}{\vphantom{([q^{+}\hat{S}])}\varepsilon}$

$\vphantom{([q^{+}\hat{S}])}S\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to327.3333pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}A}{\vphantom{([q^{+}\hat{S}])}\mathstrut
a}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A/\hat{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}S\mathord{\reflectbox{$/$}}A/\hat{S}/B}{\vphantom{([q^{+}\hat{S}])}\mathstrut\varepsilon}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}B}{\vphantom{([q^{+}\hat{S}])}\mathstrut
b}\vphantom{([q^{+}\hat{S}])}\hat{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to196.39998pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}A}{\vphantom{([q^{+}\hat{S}])}\mathstrut
a}\vphantom{([q^{+}\hat{S}])}\hat{S}\mathord{\reflectbox{$/$}}A\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}\hat{S}\mathord{\reflectbox{$/$}}A/\hat{S}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\hat{S}\mathord{\reflectbox{$/$}}A/\hat{S}/B}{\vphantom{([q^{+}\hat{S}])}\mathstrut\varepsilon}\@deduce{}[\vbox
to65.46666pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}B}{\vphantom{([q^{+}\hat{S}])}\mathstrut
b}\@deduce{}[\vbox
to130.93332pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}\hat{S}}{\vphantom{([q^{+}\hat{S}])}\mathstrut\varepsilon}$

Figure 4: Two derivations of the grammar from Example 3.3 of Vijay-Shanker and
Weir (1994).

######  Example 2.4.

Vijay-Shanker and Weir (1994) construct the following VW-CCG $G$ (Example
3.3). We only specify the lexicon and the set of rules; the vocabulary, set of
atomic categories and distinguished atomic category are left implicit. The
lexicon is defined as follows:

$a\mathrel{:=}A\,,\quad
b\mathrel{:=}B\,,\quad\varepsilon\mathrel{:=}S\mathord{\reflectbox{$/$}}A/\hat{S}/B\,,\quad\varepsilon\mathrel{:=}\hat{S}\mathord{\reflectbox{$/$}}A/\hat{S}/B\,,\quad\varepsilon\mathrel{:=}S\,,\quad\varepsilon\mathrel{:=}\hat{S}$

The set of rules consists of all instances of application and all instances of
forward composition of degree at most $3$ where the target of the secondary
input category is restricted to one of the “hatted” categories. We write $Y$
for a variable restricted to the set $\\{S,A,B\\}$, $\hat{Y}$ for a variable
restricted to the set $\\{\hat{S},\hat{A},\hat{B}\\}$, and $Z_{i}$ for an
unrestricted variable. As before, the $\mathnormal{|}_{i}$ are slashes
(forward or backward).

$\displaystyle X/Y\quad Y$ $\displaystyle\quad\Rightarrow\quad X$ (10)
$\displaystyle Y\quad X\mathord{\reflectbox{$/$}}Y$
$\displaystyle\quad\Rightarrow\quad X$ (11) $\displaystyle
X/\hat{Y}\quad\hat{Y}\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}$
$\displaystyle\quad\Rightarrow\quad
X\mathnormal{|}_{1}Z_{1}\cdots\mathnormal{|}_{d}Z_{d}$ where $0\leq d\leq 3$
(12)

As witnessed by the derivations in Figure 4, the language generated by this
grammar contains the subsets $\\{a^{n}b^{n}\mid n\geq 0\\}$ and
$\\{(ab)^{n}\mid n\geq 0\\}$.222Vijay-Shanker and Weir (1994) are mistaken in
claiming that this grammar generates _exactly_ $\\{a^{n}b^{n}\mid n\geq 0\\}$.

The ability to impose restrictions on the applicability of rules plays an
important role in terms of generative power: without them, VW-CCG is strictly
less powerful than TAG (Kuhlmann, Koller, and Satta, 2015).

##  3 Complexity Without Categories for the Empty String

As already mentioned, the ability of VW-CCG to assign lexicon entries to the
empty string contradicts one of the central linguistic principles of CCG, the
Principle of Adjacency, by which combinatory rules may only apply to entities
that are phonologically realized (Steedman, 2000, p. 54). In this section we
therefore first investigate the computational complexity of the universal
recognition problem for a restricted version of VW-CCG where this feature is
dropped and every lexical category is projected by an overt word. We will say
that a grammar $G$ whose lexicon does not contain any assignments of the form
$\varepsilon\mathrel{:=}X$ is $\mathbold{\varepsilon}$-free. We show the
following result:

######  Theorem 3.1.

The universal recognition problem for $\varepsilon$-free VW-CCG is NP-
complete.

We split the proof of this theorem into two parts: Section 3.1 shows hardness,
and Section 3.2 shows membership. Section 3.3 contains a brief discussion of
the result. For a gentle introduction to computational complexity and the
relevant proof techniques, we refer the reader to Papadimitriou (1994).

###  3.1 NP-Hardness

Our hardness proof is by a polynomial-time reduction from the Boolean
Satisfiability Problem (SAT) to the universal recognition problem for
$\varepsilon$-free VW-CCG. Since SAT is an NP-hard problem, this proves that
the recognition problem is NP-hard as well. An instance of SAT is given by a
Boolean formula $\phi$ in conjunctive normal form. This means that $\phi$ is a
conjunction of clauses $c_{i}$, where each clause consists of a disjunction of
one or more literals. A literal is either a variable $v_{j}$ or a negated
variable $\overline{v_{j}}$. The question asked about $\phi$ is whether it is
satisfiable, that is, whether there is a truth assignment to the variables
that makes $\phi$ evaluate to $\mathbf{1}$ (true). Our reduction is a
polynomial-time procedure for transforming an arbitrary instance $\phi$ into
an $\varepsilon$-free grammar $G$ and an input string $w$ such that $\phi$ is
satisfiable if and only if $w\in L(G)$. We additionally note that the combined
size of $G$ and $w$ is polynomial in the total number of literals in $\phi$,
and thus obtain the following:

######  Lemma 3.2.

The universal recognition problem for $\varepsilon$-free VW-CCG is NP-hard.

We start with a description of how to obtain the input string $w$ in Section
3.1.1, and then turn to the grammar $G$. The lexicon and the rules of the
grammar $G$ will be set up in such a way that every derivation for $w$
consists of three clearly separated parts. We will present these parts in
sequence in sections 3.1.2–3.1.4, introducing the relevant lexicon entries and
rules as we go along. The vocabulary and the set of atomic categories will be
implicit. We will say that we _construct_ the string $w$ and the grammar $G$
based on $\phi$. Throughout the description of this construction we write $m$
for the number of clauses in $\phi$ and $n$ for the total number of distinct
variables in $\phi$. The index $i$ will always range over values from $1$ to
$m$ (clauses), and the index $j$ will range over values from $1$ to $n$
(variables). To illustrate our construction we will use the following instance
of SAT:

$\phi=(v_{1}\lor\overline{v_{2}})\land(v_{1}\lor
v_{2})\land(\overline{v_{1}}\lor\overline{v_{2}})$

For this instance we have $m=3$ and $n=2$. We can verify that the only truth
assignment satisfying $\phi$ is
$\\{v_{1}\mapsto\mathbf{1},v_{2}\mapsto\mathbf{0}\\}$. We set
$c_{1}=(v_{1}\lor\overline{v_{2}})$, $c_{2}=(v_{1}\lor v_{2})$, and
$c_{3}=(\overline{v_{1}}\lor\overline{v_{2}})$.

####  3.1.1 Input String

We construct the input string as

$w=c_{m}\cdots c_{1}c_{0}v_{1}\cdots v_{n}v_{n+1}d_{n}\cdots d_{1}$

where the $c_{i}$ and $v_{j}$ are symbols representing the clauses and
variables of the input formula $\phi$, respectively. The symbols $c_{0}$ and
$v_{n+1}$ as well as the $d_{j}$ are special symbols that we use for technical
reasons, as explained below. For our running example we have
$w=c_{3}c_{2}c_{1}c_{0}v_{1}v_{2}v_{3}d_{2}d_{1}$.

####  3.1.2 Guessing a Truth Assignment

The first part of a derivation for $w$ “guesses” a truth assignment for the
variables in $\phi$ by assigning a complex category to the substring
$c_{0}v_{1}\cdots v_{n}v_{n+1}$. Figure 5 shows how this could look like for
our running example. Reading from the leaves to the root, for every symbol
$v_{j}$ in $w$, the derivation nondeterministically chooses between two
lexicon entries, $v_{j}\mathrel{:=}[\cent]/[v_{j}\mapsto\mathbf{1}]/[\cent]$
and $v_{j}\mathrel{:=}[\cent]/[v_{j}\mapsto\mathbf{0}]/[\cent]$; these entries
represent the two possible truth assignments to the variable. Note that we use
square brackets to denote atomic categories. The derivation then uses
compositions (13) and (14) to “push” these variable-specific categories to the
argument stack of the lexical category for the special symbol $c_{0}$, and a
final application (15) to yield a complex category that encodes the complete
assignment.

$\vphantom{([q^{+}\hat{S}])}[c_{0}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}[c_{0}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]/[\cent]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}[c_{0}]/[v_{1}\mapsto\mathbf{1}]/[\cent]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[c_{0}]/[\cent]}{\vphantom{([q^{+}\hat{S}])}c_{0}}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]/[v_{1}\mapsto\mathbf{1}]/[\cent]}{\vphantom{([q^{+}\hat{S}])}v_{1}}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]/[v_{2}\mapsto\mathbf{0}]/[\cent]}{\vphantom{([q^{+}\hat{S}])}v_{2}}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]}{\vphantom{([q^{+}\hat{S}])}v_{3}}$
Figure 5: Derivation fragment that “guesses” the truth assignment for the
running example.

##### Lexicon Entries and Rules

To support derivations such as the one in Figure 5, we introduce the following
lexicon entries:

$c_{0}\mathrel{:=}[c_{0}]/[\cent]\qquad
v_{j}\mathrel{:=}[\cent]/[v_{j}\mapsto\mathbf{1}]/[\cent]\qquad
v_{j}\mathrel{:=}[\cent]/[v_{j}\mapsto\mathbf{0}]/[\cent]\qquad
v_{n+1}\mathrel{:=}[\cent]$

We also introduce rules according to the following restricted schemata.
Schemata (13) and (14) yield composition rules of degree $2$; schema (15)
yields application rules.

$\displaystyle X/[\cent]\quad[\cent]/[v_{j}\mapsto\mathbf{1}]/[\cent]$
$\displaystyle\quad\Rightarrow\quad X/[v_{j}\mapsto\mathbf{1}]/[\cent]$ (13)
$\displaystyle X/[\cent]\quad[\cent]/[v_{j}\mapsto\mathbf{0}]/[\cent]$
$\displaystyle\quad\Rightarrow\quad X/[v_{j}\mapsto\mathbf{0}]/[\cent]$ (14)
$\displaystyle X/[\cent]\quad[\cent]$ $\displaystyle\quad\Rightarrow\quad X$
(15)

##### Derivational Ambiguity

It is worth mentioning here that our rules support other derivation orders
than the left-branching order shown in Figure 5. In particular, we could first
combine the variable-specific categories with each other, and then combine the
result with the category for $c_{0}$. One could rule out this derivational
ambiguity by restricting the target of the primary input of each of the rules
above to the category $[c_{0}]$, obtaining rules such as the
following:333Recall from Section 2.2 that $\mathinner{\$}$ is a variable for
the part of the category stack below the topmost element.

$\displaystyle[c_{0}]\mathinner{\$}/[\cent]\quad[\cent]/[v_{j}\mapsto\mathbf{1}]/[\cent]$
$\displaystyle\quad\Rightarrow\quad[c_{0}]\mathinner{\$}/[v_{j}\mapsto\mathbf{1}]/[\cent]$
(13’)

For the purposes of our reduction, the different derivation orders are
irrelevant, and we therefore abstain from using target restrictions.

####  3.1.3 Verifying the Truth Assignment

The second part of a derivation for $w$ verifies that the truth assignment
hypothesized in the first part satisfies all clauses. It does so by using
compositions to “pass” the stack of atomic categories encoding the truth
assignment from one clause to the next, right-to-left. For the running
example, this could be done as in Figure 6. Crucially, the rules used in this
part are restricted in such a way that the assignment can be “passed” to the
next clause $c_{i}$ only if $c_{i}$ is satisfied by at least one assignment
$v_{j}\mapsto b$. This can happen in two ways: either the assignment sets
$b=\mathbf{1}$ and $v_{j}$ occurs in $c_{i}$, or the assignment sets
$b=\mathbf{0}$ and the negated variable $\overline{v_{j}}$ occurs in $c_{i}$.
For example, the lowermost composition (16) is licensed because $v_{1}$ occurs
in $c_{1}$. At the end of this part of the derivation, we have a complex
category encoding a truth assignment as before, but where we now also have
checked that this assignment satisfies all clauses.

$\vphantom{([q^{+}\hat{S}])}[c_{3}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[c_{3}]/[c_{2}]}{\vphantom{([q^{+}\hat{S}])}c_{3}}\vphantom{([q^{+}\hat{S}])}[c_{2}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[c_{2}]/[c_{1}]}{\vphantom{([q^{+}\hat{S}])}c_{2}}\vphantom{([q^{+}\hat{S}])}[c_{1}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[c_{1}]/[c_{0}]}{\vphantom{([q^{+}\hat{S}])}c_{1}}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}[c_{0}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]}{\vphantom{([q^{+}\hat{S}])}}$
Figure 6: Derivation fragment that verifies the assignment for the running
example. The white triangle represents the derivation shown in Figure 5.

##### Lexicon Entries and Rules

To implement the second part of the derivation, for each clause $c_{i}$ we
introduce a lexicon entry $c_{i}\mathrel{:=}[c_{i}]/[c_{i-1}]$. Our rules make
crucial use of variable restrictions. To introduce them we define the
following notational shorthands:

$\displaystyle\mathbf{1}_{j}$
$\displaystyle\equiv/Y_{1}\cdots/Y_{j-1}/[v_{j}\mapsto\mathbf{1}]/Y_{j+1}\cdots/Y_{n}$
$\displaystyle\mathbf{0}_{j}$
$\displaystyle\equiv/Y_{1}\cdots/Y_{j-1}/[v_{j}\mapsto\mathbf{0}]/Y_{j+1}\cdots/Y_{n}$

Thus $\mathbf{1}_{j}$ is a sequence of $n$ slash–variable pairs, except that
the $j$th variable has been replaced with the concrete (atomic) category
$[v_{j}\mapsto\mathbf{1}]$, and similarly for $\mathbf{0}_{j}$. With this
notation, we include into $G$ all rules that match one of the following two
schemata:

$\displaystyle X/[c_{i-1}]\quad[c_{i-1}]\mathbf{1}_{j}$
$\displaystyle\quad\Rightarrow\quad X\mathbf{1}_{j}$ if $v_{j}$ occurs in
$c_{i}$ (16) $\displaystyle X/[c_{i-1}]\quad[c_{i-1}]\mathbf{0}_{j}$
$\displaystyle\quad\Rightarrow\quad X\mathbf{0}_{j}$ if $\overline{v_{j}}$
occurs in $c_{i}$ (17)

For example, the two lowermost (when reading the tree from the root to the
leaves) compositions in Figure 6 are both instances of schema (16), but their
use is licensed by two different variable–clause matchings.

##### Derivational Ambiguity

Similarly to what we noted for the first part (Section 3.1.2), the derivation
of this part can proceed in several ways, because at each step we may be able
to choose more than one rule to satisfy a clause $c_{i}$. For example, in the
derivation in Figure 6, instead of using the rule of schema (16) with witness
“$v_{1}$ occurs in $c_{2}$” we could also have used the rule of schema (17)
with witness “$\overline{v_{2}}$ occurs in $c_{2}$.” However, also as before,
there is no need to eliminate this derivational ambiguity for the purposes of
this reduction.

####  3.1.4 Finalizing the Derivation

The third and final part of a derivation of $w$ reduces the complex category
encoding the truth assignment to the distinguished category of $G$, which we
define to be $[c_{m}]$, by a sequence of applications. For the running
example, this is illustrated in Figure 7.

$\vphantom{([q^{+}\hat{S}])}[c_{3}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}[c_{3}]/[v_{1}\mapsto\mathbf{1}]\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}[c_{3}]/[v_{1}\mapsto\mathbf{1}]/[v_{2}\mapsto\mathbf{0}]}{\vphantom{([q^{+}\hat{S}])}}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[v_{2}\mapsto\mathbf{0}]}{\vphantom{([q^{+}\hat{S}])}d_{2}}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[v_{1}\mapsto\mathbf{1}]}{\vphantom{([q^{+}\hat{S}])}d_{1}}$
Figure 7: Final derivation fragment for the running example. The white
triangle represents the derivation shown in Figure 6.

##### Lexicon Entries and Rules

This part of the derivation requires two lexicon entries for each of the
auxiliary symbols: $d_{j}\mathrel{:=}[v_{j}\mapsto\mathbf{1}]$ and
$d_{j}\mathrel{:=}[v_{j}\mapsto\mathbf{0}]$. The rules are:

$\displaystyle X/[v_{j}\mapsto\mathbf{1}]\quad[v_{j}\mapsto\mathbf{1}]$
$\displaystyle\quad\Rightarrow\quad X$ (18) $\displaystyle
X/[v_{j}\mapsto\mathbf{0}]\quad[v_{j}\mapsto\mathbf{0}]$
$\displaystyle\quad\Rightarrow\quad X$ (19)

####  3.1.5 Time Complexity

We now analyze the time complexity of our reduction. For a given clause
$c_{i}$, let $|c_{i}|$ be the number of literals in $c_{i}$. We define
$|\phi|=\sum_{i}|c_{i}|$. The number of rules added in the first and the third
part of the construction of $G$ is in ${\cal O}({n})$, and the size of each
such rule is bounded by a constant that does not depend on $|\phi|$. For the
second part of the construction of $G$, for each clause $c_{i}$ we add a
number of rules that is at most $|c_{i}|$, and possibly less if there are
repeated occurrences of some literal in $c_{i}$. Thus the total number of
rules added in this part is in ${\cal O}({|\phi|})$. Each such rule has size
in ${\cal O}({n})$. Putting everything together, and observing that $n$ is in
${\cal O}({|\phi|})$, we see that the size of $G$ is in ${\cal
O}({|\phi|^{2}})$. It is not difficult to see then that our reduction can be
carried out in time polynomial in the size of $\phi$.

###  3.2 Membership in NP

We now turn to the membership part of Theorem 3.1:

######  Lemma 3.3.

The universal recognition problem for $\varepsilon$-free VW-CCG is in NP.

For the proof of this lemma, we provide a polynomial-time nondeterministic
algorithm that accepts an $\varepsilon$-free VW-CCG $G$ and a string $w$ if
and only if $G$ can derive $w$. We adopt the usual proof strategy where we
first nondeterministically guess a derivation tree for $w$ and then verify
that this tree is valid.

##### Size of a Derivation Tree

We need to argue that the total number of characters needed to encode a
derivation tree is polynomial in the combined size of $G$ and $w$. Note that
this involves both the tree structure itself and the lexicon entries and
categories at the nodes of the tree. We start by observing that any derivation
tree with $\ell$ leaf nodes (labeled with lexicon entries) has exactly
$\ell-1$ binary nodes (labeled with categories). Let $\tau$ by an arbitrary
derivation tree for $w$. Since in $G$ there are no lexical categories for the
empty string, there is a one-to-one correspondence between the leaf nodes of
$\tau$ and the symbols in $w$, which implies that the number of nodes of
$\tau$ is exactly $2|w|-1$.

##### Maximal Size of a Category

Now that we have bounded the number of nodes of $\tau$, we will bound the
sizes of the categories that these nodes are labeled with. Here, by the size
of a category $X$, denoted by $|X|$, we simply mean the number of characters
needed to write down $X$. Consider an internal node $v$ of $\tau$ and its
associated category $X$. In order to state an upper bound for $|X|$, we
distinguish two cases: If $v$ is a unary node, then $|X|$ is bounded by the
largest size of a category in the lexicon of the grammar. We denote this
quantity by $\lambda$. If $v$ is a binary node, let
$X=A\mathnormal{|}Y_{1}\cdots\mathnormal{|}Y_{q}$, with $A$ an atomic
category. A rule of the grammar can increase the number of arguments of its
primary category by at most $d$, where $d$ is the maximum degree of a rule in
the grammar. Let $\gamma$ be the maximum number of arguments in a category in
the lexicon. Since no more than $|w|-1$ rules are used in $\tau$, we conclude
that $q$ is bounded by $\gamma+d(|w|-1)$. By Lemma 3.1 in Vijay-Shanker and
Weir (1994), every argument $Y_{i}$ in $X$ must also occur as an argument in
some category in the lexicon of $G$. Thus the size of each argument of $X$ is
bounded by the largest size of an argument appearing in a category in the
lexicon, a quantity that we denote by $\alpha$. Putting everything together,
we have that $|X|$ is bounded by $1+\alpha(\gamma+d(|w|-1))$. From this it is
not difficult to see that the overall space needed to encode our derivation
tree $\tau$ for $w$ along with all of the categories at its nodes is ${\cal
O}({(\lambda+\alpha\gamma)|w|+\alpha d|w|^{2}})$. This is a polynomial in the
combined size of the grammar and the input string.

##### Nondeterministic Algorithm

We can now provide our nondeterministic algorithm for testing whether $G$
derives $w$. In a first step we write down a guess for a derivation tree
$\tau$ for $w$ based on the rules in $G$. Given our space bound on $\tau$, we
can carry out this step in time polynomial in the size of $G$ and $w$. In a
second step we visit each internal node $v$ of $\tau$ and read its associated
category $X$. If $v$ is a unary node, we check whether $X$ is a lexicon entry
for the word at $v$’s child. If $v$ is a binary node, we check whether $X$ can
be obtained by some rule of the grammar applied to the categories at the two
children of $v$. We accept if every check is successful. Even this second step
can be carried out in time polynomial in the size of $G$ and $w$. This
concludes the proof of Lemma 3.3.

###  3.3 Discussion

In the previous sections we have shown that the universal recognition problem
for $\varepsilon$-free VW-CCG is NP-complete (Theorem 3.1). This result is in
contrast with the fact that, for the weakly equivalent TAG formalism, the
universal recognition problem can be solved in polynomial time, and it
naturally raises the question what features of the VW-CCG formalism are the
source of this additional complexity. We discuss this question on the basis of
the reduction in our proof of Lemma 3.2. In this reduction we use a
combination of three central features of VW-CCG, listed below. Dropping any of
these features would break our reduction.

##### Lexical Ambiguity

The first feature of VW-CCG that we exploit in our construction is the ability
to assign more than one category to some lexical items. In part 1 of the
reduction (Section 3.1.2), this allows us to “guess” arbitrary truth
assignments for the variables in the clause $\phi$. However, the possibility
to write grammars with lexical ambiguity is an essential feature of all
interesting formalisms for natural language syntax, including also TAG.
Therefore, at least in isolation, this feature does not seem to be able to
explain the complexity of the universal recognition problem for VW-CCG. Even
if our goal was to design a new version of VW-CCG which can be parsed in
polynomial time in the size of the input grammar, we would not seriously
consider giving up lexical ambiguity.

##### Unbounded Composition

The second feature of VW-CCG that we rely on is the availability of
composition rules without a constant (with respect to the full class of
grammars) bound on their degree. This feature is crucial for our encoding of
truth assignments. In particular, without it we would not be able to percolate
arbitrarily large truth assignments through derivation trees; our construction
would work only for formulas with a bounded number of variables.

Unbounded composition has previously been discussed primarily in the context
of generative power. Weir and Joshi (1988) show that allowing unrestricted use
of _arbitrarily_ many composition rules leads to a version of VW-CCG that is
more powerful than the one considered here, where every grammar must restrict
itself to a finite set of such rules. Other authors have suggested to put
explicit (low) bounds on the maximal degree of composition. From a purely
formal point of view, a bound as low as $d\leq 2$ may suffice: Weir and Joshi
(1988) show how every VW-CCG grammar can be converted into a weakly equivalent
Linear Index Grammar (LIG) (Gazdar, 1987), and how every TAG can be converted
into a weakly equivalent VW-CCG whose composition rules all have degree $2$.
Together with the weak equivalence of LIG and TAG (Vijay-Shanker and Joshi,
1985), this shows that the subclass of VW-CCG grammars with degree of
composition at most 2 can still generate the full class of languages.444Note
however that the construction of Weir and Joshi (1988) does not produce
$\varepsilon$-free grammars. For any degree-restricted subclass of grammars,
our proof would break, which means that it may be possible (though not
obvious) to devise a polynomial-time algorithm for the universal recognition
problem. We will discuss unbounded composition further in Section 5.1.

##### Rule Restrictions

The third feature of VW-CCG that we exploit is its ability to put grammar-
specific restrictions on combinatory rules. In particular, in part 2 of our
construction (Section 3.1.3), we use rules whose secondary input categories
contain a mix of variables and concrete categories, such as

$\displaystyle X/[c_{i-1}]\quad[c_{i-1}]\mathbf{1}_{j}$
$\displaystyle\quad\Rightarrow\quad X\mathbf{1}_{j}$ if $v_{j}$ occurs in
$c_{i}$ (16)

Like the availability of composition rules of unbounded degree, the ability to
use rule restrictions seems to be a very powerful feature, and one that
perhaps most clearly sets VW-CCG apart from TAG. Moreover, as already
mentioned, rule restrictions also play a crucial role with respect to weak
generative capacity (Kuhlmann, Koller, and Satta, 2015).

Note that we could replace rules of the form (16) with rules without
variables; but then, for fixed values of $i$ and $j$ and, say, for the
assignment $[v_{j}\mapsto\mathbf{1}]$, we would have to include into the
grammar all of the $2^{n-1}$ rules of the form

$X/[c_{i-1}]\quad[c_{i-1}]/A_{1}\cdots/A_{j-1}/[v_{j}\mapsto\mathbf{1}]/A_{j+1}\cdots/A_{n}\quad\Rightarrow\quad
X/A_{1}\cdots/A_{n}$

where each $A_{h}$ is a concrete atomic category of the form
$[v_{h}\mapsto\mathbf{1}]$ or $[v_{h}\mapsto\mathbf{0}]$. This would break our
proof because reductions must use polynomial time (and space). Note also that
what is crucial here is not the use of either variables or concrete categories
in a rule’s secondary input; rather, it is the combination of the two that
allows us to check clauses against truth assignments.

##  4 Complexity With Categories for the Empty String

In this section we investigate the computational complexity of the universal
recognition problem for unrestricted VW-CCG, where one is allowed to assign
lexicon entries even to the empty string. We show the following:

######  Theorem 4.1.

The universal recognition problem for unrestricted VW-CCG is EXPTIME-complete.

The proof of this theorem is more involved than the proof of the NP-
completeness result in Section 3. We start in Section 4.1 by introducing
_alternating Turing machines_ (Chandra, Kozen, and Stockmeyer, 1981), which
provide the computational framework for our proof. The use of alternating
Turing machines instead of ordinary deterministic or nondeterministic Turing
machines is crucial here: In order to simulate the computations of a Turing
machine by a CCG grammar in a natural way, we need to restrict the machine to
use only polynomial space. However, if we used standard Turing machines with
this space restriction, then we would only be able to prove PSPACE-hardness, a
weaker result than the EXPTIME-completeness that we obtain from our proof. The
hardness part of this proof is presented in Section 4.2, and the membership
part in Section 4.3. We finally discuss our result in Section 4.4.

###  4.1 Alternating Turing Machines

The alternating Turing machine (ATM; Chandra, Kozen, and Stockmeyer, 1981) is
a generalization of the well-known nondeterministic Turing machine in which
there are two types of states: existential states and universal states. When
the machine is in an existential state, it accepts the input if there is at
least one transition that eventually leads to an accepting state. In contrast,
when the machine is in a universal state, it accepts only if _every_ possible
transition eventually leads to an accepting state. A nondeterministic Turing
machine can be viewed an alternating Turing machine with no universal states.

As already mentioned, for our proof we use ATMs working in polynomial space,
which means that the length of the tape is bounded by a polynomial in the
length of the input. This resource-restricted model is well-known in the
literature, and it exactly characterizes the class of all decision problems
that are solvable by a _deterministic_ Turing machine (i.e. a Turing machine
where there is at most one possible transition given a state and a tape
symbol) working in _exponential_ time (Chandra, Kozen, and Stockmeyer, 1981).
This is the complexity class EXPTIME.

To simplify the notation and some of our proofs, we use ATMs that operate on a
_circular tape_ , and can only move their head to the right. The same model
has previously been used by, among others, Jeż and Okhotin (2011). It is not
hard to see that, as long as we work under the restriction to polynomial
space, every move to the left in the standard model can be simulated by a
(polynomial) number of moves to the right in the circular tape model. Thus,
even ATMs with a polynomially bounded circular tapes precisely characterize
EXPTIME.

##### Formal Definition

Formally, an alternating Turing machine is a structure

$M=(Q,\Sigma,\delta,q_{0},g)$

where:

$Q$ is a finite set of states;

$\Sigma$ is an alphabet of tape symbols, which we assume includes the special
blank symbol $\\#$;

$\delta\subseteq(Q\times\Sigma)\times(Q\times\Sigma)$ is the transition
relation;

$q_{0}\in Q$ is the initial state;

and $g\mathpunct{:}\ Q\to\\{{\exists},{\forall},\mathsf{A},\mathsf{R}\\}$ is a
function that assigns a type to each state. The four different types for a
state are existential ($\exists$), universal ($\forall$), accepting
$(\mathsf{A})$, and rejecting $(\mathsf{R})$; their semantics will become
clear below.

We denote transitions in $\delta$ as $(q,a)\to(q^{\prime},a^{\prime})$.
Transitions are subject to the restriction that the state to the left of the
arrow must be either existential or universal. This means that no transition
is possible out of an accepting or a rejecting state; when an ATM reaches such
a state, it necessarily stops. To simplify the proof, we also require that for
every universal state $q$ and tape symbol $a$, there are exactly two
transitions with left-hand side $(q,a)$. This is without loss of generality:
If a machine does not already have this property, then one can construct (in
polynomial time) an equivalent polynomial-space ATM with circular tape
satisfying it; a similar construction for general ATMs is sketched by
Papadimitriou (1994, Theorem 8.2).

##### Configurations

Let $w\in\Sigma^{*}$ be an input string for $w$, and let $n=|w|$ and
$m=p_{M}(|w|)$, where $p_{M}$ is the machine-specific polynomial that defines
the maximal tape length. A configuration of $M$ relative to $w$ is a pair
$c=(q,\alpha)$, where $q\in Q$ is some state and $\alpha\in\Sigma^{*}$ is a
sequence of tape symbols with length $|\alpha|=m$. The intended interpretation
of $c$ is that the current state of $M$ is $q$, the content of the circular
tape is represented by $\alpha$, and the tape head is positioned to read the
first symbol of $\alpha$. In particular, the initial configuration of $M$ for
$w$, denoted by $I_{M}(w)$, takes the form $I_{M}(w)=(q_{0},w\\#^{m-n})$,
meaning that, at the start of the computation, the machine is in the initial
state, the tape consists of the $n$ symbols of the input string $w$ followed
by $m-n$ blanks, and the tape head is positioned to read the first symbol of
$w$. A configuration $c$ is called existential, universal, accepting or
rejecting, based on the type of its state $q$.

##### Successors

Let $t=(q,a)\to(q^{\prime},a^{\prime})$ be a transition. The intended
interpretation of $t$ is that if $M$ is in state $q$ and reads tape symbol
$a$, then overwrites $a$ with $a^{\prime}$, moves its tape head one cell to
the right (which is always possible because the tape is circular), and
continues the computation in state $q^{\prime}$. Formally, let $c=(q,a\alpha)$
be a configuration of $M$. The successor of $c$ with respect to $t$, denoted
by $t(c)$, is the configuration $c^{\prime}=(q^{\prime},\alpha a^{\prime})$,
where the string $\alpha a^{\prime}$ encodes the fact that the symbol $a$ has
been overwritten with $a^{\prime}$ and the circular tape has been rotated one
position to the right, so that the head now is posititioned to read the first
symbol of $\alpha$. Note that, due to our restrictions on the transition
relation, a universal configuration has exactly two successors.

##### Acceptance

We first discuss acceptance in ordinary nondeterministic Turing machines. As
usual, a single machine configuration $c$ may lead (in one step) to a number
of successor configurations $c_{1},\dots,c_{k}$. Acceptance is recursively
defined such that $c$ leads to acceptance if and only if at least one of
$c_{1},\dots,c_{k}$ leads to acceptance. One may view this as an existential
condition on the successor configurations. In an alternating Turing machine, a
configuration may be either existential or universal; in the universal case,
$c$ leads to acceptance if and only if _every_ successor $c_{1},\dots,c_{k}$
leads to acceptance. To make this formal, we represent computations of $M$ as
trees whose nodes are labeled with configurations of $M$, and whose edges
reflect the “successor of”-relation between configurations. Formally, the set
of accepting computations is defined recursively as follows (recall our
definition of tree terms in Section 2.3):

  * •

Every accepting configuration $c$ forms a one-node accepting computation.

  * •

Let $c$ be an existential configuration and let $\gamma$ be an accepting
computation whose root node is labeled with some successor of $c$. Then
$c(\gamma)$ is an accepting computation.

  * •

Let $c$ be a universal configuration and let $\gamma_{1}$, $\gamma_{2}$ be
accepting computations whose root nodes are labeled with the two successors of
$c$. Then $c(\gamma_{1},\gamma_{2})$ is an accepting computation.

A sample accepting computation is shown in Figure 8. A machine $M$ accepts a
string $w$ if there exists an accepting computation $\gamma$ whose root node
is labeled with the initial configuration $I_{M}(w)$. The set of all strings
that are accepted by $M$ is denoted by $L(M)$.

##### Characterization of EXPTIME

As already mentioned, the reason that we are interested in polynomial-space
alternating Turing machines is that they exactly characterize the class of
decision problems solvable in exponential time. This is expressed by the
following lemma, which is basically Corollary 3.6 of Chandra, Kozen, and
Stockmeyer (1981).

######  Lemma 4.2.

The following decision problem is EXPTIME-complete: Given a polynomial-space
alternating Turing machine $M$ and a string $w$, is $w\in L(M)$?

Since a polynomial-space circular-tape ATM can simulate any polynomial-space
ATM at no additional asymptotic space cost, we conclude that Lemma 4.2 also
holds for polynomial-space circular-tape ATMs. In the following we therefore
use Lemma 4.2 as referring to polynomial space circular tape ATMs.

$c_{1}$$(\exists)$$c_{2}$$(\forall)$$c_{3}$$(\mathsf{A})$$c_{4}$$(\exists)$$c_{5}$$(\mathsf{A})$
Figure 8: An accepting run. State types for each configuration $c_{i}$ are
indicated in parentheses.

###  4.2 EXPTIME-Hardness

Let $M$ be a polynomial-space circular-tape ATM and let $w$ be an input string
for $M$. In this section we show how to construct, in polynomial time and
space, a VW-CCG grammar $G$ such that $L(G)=\\{\varepsilon\\}$ if $w\in L(M)$,
and $L(G)=\emptyset$ if $w\not\in L(M)$. This means that we can test the
condition $w\in L(M)$ by checking whether $G$ generates the empty string. When
combined with Lemma 4.2, this reduction proves the hardness part of Theorem
4.1:

######  Lemma 4.3.

The universal recognition problem for unrestricted VW-CCG is EXPTIME-hard.

For the remainder of this section, we fix a polynomial-space circular-tape ATM
$M=(Q,\Sigma,\delta,q_{0},g)$ and an input string $w\in\Sigma^{*}$. Let
$p_{M}$ be the polynomial that bounds the length of the tape of $M$, and let
$m=p_{M}(|w|)$.

##### Basic Idea

The basic idea behind our construction is straightforward: We will set up
things in such a way that the derivations of $G$ correspond to accepting
computations of $M$ for $w$. To illustrate this idea, Figure 9 shows the
schematic structure of a derivation that corresponds to the accepting
computation in Figure 8. Note that in order to make the correspondence more
evident, contrary to our previous convention, we now draw the derivation with
the root node at the top. We see that the derivation is composed of a number
of smaller fragments (drawn as triangles). With the exception of the fragment
at the top of the tree (which we need for technical reasons), there is one
fragment per node of the accepting computation. Each fragment is labeled with
a reference to the subsection of this article that describes how we set up the
grammar $G$ to derive that fragment.

$[\text{{init}}]$$E(c_{1})$$E(c_{2})$$E(c_{3})$$E(c_{4})$$E(c_{5})$ptinitial
configuration (4.2.2)pttransition out of an existential configuration
(4.2.4)pttransition out of a universal configuration (4.2.5)ptaccepting
configuration (4.2.3)pttransition out of an existential configuration
(4.2.4)ptaccepting configuration (4.2.3) Figure 9: Schematic structure of the
derivation in $G$ that corresponds to the accepting computation in Figure 8.
The derivation is displayed with the root node at the top to make the
correspondence with Figure 8 more evident. Each $E(c_{i})$ is the category
that encodes the configuration $c_{i}$.

One way to view our construction is that it establishes a structure-preserving
map from accepting computations of $M$ to derivations of $G$. This map
replaces each configuration $c$ in an accepting computation by a fragment, and
continues the transformation at the subtrees below $c$. A fragment is like a
small derivation tree, except that one or two of its leaf nodes may be labeled
with (possibly complex) categories instead of lexicon entries. These nodes,
which we refer to as the distinguished leaf nodes of the fragment, serve as
slots at which the fragments that result from the recursive transformation of
the subtrees can be substituted. The root node of a fragment is labeled with a
category that encodes the configuration $c$ that the fragment replaces; we
denote this category by $E(c)$. More specifically, the shape of the fragment
depends on the type of $c$:

  * •

For every accepting configuration $c$, the grammar derives a fragment with no
distinguished leaf nodes. The category at the root node of this fragment is
$E(c)$. The lexicon entries and rules required to derive the fragment are
described in Section 4.2.3.

  * •

For every existential configuration $c$ and for every transition $t$ that can
be applied to $c$, the grammar derives a fragment with a single distinguished
leaf node. The category at the root node of this fragment is $E(c)$, and the
category at the distinguished leaf node is $E(t(c))$, the encoding of the
successor of $c$ under $t$. (Section 4.2.4)

  * •

For every universal configuration $c$, the grammar derives a fragment with two
distinguished leaf nodes. The category at the root node of this fragment is
$E(c)$, and the categories at the distinguished leaf nodes are $E(t_{1}(c))$
and $E(t_{2}(c))$, the encodings of the two successors of $c$. (Section 4.2.5)

  * •

Finally, for the initial configuration $I_{M}(w)$, the grammar derives a
fragment with a single distinguished leaf node. The category at the root node
of this fragment is the distinguished category of $G$, and the category at the
distinguished leaf node is $E(I_{M}(w))$. This is the highlighted fragment in
Figure 9. (Section 4.2.2)

Those leaf nodes of a fragment that are not distinguished leaf nodes will
always be labeled with lexicon entries for the empty string, that is, entries
of the form $\varepsilon\mathrel{:=}X$. Because of this, the only string that
our grammar may accept is the empty string. As we will make sure that all (and
only) the accepting computations of $M$ over $w$ receive corresponding
derivations in $G$, this amounts to saying that $G$ has at least one
derivation if and only if $w\in L(M)$. This implies that we do not need a
distinguished “reject” lexical category or any other mechanism that takes care
of the case when the Turing machine rejects its input.

##### Technical Remark

Before we continue, we would like to make a technical remark that may make the
following construction easier to understand. In the proof of Lemma 3.2, we
constructed a grammar that produced derivations simulating a process of
guessing and verifying a variable assignment for an instance of SAT. One
feature of the construction is that this process has a purely linear (albeit
nondeterministic) structure, which is reflected in the fact that the
derivation trees produced by the grammar are essentially unary-branching. For
such trees, it does not make much of a difference whether we read them
bottom–up (from the leaves to the root) or top–down (from the root to the
leaves), and in our construction we simply adopted the former perspective,
which is the conventional one for CCG.

In this proof, because of the branching nature of the computations of $M$, the
derivation trees of the grammar $G$ will no longer be unary-branching; and
because the branching in an accepting computation of $M$ occurs on the paths
from the initial configuration to the accepting configurations, the derivation
trees of the grammar $G$ need to have the encoding of the initial
configuration at the root and the encodings of the accepting configurations at
the leaves. This will require us to change perspective and read the derivation
trees top–down—and consequently the rules of $G$ from the output category to
the input categories. This is the reverse of what is conventional for CCG.

####  4.2.1 Encoding Configurations

We start the presentation of the construction of $G$ by explaining how we
encode configurations of $M$ as categories. Let $c=(q,a_{1}\cdots,a_{m})$ be a
configuration of $M$. We encode this configuration by a category

$E(c)=[q]/[a_{1}]\cdots/[a_{m}]$

where we follow the same convention as in Section 3.1 and use square brackets
to represent atomic categories. Note that in this encoding, the target of
$E(c)$ is an atomic category representing the current state, while the
arguments of $E(c)$ represent the circular tape, with the innermost argument
corresponding to the symbol under the tape head. With this representation, the
encoding of the successor of the configuration $c$ under a transition
$t=(q,a_{1})\to(q^{\prime},a^{\prime})$ can be written as

$E(t(c))=[q^{\prime}]/[a_{2}]\cdots/[a_{m}]/[a^{\prime}]$

####  4.2.2 Initial Configuration

We now present the derivation fragment for the initial configuration of $M$
for $w$. Let $c_{I}=I_{M}(w)$. To give a concrete example, suppose that this
configuration takes the form $c_{I}=(q_{0},ab)$. Then the corresponding
fragment looks as in Figure 10. The category at the root node is the
distinguished category $[\text{{init}}]$. The derivation starts by
nondeterministically pushing symbols to the tape stack of the categories along
the path (highlighted in Figure 10) from the root to the distinguished node.
This is done through rules of type (20) below. In a last step (21), the
derivation checks whether the tape stack matches the initial tape content
$ab$, and simultaneously changes the target from $[\text{{init}}]$ to
$[q_{0}]$. After this, the category at the distinguished leaf of the fragment
is $E(c_{I})$. We will see the idea of “nondeterministic guessing followed by
verification” once again in Section 4.2.5, where it will be used for making
copies of the tape stack. The reader may rightfully wonder whether there are
more direct methods for performing such straightforward manipulations of the
tape stack. Unfortunately, we have not been able to define such methods within
the VW-CCG formalism.

$\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{init}}]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{init}}]/[a]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{init}}]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\text{{init}}]/[q_{0}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}E(c_{I})={\hbox{\pagecolor{yellow!60}\mathstrut$[q_{0}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[b]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[a]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}$
Figure 10: Derivation fragment for an initial configuration
$c_{I}=(q_{0},ab)$. Note how the symbols of $c_{I}$ are collected in several
steps along the highlighted path.

##### Lexicon Entries and Rules

More generally now, assume that the initial configuration for $M$ on $w$ is
$c_{I}=(q_{0},a_{1}\cdots a_{m})$, where $w=a_{1}\cdots a_{n}$ and $a_{h}=\\#$
for each $h$ with $n<h\leq m$. To support fragments as the one in Figure 10,
we introduce lexicon entries $\varepsilon\mathrel{:=}[\text{{init}}]/[q_{0}]$
and $\varepsilon\mathrel{:=}[a]$, where $a\in\Sigma$ is any tape symbol. We
also introduce the following rules:

$\displaystyle[\text{{init}}]\mathinner{\$}/[a]\quad[a]$
$\displaystyle\quad\Rightarrow\quad[\text{{init}}]\mathinner{\$}$ (20)
$\displaystyle[\text{{init}}]\mathinner{\$}/[q_{0}]\quad[q_{0}]/[a_{1}]\cdots/[a_{m}]$
$\displaystyle\quad\Rightarrow\quad[\text{{init}}]\mathinner{\$}/[a_{1}]\cdots/[a_{m}]$
(21)

The $\mathinner{\$}$ symbol is, as usual, a variable for the part of the
category stack below the topmost stack element. A rule of the form (20) allows
the application of a category with target $[\text{{init}}]$ to any atomic
category $[a]$ representing a tape symbol; this implements the
nondeterministic pushing to the tape stack that we introduced above. A rule of
the form (21) is a composition rule of degree $m$ that restricts the target of
the primary input category to the distinguished category $[\text{{init}}]$,
and the secondary input to the category $E(c_{I})$. This implements the check
in the final step of the fragment—if the category at the distinguished leaf
does _not_ encode the initial configuration at this point, then the derivation
will reach a dead end.

##### Computational Complexity

We now deal with the computational resources required by this step of the
construction. Each of the lexicon entries above is size-bounded by a constant
that does not depend on $|M|$ or $|w|$. This size bound also holds for each
rule of the form (20). The size of a rule of the form (21) is in ${\cal
O}({m})$. We can then construct and store each lexical entry and each rule
with time (and space) in ${\cal O}({m})$. Furthermore, the total number of
lexicon entries and rules added to the grammar in this step is in ${\cal
O}({|\Sigma|})$. We thus conclude that this step of the construction can be
carried out in time (and space) polynomial in $|M|$ and $|w|$.

####  4.2.3 Accepting Configurations

Next we present lexicon entries and rules needed to terminate derivations of
the accepting configurations of $M$. To give a concrete example, suppose that
$c=(q,ab)$ is accepting, and that the grammar has already derived the category
$E(c)$. Then the grammar also derives the fragment shown in Figure 11.
Following the highlighted path from the root to the leaf, the derivation first
checks whether $E(c)$ indeed encodes an accepting configuration, and then
changes the target to a special atomic category $[\text{{accept}}]$ (22).
After this, the fragment empties the tape stack, using derivations similar to
those that we used to assemble the truth assignment in Section 3.1.2 (see
Figure 5).

$\vphantom{([q^{+}\hat{S}])}E(c)={\hbox{\pagecolor{yellow!60}\mathstrut$[q]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to267.33325pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[q]/[\text{{accept}}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{accept}}]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{accept}}]/[a]/[b]/[\cent]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{accept}}]/[a]/[\cent]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\text{{accept}}]/[\cent]$}}}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]/[a]/[\cent]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]/[b]/[\cent]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\cent]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}$
Figure 11: Derivation fragment for an accepting configuration $c=(q,ab)$.

##### Lexicon Entries and Rules

Let $q\in Q$ with $g(q)=\mathsf{A}$, and let $a\in\Sigma$. We introduce the
following lexicon entries:

$\varepsilon\mathrel{:=}[q]/[\text{{accept}}]\qquad\varepsilon\mathrel{:=}[\text{{accept}}]/[\cent]\qquad\varepsilon\mathrel{:=}[\cent]/[a]/[\cent]\qquad\varepsilon\mathrel{:=}[\cent]$

We also introduce the following rules:

$\displaystyle[q]\mathinner{\$}/[\text{{accept}}]\quad[\text{{accept}}]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[q]\mathinner{\$}/X_{1}\cdots/X_{m}$ (22)
$\displaystyle[\text{{accept}}]\mathinner{\$}/[\cent]\quad[\cent]$
$\displaystyle\quad\Rightarrow\quad[\text{{accept}}]\mathinner{\$}$ (23)
$\displaystyle[\text{{accept}}]\mathinner{\$}/[\cent]\quad[\cent]/[a]/[\cent]$
$\displaystyle\quad\Rightarrow\quad[\text{{accept}}]\mathinner{\$}/[a]/[\cent]$
(24)

A rule of the form (22) is a composition rule of degree $m$ that restricts the
target of its primary input to an accepting state; this ensures that only
categories encoding accepting configurations can yield subderivations of the
form shown in Figure 11. The derivation will either rewrite the configuration
(for existential and universal configurations—the details will be given in
Sections 4.2.4 and 4.2.5, respectively), or else will reach a dead end (for
rejecting configurations). The only rules that can be used after a rule of the
form (22) are rules of the forms (23) and (24), which jointly implement the
emptying of the tape stack that we described above.

##### Computational Complexity

Each of the lexicon entries above is size-bounded by a constant that does not
depend on $|M|$ and $|w|$. This size bound also holds for rules of the forms
(23) and (24). The sizes of rules of the form (22) are in ${\cal O}({m})$. The
number of lexicon entries and rules that we add to $G$ in this step is in
${\cal O}({|\Sigma|})$.

####  4.2.4 Transitions Out of Existential Configurations

We now turn to the fragments that simulate transitions out of existential
configurations. Figure 12 shows how such a fragment looks like for a
configuration $c=(q,ab)$ and a transition $t=(q,a)\to(q^{\prime},a^{\prime})$.
The derivation starts by checking whether the category at the root node indeed
encodes an existential configuration, and then changes the target to the
transition-specific category $[t]$ (25). The derivation then extends the tape
stack by the new symbol $a^{\prime}$ (26). In a last step it simultaneously
discards the category for the previous tape symbol $a$ and changes the target
to $[q^{\prime}]$ (27). After this, the category at the distinguished leaf
encodes the configuration $t(c)=(q^{\prime},ba^{\prime})$. We remind the
reader that an ATM accepts in an existential configuration if and only if
there is at least one transition that leads to an accepting configuration. In
the grammar $G$, this corresponds to the fact that there exists an applicable
rule that leads to acceptance. Therefore, we do not need to explicitly
simulate all possible transitions. For universal configurations (which we will
consider in Section 4.2.5), the situation is different, which will necessitate
a more involved construction.

$\vphantom{([q^{+}\hat{S}])}E(c)={\hbox{\pagecolor{yellow!60}\mathstrut$[q]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[q]/[t]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t]/[a]/[b]/[a^{\prime}]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[t]/[a]/[q^{\prime}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}E(t(c))={\hbox{\pagecolor{yellow!60}\mathstrut$[q^{\prime}]/[b]/[a^{\prime}]$}}}{\vphantom{([q^{+}\hat{S}])}}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[a^{\prime}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}$
Figure 12: Fragment for a transition $t=(q,a)\to(q^{\prime},a^{\prime})$ out
of an existential configuration $c=(q,ab)$.

##### Lexicon Entries and Rules

Let $q\in Q$ be any existential state, and let
$t=(q,a)\to(q^{\prime},a^{\prime})$ be any transition out of $q$. We introduce
the following new lexicon entries:

$\varepsilon\mathrel{:=}[q]/[t]\qquad\varepsilon\mathrel{:=}[t]/[a]/[q^{\prime}]$

We also reuse the lexicon entries $\varepsilon\mathrel{:=}[a]$ that we
introduced in Section 4.2.2. Finally, we introduce the following rules:

$\displaystyle[q]\mathinner{\$}/[t]\quad[t]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[q]\mathinner{\$}/X_{1}\cdots/X_{m}$ (25)
$\displaystyle[t]\mathinner{\$}/[a^{\prime}]\quad[a^{\prime}]$
$\displaystyle\quad\Rightarrow\quad[t]\mathinner{\$}$ (26)
$\displaystyle[t]\mathinner{\$}/[q^{\prime}]\quad[q^{\prime}]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[t]\mathinner{\$}/X_{1}\cdots/X_{m}$ (27)

A rule of the form (25) is a composition rule of degree $m$ that
simultaneously restricts the target of its primary input to $q$ and the target
of its secondary input to $t$. A rule of the form (26) is an application rule
that matches $t$ (the target of its primary input) with the tape symbol
$a^{\prime}$ produced by $t$ (its secondary input). A rule of the form (27) is
a composition rule of degree $m$ that matches $t$ (the target of its primary
input) with the state $q^{\prime}$ resulting from the application of $t$.

##### Computational Complexity

Again, each of the above lexical entries and rules has size in ${\cal
O}({m})$. The number of rules of the form (27) added to the grammar is bounded
by the possible choices of the transition $t$ ($q^{\prime}$ is unique, given
$t$), and is thus a polynomial function of $|M|$. Similar analyses apply to
the other rules and lexical entries. We thus conclude that the overall
contribution to $|G|$ in this step is polynomial in the size of the input, and
the construction can be carried out in polynomial time, too.

$\vphantom{([q^{+}\hat{S}])}E(c)={\hbox{\pagecolor{yellow!60}\mathstrut$[q]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to661.49979pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[q]/[\pi;{-}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\hbox
to0.0pt{\quad\vbox to132.29996pt{\vfil\hbox{\small duplicate the tape
stack}\vfil}\hss}\vbox
to132.29996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{-}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]/[t_{2}]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to264.59991pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\pi;{+}]/[t_{1}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\hbox
to0.0pt{\quad\vbox to132.29996pt{\vfil\hbox{\small simulate
$t_{1}$}\vfil}\hss}\vbox
to132.29996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t_{1}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}\@deduce{}[\leavevmode\hbox
to66.55pt{\vbox to66.55pt{\pgfpicture\makeatletter\hbox{\hskip
33.27498pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.07498pt}{66.14998pt}\pgfsys@lineto{-33.07498pt}{66.14998pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{29.65929pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}E(t_{1}(c))={\hbox{\pagecolor{yellow!60}\mathstrut$[q_{1}]/[b]/[a_{1}]$}}}{\vphantom{([q^{+}\hat{S}])}}}\@deduce{}[\vbox
to330.7499pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[b]/[b]/[t_{2}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\hbox
to0.0pt{\quad\vbox to132.29996pt{\vfil\hbox{\small simulate
$t_{2}$}\vfil}\hss}\vbox
to132.29996pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t_{2}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}\@deduce{}[\leavevmode\hbox
to66.55pt{\vbox to66.55pt{\pgfpicture\makeatletter\hbox{\hskip
33.27498pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.07498pt}{66.14998pt}\pgfsys@lineto{-33.07498pt}{66.14998pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{29.65929pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}E(t_{2}(c))={\hbox{\pagecolor{yellow!60}\mathstrut$[q_{2}]/[b]/[a_{2}]$}}}{\vphantom{([q^{+}\hat{S}])}}}}$
Figure 13: Bird’s-eye view of the derivation fragment for a pair of
transitions $\pi=(t_{1},t_{2})$ out of a universal configuration $(q,ab)$,
where $t_{1}=(q,a)\to(q_{1},a_{1})$ and $t_{2}=(q,a)\to(q_{2},a_{2})$.

####  4.2.5 Transitions Out of Universal Configurations

We finally present the lexicon entries and rules needed to simulate
transitions out of universal configurations. This is the most involved part of
our construction. To give an intuition, Figure 13 provides a bird’s eye view
of the fragment that our grammar derives for a universal configuration of the
form $c=(q,ab)$ and a pair of transitions $\pi=(t_{1},t_{2})$ where
$t_{1}=(q,a)\to(q_{1},a_{1})$ and $t_{2}=(q,a)\to(q_{2},a_{2})$. Recall that
we may assume that every universal configuration has exactly two applicable
transitions. On a high level, we construct two identical copies of the tape
stack and then simulate the transition $t_{1}$ on one copy and the transition
$t_{2}$ on the second copy. This is done in such a way that both $t_{1}$ and
$t_{2}$ must lead to accepting configurations in order to terminate the
derivation process. The actual derivation in the fragment proceeds in three
phases as follows. First, it duplicates the tape stack of the root category
$E(c)$. Second, it splits the duplicated stack into two identical halves, each
targeted at one of the two transitions. Third, it simulates (in two separate
branches) the two transitions on their respective halves to arrive at the two
leaf categories $E(t_{1}(c))$ and $E(t_{2}(c))$. (Note that the fragment here
differs from the one in Figure 12 in that it has _two_ distinguished leaves,
not one.) In the following we describe the three phases in detail.

##### Phase 1: Duplicating the Tape Stack

We illustrate this phase of the derivation in Figure 14. The derivation starts
by checking whether the root category $E(c)$ indeed encodes a universal
configuration, and records this fact by changing the target to the atomic
category $[\pi;{-}]$ (28). The intended interpretation of this category is
that the derivation is simulating the transition pair $\pi$ but has not yet
duplicated the tape stack (${-}$). The derivation then nondeterministically
extends the tape stack (29), in much the same way as for the initial
configuration in Section 4.2.2. At the end of the phase, the derivation tests
whether the two halves of the stack are equal, that is, whether the
nondeterministic extension indeed created an exact copy of the initial stack.
This test is crucial for our construction, and we describe it in more detail
below. If the test is successful, the derivation changes the target to
$[\pi;{+}]$, signifying that the derivation has successfully duplicated the
tape stack.

To support derivations such as the one in Figure 14, we introduce the
following lexicon entries and rules. Let $q\in Q$ be any universal state, and
let $\pi=(t_{1},t_{2})$ be any pair of transitions where
$t_{1}=(q,a)\to(q_{1},a_{1})$ and $t_{2}=(q,a)\to(q_{2},a_{2})$. Let also
$b\in\Sigma$ be any tape symbol. We introduce the lexicon entry
$\varepsilon\mathrel{:=}[q]/[\pi;{-}]$ and reuse the entries of the form
$\varepsilon\mathrel{:=}[b]$ that we introduced in Section 4.2.2. The
following rules implement the change of the target of $E(c)$ and
nondeterministic extension of the tape stack:

$\displaystyle[q]\mathinner{\$}/[\pi;{-}]\quad[\pi;{-}]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[q]\mathinner{\$}/X_{1}\cdots/X_{m}$ (28)
$\displaystyle[\pi;{-}]\mathinner{\$}/[b]\quad[b]$
$\displaystyle\quad\Rightarrow\quad[\pi;{-}]\mathinner{\$}$ (29)

A rule of the form (28) is a composition rule of degree $m$ that
simultaneously restricts the target of its primary input to $[q]$ and the
target of its secondary input to $[\pi;{-}]$. A rule of the form (29) is an
application rule that restricts the target of its primary input to
$[\pi;{-}]$.

$\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[q]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to400.99988pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[q]/[\pi;{-}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{-}]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{-}]/[a]/[b]/[a]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\hbox
to0.0pt{\quad\vbox to133.66663pt{\vfil\hbox{\small equality
test}\vfil}\hss}\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{-}]/[a]/[b]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}}}\quad\@deduce{}[\vbox
to267.33325pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[b]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\vbox
to334.16656pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[a]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}$
Figure 14: Simulation of transitions out of universal configurations, phase 1:
Duplicating the tape stack.

It remains to describe how to implement the equality test. To give an
intuition, Figure 15 shows a derivation that implements the test for the tape
$ab$ of our running example. For readability, we have numbered the arguments
on the tape stack. Step (30) uses a composition rule of degree $2m$ to change
the target of the root category to a new atomic category $[\pi;{=}_{1}]$. The
intended interpretation of this category is that the derivation needs to check
whether the two halves of the tape stack agree at position $1$ and $m+1$.
Accordingly, the composition used in step (31) is restricted in such a way
that it can only be instantiated if the two atomic categories at positions 1
and 3 are equal. Similarly, the composition used in step (32) can only be
instantiated if the two categories at positions 2 and 4 are equal. It is not
hard to see that this can be scaled up to $m$ tests, each of which tests the
equality of the categories at positions $i$ and $m+i$. Taken together, these
tests check whether the two halves of the tape are indeed identical.

More formally now, let $b\in\Sigma$ be any tape symbol. We introduce the
following shorthand notation, where $1\leq i\leq m$ is any tape position:

$\eta_{i,b}\quad\equiv\quad/X_{1}\cdots/X_{i-1}/[b]/X_{i+1}\cdots/X_{m}/X_{m+1}\cdots/X_{m+i-1}/[b]/X_{m+i+1}\cdots/X_{2m}$

Thus $\eta_{i,b}$ is a sequence of $2m$ slash–variable pairs, except that
$X_{i}$ and $X_{m+i}$ have been replaced with the concrete atomic category
$[b]$. Then to support derivations such as the one in Figure 15, we introduce
the following lexicon entries, where $1\leq i<m$:

$\varepsilon\mathrel{:=}[\pi;{-}]/[\pi;{=}_{1}]\qquad\varepsilon\mathrel{:=}[\pi;{=}_{i}]/[\pi;{=}_{i+1}]\qquad\varepsilon\mathrel{:=}[\pi;{=}_{m}]/[\pi;{+}]$

We also introduce the following composition rules of degree $2m$, for $1\leq
i<m$:

$\displaystyle[\pi;{-}]\mathinner{\$}/[\pi;{=}_{1}]\quad[\pi;{=}_{1}]/X_{1}\cdots/X_{2m}$
$\displaystyle\quad\Rightarrow\quad[\pi;{-}]\mathinner{\$}/X_{1}\cdots/X_{2m}$
(30)
$\displaystyle[\pi;{=}_{i}]\mathinner{\$}/[\pi;{=}_{i+1}]\quad[\pi;{=}_{i+1}]\eta_{i,b}$
$\displaystyle\quad\Rightarrow\quad[\pi;{=}_{i}]\mathinner{\$}\eta_{i,b}$ (31)
$\displaystyle[\pi;{=}_{m}]\mathinner{\$}/[\pi;{+}]\quad[\pi;{+}]\eta_{m,b}$
$\displaystyle\quad\Rightarrow\quad[\pi;{=}_{m}]\mathinner{\$}\eta_{m,b}$ (32)

$\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{-}]/[a]_{1}/[b]_{2}/[a]_{3}/[b]_{4}$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to200.49994pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\pi;{-}]/[\pi;{=}_{1}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{=}_{1}]/[a]_{1}/[b]_{2}/[a]_{3}/[b]_{4}$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\pi;{=}_{1}]/[\pi;{=}_{2}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{=}_{2}]/[a]_{1}/[b]_{2}/[a]_{3}/[b]_{4}$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\pi;{=}_{2}]/[\pi;{+}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]_{1}/[b]_{2}/[a]_{3}/[b]_{4}$}}}{\vphantom{([q^{+}\hat{S}])}}$
Figure 15: Equality test for the tape $abab$.

##### Phase 2: Splitting the Tape Stack

In the second phase, the derivation branches off into two subtrees, as was
illustrated in Figure 13. We present this second phase in more detail in
Figure 16. This derivation simulates the “splitting” of the tape stack into
two (identical) halves. To implement it, we introduce lexicon entries
$\varepsilon\mathrel{:=}[\pi;{+}]/[t_{1}]$ and
$\varepsilon\mathrel{:=}[b]/[b]/[t_{2}]$, where $b\in\Sigma$ is any tape
symbol. We also introduce the following rules:

$\displaystyle[\pi;{+}]\mathinner{\$}/[t_{2}]\quad[t_{2}]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[\pi;{+}]\mathinner{\$}/X_{1}\cdots/X_{m}$
(33) $\displaystyle[\pi;{+}]\mathinner{\$}/[b]\quad[b]/[b]/[t_{2}]$
$\displaystyle\quad\Rightarrow\quad[\pi;{+}]\mathinner{\$}/[b]/[t_{2}]$ (34)
$\displaystyle[\pi;{+}]\mathinner{\$}/[t_{1}]\quad[t_{1}]/X_{1}\cdots/X_{m}$
$\displaystyle\quad\Rightarrow\quad[\pi;{+}]\mathinner{\$}/X_{1}\cdots/X_{m}$
(35)

Rule of the forms (33) and (35) are composition rules of degree $m$. Note that
this ensures that the categories targeted at $[t_{1}]$ and $[t_{2}]$ encode a
tape of $m$ symbols. A rule of the form (34) is a composition rule of degree
$2$.

$\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]/[t_{2}]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[\pi;{+}]/[a]/[b]$}}\lx@proof@logical@and\vphantom{([q^{+}\hat{S}])}\@deduce{}[\vbox
to66.83331pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[\pi;{+}]/[t_{1}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t_{1}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}}\@deduce{}[\vbox
to133.66663pt{\leaders\hbox{\vphantom{x}.}\vfil\hbox{\vphantom{x}}}]{\vphantom{([q^{+}\hat{S}])}[b]/[b]/[t_{2}]}{\vphantom{([q^{+}\hat{S}])}\varepsilon}\@deduce{}[\leavevmode\hbox
to67.23pt{\vbox to67.23pt{\pgfpicture\makeatletter\hbox{\hskip
33.61665pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {} {}{{}}{}
{}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{33.41666pt}{66.83331pt}\pgfsys@lineto{-33.41666pt}{66.83331pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{30.26591pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}]{\vphantom{([q^{+}\hat{S}])}{\hbox{\pagecolor{yellow!60}\mathstrut$[t_{2}]/[a]/[b]$}}}{\vphantom{([q^{+}\hat{S}])}}$
Figure 16: Simulation of transitions out of universal configurations, phase 2:
Splitting the tape stack.

##### Phase 3: Simulating the Two Transitions

In the third and final phase, the derivation simulates the two transitions
$t_{1}$ and $t_{2}$. To implement this phase we do not need to introduce any
new lexicon entries or rules; we can simply reuse part of the construction
that we presented in Section 4.2.4 for the existential states. More
specifically, we can reuse the part of that construction that starts with a
category with target $[t]$ and uses rules (26) and (27).

##### Computational Complexity

All of the introduced lexical entries have size bounded by some constant
independent of the input size. At the same time, all of the rules introduced
in the four phases above have degree bounded by $2m$. It is easy to see that
we can construct each of these elements in time ${\cal O}({m})$. Furthermore,
the number of lexical entries and rules produced in this step is bounded by a
polynomial function of the input size. For instance, we add to $G$ a number
$|\Sigma|\cdot m$ of rules of types (30) and (31), since there is a single
rule for each choice of a tape symbol $a$ and index $i$ with $1\leq i<m$.
Similar analyses can be carried out for the remaining elements. We then
conclude that the overall contribution to $|G|$ in this step is polynomial in
$|M|$ and $|w|$, and the construction can be carried out in the same amount of
time.

####  4.2.6 Correctness

With all of the grammar components in place, we now address the correctness of
our construction. We argue that the sentential derivations of $G$ exactly
correspond to the accepting computations of $M$ when applied to the input
string $w$. To do this, we read $G$’s derivations in the canonical direction,
that is, from the leaves to the root. First of all, observe that the fragments
introduced in the various steps of the construction all use reserved target
categories, and they all use rules with target restrictions for these
categories. In this way, it is not possible in a derivation to mix fragments
from different steps—that is, fragments cannot be broken apart.

##### Accepting Configurations

A (sentential) derivation in $G$ starts with the fragments introduced in
Section 4.2.3. Each of these fragments uses composition rules to combine
several tape symbols into a category of the form $[\text{{accept}}]\alpha$,
and then switches to a category of the form $[q]\alpha$ with
$g(q)=\mathsf{A}$. Because of the degree restriction of Rule (22), the switch
is only possible if $\alpha$ has exactly $m$ arguments; in all other cases the
derivation will come to a dead end, that is, it will not derive the
distinguished category of the grammar. The categories $[q]\alpha$ composed by
the fragments of Section 4.2.3 encode accepting configurations of $M$, and it
is not difficult to see that all possible accepting configurations with
$g(q)=\mathsf{A}$ can be generated by these fragments. These are exactly the
leaves of our valid computation trees.

##### Existential Configurations

The derivation freely attempts to apply the transitions of $M$ to the
categories obtained as above and, recursively, to all the categories that
result from the application of these transitions. More precisely, a transition
$t$ applying to an existential configuration is simulated (in reverse) on a
category $[q]\alpha$ using the fragment of Section 4.2.4. This is done using
Rule (27), which switches from a category with target $[q]$ to a category with
target $[t]$, and produces a new category whose stack has $m+1$ arguments. At
this point, only some rule of type (26) can be applied, resulting in the
reduction of the stack, immediately followed by some rule of type (25), which
is a composition rule of degree $m$. If the derivation were to use more than
one occurrence of (26), then it would derive a category whose stack contains
fewer than $m$ elements. As a consequence, Rule (25) would no longer be
applicable, because of the restriction on the composition degree, and the
whole derivation would come to a dead end.

##### Universal Configurations

The derivation can also simulate (in reverse) the two transitions $t_{1}$ and
$t_{2}$ applying to a universal state $q$. This is done using the fragments of
Section 4.2.5. In this case the derivation starts with Rules (27) and (26)
used for the existential states; but now the involved categories have targets
$[t_{i}]$ disjoint from the targets used for the existential states, since
transitions $t_{i}$ apply to universal states. The simulation of $t_{1}$ and
$t_{2}$ results in categories $[q]\alpha$ and $[q]\alpha^{\prime}$ with the
same target $[q]$ and with $m$ arguments each. These categories are then
merged into a new category $[q]\alpha\alpha^{\prime}$ by concatenating their
stacks, and an equality test is successively carried out on
$\alpha\alpha^{\prime}$. If the test is successful, the derivation pops an
arbitrary number of arguments from $[q]\alpha\alpha^{\prime}$, resulting in a
new category of the form $[q]\alpha^{\prime\prime}$. Rule (28) can then be
applied only in case $[q]\alpha^{\prime\prime}$ has exactly $m$ arguments.
This means that $[q]\alpha^{\prime\prime}$ encodes one of the configurations
of $M$, and that $\alpha=\alpha^{\prime}=\alpha^{\prime\prime}$.

##### Initial Configuration

Finally, if the above process ever composes a category $[q_{0}]\alpha$
encoding the initial configuration of $M$ relative to the input string $w$,
then the derivation uses the fragment of Section 4.2.2. The rules of this
fragment switch the target category from $[q_{0}]$ to $[\text{{init}}]$, the
distinguished category of $G$, and then pop the stack arguments, providing
thus a sentential derivation for $\varepsilon$.

This correctness argument finally concludes the proof of our Lemma 4.3.

###  4.3 Membership in EXPTIME

It remains to prove the following:

######  Lemma 4.4.

The universal recognition for unrestricted VW-CCG is in EXPTIME.

To show this, we extend an existing recognition algorithm by Kuhlmann and
Satta (2014) that takes as input a VW-CCG $G$ with no empty categories and a
string $w$, and decides whether $w\in L(G)$.

##### Complexity of the Algorithm of Kuhlmann and Satta

The algorithm of Kuhlmann and Satta (2014) is based on a special decomposition
of CCG derivations into elementary pieces, adapting an idea first presented by
Vijay-Shanker and Weir (1990). These elementary pieces are specially designed
to satisfy two useful properties: First, each elementary piece can be stored
using an amount of space that does not depend on the length of $w$. Second,
elementary pieces can be shared among different derivations of $w$ under $G$.
The algorithm then uses dynamic programming to construct and store in a multi-
dimensional parsing table all possible elementary pieces pertaining to the
derivations of $w$ under $G$. From such table one can directly check whether
$w\in L(G)$. Despite the fact that the number of derivations of $w$ under $G$
can grow exponentially with the length of $w$, the two properties of
elementary pieces allow the algorithm to run in time polynomial in the length
of $w$. However, the runtime is not bounded by a polynomial function in the
size of $G$, as should be expected from the hardness results reported in
Section 3.1.

More specifically, let ${\cal A}$ be the set of all atomic categories of the
input grammar $G$, and let ${\cal L}$ be the set of all arguments occurring in
the categories in $G$’s lexicon. Let also $d$ be the maximum degree of a
composition rule in $G$, let $a$ be the maximum arity of an argument in ${\cal
L}$, and let $\ell$ be the maximum number of arguments in the categories in
$G$’s lexicon. We set $c_{G}=\max\\{d+a,\ell\\}$. Kuhlmann and Satta (2014)
report for their algorithm a running time in ${\cal O}({|{\cal A}|\cdot|{\cal
L}|^{2c_{G}}\cdot|w|^{6}})$.

To see that this upper bound is an exponential function in the size of the
input, observe that the quantities $|{\cal A}|$ and $|{\cal L}|$ are both
bounded by $|G|$, since each category in ${\cal A}$ or in ${\cal L}$ must also
occur in $G$. Furthermore, $\ell$ is bounded by the maximum length of a
category in $G$’s lexicon, and thus by $|G|$. Similarly, $d$ is bounded by the
length of some secondary component in a composition rule of $G$, and $a$ is
bounded by the length of some category in $G$’s lexicon. Then $d+a$ is bounded
by $|G|$ as well. Combining the previous observations, we have that $c_{G}$ is
bounded by $|G|$. We can then conclude that the runtime of the recognition
algorithm is bounded by

$|G|\cdot|G|^{2|G|}\cdot|w|^{6}\;=\;|G|^{1+2|G|}\cdot|w|^{6}\;=\;2^{\log{|G|}+2|G|\log{|G|}}\cdot|w|^{6}\,,$
(36)

which is indeed exponential in the size of the input.

##### Extension of the Algorithm of Kuhlmann and Satta to VW-CCG

As already mentioned, the algorithm by Kuhlmann and Satta (2014) works for a
grammar $G$ with no empty categories. More specifically, the algorithm starts
by adding to the parsing table items of the form $[X,i,i+1]$ for each category
$X$ that is assigned by $G$’s lexicon to the $i$-th word in the input string
$w$. Here $[X,i,i+1]$ represents an elementary piece of derivation consisting
of a tree with two nodes: a root with label $X$ and a child node with label
the $i$-th word of $w$. In order to extend the algorithm to unrestricted VW-
CCG, all we need to do is add to the parsing table items of the form $[X,i,i]$
for every empty category $X$ in $G$’s lexicon and for every integer $i$ with
$0\leq i\leq|w|$. This creates new elementary pieces of derivations accounting
for the empty string. These pieces can be combined with each other, as well as
with other pieces already existing in the table, triggering the construction
of derivations that involve empty categories.

The proof of the correctness of the recognition algorithm by Kuhlmann and
Satta (2014) immediately extends to the new algorithm. This is so because the
proof only rests on structural properties of CCG derivations, without any
assumption about the fact that these derivations involve words from $w$ or the
empty string. Furthermore, the exponential runtime reported above still holds
for the new algorithm. This is a consequence of the fact that we use the same
item representation as in the original algorithm for the elementary pieces of
derivations involving the empty string.

While the algorithms discussed above are designed for the random access
machine architecture, or RAM for short, it is well-known that any algorithm
working on a RAM can be computed on a deterministic Turing machine with only
polynomial-time overhead; see for instance Papadimitriou (1994, Theorem 2.5).
We can thus conclude that the universal recognition problem for VW-CCG can
still be solved in exponential time on a deterministic Turing machine.

###  4.4 Discussion

In view of our proof of Theorem 4.1, we now come back to the question raised
in Section 3.3. Specifically, we want to further investigate the features that
are responsible for the additional complexity that comes with unrestricted VW-
CCG. In our reduction in Section 4.2 we have used two features of the
formalism that were already discussed in Section 3.3, namely the capability to
define rules with restrictions on their secondary input categories, and the
capability to define rules whose secondary input categories do not have any
constant bound on their arity. In addition, we have also exploited two new
features, listed below. Again, dropping any one of these four features would
break our proof (but see our discussion in Section 5.1).

##### Derivational Ambiguity

Our grammar makes crucial use of derivational ambiguity. More precisely, $G$
encodes $M$’s configurations relative to $w$ into its own categories. We
assign all of these categories to the empty string $\varepsilon$, thus
introducing massive ambiguity in $G$’s derivations. Our proof of Lemma 4.3
would not work if we restricted ourself to the use of unambiguous grammars,
and we note that the computational complexity of the universal recognition
problem for the class VW-CCG restricted to unambiguous grammars is currently
unknown. Furthermore, on a par with lexical ambiguity discussed in Section
3.3, syntactic ambiguity is an essential feature in most formalisms for the
modeling of natural language syntax, including those whose universal
recognition problem can be parsed in polynomial time, such as TAGs. As such,
this individual feature cannot be held responsible, at least in isolation, for
the complexity of the recognition problem for the class VW-CCG, and in
designing a polynomially parsable version of VW-CCG we would not be interested
in blocking derivational ambiguity.

##### Unlexicalized Rules

We remind the reader that, broadly speaking, a lexicalized rule in a string
rewriting formalism is a rule that (directly) produces some lexical token. The
rule is also thought to be specialized for that token, meaning that the rule
contributes to the derivation by introducing some structure representing the
syntactic frame and valencies of the token itself. The basic idea of our proof
is to simulate valid computations of $M$ on $w$ through derivations of $G$. In
particular, each fragment in a derivation of $G$ uniquely represents some node
of a valid computation. It is therefore essential in our proof that each
fragment uses unlexicalized rules, that is, generates the empty string. One
may view this phenomenon in the light of computational complexity. It is not
difficult to verify that given an unlexicalized grammar $G$, it cannot be
transformed into a lexicalized grammar $G^{\prime}$ in polynomial time unless
NP $=$ EXPTIME.555This equality is considered unlikely to hold since it would,
for instance, imply that NP $=$ PSPACE, and that the polynomial hierarchy
collapses. For assume that such a polynomial-time transformation $T$ exists.
This would imply that an arbitrary instance $(G,w)$ of the universal
recognition problem with $\varepsilon$-entries can be converted (in polynomial
time) into an equivalent instance $(T(G),w)$ without $\varepsilon$-entries. We
know that the former problem is EXPTIME-complete and the latter problem is NP-
complete. Thus, the existence of $T$ imply that NP $=$ EXPTIME. One should
observe that this is not an effect of $T(G)$ being prohibitively large: the
size of the lexicalized grammar $T(G)$ is polynomially bounded in the size of
$G$, since $T$ is computable in polynomial time.

##  5 General Discussion

The computational effect of grammar structure and grammar size on the parsing
problem is rather well understood for several formalisms currently used in
computational linguistics, including context-free grammar and TAG. However, to