数理解析研究所講究録 1442 巻 2005 年 68-75

68

Logical Characterizations of LOGSPACE
Satoru Kuroda (黒田 覚)
Gunma Prefectural Women’s University (群馬県立女子大学)

1

Introduction

Bounded arithmetic is a branch of mathematical logic which characterizevarious classes of computational complexity by fragments of arithmeticaltheories. On the other hand, descriptive complexity gives another logicalmethod to characterize complexity classes. However, until recently, no actual connection was know between these two branches of mathematical
logic.
S. Cook and A. Kolokolova [2] gave an elegant method to define second
order systems of bounded arithmetic which utilizes the descriptive characterization of PTIME and. Their method uses the fragments of second
order logic which was used by E. Gradel to characterize those complexity
classes.
In this paper we will give a fragment of second order logic which characterizes LOGSPACE over finite ordered structures. This result may be used
to obtain a second order system of bounded arithmetic similar to Cook andKolokolova system for NL and P.
Descriptive characterizations for LOGSPACE is obtain ed ) Immerman
and Gr\"adel. The former one is by introducing deterministic transitive closure (DTC) to first order logic, while the latter is a fragment of second order
Krom logic. Our result is similar to the latter one, but the formula we use
is more natural.
$\mathrm{n}$$\mathrm{N}\mathrm{L}$$\mathrm{t}$$\mathrm{J}^{r}$

2

Descriptive complexity and LOGSPACE

2.1

Basic Notions

We will briefly review basic definitions of descriptive complexity. For
details, readers are encouraged to refer Immerman [4]A signature is a finite set of constant symbols and relation symbols. We

ea
do not include function symbols in signature but rather add thier graphs as
and so on.
relation symbols. Signatures are denoted by
Let a be a signature. A a-structure is a tuple
is a relation on for
is a possibly finite set called universe,
where.
for each constant symbol
andeach relation symbol
We will denote the number of elements in by .
$\sigma_{\backslash }\tau$$A=\langle A) \{R^{A}\}_{R\in\sigma}, \{c^{A},\}_{c\in\sigma}\rangle$$A$$R^{A}$$A$$R$$c\in\sigma$$\mathrm{c}^{A}\in A$$\in\sigma$

$A$

$|A$

{E}. Then the a1. Let E be a bina ry relation and a
Example 1
n $-1\})E^{A}\rangle$ repres enf“s a directed graph.
1,
structure A$=$$=\langle\{0,$\ldots ,a successor signature, where
2. The signature $\sigma=\{\min, \max, S\}$ is$\min$ and $\max$ are constant symbols denoting minimal and maximal elements of the universe respectively, and is a relation symbol denoting
relation.
the$co,ll^{\mathit{2}}‘\prime d$$S$$s\tau r,c,c_{J}essor$

3. $\sigma=\{\min, \max, \leq\}$ is called an ordered structure where $\min$ and $\max$
are as above $and\leq iS$ the usual order relation.

4.

structure where$and\cross$ are graphsof addition and multiplication respectively.

$\sigma=$

is called an$\{\min, \max, \leq)+_{)}\cross\}$$ar\mathrm{i}thmet\mathrm{i}c,al$$+$denote first order variables and upper case
Lower case letters $x,y,$ ,letters $X$ , $Y$, $Z$ , . . . denote second order variables. Since we do not havefunction symbols in signaturas, terms are either first order variables or constants. Formulae are built up from atomic formulae by applying the logical$\nearrow\lrcorner$$\ldots$. A logic is a set of formulae.
,connectives’
In order to make strict connections })etween logics and complexity classes,
it must be made clear how we regard finite structures as binary strings andvice versa.
can be regarded as a binary string by cod ing
A structuresuch thatof length
by a binary stringeach relation$\Lambda_{\backslash }$$\neg\forall\backslash$$\exists$$A=\{A,\overline{R}^{A},\overline{c}^{A}\}$$71^{k}$$R^{A}$$w_{R}A$$(x_{1}, \ldots, x_{n})\in R^{A}$a the corresponding t)it of

