In a small-step semantics with a deterministic reduction strategy,
refocusing is a transformation that connects a reduction-based
normalization function (, a normalization function that enumerates the
successive terms in a reduction sequence – the successive reducts) and a
reduction-free normalization function (, a normalization function that
does not construct any reduct because all the reducts are deforested).

This transformation was introduced by Nielsen and the author in the early
2000's with an informal correctness proof.

Since then, it has been used in a variety of settings, starting with
Biernacka and the author's syntactic correspondence between calculi and
abstract machines, and several formal proofs of it have been put forward.

This article presents a simple, if overdue, formal proof of refocusing
that uses the Coq Proof Assistant and is aligned with the simplicity of
the original idea.

small-step semantics,
Structural Operational Semantics,
context semantics,
reduction semantics,
deterministic reduction strategy,
reduction-based normalization functions,
reduction-free normalization functions,

type isomorphisms,
delimited continuations,
the Coq Proof Assistant

§ BACKGROUND AND INTRODUCTION

This article motivates and illustrates refocusing through a simple but
telling language of arithmetic expressions with the possibility of errors
using the Coq Proof Assistant <cit.>.

This language is specified with a small-step semantics which gives rise
to a reduction-based normalization function that enumerates the reduction
sequence and makes one wish for its reduction-free counterpart

This wish is fulfilled by refocusing the enumeration
from the site of a contracted redex to the site of the next potential redex
without detouring via an intermediate reduct

The structure of the rest of this article is then outlined
(subsec:roadmap) and its prerequisites and notations are stated

§.§ The programming language of discourse

We consider a simple language of arithmetic expressions over natural
numbers with addition and subtraction:

An operation involves an operator and two operands, which are values:

Performing an operation yields a term if the given potential redex is an
actual one; otherwise, it yields an error message:

A potential redex where the minuend (, the left operand of a
subtraction) is smaller than the subtrahend (, the right operand of
this subtraction) is not an actual redex, and so contracting it elicits
an error message:

Evaluation is achieved by iterating reduction.

It yields either a value (a natural number) or an error message:

§.§ Small-step semantics of the programming language of discourse

The reduction strategy is leftmost innermost, , depth first and from left to right.

Here are two examples of a reduction sequence of terms in concrete syntax:

* $(1 + 10) + (2 + 20)$
$11 + (2 + 20)$
$11 + 22$

* $(1 - (5 + 5)) - (2 - 20)$
$(1 - 10) - (2 - 20)$
“numerical underflow: $-9$”

Since in a reduction sequence, several things happen during each
reduction step, let us make them explicit:

\diagram
\circ
\rto^{\text{{\small contract}}}
\circ
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\\
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\enddiagram

In this diagram,

* the right arrow at the bottom is one-step reduction function that,
given a reducible term, yields the next reduct in the reduction sequence,

* the slanted up arrow is a decomposition function that, given a
reducible term, yields a potential redex and its

context (a context is a term with a hole),

* the horizontal arrow at the top is the contraction function that, given an
actual redex, yields a contractum (a term), and

* the slanted down arrow is a recomposition function that, given a contractum and a
context, plugs the contractum in the context and yields the next reduct
in the reduction sequence.

Reduction is stuck if the given term cannot be decomposed into a
potential redex and a context or if the potential redex is not an actual

And as captured by the “there and back” propositions in
the recomposition function is a left inverse of the decomposition function.

In the author's mind, this diagram clarifies the

presentation of

reduction in context semantics <cit.>:

C[\mathit{r}] \longrightarrow C[c]

where $C$ is the context, $\mathit{r}$ is the redex, and $c$ is the contractum,
assuming the contraction rule $r \rightarrow c$.

The turning point for this clarification
was Nielsen candidly pointing out that on the left-hand
side and on the right-hand side of the arrow, the notation $C[\cdot]$
does not mean the same thing.

And indeed on the left-hand side, the notation means that the given term
is decomposed into a reduction context and a potential redex, whereas on
the right-hand side, the notation means that the reduction context is
recomposed around the contractum, yielding the reduct.

idea of refocusing is to “deforest” – to quote
Wadler <cit.> – the successive reducts in the
reduction sequence by going directly from a contractum and its context to
the next potential redex and its context (or to a value) when the
reduction strategy is deterministic:

\diagram
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{-->}[rr]^{\text{{\small refocus}}}
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{-->}[rr]^{\text{{\small refocus}}}
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{--}[r]
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\\
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\circ
\enddiagram

Evaluating a term by following the reduction sequence (decompose,
contract, recompose, decompose, contract, recompose, etc.) is referred to
as a “reduction-based” evaluation since it enumerates the successive
reducts, and evaluating a term by short-circuiting reducts (decompose,
contract, refocus, contract, refocus, etc.) is referred to as a
“reduction-free” evaluation since it does not construct the successive

There is evidence that such a refocus function exists and is useful,
witness the very existence of abstract machines since they directly
transition from actual redex to the next potential redex (or to the final
result), without detouring via the intermediate reduct.

Furthermore, if this refocus function could be expressed tail
recursively, it would provide the control flow of an abstract machine –
not by inventing this abstract machine, but by discovering it.

§.§ From reduction-based evaluation to reduction-free evaluation

In the early 2000's <cit.>,
Nielsen and the author observed that the refocus function, essentially,
is the decomposition function itself, and they provided an informal proof
of this observation as well as a variety of examples of its relevance.

Since then, several application-specific proofs of refocusing have been
put forward (see sec:correctness-proofs-of-refocusing) and
even more applications have been reported, starting with Biernacka and
the author's syntactic correspondence between calculi and abstract
machines <cit.>.

The point of the present article is to present a simple formal proof that
is aligned with the simplicity of the original idea.

§.§ Roadmap

a Structural Operational
Semantics <cit.> for the programming
language of discourse in Gallina, the resident pure and total functional
language of the Coq Proof Assistant.

This formalization is structurally recursive and in direct style.

sec:SOS-with-one-undelimited-continuation presents an
equivalent formalization of this Structural Operational
Semantics that uses one undelimited continuation – undelimited because
its codomain is polymorphic.

presents an equivalent formalization of this Structural Operational
Semantics that uses one delimited continuation and one discontinuity –
delimited because its codomain is monomorphic, and with one discontinuity
because for stuck terms, the reduction function does not apply the
current continuation: it stops with an error message instead.

presents an equivalent formalization of this Structural Operational
Semantics that uses two delimited continuations – one for
decomposing and one for recomposing – and one
discontinuity for stuck terms.

presents a defunctionalized version of the formalization of

This non-compositional format is independently known as that of a context
semantics <cit.> or again of a reduction
semantics <cit.>.

presents an equivalent formalization of the Structural Operational
Semantics of
sec:SOS-with-two-continuations-and-one-discontinuity that
uses one delimited continuation for decomposing, one context for
recomposing, and one discontinuity for stuck terms.

This formalization is compositional and therefore

expressible in Gallina.

Using this formalization, sec:the-simple-proof presents a
simple proof of the refocusing theorem by induction on the context.

sec:assessment assesses the optimality of refocusing as well
as its intrinsic and extrinsic applicability.

sec:related-work reviews related work: the context where
refocusing arose, its formal correctness proofs,

and its many applications

sec:conclusion-and-perspectives concludes and draws

app:defunctionalization presents defunctionalization and
illustrates it with a fitting example.

§.§ Prerequisites and notations

An elementary knowledge of Structural Operational Semantics, of Gallina,
and of the Coq Proof Assistant is expected from the reader.

The entirety of this work is formalized in

and all the propositions, lemmas, and theorem are proved in the
accompanying .v file, all the way to the isomorphism
mentioned at the end of app:defunctionalization.

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, IN DIRECT STYLE

Let us implement in Gallina the one-step reduction function of a
Structural Operational Semantics of the programming language of

* a literal reduces to a value;

* if the term t1 is stuck,

then so is the term Opr t1 opr t2, for any term t2;

* if the term t1 reduces to a term t1',

then for any term t2,
Opr t1 opr t2 reduces to Opr t1' opr t2;

* if the term t1 reduces to a value v1,

* if the term t2 is stuck,
then so is the term Opr t1 opr t2;

* if the term t2 reduces to a term t2',
then Opr t1 opr t2 reduces to Opr t1 opr t2';

* if the term t2 reduces to a value v2,
then Opr t1 opr t2 is a potential redex:

* if this potential redex is an actual one,
then contracting it yields a term;

Opr t1 opr t2 reduces to this term;

* if this potential redex is not an actual one,
then Opr t1 opr t2 is stuck.

So reducing a term can yield

* a value if this term does not contain a potential redex,

* the next term in the reduction sequence if this term contains a
potential redex which is an actual one (and therefore can be
contracted), and

* an error message if the term is stuck, , contains a potential redex
which is not an actual one, and therefore cannot be contracted:

As befits a Structural Operational Semantics, the

is structurally recursive, and each of its recursive calls
emulates the traversal of the associated proof tree, which is constructed
depth first and from left to right.

In words –

* reducing a given literal yields a value;

* reducing a given operation means first attempting to reduce its left
operand, which yields a value, a term, or an error message:

* if reducing the given left operand yields an error message, then this
left operand is stuck, and so is the given operation; reducing the
given operation yields this error message;

* if reducing the given left operand yields a term, then this left operand
contains an actual redex that was contracted; reducing the given
operation yields an operation whose first operand is this term and
whose right operand is the given right operand; and

* if reducing the given left operand yields a value, then there is
nothing to reduce in the left operand, and so we attempt to reduce
the given the given right operand, which yields a value, a term, or
an error message:

* if reducing the given right operand yields an error message, then this
right operand is stuck, and so is the given operation; reducing the
given operation yields this error message;

* if reducing the given right operand yields a term, then this right
operand contains an actual redex that was contracted; reducing the
given operation yields an operation whose first operand is
the term representing the value obtained by reducing the given left operand
(, the given left operand itself)
and whose right operand is this term; and

* if reducing the given right operand yields a value, then the given
operation is a potential redex, which we attempt to contract:

* if contraction succeeds, it yields a term which is the result of
reducing the given operation; and

* if contraction fails, it yields an error message which is the
result of reducing the given operation.