Similarly, each constant symbol
such that$c^{\mathrm{A}}$$w_{R^{A}}$is coded by a binary stringis 1.
$w_{c}A$of length$7l$$c^{A},=1\Leftrightarrow j\mathrm{t}\mathrm{h}$bit of$w_{\mathrm{c}^{A}}=\{$$=j$ ,

1 if

$n$

0if

$i\neq j$.

Finally, the code of the whole structure $A$ is the concatenation of codes for
relations and constants defined as above.
Conversely, a binary string of length can be represented by a structure
by introducing a unary relation $P$ such that$n/$$\langle\{0,1, \ldots, n.

$n$-1\}, \min, \mathrm{m}_{\mathrm{r}}^{l}]\mathrm{x}, \leq\rangle$$\mathrm{P}(\mathrm{i})\Leftrightarrow \mathrm{i}\mathrm{t}\mathrm{h}$bit of$\tau v$

is 1.

70
Now we a ready to state what it means that a logic corresponds to a.
complexity$\mathrm{c}1_{c\mathrm{L}}^{r}\mathrm{s}\mathrm{s}$Definition 1 Let be a logic, be a complexity class and 72 be a set offinite structures. We say thai captures over if the following conditions
hold:$\mathrm{C}$$\mathcal{L}$$C$

1. For all$\varphi\in \mathcal{L}$$d\xi^{\}}x\mathrm{i}dabl,e$$\mathrm{C}$$D$

and $A\in D_{f}$ the model checking problem$A\models\varphi$

is

in C.

2. For each set C$\in \mathrm{C}$th eve eists$\varphi\in \mathcal{L}S\uparrow J_{J}Ch$

that

.

$\forall A\in D(A\in \mathrm{C} \Leftrightarrow A\models\varphi)$

Some relations between logics and complexity classes are well-knownthe set of first order formulae, that , all quantifiers
Definition 2
isare first order quantifiers. SO is the set of second order formulae.
here $\in FO$ .
the set of formulae of the form
$FO\iota s$$\mathrm{i}_{\backslash },9$$SO\exists$$\exists\overline{P}\varphi(\overline{P})$$t$$\varphi$

Theorem 1 Over ordered structures, $FO$ cap rures the class rrniform
sizethat is, the class of sets computable by constant depth,
boolean circuits of unbounded fan-in.
$AC_{f}^{0}$$pol,\tau/nom\iota al$

Theorem 2 (Fagin’s Theorem) SO captures the polynomial hierarchy
cap rures the class $NP$ over all structures,.
over all$SO\exists$$stmctur\epsilon_{\nearrow}^{l}s$

It is not known whether there exists a logic which captures or smaller
complexity classes over all structures, However, several results are known
about the relations between logic and com plexity classes over ordered struc$\mathrm{P}$tures. So in the following, will concentrate on ordered structures.
There are two ways to capture complexity classes such as

andso on, namely, extending first order logic by operators or generalized quantifiers, and restricting second order logic.
$\mathrm{P}_{\backslash }\mathrm{N}\mathrm{L}_{\backslash }\mathrm{L}$2.2

Extending first order logic

By introducing additional operators to first order logic. various complexity classes below are characterized. Below we will give some examples.
$\mathrm{P}$Definition 3 Let, be a predicate symbol not in the signature a andbe a formula of the signature a $\cup\{P\}$ with only positive occurrences of,, . For each $\sigma- str?J,cture$
and with free variables
defines
mappin:.
$P$$\varphi(\overline{x})$$\overline{x}=x_{1}$$\varphi_{A}$$\ldots$$x_{\iota},$$P\mapsto\{\overline{rx} :(A, P)\models\varphi(\overline{\mathrm{r}x})\}$$A_{J}\varphi$

$P$

$a$

71
appears only positively, this rnapping is monotone. So
Since
least fixed point defined by$P$$\varphi A$

has

$a$

$P^{0}:=\emptyset)$$P^{j’+1}:=\varphi_{A}(P^{i})$,$P^{\omega}.-- \bigcup_{j\in\omega}\varphi_{A}(P^{j})$.

Norn we introd $uce$ the least fixed point operator $LFP$ such thatin the least fixed point of on the structure $A$ .
if and only if is$FO+LFP$ is definea as th first order logic with a positive least fixed$A\models[LFPP.\overline{x}\varphi](\overline{\mathrm{r}x})$$c,onto_{l}\mathrm{i}ned$$\overline{a}$$\varphi$

$e$

poin

$rt$

operator$[LFP_{P_{\backslash }\overline{x}}\varphi]$.

Theorem 3 (Immerman [5]) $FO+LFP$ captures the class P over orderei structures.

Another prominent example is the connection between transitive closureand logarithmic space.
,
be forrrvttla with free variables
Definition 4 Let
to be a. Then we define..
aridsuch that
if and only if there exists ,.
andsuch thatfor all$FO+TC$ is the first order logic extended by the operator $TC$ .
$\overline{?/}=y_{1},$$\overline{x,}=x_{1}$$0$$\varphi(\overline{x}_{7}\overline{?/})$$y_{k}$$c^{-}\circ$$A|=[TC_{\overline{x}.\overline{y}}\varphi(\overline{x},\overline{\tau j})](\overline{u},\overline{?)})$$x_{k}$,$\dot{\prime}c_{r\iota}^{-}\in A$$\ldots$$\mathrm{i}<7l$$A\models\varphi(\overline{c_{i},}, c_{i+1}^{-})$$c_{0}^{-}=\overline{\mathrm{f}J}_{f},\overline{c_{r\iota}}=\overline{b}$,$form\tau r_{l}lo$$[TC_{\overline{x}.\overline{y}}\varphi(\overline{x},\overline{\tau/})](\overline{u},\cdot\overline{lJ})$.)$\ldots$

Theorem 4 (Immerman [5]) $FO+TC$ cap rures the class of nondeterminintic logarithmic space computable sets NL over ordered structures.
There is also a deterministic version of $TC$ .

Definition 5 The deterministic transitive closure operator$DTC\uparrow,\mathrm{t}9$definedby$[DTC_{\overline{x},\overline{y}}\varphi(\overline{x},\overline{\tau/})]\equiv$[$TC_{\overline{x},\overline{y}}(\varphi(.’\overline{x},\overline{y})$A$\forall\overline{z}(\varphi(\overline{x},\overline{\nearrow.})arrow\overline{y}=\overline{z})$].

Theorem 5 (Immerman [5]) $FO+DTC$ captures the class of logarithmic space computable sets NL over ordered $st_{J}r?r,cture*9$ .

2.3

Fragments of second order logic

Second order logic can also be used to capture complexity classes. The
follow ing results are chie to Gr\"adel [3].
Definition 6 A second order formula is SO-Horn if it is of the$Q_{1}P_{1}\cdots Q_{k}P_{k}\forall\overline{y}\varphi(P_{1,7}\ldots P_{k},\overline{y})$$f^{l}orm$

72,,
or and is a quantifier free Hornis eitherwhere eachfor rmula with respect to , . . . , , thai is, it is in conjunctive norman form
such that in each clause there is at most one positive occu rrence of $sec,ond$order variable.
-Horn if all second order quantifiers are existential.
A formula is$Q_{1}$$\ldots$$Q_{k}$$\exists$$\forall$$\varphi$$P_{k}$$P_{1}$$(SO\exists)$

Proposition 1 SO-Horn collapses to (803) -Horrt,, that is, for all SOthat for arvy
there exists $a(SO\exists)$ Horn formulaHorn formula$\psi srl,c_{J}h$$\varphi$.

$st_{J}r\uparrow xct,\tau \mathit{1}1reA_{\mathrm{Z}}A\models\varphirightarrow\psi$

Theorem 6 (Gradel [3]) SO-Ho rn captures P over ordered struc rures.

Definition 7 A second order formula is SO-Krom if it is of the form
$Q_{1}P_{1}\cdots Q_{k}P_{k^{\wedge}}\forall\overline{\tau/}\varphi(^{\mathrm{p}_{1}..P_{k_{2}}\overline{?/}},.,)$or and is a quantifier free Kromis either,,where eachis, it is in conjunctive no rman forrn
formula with respect to , .. .
occurrences of second ordersuch that in each clause there are at mostvariabl, es.
-Krom if all second order $quo,n$ tifiers are existential.
for rmula is$Q_{1}$$\ldots$$Q_{k}$$\exists$$\forall$$\varphi$$P_{1}$)$P_{k;}t_{J}ho_{t}t$$t^{J}uJo$$A$$(SO\exists)$-Krom, that is, for all 50Proposition 2 SO-Krom collapses tosuch that for any-Krom
Krom formula there eists ,.
structure $A$ ,$(SO\exists)$$\varphi$$a$$fom\uparrow\gamma_{J}la$$(SO\underline{\exists})$$\psi$$A\models\varphirightarrow\psi$