(The accompanying .v file contains a variation on
reduce_d where Term (Opr t1 opr t2') is returned
instead of Term (Opr (term_of_value v1) opr t2') and a proof
of its equivalence.)

Evaluation is implemented as iterated reduction.

To make it structurally recursive and therefore a valid Gallina program,
we thread a decreasing counter in the manner of Bove and
Capretta <cit.>:

Each reduction step performs an operation – and therefore removes one
operator – in the given term.

So given a natural number that is larger than the number of operators in any
given term, normalizing this given term terminates:

This implementation of one-step reduction is in direct style.

The next section describes an implementation in continuation-passing
style (CPS).

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, WITH ONE
UNDELIMITED CONTINUATION

As a first stepping stone towards refocusing,

here is

an equivalent implementation of the one-step reduction function that is
in (undelimited) continuation-passing style.

Again, as befits a Structural Operational Semantics, the implementation
is structurally recursive, and each of its tail-recursive calls emulates
the traversal of the associated proof tree, which is constructed depth
first and from left to right.

In words, given a continuation –

* reducing a given literal continues with a value;

* reducing a given operation means first attempting to reduce its left
operand with a new continuation, which is then sent a value, a term, or
an error message:

* if the continuation is applied to an error message, then this
left operand is stuck, and so is the given operation; reducing the
given operation continues with this error message;

* if the continuation is applied to a term, then this left operand
contains an actual redex that was contracted; reducing the given
operation continues with an operation whose first operand is this term and
whose right operand is the given right operand; and

* if the continuation is applied to a value, then there is nothing to
reduce in the left operand, and so we attempt to reduce the given
right operand with a new continuation, which is then sent a value, a
term, or an error message:

* if the continuation is applied to an error message, then this
right operand is stuck, and so is the given operation; reducing the
given operation continues with this error message;

* if the continuation is applied to a term, then this right
operand contains an actual redex that was contracted; reducing the
given operation continues with an operation whose first operand is
the given left operand

and whose right operand is this term; and

* if the continuation is applied to a value, then the given
operation is a potential redex, which we attempt to contract:

* if contraction succeeds, it yields a term and reducing the given
operation continues with this term; and

* if contraction fails, it yields an error message and reducing the given
operation continues with this error message.

The codomain of reduce3_c' is polymorphically typed and so is
the codomain of its continuation, which is thus undelimited.

This tail-recursive implementation of one-step reduction is in
continuation-passing style <cit.>.

Analyzing the structure of the continuation, we see that when the given
term is stuck, the continuation is applied to an error message, which
triggers the previous continuation (k3) to be applied to an
error message, etc., all the way to the initial continuation, just as in
the definition of reduce_d.

If we were to split the continuation into a pair of continuations, one
applied to values or to terms, and the other to error messages, we could
bypass this propagation of error messages.

(This splitting is made possible by the isomorphism between $A + B
\rightarrow C$ and $(A \rightarrow C) \times (B \rightarrow C)$.)

Furthermore, we would then be in position to anticipate the instantiation of
the polymorphic type of answers in the definition of
reduce3_c and directly apply the second continuation for
potential redexes that are not actual ones to return the error message.

This massaging leads to the one-step reduction function described in the
next section, where

* the continuation is delimited because its codomain of answers is
monomorphically typed, and

* for potential redexes that are not actual ones, the continuation is not
applied, which is a discontinuity.

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, WITH ONE
DELIMITED CONTINUATION AND ONE DISCONTINUITY

As a second stepping stone towards refocusing,

here is

an equivalent implementation of the one-step reduction function that is
in delimited continuation-passing style and has a discontinuity.

As still befits a Structural Operational Semantics, the implementation
is structurally recursive, and each of its tail-recursive calls emulates
the traversal of the associated proof tree, which is constructed depth
first and from left to right.

In words, given a continuation –

* reducing a given literal continues with a value;

* reducing a given operation means first attempting to reduce its left
operand with a new continuation, which is then sent a value or a term:

* if the continuation is applied to a term, then this left operand
contains an actual redex that was contracted; reducing the given
operation continues with an operation whose first operand is this term and
whose right operand is the given right operand; and

* if the continuation is applied to a value, then there is nothing to
reduce in the left operand, and so we attempt to reduce the given
right operand with a new continuation, which is then sent a value or
a term:

* if the continuation is applied to a term, then this right
operand contains an actual redex that was contracted; reducing the
given operation continues with an operation whose first operand is
the given left operand

and whose right operand is this term; and

* if the continuation is applied to a value, then the given
operation is a potential redex, which we attempt to contract:

* if contraction succeeds, it yields a term and reducing the given
operation continues with this term; and

* if contraction fails, it yields an error message and reducing the given
operation directly yields this error message, which is the discontinuity.

The codomain of reduce2_c' is monomorphically typed and so is
the codomain of its continuation, which is thus
delimited <cit.>.

So stricto sensu this tail-recursive implementation of one-step reduction
is not in continuation-passing

style –

it is in delimited continuation-passing style.

Analyzing the structure of the continuation, we see that

either it continues the decomposition or it carries out a recomposition.

In the next section, we split this delimited continuation into two: one
delimited continuation that is applied to values to continue the
decomposition, and one delimited continuation that is applied to terms to
carry out the recomposition.

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, WITH TWO
DELIMITED CONTINUATIONS AND ONE DISCONTINUITY

As a third stepping stone towards refocusing,

here is

an equivalent implementation of the one-step reduction function that uses
two delimited continuations – one that is applied to values to continue
the decomposition and has type value -> value_or_term, and
one that is applied to terms to carry out the recomposition and has type
term -> term – and one discontinuity

for stopping

with an error message in case the potential redex is not an actual one.

We refer to the continuation of type value -> value_or_term
as “the decomposing continuation” and the other, which has type
term -> term, as “the recomposing continuation.”

§.§ Decomposition

Let us factor out the decomposition facet of the one-step reduction
function into a (tail-recursive) decomposition function:

This decomposition function either returns a value or a decomposition.

In the latter case, this decomposition contains a potential redex and the
two continuations that were in effect when this potential redex was

As mentioned in
the recomposing continuation is a left inverse of the decomposition function:

§.§ One-step reduction

Using the decomposition function, the one-step reduction function is
stated as follows:

To prove its equivalence with the one-step reduction function in direct
style (sec:SOS-in-direct-style), we make use of the
following three lemmas that relate reduce_d and

* For any given term, if applying reduce_d to it yields a
value, then applying decompose_term_cc to this term, a
decomposing continuation, and a recomposing continuation yields
the same result as applying this decomposing continuation to this

* For any given term, if applying reduce_d to it yields
another term, then (1) applying decompose_
term_cc to this term, a decomposing continuation, and a
recomposing continuation yields a decomposition of this term into a
potential redex, another decomposing continuation, and another
recomposing continuation, (2) contracting the potential redex yields a
contractum and (3) applying the new recomposing continuation to this
contractum yields the same reduct as applying the recomposing
continuation to this other term:

* For any given term, if applying reduce_d to it yields an
error message, then applying decompose_term_cc to this
term, a decomposing continuation, and a recomposing continuation
yields a potential redex whose contraction yields the same error

The equivalence of reduce_d and reduce_cc
follows, and likewise for the corresponding reduction-based normalization

§.§ A more convenient reduction-based normalization function

Currently, the normalization function tests the result of one-step
reduction and the reduction function tests the result of the
decomposition function.

Let us streamline these two tests into one by iterating on the result of
decomposition, , the final value or the next decomposition:

We are getting close to the first diagram of

(The slanted down arrow is the recomposing continuation.)

In words – after an initial decomposition, the iteration function tests
whether normalization should stop (with a value or with an error message)
or continue by (1) recomposing the reduction context over the contractum
with kr and (2) decomposing the resulting reduct with
decompose_cc, as underlined above with .

§.§ The corresponding reduction-free normalization function

The thesis here is that there is no need to recompose the context
around the contractum and then decompose the resulting reduct – one can
instead continue the decomposition over the contractum to obtain a final
value or the next decomposition with decompose_term_cc, as
underlined below with .

We are getting close to the second diagram of

(The dashed arrow (, refocus) is the decomposition function.)

Here is the equivalence between reduction-based normalization and
reduction-free normalization we want to prove:

By extension, here is the refocusing theorem we want to prove:

In words – if decomposing a given term yields a potential redex, a
decomposition continuation, and a recomposing continuation, then for any
term, it is equivalent (a) to recompose the reduction context over this
term and then decompose the result and (b) to continue the decomposition
of this term with the decomposition continuation and the recomposing

Proving this theorem would most naturally be done by induction over the
recomposing continuation, were it not for it being a function.

So, defunctionalization to the rescue.

In sec:SOS-with-one-context-and-one-discontinuity, we
defunctionalize both the decomposing continuation and the recomposing
continuation, but even though the result is of independent interest, that
is overshooting.

So in
we only defunctionalize the recomposing continuation, and that is
enough for proving the refocusing theorem by induction on the data type
of the recomposing continuation – , the context – in

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, WITH ONE
CONTEXT AND ONE DISCONTINUITY

Since they were split from the same delimited continuation in
defunctionalizing the two delimited continuations in
sec:SOS-with-two-continuations-and-one-discontinuity yields
the same data type of reduction contexts and two dispatching functions:
one to continue the decomposition and one to continue the recomposition.

This format is independently known as that of a context
semantics <cit.> or again of a reduction
semantics <cit.>.

Implementing it in Gallina, however, is

not immediate because – as usual –
after defunctionalizing the continuation of a recursive function, the
resulting program is not compositional.

Therefore, a functional representation requires an encoding in the manner
of Bove and Capretta <cit.> to make it
structurally recursive.

Alternatively, the representation could be relational instead of
functional, which

brings us from the frying pan into two fires since

the formalization is no longer an executable functional program and
unique decomposition becomes an issue that needs to be addressed.

The next section goes halfway by only defunctionalizing the recomposing
continuation: the result is still compositional and therefore expressible
in Gallina.

§ A STRUCTURAL OPERATIONAL SEMANTICS, FUNCTIONALLY, WITH ONE
DELIMITED CONTINUATION, ONE CONTEXT, AND ONE DISCONTINUITY

In this section, we only defunctionalize the recomposing continuation
from sec:SOS-with-two-continuations-and-one-discontinuity,
which gives rise to a grammar of recomposing contexts.

These contexts can be represented inside-out
(subsec:inside-out-contexts) or outside-in

We then implement the decomposition function with a decomposing
continuation, a recomposing context, and a discontinuity, and we prove
that the recomposition function is a left inverse of the decomposition

In addition though, we present an inductive relation that connects the
decomposing continuation and the recomposing context, and we prove that
if decomposing a term yields a potential redex, a decomposing
continuation, and a recomposing context, then this continuation and this
context are in this relation.

We then implement the corresponding one-step reduction function
the corresponding reduction-based normalization function
(subsec:the-reduction-based-normalization-function), and the
corresponding reduction-free normalization function

And that puts us in position to prove the refocusing theorem by
induction over the context (sec:the-simple-proof).

§.§ Inside-out contexts

Let us defunctionalize the recomposing continuation.

The resulting data type is that of the inside-out contexts from the
left-to-right reduction strategy,

which independently gave rise to `zippers' <cit.>.

This data type is flat and so isomorphic to lists.

Accordingly, let us represent a context as a list of control frames:

Since the context is inside-out and was accumulated iteratively by the
decomposition function, its associated recomposition function is also
tail recursive:

§.§ Outside-in contexts

Nothing prevents one from representing contexts outside in.

(To quote, “contexts are specified so that a context can easily be
extended to the left or to the
right <cit.>.)

The associated recomposition function is then recursive:

The two recomposition functions are related in the manner of Burge and
Landin's loop fusion <cit.> and of Bird and
Wadler's third duality theorem <cit.>:

In words – outside-in contexts and inside-out contexts are reverse of
each other.

The accompanying .v file contains a recursive implementation
of decomposition that returns a value or a potential redex together with
its context.

This context is not accumulated at call time (like the accumulator in the
tail-recursive list reverse function), it is constructed at return time
(like the result of the recursive list copy, list append, and list map

So if the tail-recursive decomposition function yields a potential redex
and its context, this context is inside out, and if the recursive
decomposition function yields a potential redex and its context, this
context is outside in.

As proved in the accompanying .v, these two potential redexes
are the same one and these two contexts are inverses of each other.

§.§ Decomposition

Here is the defunctionalized counterpart of the result of decomposition
in sec:SOS-with-two-continuations-and-one-discontinuity:

Here is the defunctionalized counterpart of the decomposition function
in subsec:SOS-with-two-continuations-and-one-discontinuity:decomposition

This decomposition function either returns a value or a decomposition,
and this decomposition contains a potential redex and the decomposing
continuation and recomposing context that were in effect when this
potential redex was found.

As mentioned in
the recomposition function is a left inverse of the decomposition function:

The following relation characterizes the correspondence between the
decomposing continuation and the recomposing context in a decomposition:

If decomposing a term yields a potential redex, a continuation, and a
context, then this continuation and this context are in this relation:

Incidentally, since defunctionalizing the decomposing continuation gives
rise to this very data type of contexts, this relation also connects this
decomposing continuation and its defunctionalized counterpart: it is the
relational content of defunctionalization (and refunctionalization) here.

§.§ One-step reduction

Using the decomposition function, the one-step reduction function is
stated as follows:

For brevity, we omit the

lemmas that relate reduce_d and

Their statements can be deduced from the similar lemmas in

(The accompanying .v file contains them as well as their proof.)

The equivalence of reduce_d and reduce_cC

§.§ The reduction-based normalization function

Here is the defunctionalized counterpart of the reduction-based
normalization function from

We are now implementing the first diagram of

§.§ The reduction-free normalization function

The thesis here is still that there is no need to recompose the context
around the contractum and then decompose the resulting reduct – one can
instead continue the decomposition over the contractum to obtain a final
value or the next decomposition:

We are now implementing the second diagram of

Here is the equivalence between reduction-based normalization and
reduction-free normalization

we wish for,

and that we are now in position to prove simply:

§ THE SIMPLE PROOF

After de Bruijn presented his eponymous indices and levels to represent
bound variables in $\lambda$ terms <cit.>, the indices
became a hit because they correspond to the lexical offsets of the bound
variables <cit.>.

Later in his life, de Bruijn pointed out that the levels are a better fit when
generating $\lambda$ terms, which is very true in normalization by
evaluation for example <cit.>.

A similar situation occurs here.

A priori we want to write something like the following:

In words – given a term that can be decomposed into a potential redex, its
decomposing continuation, and its recomposing context, decomposing
the result of recomposing this context over any other term gives the
same result as decomposing this other term with the same context and the
same continuation.

Proving this theorem is challenging because decompose_cC
consumes the outer component of the recomposed term, which is constructed
last since the context is inside out.

If the context were outside in, we would be in position to “cancel out”
the outside constructors of the context and their subsequent
decomposition, inductively, in the proof.

So should we represent contexts outside in?

That would inflict a linear overhead to extending the contexts during the

Instead, let us exploit

the relation between recomposing_io and recomposing_oi

from subsec:outside-in-contexts and transiently reverse the
context once it has been constructed – in the proof, not in the program.

Generalizing, here is a Eureka lemma that captures what happens in the

In words – we are given a term, a potential redex, a decomposing
continuation k_rf, an outside-in context, and an inside-out
context that are such that the term decomposes into this potential redex,
k_rf, and the concatenation of the reverse of the outside-in
context and the inside-out context.

Then, for any decomposing continuation k_rb that is related
to the inside-out context, decomposing the result of recomposing the
outside-in context over any other term with k_rb and the
inside-out context gives the same result as decomposing this other term
with k_rf and the concatenated context.

This lemma is proved by induction on C_io.

The refocusing theorem is a corollary of this lemma, witness the last
line of its proof:

The equivalence of iterate_cC_rb and
iterate_cC_rf follows, and so does the equivalence of
normalize_cC_rb and normalize_cC_rf.

§ ASSESSMENT

This section briefly

discusses the optimality of the refocus function,

analyzes the applicability of refocusing,

puts this applicability into perspective.

§.§ Optimality of the traversal after refocusing

If there is something to optimize after refocusing then it is the
decomposition function that needs to be optimized, and that means that it
was not optimal in the first place, which is hard to imagine for the
functional implementation of the reduction strategy in a Structural
Operational Semantics when this strategy is deterministic.

Here is another argument for this optimality:

In the syntactic correspondence between calculi and abstract
machines <cit.>, the next step after refocusing is
lightweight fusion by fixed-point promotion <cit.> of
iterate_cC_rf and decompose_term_cC.

Performing this next step and inlining the contraction function then
yields the compositional evaluation function for arithmetic expressions
that one would authoritatively write by hand using a delimited
continuation and with a discontinuity to account for numerical underflow.

And likewise, defunctionalizing this continuation yields the canonical
abstract machine for arithmetic expressions with left-to-right evaluation
that is such a pleasure to invent <cit.>.

This compositional evaluation function and this abstract machine,
however, were not invented – they were discovered.

(Precedents include

Knuth discovering and Morris inventing the KMP
string-matching algorithm <cit.>,

Reynolds discovering <cit.>
and Felleisen and Friedman inventing <cit.>
the CEK machine,

Schmidt discovering <cit.>
and Krivine designing <cit.>
the Krivine machine –

illustrations of Rota's insightful piece about theorizers and problem
solvers <cit.>.)

§.§ Applicability

Refocusing scales to context-sensitive contraction
rules <cit.>.

For outermost reduction strategies <cit.>, if
the contraction rules overlap, one needs to recompose the contractum with
a prefix of the context to resolve the ambiguity – a local solution for
a local problem – and then the decomposition can unambiguously be

The salient point here is that we are not inventing, we are discovering
and ending with the reduction-free normalization function that one would
– a priori or a posteriori – happily invent in the first place.

The author is aware that the previous sentence contains a strong
statement – as well as a subjective one – but this statement has not been
invalidated in the 20+ years of existence of refocusing.

§.§ On the inter-derivation of semantic artifacts

Just like the measure of goodness for a programming language is how
convenient a notation it offers for expressing computation (, for
programming), the measure of goodness for a formal semantics is how
convenient a notation it offers for reasoning (, for proving).

In practice – and the present article makes no exception – formal
semantics are inter-derived to put oneself in position to prove a

In the present case,
document such a derivational journey.

Consider the derived Structural Operational Semantics with one delimited
continuation, one context, and one discontinuity

at the end of this journey.

A decomposition is a triple – potential redex, recomposing context,
and decomposing continuation.

The reduction-based normalization function
(subsec:the-reduction-based-normalization-function) ignores
the decomposing continuation and the reduction-free normalization
function (subsec:the-reduction-free-normalization-function)
ignores the recomposing context.

And so this semantics is teetering between reduction-based normalization
and reduction-free normalization,

making it simple

to state the refocusing theorem and prove it.

More broadly, though, all the work invested in inter-deriving formal
semantics can also be seen as a collective effort for establishing the
semantic analogue of Turing completeness for programming languages, which
makes some kind of sense considering the Curry-Howard correspondence,
where programming is proving and proving is programming.

Induction proofs would be akin to recursive programming, rule induction to
logic programming, coinduction to rewriting, etc., suggesting which kind
of program should be extracted from which kind of proof.

To sketch a taxonomy for inter-deriving semantic artifacts based on the
operational content of their format,

* refocusing connects reduction-based normalization
(discrete, observable reduction steps) and
reduction-free normalization (continuous, unobservable reduction steps),

* lightweight fusion by fixed-point promotion <cit.>
connects small-step normalization and big-step
normalization <cit.>,

* continuation-passing
style <cit.>
ensures evaluation-order
independence <cit.>,
in one big step,

* direct style provides a granularity for big steps,

* defunctionalization <cit.>
provides first-orderness, witness the rational reconstruction of
reduction semantics in

* closure conversion <cit.> connects compositional and
non-compositional normalization functions when expressible values are

* explicit substitutions <cit.> provide a
foundation for environments <cit.>, and

* abstract machines provide a welcoming intersection where theoreticians
feel that they are doing implementation work and implementors feel
that they are doing theory.

The elements above do not fall out of the sky – they are part of the
syntactic correspondence between context-sensitive calculi and abstract
machines <cit.> and of the functional
correspondence between evaluators and abstract
machines <cit.>, but the taxonomy above is just a sketch.

Still, this sketch seems to be in the right ballpark, considering the
coincidence of the reduction contexts in a small-step semantics and of
the evaluation contexts in a big-step semantics.

The reduction contexts in a small-step semantics are interpreted by the
recomposition function, and are the defunctionalized counterpart of the
continuation in the corresponding one-step reduction function.

The evaluation contexts in a big-step semantics are interpreted by a
“continue” function (cf. eval/continue abstract machines) and are the
defunctionalized counterpart of the continuation in the corresponding
big-step evaluation function.

This coincidence heralds a global unity between small-step and big-step
semantics, one that links Plotkin's motto that well-typed programs do not
get stuck in a small-step semantics and Milner's motto that well-typed
programs do not go wrong in a big-step semantics as two sides of the same
computational coin.

Along the same line, it is also spectacular how monadic effects in a
big-step semantics <cit.> are mirrored by context-sensitive
contraction rules in small-step semantics <cit.>.

So, ballpark.

§ RELATED WORK

This section reviews related work: the context where refocusing arose,
its few other correctness proofs, and its many applications.

§.§ Context of refocusing

Let us revisit the programming language of discourse and its small-step

Structural Operational Semantics is a small-step direct semantics and one
reduction step gives rise to constructing a proof tree.

At the top of this proof tree, a redex is contracted:

\displaystyle
\frac
\frac
\frac
{5 + 5 \rightarrow 10}}
{1 - (5 + 5) \rightarrow 1 - 10}}
{(1 - (5 + 5)) - (2 - 20) \rightarrow (1 - 10) - (2 - 20)}

Let us reformat this proof tree to emphasize its implicit decomposition,
its contraction, and its implicit recomposition:

\diagram
\
\rrto^{\Text{contraction}}
\
\ddto^{\Text{implicit \\ recomposition}}
\\
\
{\begin{array}{l@{\ }c@{\ }l}
\phantomoutercontextp{\phantominnercontextp{\phantom{(}5 + 5}}
\rightarrow
\phantomoutercontextp{\phantominnercontextp{10}}
\\
\hline
\phantomoutercontextp{\innercontextp{5 + 5}}
\rightarrow
\phantomoutercontextp{\innercontext{10}}
\\
\hline
\outercontextp{\innercontextp{5 + 5}}
\rightarrow
\outercontextp{\innercontext{10}}
\end{array}}
\
\\
\
\uuto^{\Text{implicit \\ decomposition}}
\
\enddiagram

Reduction semantics is a small-step continuation semantics where the
continuation is delimited and represented as a context, and so one
reduction step gives rise to (1) constructing the context of the redex,
(2) contracting the redex, and (3) recomposing the context around the
contractum to yield the reduct:

\begin{align*}
\begin{array}{@{}l@{ }c}%
\left.
\begin{array}{@{}l@{ }}%
\phantom{[}(1 - (5 + 5)) - (2 - 20)\phantom{]}
\\
{}[(1 - (5 + 5)) - (2 - 20)]
\\
{}[\phantom{\hspace{0.4mm}}[1 - (5 + 5)]\phantom{\hspace{0.4mm}} - (2 - 20)]
\\
{}[\phantom{\hspace{0.4mm}}[1 - \phantom{\hspace{0.4mm}}[5 + 5]\phantom{\hspace{0.4mm}}]\phantom{\hspace{0.4mm}} - (2 - 20)]
\end{array}
\right\rbrace
\begin{array}{@{}c@{}}
\mathrm{explicit}
\\
\mathrm{decomposition}
\end{array}
\\
\mathrm{contraction}
\\
\left.
\begin{array}{@{}l@{ }}%
\phantom{\hspace{0.5mm}}[\phantom{\hspace{0.4mm}}[1 - \phantom{\hspace{0.4mm}}[\phantom{\hspace{2.26mm}}10\phantom{\hspace{2.26mm}}]\phantom{\hspace{0.4mm}}]\phantom{\hspace{0.4mm}} - (2 - 20)]
\\
{}[\phantom{\hspace{0.4mm}}[1 - \phantom{\hspace{0.4mm}}{\phantom{[}}\phantom{\hspace{2.28mm}}10\phantom{\hspace{2.28mm}}{\phantom{]}}\phantom{\hspace{0.4mm}}]\phantom{\hspace{0.4mm}} - (2 - 20)]
\\
{}[(1 - \phantom{\hspace{0.4mm}}{\phantom{[}}\phantom{\hspace{2.28mm}}10\phantom{\hspace{3.4mm}})\phantom{\hspace{0.4mm}} - (2 - 20)]
\\
{}\phantom{[}(1 - \phantom{\hspace{0.4mm}}{\phantom{[}}\phantom{\hspace{2.28mm}}10\phantom{\hspace{3.4mm}})\phantom{\hspace{0.4mm}} - (2 - 20)\phantom{]}
\end{array}
\right\rbrace
\begin{array}{@{}c@{}}
\mathrm{explicit}
\\
\mathrm{recomposition}
\end{array}
\end{array}
\end{align*}

At the turn of the century <cit.>, the
question arose how to “short-circuit” the construction of the
intermediate reduct to go directly from a contractum and its context to
the next potential redex and its context.

Refocusing is the answer to this question, and the value of this answer
is that as it happens, refocused reduction semantics are in one-to-one
correspondence with abstract machines that were independently

designed <cit.>.

§.§ Correctness proofs of refocusing

Nielsen and the author stated structural conditions
about reduction semantics under which refocusing is possible, and
provided an informal proof for them <cit.>.

These structural conditions are essentially the same as in Xiao et al.'s
work <cit.>.

In his MSc thesis <cit.>, Sieczkowski formalized
refocusing using the Coq Proof Assistant.

Sieczkowski, Biernacka, and Biernacki presented a generic formalization
of refocusing and formally proved its correct, using the Coq
Proof Assistant <cit.>.

In his PhD thesis <cit.>, Bach Poulsen proved the
correctness of refocusing for XSOS using rule induction.

When studying how the syntactic correspondence fares for outermost
reduction strategies instead of for innermost
ones <cit.>, Johannsen and the author noticed
another condition about the contraction rules when they are
context-sensitive and overlap: after a contraction, decomposition should
not continue on the contractum with its context but on the partially
recomposed contractum that disambiguates the overlap and with the rest of
this context.

García-Pérez and Nogueira characterized this other
condition as a hybrid reduction strategy <cit.>.

Biernacka, Charatonik, and Zielinska generalized refocusing to both
uniform and hybrid strategies and formally proved it correct, using the
Coq Proof Assistant <cit.>.

Using Agda, Swiestra formalized the syntactic correspondence between the
$\lambda\widehat{\rho}$ calculus (a version of Curien's $\lambda\rho$
calculus of explicit substitutions <cit.> that is closed
under reduction <cit.>) with a normal-order
reduction strategy and the Krivine machine <cit.>, which
included proving the refocusing step.

Also using Agda, Rozowski formalized the syntactic correspondence between
the $\lambda\widehat{\rho}$ calculus with an applicative-order reduction
strategy and the CEK machine <cit.>, which also included
proving the refocusing step.

§.§ Applications of refocusing

The author's doctoral thesis <cit.> lists
applications of refocusing until 2006:
to context-based CPS transformations,
to specifications of the $\lambda$ calculus with implicit and with explicit substitutions,
to specifications of the $\lambda$-calculus with explicit substitutions and computational effects,
with more examples listed at a summer school <cit.>.

Since then, refocusing has been used in a variety of settings including

normalization by evaluation <cit.>,

object-oriented programming <cit.>,

call by need <cit.>,

combinatory graph reduction <cit.>,

the SECD machine <cit.>,

a block-structured imperative language <cit.>.

Şerbănuţă, Roşu, and Meseguer used refocusing for
the chemical abstract machine <cit.>.

Bach Poulsen and Mosses used refocusing to implement SOS and
MSOS <cit.>.

As a component of the syntactic correspondence between calculi and
abstract machine, refocusing has been used

to derive type systems and implementations for coroutines <cit.>,

to go from type checking via reduction to type checking via evaluation <cit.>,

to derive a classical call-by-need sequent calculus <cit.>,

to derive interpretations of the gradually-typed lambda calculus <cit.>,

for full reduction <cit.>,

to construct abstract machines for JavaScript <cit.>.

§ CONCLUSION

Given a small-step semantics with a deterministic reduction strategy,
the point of refocusing is pragmatic: to deforest the reducts in
reduction sequences, , to not construct them on the way from the site
of each redex to the site of the next redex:

\diagram
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{-->}[rr]^{\text{{\small refocus}}}
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{-->}[rr]^{\text{{\small refocus}}}
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\circ
\rto^{\text{{\small contract}}}
\circ
\ar@{--}[r]
\drto_>>>>>>>>>>>>>>>{\text{{\small recompose}}\atadless}
\\
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\urto_>>>>>>>>>>>>{\atadless\text{{\small decompose}}}
\ar@{->}[rrr]_{\text{{\small reduce}}}
\circ
\enddiagram

In the early 2000's, Nielsen and the author identified the issue, which
was obvious, and observed that an optimal refocus function is simply the
decomposition function, which was less obvious.

Formally proving the correctness of refocusing was complicated because the
recomposing context is represented inside out and accumulated during

But contexts can be represented outside in too, and then structural
induction is enough for the proof to go through, witness

And since the shortcut is achieved by a call to the decomposition
function, the result is as correct and as efficient as this decomposition

In fact, experience has consistently shown that the resulting discovery
coincides with what we invent when we implement a reduction-free
normalization function,

, in a definitional interpreter, for weak – or for full – normalization by

The proof presented here was a long time coming.

It came to be thanks to the availability of proof assistants.

There is a thin line between assumptions and conclusion.

The author is grateful to Lasse R. Nielsen's for our initial joint work
about refocusing

and to Małgorzata Biernacka for its continuation.

Thanks are also due to Julia Lawall for commenting on the first drafts of
this article in August 2022.

§ DEFUNCTIONALIZATION

In a given functional program, function spaces are only populated by
instances of the function abstractions that occur in this

For example, consider

term -> term in the
definitions of decompose_term_cc and decompose_cc

Only three function abstractions – one in the initial call to
decompose_term_cc and two in the tail-recursive calls to
decompose_term_cc – give rise to inhabitants of this
function space.

The idea of defunctionalization here is to represent this function space
as a ternary sum, with the first summand standing for the function
abstraction in the initial call and with the two others standing for the
function abstractions in the tail-recursive calls.

Furthermore each summand is first order and contains the denotations of
the free variables of the corresponding function abstraction:

Applying this representation of functions is carried out with a dispatch

This defunctionalization ripples out in the codomain of

And here is the defunctionalized version of decompose_term_cc
and decompose_cc:

The type term_arrow_term is isomorphic to the type of lists
of control frames:

And so that is, mutatis mutandis, how we end with the defunctionalized
version of the decomposition function in
each function abstraction is replaced by a list construction, and each
function application is replaced by the application of a dispatch

Since the function that is defunctionalized is a recomposing
continuation, its first-order type is the type of contexts and its
dispatch function is the recomposition function.


$\Theta^{\ast}_{X_{\Omega}}$ in the normal form. To simplify notations, we
write $\Theta^{\ast}_{\mathbf{0}}$ for the formula
$\bot\wedge\mathop{\mbox{\small\rm NE}}$ and view $\mathbf{0}$ as a void team.
Note that $\Theta^{\ast}_{\mathbf{0}}\neq\Theta^{\ast}_{\emptyset}=\bot$.

######  Lemma 5.15.

Let $\Lambda$ be the set of all maximal strongly realizing sequences of a
formula $\phi(p_{i_{1}},\dots,p_{i_{n}})$ in the language of
$\mathbf{CPL^{+}}$.

(i)

For each $\Omega\in\Lambda$, we have
$\phi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}$ for some team
$X_{\Omega}$ on $N=\\{i_{1},\dots,i_{n}\\}$ or $X_{\Omega}=\mathbf{0}$.

(ii)

Let $\Lambda_{0}=\\{\Omega\in\Lambda\mid X_{\Omega}\neq\mathbf{0}\\}$. We have
$\phi\,\equiv\,\operatorname*{\bigvee}_{\Omega\in\Lambda_{0}}\Theta^{\ast}_{X_{\Omega}}$.

###### Proof.

(i) We prove the lemma by induction on the subformulas $\psi$ of $\phi$. If
$\psi$ is an atom, then $\psi^{\ast}_{\Omega}=\Theta^{\ast}_{X_{\Omega}}$ for
some team $X_{\Omega}$ on $N$ that satisfies $\psi$ and trivially
$\psi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}$.

If $\psi=\delta\otimes\chi$, then by the induction hypothesis, we have

$\delta^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}\text{ and
}\chi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{Y_{\Omega}},$ (11)

By $\otimes\textsf{Sub}^{-}$ we have
$\delta^{\ast}_{\Omega}\otimes\chi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}\otimes\Theta^{\ast}_{Y_{\Omega}}$.
It then suffices to show that
$\Theta^{\ast}_{X_{\Omega}}\otimes\Theta^{\ast}_{Y_{\Omega}}\dashv\vdash\Theta^{\ast}_{Z}$
for some team $Z$ on $N$.

If $X_{\Omega}=\mathbf{0}$, then taking $Z=\mathbf{0}$, we derive
$\Theta^{\ast}_{\mathbf{0}}\dashv\vdash\Theta^{\ast}_{\mathbf{0}}\otimes\Theta^{\ast}_{Y_{\Omega}}$
by $\it{\textsf{ex falso}}^{+}$ and $\mathbf{0}\textsf{Ctr}$. The case
$Y_{\Omega}=\mathbf{0}$ is proved similarly. If
$X_{\Omega},Y_{\Omega}\neq\mathbf{0}$, then by $\otimes\textsf{W}$ and
$\otimes\textsf{E}^{-}$, we derive
$\Theta^{\ast}_{X_{\Omega}}\otimes\Theta^{\ast}_{Y_{\Omega}}\dashv\vdash\Theta^{\ast}_{X_{\Omega}\cup
Y_{\Omega}}$.

If $\psi=\delta\wedge\chi$, then the induction hypothesis implies (11). By
$\wedge\textsf{I}$ and $\wedge\textsf{E}$ we have
$\delta^{\ast}_{\Omega}\wedge\chi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}\wedge\Theta^{\ast}_{Y_{\Omega}}$.
It then suffices to show that
$\Theta^{\ast}_{X_{\Omega}}\wedge\Theta^{\ast}_{Y_{\Omega}}\dashv\vdash\Theta^{\ast}_{Z}$
for some team $Z$ on $N$.

If $X_{\Omega}=\mathbf{0}$, then taking $Z=\mathbf{0}$, we derive
$\Theta^{\ast}_{\mathbf{0}}\dashv\vdash\Theta^{\ast}_{\mathbf{0}}\wedge\Theta^{\ast}_{Y_{\Omega}}$
by $\it{\textsf{ex falso}}^{+}$ and $\wedge\textsf{E}$. The case
$Y_{\Omega}=\mathbf{0}$ is proved similarly. If
$X_{\Omega}=Y_{\Omega}\neq\mathbf{0}$, then by $\wedge\textsf{E}$ and
$\wedge\textsf{I}$, we derive
$\Theta^{\ast}_{X_{\Omega}}\wedge\Theta^{\ast}_{Y_{\Omega}}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}$.
If $X_{\Omega},Y_{\Omega}\neq\mathbf{0}$ and $X_{\Omega}\neq Y_{\Omega}$, then
we derive
$\Theta^{\ast}_{\mathbf{0}}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}\wedge\Theta^{\ast}_{Y_{\Omega}}$
by $\it{\textsf{ex falso}}^{+}$ and $\mathbf{0}\textsf{I}$.

(ii) It follows from the item (i), the Soundness Theorem and Lemma 5.10 that
$\phi\,\equiv\,\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}\,\equiv\,\operatorname*{\bigvee}_{\Omega\in\Lambda}\Theta^{\ast}_{X_{\Omega}}.$
If $\Lambda_{0}\neq\emptyset$, then the statement clearly follows, as
$\Theta^{\ast}_{\mathbf{0}}\vee\psi=\big{(}\bot\wedge\mathop{\mbox{\small\rm
NE}}\big{)}\vee\psi\equiv\psi$ for all formulas $\psi$. If
$\Lambda_{0}=\emptyset$, then
$\phi^{\ast}_{\Omega}\equiv\bot\wedge\mathop{\mbox{\small\rm NE}}$ for each
$\Omega\in\Lambda$. Thus
$\phi\equiv\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}\equiv\bigvee_{\Omega\in\Lambda}(\bot\wedge\mathop{\mbox{\small\rm
NE}})\equiv\bot\wedge\mathop{\mbox{\small\rm NE}}\equiv\bigvee\emptyset$. ∎

Finally, let us give the proof of the Completeness Theorem.

######  Theorem 5.16 (Completeness Theorem).

For any formulas $\phi$ and $\psi$ in the language of $\mathbf{CPL^{+}}$, we
have $\phi\models\psi\,\Longrightarrow\,\phi\vdash\psi.$

###### Proof.

Suppose $\phi\models\psi$, where $\phi=\phi(p_{i_{1}},\dots,p_{i_{n}})$ and
$\psi=\psi(p_{i_{1}},\dots,p_{i_{n}})$. By Lemma 5.15 and the Soundness
Theorem, we have

$\phi\equiv\operatorname*{\bigvee}_{\Omega\in\Lambda_{0}}\Theta^{\ast}_{X_{\Omega}}\models\operatorname*{\bigvee}_{\Upsilon\in\Lambda_{0}^{\prime}}\Theta^{\ast}_{Y_{\Upsilon}}\equiv\psi.$
(12)

where

(i)

$\Lambda$, $\Lambda^{\prime}$ are the sets of all strongly realizing sequences
of $\phi$ and $\psi$, respectively and each $X_{\Omega}$ and $Y_{\Upsilon}$
are teams on $\\{i_{1},\dots,i_{n}\\}$;

(ii)

$\phi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{X_{\Omega}}$ and
$\psi^{\ast}_{\Upsilon}\dashv\vdash\Theta^{\ast}_{Y_{\Upsilon}}$ for all
$\Omega\in\Lambda$ and $\Upsilon\in\Lambda^{\prime}$;

(iii)

$\Lambda_{0}=\\{\Omega\in\Lambda\mid X_{\Omega}\neq\mathbf{0}\\}$ and
$\Lambda_{0}^{\prime}=\\{\Upsilon\in\Lambda^{\prime}\mid
Y_{\Upsilon}\neq\mathbf{0}\\}$.

If $\Lambda_{0},\Lambda_{0}^{\prime}\neq\emptyset$, then for any
$\Omega\in\Lambda$, by Lemma 5.4 there exists $\Upsilon\in\Lambda^{\prime}$
such that $X_{\Omega}=Y_{\Upsilon}$. We then have

$\phi^{\ast}_{\Omega}\vdash\Theta^{\ast}_{X_{\Omega}}=\Theta^{\ast}_{X_{\Upsilon}}\vdash\psi^{\ast}_{\Upsilon}\vdash\psi$

by (ii) and Lemma 5.11. Finally, we obtain $\phi\vdash\psi$ by Lemma 5.14.

If $\Lambda_{0}=\emptyset$, then for each $\Omega\in\Lambda$ we have
$\phi^{\ast}_{\Omega}\dashv\vdash\Theta^{\ast}_{\mathbf{0}}=\bot\wedge\mathop{\mbox{\small\rm
NE}}$. Then by $\it{\textsf{ex falso}}^{+}$ we derive
$\phi^{\ast}_{\Omega}\vdash\psi$ and $\phi\vdash\psi$ follows from Lemma 5.14
again. If $\Lambda^{\prime}_{0}=\emptyset$, then
$\psi\equiv\bigvee\emptyset=\bot\wedge\mathop{\mbox{\small\rm NE}}$. But in
view of (12), we must also have $\phi\equiv\bot\wedge\mathop{\mbox{\small\rm
NE}}$ and $\Lambda_{0}=\emptyset$. This then reduces to the previous case. ∎

###  5.3 $\mathbf{PI}^{+}$, $\mathbf{PInc}^{+}$ and other extensions of
$\mathbf{CPL^{+}}$

The argument in the previous section can also be applied to axiomatize other
propositional team logics obtained by adding new atoms with the empty team
property to the language of $\mathbf{CPL^{+}}$, such as strong propositional
independence logic ($\mathbf{PI}^{+}$) and strong propositional inclusion
logic ($\mathbf{PInc}^{+}$). Throughout the section, we write $\mathsf{L}$ for
an arbitrary such logic. In this section, we will show how to generalize the
method in the previous section to axiomatize $\mathsf{L}$, and
$\mathbf{PI}^{+}$ and $\mathbf{PInc}$ in particular.

What was crucial in the axiomatization of $\mathbf{CPL^{+}}$ was the notion of
a _strong realization_ of a formula. This notion can be generalized to richer
languages, such as $\mathbf{PI}^{+}$ and $\mathbf{PInc}^{+}$. A _strong
realization_ $\alpha^{\ast}_{Y}$ of an atom $\alpha$ (such as independence
atom and inclusion atom) over a team $Y$ that satisfies $\alpha$ is defined as
$\alpha^{\ast}_{Y}:=\Theta^{\ast}_{Y}$. A _strongly realizing sequence of a
formula $\phi$ over a sequence $o$_ of some occurrences of atoms in $\phi$ and
a _strong realization_ (over $o$) are defined the same way as in the logic
$\mathbf{CPL^{+}}$, except that a richer language $\mathsf{L}$ may contain
more atoms.

Our natural deduction system of $\mathsf{L}$ consists of all of the axioms and
the rules from the system of $\mathbf{CPL^{+}}$ (Definition 5.8), together
with the Introduction Rule and the Elimination Rule ($\alpha\textsf{I}$ and
$\textsf{SE}_{\alpha}$ presented below) that characterize the equivalence
between an arbitrary new atom $\alpha$ and the Boolean disjunction
$\bigvee_{Y}\Theta^{\ast}_{Y}$ of its strong realizations.

######  Definition 5.17 (A natural deduction system of $\mathsf{L}$).

AXIOM
---
Atomic excluded middle
$\textsf{EM}_{0}$ $p_{i}\otimes\neg p_{i}$

RULES
---
All of the rules from Definition 5.8, together with the following two rules
for each new atom $\alpha$ in $\mathsf{L}$:
Atom $\alpha$ introduction
$D$ $\Theta^{\ast}_{Y}$ $\alpha\textsf{I}$ $\alpha$
where $Y$ is a team on a set $N$ of indices that satisfies $\alpha$444On the
surface this looks like a confusion between syntax and semantics. However, it
is as in the Conjunction Introduction Rule “From $\phi$ and $\psi$ we infer
$\phi\wedge\psi$”. On the basic level the rules establish a connection between
logical operations and their intended meaning. We could replace here the
assumption “$Y$ satisfies the atom $\alpha$” by explicitly listing teams on
$N$ that satisfy $\alpha$, but that would be more cumbersome.
Strong elimination rule for $\alpha$
$D_{0}$ $\phi$ [$\phi(\Theta^{\ast}_{Y_{1}}/[\alpha,m])$] $D_{1}$ $\theta$
$\ldots$ [$\phi(\Theta^{\ast}_{Y_{k}}/[\alpha,m])$] $D_{k}$ $\theta$
$\textsf{SE}_{\alpha}$ $\theta$
where $\\{Y_{1},\dots,Y_{k}\\}$ is the set of all teams on a set $N$ of
indices that satisfy $\alpha$

Next, we prove the Soundness Theorem and the (Strong) Completeness Theorem for
the system.

######  Theorem 5.18 (Soundness Theorem).

For any set $\Gamma\cup\\{\phi\\}$ of formulas in the language of
$\mathsf{L}$, we have $\Gamma\vdash\phi\,\Longrightarrow\,\Gamma\models\phi.$

###### Proof.

We show that for each derivation $D$ with the conclusion $\phi$ and the
hypotheses in $\Gamma$ we have $\Gamma\models\phi$. We only verify the cases
when the rules $\alpha\textsf{I}$ and $\textsf{SE}_{\alpha}$ are applied.

$\alpha\textsf{I}$: Assume that $D$ is a derivation for
$\Pi\vdash\Theta^{\ast}_{Y}$ where $Y$ is a team on $N$ that satisfies the
atom $\alpha$. We show that $\Pi\models\alpha$ follows from the induction
hypothesis $\Pi\models\Theta^{\ast}_{Y}$. This is reduced to showing
$\Theta^{\ast}_{Y}\models\alpha$. For any team $X$ such that
$X\models\Theta^{\ast}_{Y}$, by Lemma 5.4 we have $X=Y$. Thus $X\models\alpha$
follows from the assumption.

$\textsf{SE}_{\alpha}$: Put
$\phi^{\ast}_{i}=\phi(\Theta^{\ast}_{Y_{i}}/[\alpha,m])$ for each
$i\in\\{1,\dots,k\\}$. Assume that $D_{0},D_{1},\dots,D_{k}$ are derivations
for $\Pi_{0}\vdash\phi$, $\Pi_{1},\phi^{\ast}_{1}\vdash\theta$, …,
$\Pi_{k},\phi^{\ast}_{k}\vdash\theta$, respectively. We show that
$\Pi_{0},\Pi_{1},\dots,\Pi_{k}\models\theta$ follows from the induction
hypothesis $\Pi_{0}\models\phi$, $\Pi_{1},\phi^{\ast}_{1}\models\theta$, …,
$\Pi_{k},\phi^{\ast}_{k}\models\theta$. This is reduced to showing that
$\phi\models\phi^{\ast}_{1}\vee\dots\vee\phi^{\ast}_{k}$ by induction on
$\phi$. If $\phi$ is the atom $\alpha$, then the statement follows from Lemma
5.4 and the choice of the $Y_{i}$’s. The other cases are left to the reader. ∎

######  Theorem 5.19 (Completeness Theorem).

For any formulas $\phi$ and $\psi$ in the language of $\mathsf{L}$, we have
$\phi\models\psi\,\Longrightarrow\,\phi\vdash\psi.$

###### Proof.

The theorem is proved by a similar argument to that of the proof of Theorem
5.16. Especially, all the lemmas leading to Theorem 5.16 can be easily
generalized to the case of any extension $\mathsf{L}$ of $\mathbf{CPL^{+}}$
with new atoms having the empty team property. In particular, in the proof of
the lemma that corresponds to Lemma 5.11, if $\psi$ is a new atom $\alpha$,
then $\psi^{\ast}_{\Omega}\vdash\psi$ follows from $\alpha\textsf{I}$. When
proving the lemma that corresponds to Lemma 5.13, one applies
$\textsf{SE}_{\alpha}$ when $\alpha$ is a new atom. ∎

Instantiating the new atoms $\alpha$ in the deduction system of Definition
5.17 with independence atoms or inclusion atoms, we obtain sound and
(strongly) complete deduction systems of $\mathbf{PI}^{+}$ and
$\mathbf{PInc}^{+}$. We end this section with a demonstration of the natural
deduction system of $\mathbf{PI}^{+}$. Below we derive the Geiger-Paz-Pearl
axioms [12]. To simplify notation, we write IndI for the Independence Atom
Introduction Rule and $\textsf{SE}_{\textsf{Ind}}$ for the Independence Atom
Elimination Rule.

######  Example 5.20.

Let $\vec{x}=p_{i_{1}}\cdots p_{i_{k}}$, $\vec{y}=p_{j_{1}}\cdots p_{j_{m}}$
and $\vec{z}=p_{l_{1}}\cdots p_{l_{n}}$. The following Geiger-Paz-Pearl axioms
are derivable in the natural deduction system of $\mathbf{PI}^{+}$:

(i)

$\vec{x}\perp\vec{y}~{}\vdash\vec{y}\perp\vec{x}$

(ii)

$\vec{x}\perp\vec{y}~{}\vdash\vec{z}\perp\vec{y}$, where $\vec{z}$ is a
subsequence of $\vec{x}$.

(iii)

$\vec{x}\perp\vec{y}~{}\vdash\vec{u}\perp\vec{v}$, where $\vec{u}$ is a
permutation of $\vec{x}$ and $\vec{v}$ is a permutation of $\vec{y}$.

(iv)

$\vec{x}\perp\vec{y},~{}\vec{x}\vec{y}\perp\vec{z}~{}\vdash\vec{x}\perp\vec{y}\vec{z}$.

###### Proof.

We are going to use the Independence Atom Introduction Rule IndI a lot here.
Therefore the proofs below seem entirely semantical. However, we have built
the meaning of the independence atom into the rule IndI, so it is only natural
that we refer to this meaning in the proofs. This is more complicated but, in
principle, analogous to the way we often use in elementary logic the meaning
of “and” and “or” when we prove e.g. distributivity laws using just the
Elimination Rule and Introduction Rule for $\wedge$ and $\vee$.

Put $K=\\{i_{1},\dots,i_{k}\\}$, $M=\\{j_{1},\dots,j_{m}\\}$ and
$N=\\{l_{1},\dots,l_{n}\\}$.

(i) By $\textsf{SE}_{\textsf{Ind}}$, it suffices to show that for any team $Y$
on $K\cup M$ such that $Y\models\vec{x}\perp\vec{y}$ we have
$\Theta^{\ast}_{Y}\vdash\vec{y}\perp\vec{x}$. But this follows from IndI, as
$Y\models\vec{y}\perp\vec{x}$ also holds.

(ii) By $\textsf{SE}_{\textsf{Ind}}$, it suffices to show that for any team
$Y$ on $K\cup M\cup N$ such that $Y\models\vec{x}\perp\vec{y}$ we have
$\Theta^{\ast}_{Y}\vdash\vec{z}\perp\vec{y}$, where $\vec{z}$ is a subsequence
of $\vec{x}$. In view of IndI, this is reduced to showing
$Y\models\vec{z}\perp\vec{y}$. But this is obvious.

(iii) By $\textsf{SE}_{\textsf{Ind}}$, it suffices to show that for any team
$Y$ on $K\cup M$ such that $Y\models\vec{x}\perp\vec{y}$ we have
$\Theta^{\ast}_{Y}\vdash\vec{u}\perp\vec{v}$, where $\vec{u}=p_{i_{1}}\cdots
p_{i_{a}}$ is a permutation of $\vec{x}$ and $\vec{v}=p_{m_{1}}\cdots
p_{m_{b}}$ is a permutation of $\vec{y}$. In view of IndI this is reduced to
showing $Y\models\vec{u}\perp\vec{v}$, which follows from that
$Y\models\vec{x}\perp\vec{y}$.

(iv) We will show that
$(\vec{x}\perp\vec{y})\wedge(\vec{x}\vec{y}\perp\vec{z})\vdash\vec{x}\perp\vec{y}\vec{z}$.
By $\textsf{SE}_{\textsf{Ind}}$, it suffices to show that for any team $X$ on
$K\cup M\cup N$ such that $X\models\vec{x}\perp\vec{y}$, we have
$\Theta^{\ast}_{X}\wedge(\vec{x}\vec{y}\perp\vec{z})\vdash\vec{x}\perp\vec{y}\vec{z}$.
But this, by $\textsf{SE}_{\textsf{Ind}}$, is further reduced to showing that
for any team $Y$ on $K\cup M\cup N$ such that
$Y\models\vec{x}\vec{y}\perp\vec{z}$, we have
$\Theta^{\ast}_{X}\wedge\Theta^{\ast}_{Y}\vdash\vec{x}\perp\vec{y}\vec{z}$.

Now, if $X\neq Y$, then by $\mathbf{0}\textsf{I}$ and $\it{\textsf{ex
falso}}^{+}$, we derive
$\Theta^{\ast}_{X}\wedge\Theta^{\ast}_{Y}\vdash\bot\wedge\mathop{\mbox{\small\rm
NE}}\vdash\vec{x}\perp\vec{y}\vec{z}$.

If $X=Y$, then $\Theta^{\ast}_{X}=\Theta^{\ast}_{Y}$. By IndI, it suffices to
show $X\models\vec{x}\perp\vec{y}\vec{z}$. For any $s_{1},s_{2}\in X$, since
$X\models\vec{x}\perp\vec{y}$, there exists $s_{3}\in X$ such that
$s_{1}(\vec{x})=s_{3}(\vec{x})$ and $s_{2}(\vec{y})=s_{3}(\vec{y})$. But as
$X\models\vec{x}\vec{y}\perp\vec{z}$, there exists $s_{4}\in X$ such that
$s_{4}(\vec{x})s_{4}(\vec{y})=s_{3}(\vec{x})s_{3}(\vec{y})$ and
$s_{4}(\vec{z})=s_{2}(\vec{z})$. We then conclude that
$s_{4}(\vec{x})=s_{3}(\vec{x})=s_{1}(\vec{x})$ and
$s_{4}(\vec{y})s_{4}(\vec{z})=s_{3}(\vec{y})s_{2}(\vec{z})=s_{2}(\vec{y})s_{2}(\vec{z})$.
Hence $X\models\vec{x}\perp\vec{y}\vec{z}$ and this completes the proof. ∎

##  6 Concluding remarks

In our previous work [34] we have investigated classical propositional logic,
and several versions of propositional dependence logic. We proved their
expressive completeness for downward closed team properties, and gave several
complete axiomatizations of such logics. In this paper, we have studied
propositional team logics more generally, recognizing that there is a whole
hierarchy of them. We have established the results in Figure 1 concerning the
expressive power of these logics. Several expressively complete logics are
identified. For example, we have proved that $\mathbf{PU}^{+}$ is expressively
complete for the set of union closed team properties. We also derived normal
forms for many of the logics. Some of the logics we considered have the empty
team property, and some do not. We axiomatized the logics ($\mathbf{PT}^{+}$,
$\mathbf{CPL^{+}}$, $\mathbf{PI}^{+}$ and $\mathbf{PInc}^{+}$) without the
empty team property, and we leave the concrete axiomatization of
$\mathbf{PU}^{+}$ for future research. As is reflected by the sophisticated
Strong Elimination Rules we gave in this paper, propositional logics of
independence are more intricate than propositional logics of dependence. In
particular, we feel that we have not yet fully understood the notion of
independence, and neither a characterization of expressive power nor a
complete axiomatization is given for $\mathbf{PI}$ here. Nevertheless, it is
our hope that the results obtained concerning logics around $\mathbf{PI}$ will
set the stage for further research in this field and lead to a better
understanding of $\mathbf{PI}$, propositional independence logic, itself.

## Acknowledgements

The authors would like to thank Maria Aloni, Pietro Galliani, Lauri Hella,
Juha Kontinen, Vít Punčochář, Floris Roelfsen and Dag Westerståhl for useful
conversations related to this paper.

## References

  * [1] Abramsky, S., and Väänänen, J. From IF to BI.  Synthese 167, 2 (2009), 207–230.
  * [2] A.S.Troelstra, and H.Schwichtenberg.  Basic Proof Theory.  Cambridge University Press, 1996.
  * [3] Ciardelli, I. Inquisitive semantics and intermediate logics.  Master’s thesis, University of Amsterdam, 2009.
  * [4] Ciardelli, I. Questions in Logic.  PhD thesis, University of Amsterdam, 2016.
  * [5] Ciardelli, I., and Roelofsen, F. Inquisitive logic.  Journal of Philosophical Logic 40, 1 (2011), 55–94.
  * [6] Codd, E. F. Further normalization of the data base relational model.  IBM Research Report, San Jose, California RJ909 (1971).
  * [7] Ebbing, J., Hella, L., Meier, A., Müller, J.-S., Virtema, J., and Vollmer, H. Extended modal dependence logic.  In 20th International Workshop, WoLLIC 2013, Proceedings, vol. 8071 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2013, pp. 126–137.
  * [8] Ebbing, J., and Lohmann, P. Complexity of model checking for modal dependence logic.  In SOFSEM, M. Bieliková, G. Friedrich, G. Gottlob, S. Katzenbeisser, and G. Turán, Eds., vol. 7147 of Lecture Notes in Computer Science. Springer, 2012, pp. 226–237.
  * [9] Ebbing, J., Lohmann, P., and Yang, F. Model checking for modal intuitionistic dependence logic.  In Post-proceedings of the Ninth Tbilisi Symposium on Language, Logic and Computation (2013), vol. 7758 of Lecture Notes in Computer Science, pp. 231–256.
  * [10] Galliani, P. Inclusion and exclusion in team semantics: On some logics of imperfect information.  Annals of Pure and Applied Logic 163, 1 (January 2012), 68–84.
  * [11] Galliani, P., and Hella, L. Inclusion logic and fixed point logic.  In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy (2013), pp. 281–295.
  * [12] Geiger, D., Paz, A., and Pearl, J. Axioms and algorithms for inferences involving probabilistic independence.  Information and Computation 91, 1 (March 1991), 128–141.
  * [13] Grädel, E., and Väänänen, J. Dependence and independence.  Studia Logica 101, 2 (April 2013), 399–410.
  * [14] Hella, L., Luosto, K., Sano, K., and Virtema, J. The Expressive Power of Modal Dependence Logic.  arXiv: http://arxiv.org/abs/1406.6266v1.
  * [15] Hella, L., and Stumpf, J. The expressive power of modal logic with inclusion atoms.  In Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (2015), J. Esparza and E. Tronci, Eds., Electronic Proceedings in Theoretical Computer Science 193, pp. 129–143.
  * [16] Hintikka, J., and Sandu, G. Informational independence as a semantical phenomenon.  In Logic, Methodology and Philosophy of Science, R. H. J. E. Fenstad, I. T. Frolov, Ed. Amsterdam: Elsevier, 1989, pp. 571–589.
  * [17] Hodges, W. Compositional semantics for a language of imperfect information.  Logic Journal of the IGPL 5 (1997), 539–563.
  * [18] Hodges, W. Some strange quantifiers.  In Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, J. Mycielski, G. Rozenberg, and A. Salomaa, Eds., vol. 1261 of Lecture Notes in Computer Science. London: Springer, 1997, pp. 51–65.
  * [19] Hyttinen, T., Paolini, G., and Väänänen, J. Quantum team logic and Bell’s inequalities.  Rev. Symb. Log. 8, 4 (2015), 722–742.
  * [20] Iemhoff, R., and Yang, F. Structural completeness in propositional logics of dependence.  Archive for Mathematical Logic 55, 7 (November 2016), 955–975.
  * [21] Kontinen, J., and Nurmi, V. Team logic and second-order logic.  Fundamenta Informaticae 106 (2011), 259–272.
  * [22] Lindström, P. On extensions of elementary logic.  Theoria 35 (1969), 1–11.
  * [23] Lohmann, P., and Vollmer, H. Complexity results for modal dependence logic.  Studia Logica 101, 2 (2013), 343–366.
  * [24] Lück, M. Axiomatizations for propositional and modal team logic.  In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (Dagstuhl, Germany, 2016), J.-M. Talbot and L. Regnier, Eds., vol. 62, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp. 33:1–33:18.
  * [25] Mann, A. L., Sandu, G., and Sevenster, M. Independence-Friendly Logic: A Game-Theoretic Approach.  London Mathematical Society Lecture Note Series. Cambridge University Press, 2011.
  * [26] Sevenster, M. Model-theoretic and computational properties of modal dependence logic.  Journal of Logic and Computation 19, 6 (2009), 1157–1173.
  * [27] Väänänen, J. Dependence Logic: A New Approach to Independence Friendly Logic.  Cambridge: Cambridge University Press, 2007.
  * [28] Väänänen, J. Modal dependence logic.  In New Perspectives on Games and Interaction, K. R. Apt and R. van Rooij, Eds., vol. 4 of Texts in Logic and Games. Amsterdam University Press, 2008, pp. 237–254.
  * [29] Väänänen, J. Multiverse set theory and absolutely undecidable propositions.  In Interpreting Gödel, J. Kennedy, Ed. Cambridge University Press, 2014, pp. 180–208.
  * [30] van Dalen, D. Logic and Structure, 5 ed.  Springer, 2012.
  * [31] Virtema, J. Complexity of validity for propositional dependence logics.  In Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014 (2014), no. 161 in EPTCS, pp. 18–31.
  * [32] Yang, F. On Extensions and Variants of Dependence Logic.  PhD thesis, University of Helsinki, 2014.
  * [33] Yang, F. Uniform definability in team semantics setting, manuscript, 2015\.
  * [34] Yang, F., and Väänänen, J. Propositional logics of dependence.  Annals of Pure and Applied Logic 167, 7 (July 2016), 557–589.


# An effective and efficient label initialization method based on similarity
for community detection in networks

Jyothimon Chandran  Madhuviswanatham Vankadara*
School of Computer Science and Engg.
Vellore Institute of Technology Vellore  India
<EMAIL_ADDRESS>
(December 04, 2021)

###### Abstract

Identifying clusters or community structures in networks has become an
integral part of social network analysis. Though many methods were proposed,
the label propagation algorithm (LPA) is a popular computationally efficient
method with running time linear. However, the LPA provides different
combination of communities on the same network due to the randomness in LPA.
Many improvements have been proposed to tackle this stability problem by
eliminating the randomness. This paper put forward an improvement to the
standard LPA by proposing a label initialization method based on link
similarity. The similarity is measured based on the connection strength
between two nodes. The method is tested on real and synthetic measures to
analyze the performance.

##  1 Introduction

Complex network representation of complex systems [1, 2] are wide spread in
various domains of research including biology, computer science, and physics.
It simplifies the complexity inherent in the system by denoting the components
and their relations or interactions. Generally, the nodes denote the
components and links indicate the interactions or relations between entities
in complex networks. Community structures [3] is an important property of
complex networks, which helps to provide more meaningful structures in
network. Understanding these structures bring insights into various dynamics
of various systems [1].

There exist a plenty of literature for finding community structures in
networks using various techniques [4]. Some studies treat community detection
as an optimization problem, in which maximizing the optimization function such
as modularity are among wide spread. Since many of these methods are not
computationally efficient, methods based on some heuristic rules are also
recommended. Among that, label propagation algorithm [5] is one of the most
time efficient heuristic methods with time complexity nearly linear $(O(t.n))$
where $n$ denotes the number of nodes. However, when LPA is applied on a
network, it returns community structures which are different in different
runs. This shows that the LPA is unstable.

Though there are several reasons for the unstable results. The major reason is
the randomness in node label update as well as the random node order. When the
random labeling strategy is performed on each node, the random selection can
lead to various combinations of communities. Recently, various studies propose
several methods for improving LPA by recommending various label update
strategies focusing on eliminating randomness. These methods focus mainly on
the node label update strategy which selects labels according to an order-
based selection strategy that includes node importance, label influence, and
link importance.

The first step in the original LPA is to assign unique labels to every node in
the network. The impact of initial node labels on the stability is not fully
explored. This paper proposes a method (ILI-LPA) which initializes node labels
based on node influence. The ILI-LPA eliminates the unique label
initialization of LPA with a new label initialization which assigns identical
labels to nodes which express high probability to be in the same community at
the end the label propagation. The main aim of the paper is to assign
structurally densely connected nodes with same labels as initial labels to
improve the stability and accuracy of the communities.

##  2 Related works

To eliminate random label update process in the LPA, [6] proposed a method
which applies modularity to avoid random selection of labels. Recently, Le et
al. [7] put forward a modified LPA which also applies modularity.

Node influence is also considered as an effective method for label update to
improve stability. Several methods that improve LPA on the stability of
communities based on node influence are also available [8, 9, 10]. Estimating
the importance or influence of nodes is the main step in those methods. The
k-shell value of each node is estimated to find the node importance in [8].
Whereas in [9] the node degree as well as the neighbors influence is measured
to estimate node importance. However, the increase in time complexity is a
major drawback of these methods. Some studies focus on the link importance
assuming that links contribute significantly to the community structure
identification. The label influence is considered in [11]. LPAc [12] based on
edge clustering coefficient is a popular method that considers the link
importance through edge clustering coefficient. Similarity [13] also proposed
a link strength for LPA. Motifs in network are also considered for improving
the LPA stability [14]. Also, methods based on genetic algorithms [15] and
considering attributes [16] are introduced. Still, the stability and accuracy
is a problem unsolved.

##  3 Proposed method

This paper recommends a node labeling method based on link similarity for
finding communities in networks. The main aim of the proposed method is to
improve the stability of the standard label propagation algorithm. The
proposed method replaces the unique label initialization of the LPA and put
forward a more accurate label initialization to minimize the impact of
randomness in LPA.

The method is called ILI-LPA (Identical Label Initialization LPA). The ILI-LPA
focuses on the initial node labels. The authors of this paper assume that the
strategy of assigning unique labels to nodes as initial node labels has
several drawbacks which affect the stability at the label propagation. This is
because if unique labels are assigned to nodes in a community, the boundary
nodes cannot differentiate its own community participation hence randomness
create uncertainty.

It is well known that nodes with dense connections will stay in a single
community once the community detection process is over. If we can identify
some of the densely connected regions and assign same labels, we can minimize
the effect of randomness. Based on this concept, this paper introduces $tsi$
which evaluates the strength of connections between nodes.

$tsi(i,j)=\frac{1+|N(i)\cap N(j)|}{|N(j)|}$ (1)

where $N(i)$ indicates the neighbor set of node $i$. Consider node $(i,j)$ are
adjacent nodes in $G((i,j)\in E)$. The more the node $i$ is connected with the
neighbors of $j$, the higher the influence of node $i$ to node $j$. The higher
influence indicates not only the strength of connections, but also the
probability that how much a node accept node the other. This is more
meaningful to the label propagation process in LPA. We replace the unique
label assigning method of LPA to set initial node labels with identical label
initialization. It is based on the following condition.

$tsi(i,j)\geq tsi(j,i)\&\&tsi(i,j)\geq\beta$ (2)

Algorithm 1 Identical Label Initialization-LPA

Input: Network $G=(V,E)$, parameter $\beta$
Output: Communities $C_{D}$ = {$C_{D1}$, $C_{D2}$, $C_{D3}$,…$C_{Dk}$}

1:procedure ILI-LPA(G,$\beta$)

2: for each $(i,j)\in E$ do

3: $tsi(i,j)\leftarrow\frac{1+|N(i)\cap N(j)|}{|N(j)|}$

4: $tsi(j,i)\leftarrow\frac{1+|N(i)\cap N(j)|}{|N(i)|}$

5: $Weight(i,j)\leftarrow tsi(i,j)$

6: $Weight(j,i)\leftarrow tsi(j,i)$

7: end for

8: for each $i\in V$ do

9: if $tsi(j,i)\leq tsi(i,j)$ and $tsi(i,j)\geq\beta$ then

10: $label(j)\leftarrow label(i)$

11: end if

12: end for

13: for each $i\in V$ do

14: if $size(l)=1$ then

15: $label(i)\leftarrow l$

16: else

17: $label(i)\leftarrow random\\_select(l)$

18: end if

19: end for

20: Repeat steps 13-19, until all node labels are similar to its neighbors
majority.

21: According to the node labels, seperate the communities

22:end procedure

Each node $i$ update the label of neighbor $j$, if the condition is satisfied.
The $\beta$ indicates the input parameter. This ensures that some percent of
nodes possess labels which are same, such as the nodes in densely connected
regions. The original label propagation is performed after initialization of
node labels. During the label propagation, each node accepts the label of its
neighbors majority1y label. When more than one label satisfies majority label,
the random label selection is adopted.

The time complexity of the proposed method is reported as $O(n.d)$ where d
denotes the averge degree.

##  4 Results

The algorithm is coded in Python NetworkX and experimented on an Intel i7
machine of 16GB RAM. The input parameter is assigned as value 0.35. Two
quality measures, modularity [22] and Normalized mutual information [nmi] [23]
is used to assess the performance.

The obtained modularity on networks karate [17], dolphin [18], football [3],
and polbooks [19] are 0.371, 0.523, 0.604, and 0.526 respectively. However,
the modularity of LPA on the same networks are 0.357, 0.487, 0.589, 0.511
respectively. On network science [20] is 0.921 and email_enron [20] is 0.562.
The nmi reported in karate, dolphin, football, and polbooks are 0.837, 0.366,
0.927, and 0.593 respectively. Whereas, the LPA returns nmi values 0.649,
0.540, 0.893, 0.524. This shows that the initial node labels affect the
quality of the communities.

Compared to the LPA, the ILI-LPA perform better on LFR network. On a network
of 1000 nodes, the LPA modularity drops to 0 when $\mu$ is 0.55, whereas the
ILI-LPA maintains quality upto $\mu$ is 0.70. Similar pattern has been
observed on LFR networks of size 2000 and 5000. This shows that the initial
node labels has significant impact of the performance of the random label
propagation process.

##  5  Conclusion

The LPA is an efficient community detection method. The stability of
communities extracted by LPA is a major concern. To improve the stability,
this paper proposes a label initialization method, which replaces the unique
label initialization method adopted by LPA and other improvements. The
proposed method identify densely connected regions based on link similarity
and assigns same labels as initial node labels without consuming much
computational time. The performance is verified on real-world and LFR
networks. The results show effectiveness of label initialization. The main
findings of the paper is that appropriate label initialization improves
performance compared to distinct label initialization.

## References

  * [1] Newman, M. E.: The structure and function of complex networks. SIAM review, Vol. 45, 2003, No. 2, pp. 167-256.
  * [2] Newman, M.: Networks. Oxford university press, 2018.
  * [3] Girvan, M., Newman, M. E.: Community structure in social and biological networks. Proceedings of the national academy of sciences, Vol. 99, 2002, No. 12, pp. 7821-7826.
  * [4] Xu, G., Guo, J., Yang, P.: TNS-LPA: An Improved Label Propagation Algorithm for Community Detection Based on Two-Level Neighbourhood Similarity. IEEE Access, Vol. 9, 2020, pp. 23526-23536.
  * [5] Raghavan, U. N., Albert, R., Kumara, S.: Near linear time algorithm to detect community structures in large-scale networks. Physical review E, Vol. 76, 2007, No. 3, p. 036106.
  * [6] Barber, M. J., Clark, J. W.: Detecting network communities by propagating labels under constraints. Physical review E, Vol. 80, 2009, No. 2, p. 026129.
  * [7] Le, B. D., Shen, H., Nguyen, H., Falkner, N.: Improved network community detection using meta-heuristic based label propagation. Applied Intelligence, Vol. 49, 2019, No. 4, pp. 1451-1466,
  * [8] Xing, Y., Meng, F., Zhou, Y., Zhu, M., Shi, M., Sun, G.: A node influence based label propagation algorithm for community detection in networks. The Scientific World Journal, Vol. 2014, 2014.
  * [9] Zhang, X. K., Ren, J., Song, C., Jia, J., Zhang, Q.: Label propagation algorithm for community detection based on node importance and label influence. Physics Letters A, Vol. 381, 2017, No. 33, pp. 2691-2698.
  * [10] Wang, T., Chen, S., Wang, X., Wang, J.: Label propagation algorithm based on node importance. Physica A: Statistical Mechanics and its Applications, Vol. 551, 2020, pp. 124137.
  * [11] Zhang, Y., Liu, Y., Li, Q., Jin, R., Wen, C.: Lilpa: A label importance based label propagation algorithm for community detection with application to core drug discovery. Neurocomputing, Vol. 413, 2020, No. 1, pp. 107-133.
  * [12] Zhang, X. K., Tian, X., Li, Y. N., Song, C.: Label propagation algorithm based on edge clustering coefficient for community detection in complex networks. International Journal of Modern Physics B, Vol. 28, 2014, No. 30, p. 1450216.
  * [13] Berahmand, K., Bouyer, A.: A link-based similarity for improving community detection based on label propagation algorithm. Journal of Systems Science and Complexity, Vol. 32, 2019, No. 3, pp. 737-758.
  * [14] Li, P. Z., Huang, L., Wang, C. D., Lai, J. H., Huang, D.: Community detection by motif-aware label propagation. ACM Transactions on Knowledge Discovery from Data (TKDD), Vol. 14, 2020, No. 2, pp. 1-19.
  * [15] Hosseini, R., Rezvanian, A.: AntLP: ant-based label propagation algorithm for community detection in social networks, CAAI Transactions on Intelligence Technology, Vol. 5, 2020, No. 1, pp. 34-41.
  * [16] Berahmand, K., Haghani, S., Rostami, M., Li, Y.: A new attributed graph clustering by using label propagation in complex networks. Journal of King Saud University-Computer and Information Sciences, 2020.
  * [17] Zachary, W. W.: An information flow model for conflict and fission in small groups. Journal of anthropological research, Vol. 33, 1977, No. 4, pp. 452-473.
  * [18] Lusseau, D., Schneider, K., Boisseau, O. J., Haase, P., Slooten, E., Dawson, S. M.: The bottlenose dolphin community of Doubtful Sound features a large proportion of long-lasting associations. Behavioral Ecology and Sociobiology, Vol. 54, 2003, No. 4, pp. 396-405.
  * [19] Krebs, V.: A network of co-purcheased books about US politics. October, Vol. 20, 2008, No. 1, pp. 0-03.
  * [20] Newman, M. E. J.: Network data, 2013, www-personal. umich. edu/ mejn/netdata.
  * [21] Lancichinetti, A., Fortunato, S., Radicchi, F.: Benchmark graphs for testing community detection algorithms. Physical review E, Vol. 78, 2008, No. 4, p. 046110.
  * [22] Newman, M. E.: Modularity and community structure in networks. Proceedings of the national academy of sciences, Vol. 103, 2006, No. 23, pp. 8577-8582.
  * [23] Danon, L., Diaz-Guilera, A., Duch, J., Arenas, A.: Comparing community structure identification. Journal of statistical mechanics: Theory and experiment, Vol. 2005, 2005, No. 09, p. 09008.