Theorem 7 (Gradel [3]) SO-Krom captures NL over ordered sstructures.

2.4

A second order logic for LOGSPACE

Now we will state and prove our main result of this section. That is,
we will present a fragment of second order logic which captures the class

LOGSPACE.
Gradel’s second order logics SO-Horn and SO-Krom make use of satisfiability problems which are complete for and NL respectively. Analogously,
we will use a satifiability problem which is complete for to build a second
order logic capturing L.
Johannsenn [6] showed that the following satisfiability problem is complete for L.
$\mathrm{P}$$\mathrm{L}$Definition 8 A propositional formula is $CNF(2)$ if it is in conjunctive
normal form and each propositional variable occurs at most twice,
SAT(2) $:=$ { $\varphi\in CNF(2)$ :$\varphi$issatisfiable}

73
Theorem 8 (Johannsen [6]) SAT{2) is complete for$L$.

Using this result, we can define a fragment of second order logic as follows:

Definition 9 $(SO\exists)- CNF(2)$ is the set of formulae of the form$\exists P_{1}\cdots$$\exists P_{k}\forall\overline{y}\varphi(P_{1},$$\ldots$,$P_{k},\overline{?/}\mathrm{I}$is $CNF(2)$ with respect to , . . . , , that is, a quantifier free formula in conjunctive normal form such that each appears at

where$P_{1}$$\varphi(P_{1,\}}\ldots P_{k},\overline{?/})$$P_{k}$$P_{\iota}$most rwice.
First we will show that the model checking problem for $(SO\exists)-CNF(2)$formula is in L.
Theorem 9 Let $\varphi\in(SO\exists)- CNF(2)$ . Then the set of finite models ofin$L$$\varphi$is.

is a $CNF(2)$ forwhere(Proof). Let..,
and let $A$ t) a finite structure. First eIimimula with respect toto a conjunction
nate the universal quantifier by transforming
over all elements of $A$ . This yields a formula of the form$\varphi\equiv\exists P_{1}\cdots P_{k}\forall\overline{y}\varphi 0(P_{1}, \ldots, P_{k},\overline{\tau/})$$P_{k}$$P_{17}.$$\varphi 0$$\mathrm{e}$$\forall\overline{y}\varphi 0(\overline{P},\overline{y})$$\forall\overline{y}$$\exists P_{0}\cdot$..

$\exists P_{k}\varphi_{1}(P_{1}, \ldots, P_{k})$formula such that each clause is a disjunction of ’s
is a
where
and first order atomic formulae. Evaluate eahc atomic formula in $A$ . If it
is evaluated to true then eliminate all clauses which contain it. Otherwise
eliminate all occurrences of the atomic formula.
Now the original formu Ja is transformed into a formula of the form
$P_{?}$$\mathrm{C}\mathrm{N}\mathrm{F}$$\varphi_{1}$$\exists P_{1}$...

$P_{k^{\sim}}\varphi_{2}(P_{1}, \ldots, P_{k})$is considered as a propositional $CNF(2)$ formula. Thus checkwhereis the satisfiability problem of, .. . ’ing whether$CNF(2)$ formula. So ) Theorem 8 it is in L.
Next we will show that $(SO\exists)-CNF(2)$ is strong enought to express all
LOGSPACE relations. To do this, we will use an operator representing a$\varphi_{2}$$A|=\exists P_{1}\cdots\exists P_{k}\varphi_{2}(P_{1}$$P_{k})$$1$$\mathrm{y}$$\mathrm{n}\mathrm{g}$cor plete problem for LOGSPACE.
Proposition 3 (Johannsen [6]) The following tree-freeness (TF) pro btlen is ) $mp$ lete for OGSPA CE:$L$$c,\zeta$: Given an undirected graphponent in contain a cycle
$TF$

$G$

$G_{f}$

does$e\tau$) $er\uparrow/$connected$c_{J}om-$

74
be for rmulo.
Definition 10 Let
free parameters as shown,inhere and are -tuples of variables. We define the tree-freeness operator
that
in such aif and only if the undirecte graphwhose edge relation is defined by on the structure $A$ is tree-free,whereis the logic which consists ofform ulae of the form$\overline{x}$$\overline{?/}$$\uparrow \mathit{1}Jit_{J}h$$a$$\varphi(\overline{x},\overline{\tau}./)$

$k$

$d$

$A|=\mathrm{T}F_{\overline{x}_{\backslash }\overline{y}}\varphi$$\mathit{8}\mathit{1}jay$$\mathrm{T}\Gamma_{\overline{x}.\overline{y}}^{;}\varphi$$\varphi$$\mathrm{T}F_{\overline{x}_{\backslash }\overline{y}}\varphi$$\mathrm{T}F(FO)$$\varphi$

is a quantifier

free

$fo$

rmula.

Then the following holds:
Theorem 10 $\mathrm{T}F(FO)$ captures LOGSPACE over ordered structures,(Proof). This is an immediate consequence of Proposition 3.
Now it suffices to show that $(SO\exists)- CNF(2)$ formulae can express the.
tree-freeness operator$\mathrm{T}F$

Theorem 11 For $alt$ quantifier free formula there exists $a(SO\exists)- CNF(2)$.
for rmula such that for all ordered structure$\varphi$$A_{J}A|=\mathrm{T}F_{\overline{x},\overline{y}}\varphirightarrow\psi$$\psi$

Given an undirected graph $G=(V_{)}E)$ we will construct a
for each edge
$CNF(2)$ formula as follows: First introduce a variablewhich contains one$e\in E$ . For each vertex $v\in V$ we construct a clause
literal for each edge which is incident upon . If connects to a vertex
otherwise.
contains
andcontains
with greater number thenNow it is obvious that This formula is $CNF(2)$ and it is also readily
proved that is tree free if and only if this formula is satisfiable. Thus wehave proved the theorem,(Proof).

$\mathrm{d}$$P_{e}$$C_{v}$$v$$e$$C_{v}$$x_{e}$$v$$e$$C_{v}$$\overline{x}_{e}$$G$3Further research

Combining the result in this paper and the work of Cook and Kolokolova[2], we can construct a second order bounded arithmetic which corresponds
to LOGSPACE. Several other theory for LOGSPACE are obtained by D.
Zam t)ella [7] and Clote and Takeuti [1]. Using our result, we can construct a theory whose only nontrivial axiom is the comprehension scheme
for $(SO\exists)- CNF(2)$ formulae, which is simpler than other systems.
It is known that LOGSPACE is equivalent to the class of predicates which
are computable by polynomial size branching program . This fact has some
applications in logical approaches to the class LOGSPACE. Cook defined
the first propositional proof system which corresponds to LOGSPACE using
the branching program based characterization of the class.
Concering bounded arithmetic, we can define a t)oolean algebra basedon the set of polynomial size branching programs. So the boolean valued
method of Takeuti and Yasumoto [8] is also available for LOGSPACE.
$\mathrm{s}$75References[1] Clote, P. and G. Takeuti, First order bounded arithmetic andsmall boolean circuit complexity classes. In Feasible Mathematics, II,
Birkhauser, (1995).

[2] Cook, S. and A. Kolokolova, A second order theory for NL.
[3] Gridel, E., Capturing complexity classes by fragments of second-orderlogic. Theoretical Computer Science, 101 (1992), pp.35-57.
[$41\lrcorner$

Imr erman, N., Descriptive Complexity. Graduate Texts in Computer

Science, 1998, Springer.
[5] Immerman, N., Languages that capture complexity classes, SIAM J.
Compt., 16 (1987), pp. 760-778,[6] Johannsen, J., Satisfiability problems complete for deterministic loga. STACS 2004, Lecture
rithmic space. In: V.Diekert and M. Habib
Notes in Computer Science, 2996 (2004), pp. 317-325.
$\mathrm{e}\mathrm{d}\mathrm{s}$[$7_{\mathrm{J}}^{\rceil}$Zambella, D., Notes on polynomially t)ounded arithmetic. The Journalof Symbolic Logic, 61(1996), pp. 942-966.
[8] Takeuti, G. and M. Yasumoto, Forcing on Bounded Arithmetic, In.
G\"odel ’
A Peters, (1996), pp. 120-138$96_{\backslash }$$\mathrm{K}$