Relational semantics of linear logic and
higher-order model-checking
Charles Grellois1 and Paul-André Melliès2
1
2

Laboratoires PPS & LIAFA, Université Paris Diderot
grellois@pps.univ-paris-diderot.fr
Laboratoire PPS, CNRS & Université Paris Diderot
mellies@pps.univ-paris-diderot.fr

arXiv:1501.04789v3 [cs.LO] 1 May 2015

Abstract
In this article, we develop a new and somewhat unexpected connection between higher-order
model-checking and linear logic. Our starting point is the observation that once embedded in
the relational semantics of linear logic, the Church encoding of a higher-order recursion scheme
(HORS) comes together with a dual Church encoding of an alternating tree automata (ATA)
of the same signature. Moreover, the interaction between the relational interpretations of the
HORS and of the ATA identifies the set of accepting states of the tree automaton against the
infinite tree generated by the recursion scheme. We show how to extend this result to alternating
parity automata (APT) by introducing a parametric version of the exponential modality of linear
logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We
show in particular how to reunderstand in this way the type-theoretic approach to higher-order
model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper
how this analysis driven by linear logic results in a new and purely semantic proof of decidability
of the formulas of the monadic second-order logic for higher-order recursion schemes.
1998 ACM Subject Classification Dummy classification – please refer to http://www.acm.org/
about/class/ccs98-html
Keywords and phrases Higher-order model-checking, linear logic, relational semantics, parity
games, parametric comonads.
Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

1

Introduction

Thanks to the seminal works by Girard and Reynolds on polymorphism and parametricity
in the 1970s, it has been recognized that every finite tree t on a given signature Σ can be
seen alternatively as a simply-typed λ-term of an appropriate type depending on Σ. This
correspondence between trees and λ-terms is even bijective if one considers λ-terms up to
βη-equivalence, see for instance Girard [7]. Typically, a finite tree t on the signature
Σ

=

{a : 2, b : 1, c : 0}

(1)

is the same thing under this Church encoding as a simply-typed λ-term t of type
(o → o → o) → (o → o) → o → o

(2)

modulo βη-equivalence. The idea underlying the correspondence is that every constructor a, b, c of the signature Σ should be treated as a variable
a : o → o → o

b : o → o

c : o

© Charles Grellois and Paul-André Melliès;
licensed under Creative Commons License CC-BY
Conference title on which this volume is based on.
Editors: Billy Editor and Bill Editors; pp. 1–24
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

(3)

2

Relational semantics of linear logic and higher-order model-checking

where the number of inputs o in the type o → · · · → o → o of the variable a, b, c indicates
the arity of the combinator. An equally well-known fact is that this translation extends to
infinite trees generated by higher-order recursion schemes on the signature Σ if one extends
the simply-typed λ-calculus with a fixpoint operator Y . For example, the higher-order
recursion scheme G on the signature Σ

S
7→ F a b c
G =
(4)
F x y z 7→ x (y z) (F x y (y z))
constructs the infinite tree
a
a

b
b

c

[[G]]

=

a

b

b

c

b

(5)

b
c

and can be formulated as a λ-term of the same type (3) as previously but defined in the
simply-typed λ-calculus extended with the fixpoint operator Y :
λabc. ((Y (λF. (λxyz. x (y z) (F x y (y z))))) a b c)

(6)

A natural temptation is to study the correspondence between higher-order recursion schemes
(4) and simply-typed λ-terms with fixpoints (6) from the resource-aware point of view of
linear logic. Recall that the intuitionistic type (3) is traditionally translated in linear logic
as the formula
A

! ( ! o ( ! o ( o ) ( ! ( ! o ( o ) ( ! o ( o.

=

As expected, the higher-order recursion scheme G in (4) can be translated as a proof tA of
this formula A in linear logic extended with a fixpoint operator Y . An amusing and slightly
puzzling observation is that the scheme G can be alternatively translated as a proof tB of
the formula B below:
B

=

!( o ( o ( o ) ( !( o ( o ) ( !o ( o

with the same underlying simply-typed λ-term with fixpoint operator Y . The difference
between the terms tA and tB is not syntactic, but type-theoretic: in the case of the term
tA , the type A indicates that each tree-constructor a, b and c of the signature Σ is allowed
to call its hypothesis as many times as desired:
a : !o ( !o ( o

b : !o ( o

c : o

whereas in the case of the term tB , the type B indicates that each variable a, b, c calls each
of its hypothesis exactly once:
a : o ( o ( o

b : o ( o

c : o

As a matter of fact, it appears that the proof tB is the image of the proof tA along a canonical
coercion of linear logic
` ι : A ( B.

C. Grellois and P.-A. Melliès

3

The status of this program transformation ι is difficult to understand unless one recalls
that linear logic is based on the existence of a perfect duality between the programs of a
given type A and their environments or counter-programs which are typed by the linear
negation A⊥ of the original type A. Accordingly, since the two terms tA and tB = ι ◦ tA are
syntactically equal, their difference should lie in the class of counter-programs of type A⊥
or B ⊥ which are allowed to interact with them. This idea takes its full flavour in the context
of model-checking, when one realizes that every tree automaton A on the signature Σ may
be seen as a counter-program whose purpose is indeed to interact with tA or tB in order to
check whether a specific property of interest is satisfied by the infinite tree [[G]] generated by
the recursion scheme G. This leads to the tentative duality principle:
higher-order
recursion schemes G

!

tree automata A

where a tree automaton A on the signature Σ is thus seen as a counter-program of type A⊥
or B ⊥ interacting with the higher-order recursion scheme G seen as a program of type A or B.
An apparent obstruction to this duality principle is that, in contrast to what happens with
recursion schemes G, it is in general impossible to translate a tree automaton A as a proof of
linear logic — in particular because linear logic lacks non-determinism. However, one neat
way to resolve this matter and to extend linear logic with non-determinism is to embed the
logic in its relational semantics, based on the monoidal category Rel of sets and relations.
The relational semantics of linear logic is indeed entitled to be seen as a non-deterministic
extension of linear logic where every nondeterministic tree automaton A = hΣ, Q, δ, q0 i may
be “implemented” by interpreting the base type o as the set Q of states of the automaton,
and by interpreting each variable a, b, c as the following relations
a : Q ( Q ( Q

b : Q ( Q

c : Q

deduced from the transition function δ of the automaton:
a = {(q1 , q2 , q) ∈ Q × Q × Q | (1, q1 ) ∧ (2, q2 ) ∈ δ(q, a)}
b = {(q1 , q) ∈ Q × Q | (1, q1 ) ∈ δ(q, b)}
c = {q ∈ Q | δ(q, c) = true}
The nondeterministic tree automaton A is then interpreted as the counter-program AB =
! a ⊗ ! b ⊗ ! c ⊗ d of type
B ⊥ = ! (Q ( Q ( Q) ⊗ ! (Q ( Q) ⊗ ! Q ⊗ Q⊥ .
obtained by tensoring the three relations a, b, c lifted with by the exponential modality !
together with the singleton d = {q0 } consisting of the initial state of the automaton, and
understood as a counter-program of type Q⊥ . Note that by composition with the contraposite ι⊥ : B ⊥ ( A⊥ of the coercion ι, one gets a counter-program AA = ι⊥ ◦ AB of
type
A⊥ = ! ( ! Q ( ! Q ( Q) ⊗ ! (! Q ( Q) ⊗ ! Q ⊗ Q⊥ .
Note also that when the type o is interpreted as Q in the relational model, the counterprograms of type B ⊥ of the form ! a ⊗ ! b ⊗ ! c ⊗ d with d = {q0 } correspond exactly to
the non-deterministic tree automata on the signature Σ with set of states Q and initial
state q0 . The difference between the two types A and B becomes very clear and meaningful
at this stage: shifting to the type A⊥ enables one to extend the class of nondeterministic

4

Relational semantics of linear logic and higher-order model-checking

tree automata to nondeterministic alternating tree automata A with typical transitions of
the form
δ(q, a)

=

(1, q1 ) ∧ (1, q2 )

(7)

meaning that the tree automaton A meeting the tree a(t1 , t2 ) at state q explores the left
subtree t1 twice with states q1 and q2 and does not explore at all the right subtree t2 . Such
a transition δ(q, a) is typically represented in the relational semantics of linear logic by the
singleton relation
a = { ( {|q1 , q2 |} , ∅ , q ) } : ! Q ( ! Q ( Q

(8)

where one uses the set ! Q of finite multisets of Q to encode the transition (7) with the
finite multiset {|q1 , q2 |} consisting of the two states q1 , q2 ∈ Q and the empty multiset ∅
of states. It should be stressed that a tree automaton A admitting such an “alternating”
transition δ(q, a) cannot be encoded as a counter-program of type B ⊥ because the transitions
of the tree automaton A are linear in that type and thus explore exactly once each subtree t1
and t2 of the tree a(t1 , t2 ). Summarizing the current discussion, we are entitled to consider
that each linear type A⊥ and B ⊥ reflects a specific class of tree automata on the signature Σ:
B⊥
A⊥

↔
↔

non-deterministic tree automata
non-deterministic alternating tree automata

Accordingly, the purpose of the coercion ι from tA to tB is to restrict the power of the
class of alternating non-deterministic tree automata allowed to explore the infinite tree [[G]]
generated by the higher-order recursion scheme G of signature Σ.

Description of the paper
The purpose of this paper is to show that this duality between recursion schemes and tree
automata underlies several of the recent developments in the field of higher-order modelchecking. To that purpose, we start by establishing in §2 an equivalence between the intersection type system introduced by Kobayashi to describe infinitary coinductive proofs,
and an infinitary variant of the traditional relational semantics of linear logic developed
in [10]. This correspondence between an intersection type system and a relational semantics
of linear logic adapts to the field of higher-order model-checking ideas dating back to Coppo,
Dezani, Honsell and Longo [4] and recently revisited by Terui [25] and independently by de
Carvalho [5] in order to establish complexity properties of evaluation in the simply-typed
λ-calculus. It may be also seen as an account based on linear logic of the semantic approach
to higher-order model-checking developed by Aehlig in the early days of the field [1]. The
main contribution of the paper is the observation developed in §3 that this correspondence
between intersection type systems and the relational semantics of linear logic extends to
alternating parity games, and thus to the full hierarchy of the modal µ-calculus. This extension relies on the construction of a parametric comonad in the sense of [16] defined as
a family of modalities 2m indexed by colors (or priorities) m ∈ N, equipped with a series
of structural morphisms satisfying suitable coherence properties. The resulting intersection
type system provides a clean and conceptual explanation for the type system designed by
Kobayashi and Ong [15] in order to accomodate the hierarchy of colors. In particular, we
show that a simpler but equivalent treatment of colors is possible. Finally, we explain in
§3 in what sense the parametric comonad exhibited at the level of intersection types corresponds to a traditional notion of exponential modality at the level of the relational semantics

C. Grellois and P.-A. Melliès

5

of linear logic. We obtain in this way a semantic reformulation of alternating parity games
in an infinitary and colored variant of the relational semantics of linear logic. In particular,
just as for finitary tree automata, a state q ∈ Q of the alternating parity automaton is
accepted if and only if it is an element of the composite (in the relational semantics) of the
recursion scheme with the tree automaton.

2

The type-theoretic approach to higher-order model-checking

Developing an idea by Hosoya, Pierce and Vouillon [13], Kobayashi designed in [14] a typetheoretic account of higher-order model-checking in the particular case of an alternating tree
automata (ATA) testing for coinductive properties — and thus without parity conditions. In
this section, we briefly recall his terminology and results, and explain the hidden connection
with relational semantics.

2.1

Recursion schemes and simply-typed λ-terms with fixpoint

Given a ranked alphabet Σ, we will consider in this paper two kinds of Σ-labelled trees of
finite or countable depth:
ranked trees, typically generated by higher-order recursion schemes, in which the number
of children of a node labelled with f ∈ Σ is equal to the arity ar(f ) of its label,
unranked trees, typically used to describe run-trees of alternating automata, and where
the previous arity constraint is relaxed.
Given a base type ⊥, we will consider the set K of simple types, generated by the grammar
κ ::= ⊥ | κ → κ
modulo associativity of the arrow to the right. Every simple type has a unique decomposition
κ = κ1 → · · · → κn → ⊥
where n is the arity of κ, denoted ar(κ). The complexity of κ is typically measured by its
order, defined inductively by order(κ) = 0 if n = 0 and
order(κ) = 1 + max(order(κ1 ), . . . , order(κn ))
In the sequel, following Kobayashi [14], we shall refer to simple types as kinds, to prevent
confusions with intersection types. We write f :: κ or t :: κ when a symbol f or a term
t has kind κ. The formalism of higher-order recursion schemes (HORS) on a given ranked
signature Σ may be seen as equivalent to simply-typed λ-calculus with a recursion operator
Y and free variables f ∈ Σ of order at most 1. Consequently, every free variable f ∈ Σ of
the λY -term corresponding to the recursion scheme has kind
⊥
· · → ⊥} → ⊥.
| → ·{z

(9)

ar(f )

where ar(f ) denotes the arity of the terminal f ∈ Σ. The normalization of the λY -term
associated to the recursion scheme G produces a potentially infinite ranked tree, labelled
by its free variables. As we explained in the introduction, this translation of higher-order
recursion schemes into λY -terms may be seen as an instance of the Church encoding of
ranked trees over the signature Σ.

6

Relational semantics of linear logic and higher-order model-checking

In order to check whether a given monadic second-order formula holds at the root of the
infinite tree generated by a HORS, a traditional procedure is to explore it using an alternating parity automaton (APT). Every exploration of the APT produces a run-tree labelled
by the same signature, but unranked because of the alternating nature of the automaton.
The subclass of APT in which every state of the automaton is assigned color 0 (the least
coinductive priority) defines the class of alternating tree automata (ATA), which can test
coinductive properties like safety, but cannot test inductive properties like reachability. The
definitions of HORS and APT, as well as the correspondence between APT and monadic
second-order logic, are recalled in the Appendix. In the sequel, S denotes the start symbol of
a recursion scheme G, N its set of non-terminals, and R(F ) denotes for every non-terminal
F ∈ N the simply-typed λ-term it rewrites to as F →G R(F ) in the recursion scheme G.

2.2

From kinds to intersection types

In his original work, Kobayashi reduces the study of coinductive properties of higher-order
recursion schemes to the definition of an intersection type system. The general idea is that
every transition of an alternating tree automaton
δ(q0 , if) = (2, q0 ) ∧ (2, q1 )

(10)

may be understood type-theoretically as a refinement of the simple type
if :: ⊥ → ⊥ → ⊥
and reformulated as an intersection type
∅ → (q0 ∧ q1 ) → q0 .
This intersection type expresses the fact that, given any tree T1 and a tree T2 accepted from
both states q0 and q1 , the composed tree if T1 T2 is accepted from the state q0 . Following
this connection, Kobayashi defines for every HORS G and every alternating tree automaton A
without parity condition a type system Kob(G, A) satisfying the following property:
I Theorem 1 (Kobayashi [14]). The sequent
`G,A S : q :: ⊥
is provable in Kob(G, A) if and only if there is a run-tree of A over [[G]] with initial state q.
Note that the intersection type system Kob(G, A) is somewhat ad hoc since it depends on G
and A, in contrast to the approach developed in the present paper, based on a Church
encoding of G and A in a single intersection type system formulated in §3 and §4.

2.3

Intersection types and the relational semantics of linear logic

As a warm-up to the next two sections §3 and §4, and to the modal treatment of colors in
alternating parity automata (APT), we explain here in the simpler coinductive case, how
to relate Kobayashi’s intersection type system for alternating tree automata (ATA) to an
infinitary variant of the relational semantics of linear logic. As already explained, the Church
encoding of a ranked tree over the signature Σ = {fi : ari | i ∈ I} defines a λY -term t of
simple type ⊥ with free variables fi of kind (9) translated as the following formula of linear
logic:
for i ∈ I.
fi : |! ⊥ ( ·{z
· · ( ! ⊥} ( ⊥
ari

C. Grellois and P.-A. Melliès

7

The λY -term t itself is thus typed by the following sequent of linear logic:


· · · , fi : ! |! ⊥ ( ·{z
· · ( ! ⊥} ( ⊥
, ··· ` t :

⊥

ai

From this follows that its interpretation [[t]] in the relational semantics of linear logic defines
a subset of the following set of “higher-order states”




O
[[t]] ⊆ 
! !|⊥ ( ·{z
· · ( ! ⊥} ( ⊥ ( ⊥ 
i∈I

ari

where the return type ⊥ is naturally interpreted as the set of states [[⊥]] = Q of the alternating tree automaton. As explained in the introduction, the transition function δ of the
alternating tree automaton A is itself interpreted as a subset


 
¯
! ⊥ ( · · · ( ! ⊥ ( ⊥ 
[[δ]] ⊆ 
|
{z
}
i∈I

ari

which may be “strengthened” in the categorical sense as a subset
 




O


[[δ † ]] ⊆ 
! !|⊥ ( ·{z
· · ( ! ⊥} ( ⊥ 
i∈I

ari

where we turn to our advantage the well-known isomorphism of linear logic:
!(A&B )

∼
= !A ⊗ !B.

As explained in the introduction, a first contribution of the article is to establish the following
result in the case of the traditional relational semantics of linear logic, extended here with
a fixpoint operator Y :
I Theorem 2. An alternating tree automaton A with a set of states Q has a finite accepting
run-tree with initial state q0 over the possibly infinite tree generated by a λY -term t if and
only if there exists u ∈ [[δ † ]] such that (u, q0 ) ∈ [[t]], where [[δ † ]] = Mf in ([[δ]]) denotes the set
of finite multisets of elements of [[δ]].
Another equivalent way to state the theorem is that the set of accepting states q0 for a
finite run-tree of the alternating tree automaton A is equal to the composition of [[t]] and
of [[δ † ]] in the relational semantics. At this point, it appears that the only hurdle towards
an extension of this theorem to the alternating tree automata with coinductive (rather than
inductive) acceptance condition is the finiteness of multiplicities in the traditional relational
interpretation of the exponential modality. For this reason, the authors developed in a
companion paper [10] an infinitary variant Rel of the relational model of linear logic, where
the exponential modality noted there « » in order to distinguish it from the traditional « ! »
transports every set A (of cardinality required to be smaller than the reals) to the set
A = Mcount (A)
of finite-or-countable multisets of elements of A. In this alternative relational semantics,
there is a coinductive fixpoint operator Y satisfying the equations of a Conway operator,
and thus providing an interpretation of the λY -calculus. The infinitary interpretation of a

8

Relational semantics of linear logic and higher-order model-checking

λY -term is denoted [[t]] in order to distinguish it from the traditional finitary interpretation.
Note that the interpretation [[δ]] = [[δ]] is unchanged, and that its strengthening to [[δ † ]]
reflects now the infinitary principles of the model. In particular, it is possible to detect
whether a transition has been called a countable number of times. This brings us to the
second main contribution of this article, which is to adapt the previous theorem for finite
accepting run-trees to the general case of possibly infinite accepting run-trees:
I Theorem 3. An alternating tree automaton A with a set of states Q has a possibly infinite
accepting run-tree with initial state q0 over the possibly infinite tree generated by a λY -term t
if and only if there exists u ∈ [[δ † ]] such that (u, q0 ) ∈ [[t]] , where [[δ † ]] = Mcount ([[δ]] )
denotes the set of finite-or-countable multisets of elements of [[δ]] .
This theorem should be understood as a purely semantic counterpart to Theorem 1. The
connection is provided by the foundational and elegant work by Bucciarelli and Ehrhard
[2, 3] on indexed linear logic, which establishes a nice correspondence between the elements
of the relational semantics and a finitary variant of intersection types. By shifting from
finite to finite-or-countable multisets and intersection types, we are able to recover here the
discriminating power of general alternating tree automata. In particular, the set of accepting
states of the alternating tree automaton A is equal to the composition of [[t]] and of [[δ † ]]
in our infinitary variant of the relational semantics.
We should mention however that there is a minor difference between our semantic result
and the original Theorem 1, related to the fact that Kobayashi chose to work in a type system
where intersection is understood as an idempotent operation. This choice is motivated in
his work by the desire to keep the type system finitary, and thus to obtain decidability
results. We prefer to work here with an infinitary relational semantics, corresponding to an
infinitary and non-idempotent variant of Kobayashi’s intersection type system. The reason is
that shifting from an infinitary to an idempotent intersection type system corresponds from
a semantic point of view to shifting from an infinitary relational semantics to its extensional
collapse. Ehrhard [6] has recently established that the extensional collapse of the relational
semantics is provided by a lattice model, where the formulas of linear logic are interpreted as
partially ordered sets. This means that the corresponding intersection type systems should
include a subtyping relation, as well-understood for instance by Terui in [25]. This subtyping
relation is not mentioned in the original work by Kobayashi [14] nor in the later work by
Kobayashi and Ong [15] and although their final result is certainly valid, this omission has
lead to much confusion.

3

A type-theoretic account of alternating parity automata

3.1

Colored intersection types

After designing in [14] the type-theoretic approach to alternating tree automata recalled in
the previous section, Kobayashi carried on in this direction and generalized it with Ong [15]
to the larger class of alternating parity automata. The basic idea of this work is to incorporate coloring annotations in the intersection types, in order to reflect in the type system the
parity conditions of the tree automata. Suppose for instance that a binary terminal a ∈ Σ
induces a transition δ(q, a) = (1, q1 ) ∧ (2, q2 ) in an alternating parity tree automaton with
coloring function Ω : Q → N. In that case, the terminal a is assigned in [15] the intersection
type
a

:

(q1 , m1 ) → (q2 , m2 ) → q

(11)

C. Grellois and P.-A. Melliès

9

where m1 = max(Ω(q1 ), Ω(q)) and m2 = max(Ω(q2 ), Ω(q)) are colors indicating to the type
system the colors of the states q, q1 , q2 of the parity tree automaton.
In order to prepare the later development of paper, we find useful to simplify the colored
intersection type system originally formulated by Kobayashi and Ong, and to stress at the
same time the modal nature of colors (or priorities) in higher-order model-checking. So,
given a set of states Q and a coloring function Ω : Q → N, we define the set of colors
Col = { Ω(q) | q ∈ Q } ] {  }
which contains the colors used by Ω, together with an additional color  which will play the
role of neutral element. The intersection types are then generated by the grammar
θ
τ

::=
::=

q | τ →θ
V
mi θi
i∈I

(q ∈ Q)
(I finite, mi ∈ Col)

The refinement relation between intersection types and kinds is defined by the inductive
rules below:
q∈Q
q :: ⊥

∀i ∈ I θi :: κ
mi θi :: κ
i∈I

τ :: κ1
θ :: κ2
τ → θ :: κ1 → κ2

V

Note that the color modality acts on intersection types and contexts by

V
V
m

i∈I

mi θi

=

i∈I

max(m,mi ) θi

m ( x : τ , ∆ )

=

x : m τ , m ∆

Note also that the neutral color  is only introduced here to allow a uniform definition of
types and contexts. It does not affect the coloring of types, and should be understood as
the absence of a coloring annotation. From this, one obtains an intersection type system
Z(A) parametrized by the alternating tree automaton A, whose rules are given in Figure 1.
Here we use the Hebrew letter Z which should be read “tsadi”. The resulting type system
Z(A) enables us to type the rewriting rules of a higher-order recursion scheme
∆ ` R(F ) : σ :: κ

(12)

where the non-terminals occurring in the λ-term R(F ) appear as variables in the context ∆
of the typing judgement. On the other hand, the intersection type system Z(A) does not
include a fixpoint operator Y and for that reason does not accomodate recursion.

3.2

Interpretation of recursion

In order to accomodate recursion in the intersection type system Z(A), we need to extend
it with a rule f ix whose purpose is to expand the non-terminals F ∈ N of the recursion
scheme G in order to obtain possibly infinitary derivation trees. So, given a higher-order
recursion scheme G and an alternating parity automaton A, we define the intersection type
system Zf ix (G, A) as Z(A) where we add the recursion rule
f ix

Γ ` R(F ) : θ :: κ
F :  θ :: κ ` F : θ :: κ

dom(Γ) ⊆ N

and at the same time restrict the Axiom rule to variables x ∈ V, and in particular do not
allow the Axiom rule to be applied on non-terminals any more.
An important aspect of the resulting intersection type system Zf ix (G, A) is that its derivation
trees may be of countable depth. As in Kobayashi’s original type system, this infinitary
nature of the intersection type system enables one to reflect the existence of infinitary runs

10

Relational semantics of linear logic and higher-order model-checking

Axiom

x :

V
{i}

 θi :: κ ` x : θi :: κ

(x ∈ V ∪ N )

{ (i, qij ) | 1 ≤ i ≤ n, 1 ≤ j ≤ ki } satisfies δA (q, a)

δ

∅`a :

App

Vk 1
j=1

Ω(q1j ) q1j → . . . →

Vk n
j=1

Ω(qnj) qnj → q :: ⊥ → · · · → ⊥ → ⊥

∆ ` t : (m1 θ1 ∧ · · · ∧ mk θk ) → θ :: κ → κ0

∆1 ` u : θ1 :: κ

∆ + m1 ∆1 + . . . + mk ∆k ` t u : θ :: κ

∆, x :
λ

V
i∈I

mi θi :: κ ` t : θ :: κ0

∆ ` λx.t :

V

j∈J

mj θj



···

a∈Σ

∆k ` u : θk :: κ

0

I ⊆ J

→ θ :: κ → κ0

Figure 1 The type system Z(A) associated to the alternating parity tree automaton A.

in the alternating parity automaton A. In order to articulate the parity condition of the
automaton with the typing derivations, a color is assigned to each node of the derivation
tree, in the following way:
the node ∆i ` u : θi :: κ is assigned the color mi in every Application rule
∆ ` t : (m1 θ1 ∧ · · · ∧ mk θk ) → θ :: κ → κ0
· · · ∆i ` u : θi :: κ
∆ + m1 ∆1 + . . . + mk ∆k ` t u : θ :: κ0

···

of the derivation tree,
all the other nodes of the derivation tree are assigned the neutral color , which means
in some sense that they are not colored by the typing system.
A nice aspect of our approach compared to the original formulation in [15] is that the parity
condition traditionally applied to the alternating parity automaton A extends to a very
simple parity condition on the derivation trees of Zf ix (G, A). Indeed, the color of an infinite
branch of a given derivation tree can be defined as
the neutral color  if no other color m ∈ Col occurs infinitely often in the branch,
otherwise, the maximal non-neutral color m ∈ Col \ {} seen infinitely often.
Then, an infinite branch of the derivation tree is declared winning precisely when its color
is an even integer (and in particular different from the neutral color). A winning derivation
tree is then defined as a derivation tree whose infinite branches are all winning in the sense
just explained.

3.3

Soundness and completeness

Once the notion of infinite winning derivation tree explicated, as we have just done in the
previous section, there remains to relate this winning condition to the acceptance condition
of alternating parity automata. To that purpose, and for the sake of the presentation, we
choose to restrict ourself to productive recursion schemes, as it is also done in [15]. Note that
it is only a very mild restriction, since every recursion scheme G can be transformed in to a
productive recursion scheme G 0 which outputs a special leaf symbol Ω whenever the Böhm
evaluation of the original scheme G would have infinitely looped. The following theorem
establishes a soundness and completeness theorem which relates the winning condition on the
infinite derivation trees of Zf ix (G, A) to the parity acceptance condition of the automaton A
during its exploration of the infinite tree [[G]] generated by the recursion scheme G:

C. Grellois and P.-A. Melliès

11

I Theorem 4 (soundness and completeness). Suppose given a productive recursion scheme
G and an alternating parity automaton A. There exists a winning run-tree of A over [[G]]
with initial state q if and only if the sequent
S :  q :: ⊥ ` S : q :: ⊥

(13)

has a winning derivation tree in the type system Zf ix (G, A).
There are several ways to establish the theorem. One possible way is to establish an equivalence with the original soundness and completeness by Kobayashi and Ong [15]. One should
be careful however that the original proof in [15] was incomplete, and has been corrected
in the (unpublished) journal version of the paper. In order to establish the equivalence,
one shows that the existence of a winning derivation tree of the sequent (13) in the intersection type system Zf ix (G, A) is equivalent to the existence of a winning strategy for Eve
in the parity game defined in [15]. Another more direct proof is possible, based on the
reformulation by Haddad [11] of Kobayashi and Ong’s treatment of infinitary (rather than
simply finitary) sequences of rewrites on higher-order recursion schemes. It is in particular
important to observe that the infinitary nature of computations requires to extend the usual
soundness and completeness arguments based on Böhm trees, finite rewriting sequences and
continuity. This point was apparently forgotten in [15] and corrected in the journal version
of the paper.

4

An indexed tensorial logic with colors

The notation m θ is used in our intersection type system Zf ix (G, A) as a way to stress the
modal nature of colors, and it replaces for the better the notation (θ, m) used by Kobayashi
and Ong in [15]. As we will see, the discovery of the modal nature of colors is fundamental,
and is not just a matter of using the appropriate notation. In particular, it enables us to
simplify both technically and conceptually the original intersection type system in [15]. By
way of illustration, the original intersection type (11) of the binary terminal a ∈ Σ considered
in §3.1 is replaced by the simpler intersection type:
a

:

n1 q1 → n2 q2 → q

(14)

where n1 = Ω(q1 ) and n2 = Ω(q2 ). Interestingly, the color of the state q is not mentioned
in the type anymore. The reason is that this alternative account of colors achieved in our
type system is not just “simpler” than the original one: it also reveals a deep and somewhat
unexpected connection with linear logic, since as we will see, this “disparition” of the color
Ω(q) in (14) is related to the well-known linear decomposition A ⇒ B = !A ( B of
the intuitionistic implication in linear logic. One essential difference however is that the
exponential modality « ! » of linear logic is replaced by a family of modal boxes Ω(m) which
formally defines what Melliès calls a parametric comonad in [19] [17].
This key observation enables us to translate the intersection type system Zf ix (G, A) into
an infinitary variant of linear logic equipped with a family of color modalities noted 2m
for m ∈ N. A nice feature of the translation is that it transports the intersection type
system Zf ix (G, A) which depends on G and A into an intersection type system which does
not depend on them anymore — although it still depends on the set Q of states of the
automaton. The infinitary variant of linear logic which we use for the translation is
indexed in the sense of Bucciarelli and Ehrhard [2,3]. In particular, the finite or countable
V
intersection types i∈I θi of Zf ix (G, A) are translated as finite or countable indexed
families [θi | i ∈ I] of formulas of the logic,

12

Relational semantics of linear logic and higher-order model-checking

tensorial in the sense of Melliès [18–20]. In this specific case, every negated formula of
the logic is negated with respect to a specific state q ∈ Q of the automaton, and is thus
q
of the form σ ( q, which may be alternatively written as ¬q σ or even as ¬ σ.
In this way, one obtains an indexed and colored variant of tensorial logic, called LT(Q) in
the sequel, and whose formulas are inductively generated by the following grammar:
A, B

::=

1 | A⊗B

|

¬q A

| m A

| [ Aj | j ∈ J ]

(m ∈ Col, q ∈ Q)

As already mentioned, following the philosophy in [3], the finite or countable indexed set
[σj | j ∈ J] internalizes the intersection operator of Zf ix (G, A) in our indexed tensorial logic,
see our companion paper [9] for details. Importantly, the resulting indexed logic T L(Q) can
be used as an intersection type system refining the simply-typed λ-calculus in just the same
way as Zf ix (G, A), see the Appendix . In particular, the fact that  defines a parametric
monoidal comonad in the logic means that the sequents
`
`
`

 A
max(m1 , m2 ) A
m A ⊗ m B

A
m1 m2 A
m (A ⊗ B)

are provable for all colors m, m1 , m2 ∈ N, and all formulas A, B. In order to deal with
recursion schemes, we admit derivation trees with finite or countable depth in the logical
system T L(Q). The nodes of the derivation trees of T L(Q) are then colored in the following
way:
every node Γ ` M : A :: κ in a Right introduction of the modality 2m :
Γ ` M : A :: κ
m Γ ` M : m A :: κ

Right m

is assigned the color m of the modality,
all the other nodes of the derivation tree are assigned the neutral color .
The winning condition on an infinite derivation tree of T L(Q) is then directly adapted
from the similar condition in Zf ix (G, A). Thanks to this condition, we are ready to state a
useful correspondence theorem between Zf ix (G, A) and T L(Q) for any (productive) recursion
scheme G. Suppose that for each F ∈ N of kind κ(F ) of the recursion scheme G, we introduce
a new free variable f reeze(F ) of kind κ(F ) → κ(F ) ; that we replace each λ-term R(F )
by its βη-long normal form ; and finally, that we substitute each occurrence of F appearing
in any βη-long normal form R(G) of the recursion scheme G with the λ-term f reeze(F ) F
of the same kind κ(F ). This transformation induces a context-free grammar of « blocks»
consisting of the βη-long R(G)’s, which generates an infinite λ-term in βη-long normal form,
noted term(G), with free variables of the form f reeze(F ). Moreover, this infinite λ-term
term(G) is coinductively typed in the simply-typed λ-calculus by the typing judgment:
...

,

f reeze(F ) : κ(F ) → κ(F ) ,

...

`

term(G)

:

⊥

(15)

where F runs over all the non-terminals F ∈ N of the higher-order recursion scheme G. At
this point, we are ready to recast our Theorem 4 in the proof-theoretic language of indexed
tensorial logic:
I Theorem 5. There exists a winning derivation tree in Zf ix (G, A) of the sequent
S :  q0 :: ⊥ ` S : q0 :: ⊥

(16)

if and only if there exists a winning derivation tree in T L(Q) of a sequent
Γ ` term(G) : q0 :: ⊥
refining the typing judgment (15).

(17)

C. Grellois and P.-A. Melliès

5

13

Putting all together: relational semantics of linear logic and
higher-model model-checking

Once the connection between higher-order model-checking and indexed tensorial logic established in §4, there remains to exhibit the associated relational semantics of linear logic,
following the ideas of Bucciarelli and Ehrhard [2, 3]. This trail leads us to an infinitary and
colored variant of the usual relational semantics of linear logic, developed in our companion
paper [10]. The key observation guiding the construction is that the functor


:

A

7→

Col × A

:

→

Rel

Rel

equipped with the coercion maps
{(((m, a) , (m, b)) , (m, (a, b))) | a ∈ A, b ∈ B, m ∈ Col}
{ (?, (m, ?)) | m ∈ Col }
{ ( ( max(m1 , m2 ), a) , ( m1 , (m2 , a) ) ) | a ∈ A }
{ ( ( , a) , a) | a ∈ A }

:
:
:
:

A ⊗ B
1
A
A

→
→
→
→

 (A ⊗ B)
1
A
A

defines a lax monoidal comonad 2 : Rel → Rel on the category Rel of sets and relations.
Moreover, the comonad distributes (or better: commutes) with the exponential modality ,
in such a way that these two comonads compose into a new exponential modality of linear
logic defined by the equation A = 2 A. A Conway operator Y can be then defined
in order to reflect in the relational semantics the definition of the winning condition on
the infinite derivations of T L(Q). This fixpoint operator can be seen as a combination of
the inductive and coinductive fixpoints of the model, where the color of an input indicates
whether the fixpoint operator should be defined inductively (when the color is odd or neutral)
or coinductively (when the color is even). The relational interpretation of a λY -term t in
this infinitary model is denoted as [[t]] . The interpretation [[δ]] of the transition function
δ is defined similarly as for [[δ]] , except that the color information is incorporated in the
semantics following the comonadic principles underlying the translation (14) in §4. Typically,
the transition (10) is interpreted in the colored relational semantics as
([ ], ([(Ω(q0 ), q0 ), (Ω(q1 ), q1 )], q0 ))

∈

[[δ]]

The last contribution of this paper, which underlies our companion paper [10] but is not
stated there, establishes a clean correspondence between the relational semantics of a higherorder recursion scheme G (seen below as a λ Y -term tG ) and the exploration of the associated
ranked tree [[G]] by an alternating parity automaton A:
I Theorem 6. An alternating parity tree automaton A with a set of states Q has a winning
run-tree with initial state q0 over the ranked tree [[G]] generated by the λY -term tG if and
only if there exists u ∈ [[δ † ]] such that (u, q0 ) ∈ [[tG ]] , where [[δ † ]] = Mcount (Col × [[δ]] )
denotes the set of finite-or-countable colored multisets of elements of [[δ]] .

6

Related works

The field of higher-order model-checking was to a large extent started at the turn of the century by Knapik, Niwinski, Urzyczyn, who established that for every n ≥ 0, Σ-labelled trees
generated by order-n safe recursion schemes are exactly those that are generated by order-n
pushdown automata, and further, that they have decidable MSO theories. The safety condition was relaxed a few years later by Ong, who established the MSO decidability for general
order-n recursion schemes, using ideas imported from game semantics. Unfortunately, Ong’s

14

Relational semantics of linear logic and higher-order model-checking

proof was intricate and somewhat difficult to understand. Much work was thus devoted to establish the decidability result by other means. Besides the type-theoretic approach initiated
by Kobayashi [14, 15], Hague, Murawski, Ong, Serre [12] developed an automata-theoretic
approach based on the translation of the higher-order recursion scheme G into a collapsible
pushdown automaton (CPDA), which led the four authors to another proof of MSO decidability for order-n recursion schemes. A clarifying connection was then made by Salvati and
Walukiewicz between this translation of higher-order recursion schemes into CPDAs and the
traditional evaluation mechanism of the environment Krivine machine [22]. Following this
discovery, Salvati and Walukiewicz are currently developing a semantic approach to higherorder model checking, based on the interpretation in finite models of the λ-calculus with
fixpoint operators, see [23, 24] for details. The idea of connecting linear logic to automata
theory is a longstanding dream which has been nurtured by a number of important contributions. Among them, we would like to mention the clever work by Terui [25] who developed a
semantic and type-theoretic approach based on linear logic, intersection types and automata
theory in order to characterize the complexity of evaluation in the simply-typed λ-calculus.
In a different but related line of work, explicitly inspired by Bucciarelli and Ehrhard’s indexed linear logic [2, 3], de Carvalho [5] establishes an interesting correspondence between
intersection types and the length of evaluation in a Krivine machine.

7

Conclusions and perspectives

The purpose of the present paper is to connect higher-order model-checking to a series of
advanced ideas in contemporary semantics, like linear logic and its relational semantics,
indexed linear logic, distributive laws and parametric comonads. All these ingredients meet
and combine surprisingly well. The approach reveals in particular that the traditional treatment of inductive-coinductive reasoning based on colors (or priorities) is secretly based on
the same comonadic principles as the exponential modality of linear logic.
Besides the conceptual promises offered by these connections, we would like to conclude
the paper by mentioning that this stream of ideas leads us to an alternative and purely
semantic proof of MSO decidability for higher-order recursion schemes, after [12, 15, 21].
The basic idea is to replace the infinitary colored relational semantics constructed in §5
by a finitary variant based on the prime-algebraic lattice semantics of linear logic. From
a type-theoretic point of view, this lattice semantics corresponds to an intersection type
system with subtyping for linear logic recently formulated by Terui [25]. We have shown
in a companion paper [8] how to recover the MSO decidability result for order-n recursion
schemes by adapting to this finitary semantics of linear logic the constructions performed
here for its relational semantics. One interesting feature of the resulting model of the λ Y calculus is that a morphism D → E in the Kleisli category consists in a continuous function
f

:

D × ··· × D
{z
}
|

−→

E

n

where n is the number of colors considered in the semantics ; and that the fixpoint Y f of a
morphism f : D → D is defined in that case by the alternating formula
Yf

=

νxn . µxn−1 . . . νx2 . µx1 . νx0 .f (x0 , . . . , xn )

where we suppose (without loss of generality) that n is even, where µ and ν denote the
least and greatest fixpoint operators, respectively. We believe that the apparition of this
simple formula and the fact that it defines a Conway operator Y and thus a model of the

C. Grellois and P.-A. Melliès

λ Y -calculus is a key contribution to the construction of a semantic and purely compositional
account of higher-order model-checking.
References
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata.
Logical Methods in Computer Science, 3(3), 2007.
Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics
in multiplicative-additive linear logic. Ann. Pure Appl. Logic, 102(3):247–282, 2000.
Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics:
the exponentials. Ann. Pure Appl. Logic, 109(3):205–241, 2001.
M. Coppo, M. Dezani-Ciancaglini, F. Honsell, and G. Longo. Extended Type Structures
and Filter Lambda Models. In Logic Colloquium 82, 1984.
Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009.
Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational
model. Theor. Comput. Sci., 424:20–45, 2012.
Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. C.U.P., 1989.
Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order
model-checking. available at http://arxiv.org/abs/1502.05147, 2015.
Charles Grellois and Paul-André Melliès. Indexed linear logic and higher-order model
checking. In Intersection Types and Related Systems 2014, EPTCS 177, 2015.
Charles Grellois and Paul-André Melliès. An infinitary model of linear logic. preprint at
http://arxiv.org/abs/1411.4380, Fossacs 2015.
Axel Haddad. Shape-preserving transformations of higher-order recursion schemes. PhD
thesis, Université Paris Diderot, 2013.
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible
pushdown automata and recursion schemes. In LICS, 2008.
Haruo Hosoya, Jerome Vouillon, and Benjamin C. Pierce. Regular expression types for
XML. In Martin Odersky and Philip Wadler, editors, ICFP, 2000.
Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order
programs. In Zhong Shao and Benjamin C. Pierce, editors, POPL, 2009.
Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus
model checking of higher-order recursion schemes. In LICS, 2009.
Paul-André Melliès. Parametric monads and enriched adjunctions. LOLA 2012.
Paul-André Melliès. Functorial boxes in string diagrams. In Zoltán Ésik, editor, CSL,
volume 4207 of Lecture Notes in Computer Science, pages 1–30. Springer, 2006.
Paul-André Melliès. Game semantics in string diagrams. In LICS, 2012.
Paul-André Melliès. The parametric continuation monad. Math. Struct. Comp. Sci., 2014.
Paul-André Melliès and Nicolas Tabareau. Resource modalities in game semantics. In
LICS, pages 389–398. IEEE Computer Society, 2007.
C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In
LICS, pages 81–90. IEEE Computer Society, 2006.
Sylvain Salvati and Igor Walukiewicz. Recursive schemes, krivine machines, and collapsible
pushdown automata. In RP, 2012.
Sylvain Salvati and Igor Walukiewicz. Evaluation is msol-compatible. In FSTTCS, volume 24 of LIPIcs, 2013.
Sylvain Salvati and Igor Walukiewicz. Using models to model-check recursive schemes. In
TLCA, volume 7941 of LNCS, 2013.
Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed
lambda calculus. In RTA, volume 15 of LIPIcs, 2012.

15

16

Relational semantics of linear logic and higher-order model-checking

A

Logical specification and automata theory

A.1

Monadic second-order logic and modal µ-calculus

The purpose of higher-order model-checking is to abstract the behavior of a functional
program with recursion as a tree approximating the set of its potential executions, and
then to specify a logical property to check over this tree. The tradition in higher-order
model-checking is to consider monadic second-order logic, a well-balanced choice between
expressivity – it contains most other usual logics over trees – and complexity: the satisfiability of a formula is decidable for infinite structures of interest – as infinite trees (Rabin
1969). Higher-order verification has a different approach: the question is whether a given
tree satisfies the formula – or whether an equivalent automaton accepts it. A first step
towards this automata model for MSO is
I Theorem 7 (Janin-Walukiewicz 1996). MSO is equi-expressive to modal µ-calculus over
trees.
where modal µ-calculus formulae are defined by
φ ::= X | f | φ ∨ φ | φ ∧ φ |  φ | i φ | µX. φ | νX. φ
for f ∈ Σ. Given a ranked tree, the semantics of a formula is the set of nodes where it holds.
The predicate f is true on f -labelled nodes,  φ is true on nodes whose succesors all satisfy
φ, i φ is true on nodes whose ith succesor satisfies φ, and the µ and ν are two fixpoints
operators which can be understood in two different manners. Semantically, they are dual
operators, µ and ν being respectively the least and greatest fixpoint on the semantics of
formulae.
Given a Σ-labelled ranked tree whose set of nodes is N , whose branching structure is given
by a finite family of successor functions succi : N → N , and whose labelling is described by
a function label : N → Σ, the semantics of a closed modal µ-calculus formula φ is defined
as ||φ||∅ where ∅ denotes the unique function ∅ → N , and for a function V : V ar → N and
a modal µ-calculus formula ψ, the semantics ||ψ||V are defined inductively:
||a||V = {n ∈ N | label(n) = a}
||X||V = V(X)
||¬φ||V = N \ ||φ||V
||φ ∨ ψ||V = ||φ||V ∪ ||ψ||V
|| i φ||V = {n ∈ N | ar(n) ≥ i and succi (n) ∈ ||φ||V }
T
||µX. φ(X)||V =
{M ⊆ N | ||φ(X)||V[X←M ] ⊆ M }
where V[X ← M ] coincides with V except on X which it maps to M . The semantics of
∧,  and ν are defined using de Morgan duality.
Another understanding of µ and ν is syntactic and closer to automata theory: both allow
the unfolding of formulae
µX. φ[X] →µ φ[µX. φ[X]] and νX. φ[X] →ν φ[νX. φ[X]]
but →µ may only be expanded finitely, while →ν is unconstrained. The semantics of a
formula may then be understood as the set of positions from which it admits unfoldings
which are logically true and which do not use →µ infinitely.

C. Grellois and P.-A. Melliès

A.2

Alternating parity tree automata

From this syntactic interpretation of fixpoints over formulae, we can define a class of automata corresponding to modal µ-calculus, namely alternating parity automata (APT),
whose purpose is to synchronise the unraveling of formulas with symbols of the tree. These
automata are top-down tree automata, with two additional features:
alternation: they have the power to duplicate or drop subtrees, and to run with a different
state on every copy,
and parity conditions: since run-trees are infinitary by nature, these automata discriminate a posteriori the run-tree unfolding →µ infinitely.
The transition function takes values in positive Boolean formulae over couples of states
and directions, its generic shape being
_ ^
(di,j , qi,j )
(18)
δ(q, a) =
i∈I j∈Ji

which consists of a non-deterministic choice of i followed by the execution of |Ji | copies of
the automaton, each on the successor in direction di,j of the current node, with state qi,j .
When for every i ∈ I and every direction d there is a unique j such that di,j = d, we
recover the usual notion of non-deterministic parity automaton. States of an APT may be
understood as subformulae of the formula of interest, so that some correspond to subformulae
µX. φ and others to subformulae νX. φ. To exclude infinite unfoldings of µ, every state q
is given a color Ω(q) ∈ N. States in the immediate scope of a µ receive an odd color, and
the others an even one. If q corresponds to a subformula of q 0 , then the coloring will satisfy
Ω(q) ≤ Ω(q 0 ). The construction of Ω is such that the greatest color among the ones seen
infinitely often in an infinite branch informs the automaton about which fixpoint operator
was unfolded infinitely along it.
A branch of a run-tree is winning when the greatest color seen infinitely often along it
is even. A run-tree is declared winning when all its infinite branches are. Every modal
µ-calculus formula φ can be translated to an APT Aφ such that
I Theorem 8 (Emerson-Jutla 1991). Given a Σ-labelled ranked tree T , φ holds at the root
of T if and only if Aφ has a winning run-tree over T .

A.3

An interactive interpretation of APT

Recall that a parity game is a graph in which each vertex v ∈ V belongs to a player: Eve or
Adam. It can be understood as a game where a token moves from vertex to vertex, starting
from the initial one, and taking on each vertex an outgoing edge chosen by the player who
controls it. The resulting interaction is called a play, and a maximal play is finite if and only
if it ends on a vertex without outgoing edges. There is a coloring function Ω : V → N, and
the winning condition over infinite plays is defined just as for infinite branches of run-trees.
For finite maximal plays, the player controlling the last vertex loses.
A strategy for a player is a map from the set of plays ending with a node he controls to
V. It indicates the player which move he should take during a play. It is positional if it can
be recovered from a function V → V. The strategy is winning (resp. colorblind) if every
maximal play (resp finite maximal play) in which it is followed by the player is winning for
him.
I Theorem 9 (Martin 1975). Parity games enjoy positional determinacy: given an initial
vertex, one of the players has a winning positional strategy from it. It is computable when
the game is finite.

17

18

Relational semantics of linear logic and higher-order model-checking

The execution of an APT over a tree T may then be understood as a parity game in
which Eve constructs a run-tree by playing the non-deterministic choice of the transition
function (18): she selects i, while Adam chooses a direction to explore by picking j ∈ Ji . A
play is thus an exploration of a branch – controlled by Adam – of a run-tree built by Eve.
Then Eve has a winning strategy from the root (and the initial state) if and only if she can
build a run-tree in which Adam can not find a branch that violates the parity condition or
is rejected by the automaton: she has a winning strategy if and only if A has a winning
run-tree over T .

B

Higher-order recursion schemes

Functional programs are a challenge for verification, as they feature higher-order recursion.
Higher-order recursion schemes (HORS) provide an abstract model of functional programs
which precisely focuses on the complex program flow induced by this recursive power. HORS
produce trees abstracting the set of executions of programs. They notably do not allow the
evaluation of conditionals nor the treatment of references.
Consider a signature Σ, a set of variables V, and a set of non-terminals N . The function
kind is extended to V ]N with a simple type for each variable and non-terminal. A HORS is
the data of an axiom S ∈ N of simple type ⊥ and of a function R mapping each non-terminal
N to a closed term
R(F ) = λx1 . . . . λxn . t

(19)

of simple type kind(F ), and such that each of the xi is in V and that t is a term without
abstractions.
The order of G is max ({order(kind(F )) | F ∈ N }). We define inductively the rewriting
relation →G over terms by:
F t1 · · · tn →G t[xi := ti ] if R(F ) = λx1 · · · λxn . t,
if s →G t then s u →G t u and u s →G u t.
The value tree [[G]] of the scheme, when it exists, is defined as the limit tree obtained by this
infinite rewriting process starting from S, and is a Σ-labelled ranked tree.
We define the term t(G) as the one obtained by considering R as a regular grammar. It
is the infinite term corresponding to G; its β-reduction computes [[G]].
I Example 10. Given Σ = { if : 2, data : 1, Nil : 0, }, consider the recursion scheme
S
L

=
=

L Nil
λx. if x (L (data x )

Its value tree is depicted in Figure 2. Even though the scheme is very simple, this is not a
regular tree: it has infinitely many different subtrees. A consequence is that the application
of Theorem 9 over [[G]] does not suffice to decide the existence of a winning run-tree over it.
The effect of the transitions
δ(q0 , if) = (2, q0 ) ∧ (2, q1 ) and δ(q1 , if) = (1, q1 ) ∧ (2, q0 )
is depicted in Figure 3.

C. Grellois and P.-A. Melliès

19

if
if q0

if

Nil
data
Nil

if q1

if q0

if
.
data ..

if q0 if q1 data q1 if q0

Nil

..
.

..
.

..
.

data

..
.

Figure 3 An APT run-tree.

Figure 2 An order-1 value tree.
Axiom

x :

V
{i}

(x ∈ V ∪ N )

Ω(θi ) θi :: κ ` x : θi :: κ

{ (i, qij ) | 1 ≤ i ≤ n, 1 ≤ j ≤ ki } satisfies δA (q, a)

δ

∅`a :

App

Vk1
j=1

m1j q1j → . . . →

Vk n
j=1

mnj qnj → q :: ⊥ → · · · → ⊥ → ⊥

∆ ` t : (m1 θ1 ∧ · · · ∧ mk θk ) → θ :: κ → κ0

∆1 ` u : θ1 :: κ

for a ∈ Σ and mij = max(Ω(qij ), Ω(q))

···

∆k ` u : θk :: κ

∆ + m1 ∆1 + . . . + mk ∆k ` t u : θ :: κ0

∆, x :
λ

V
i∈I

mi θi :: κ ` t : θ :: κ0

∆ ` λx.t :

V

j∈J

mj θj



I ⊆ J

→ θ :: κ → κ0

Figure 4 The Kobayashi-Ong type system KO(A) associated to the alternating parity tree
automaton A

C
C.1

Connection with the Kobayashi-Ong approach
The Kobayashi-Ong type system

Consider a coloring function Ω : Q → N, we extend it to intersection types by setting
Ω(τ → σ) = Ω(σ). The original type system of Kobayashi and Ong is recasted in Figure
4. Note that every rule of a recursion scheme admits a finite number of colored intersection
typings (12), where the contexts consist of refined typings of the non-terminals occuring in
R(F ). In a context ∆, a non-terminal G typically occurs as
^
G :
mi θi :: kind(G)
(20)
i∈I

C.2

Recursion as a parity game

Fixing a recursion scheme G and an APT A, we obtain a finite set of typings (12) for each
rewrite rule. In order to account for recursion, Kobayashi and Ong introduce the finite
parity game Adamic(G, A), in which Adam incrementally tries to disprove Eve’s typing by
picking non-terminals to unfold.
More specifically, Eve’s vertices correspond to colored typings for non-terminals, while
Adam’s vertices are typing contexts. There is an edge from a typing F : m θ :: κ to a

20

Relational semantics of linear logic and higher-order model-checking

context ∆ if and only the sequent
∆ ` R(F ) : θ :: κ

(21)

is provable in the colored type system KO(A), and there is an edge from a context ∆ to a
typing G : m θ :: κ if and only if G occurs in ∆ with this refined type – that is, if G occurs
in ∆ as in (20), if there is i ∈ I such that m = mi and θ = θi . Note that the resulting game
is finite, due to the idempotency of the intersection operator. Vertices F : m θ :: κ receive
color m; other vertices receive the neutral color .
A play is winning for Adam if and only if it ends on a node F : m θ :: κ from which Eve
has no move - that is, if she made a typing assumption she can not prove - or if it is infinite
and such that Adam could choose infinitely often to expand a non-terminal of maximal odd
color. Therefore, Eve has a winning strategy in this game if and only if she can ensure the
existence of a winning sequence of typings along every possible branch of reductions in the
scheme, leading to
I Theorem 11 (Kobayashi-Ong 2009 [15]). Eve has a winning strategy in the parity game
Adamic(G, A) iff the alternating parity tree automaton A has a winning run-tree over [[G]].

C.3

From Adamic(G, A) to Edenic(G, A)

Despite its intuitive connection with type theory, the game Adamic(G, A) does not describe
the on-the-fly construction of a branch of a typing proof, for two essential reasons:
Eve does not provide a witness of the typing proof of the sequent (21) which builds ∆,
so that proofs can not be extracted from plays, and that no distinction is made between
different derivations with the same conclusion,
and Adam does not play an occurence of a non-terminal in R(F ), but a typing which
could, due to idempotency, correspond to several Axiom leaves of a derivation tree.
In order to understand the game Adamic(G, A) from a purely type-theoretic point of view,
we introduce the parity game Edenic(G, A), which only differs on these two points:
Eve plays typing proofs of sequents (21) in addition to the context ∆ they build,
and Adam plays occurences of non-terminals appearing in the term R(F ) – or, equivalently, picks an Axiom leaf introducing a non-terminal in the proof π provided by Eve at
the previous turn.
Note that the resulting game is bigger, yet finite. We prove the following correspondence:
I Proposition 1. The parity games Adamic(G, A) and Edenic(G, A) are equivalent, in the
sense that a player has a winning strategy in a game if and only if he does in the other.
Note that the collapse of strategies of Edenic(G, A) to strategies of Adamic(G, A) relies
on a uniformization property which is reminiscent of the proof of the positional determinacy
of parity games: from a winning strategy for Eve in Edenic(G, A), one can extract such a
strategy in which, given a colored type, any occurence of a non-terminal with this type will
be mapped to the same typing proof.

C.4

Colored typings

From the parity game Edenic(G, A), we can easily define a corresponding type system
similar in the spirit to Zf ix (G, A), but using Kobayashi and Ong’s original coloring policy.
Consider the system KO f ix (G, A) obtained from KO(A) by restricting the Axiom rule to

C. Grellois and P.-A. Melliès

21

variables x ∈ V, and by adding the f ix rule
f ix

Γ ` R(F ) : θ :: κ
F : Ω(θ) θ :: κ ` F : θ :: κ

dom(Γ) ⊆ N

As in Zf ix (G, A), derivations of infinite depth are allowed in KO f ix (G, A). Colorblind strategies σ for Eve in Edenic(G, A) are easily translated as proofs π(σ) in KO f ix (G, A), by incrementally plugging to every f ix rule the finite proof-tree she answers in σ, starting from
the unfolding of the axiom S of the scheme

f ix

..
.
Γ ` R(S) : q0 :: ⊥
S : Ω(q0 ) q0 :: ⊥ ` S : q0 :: ⊥

Of course, the inverse process can be defined as well, leading to the unique definition for
every derivation tree π in KO f ix (G, A) of a colorblind strategy σ(π) for Eve in Edenic(G, A).
Adam’s rôle in Edenic(G, A) is also transported in KO f ix (G, A): its strategies leading to
infinite interactions with σ are in one-to-one bijection with the infinite branches of π(σ).
Strategies resulting in finite interactions are not quite branches, but paths leading to an
instance of a f ix rule expanding a term without non-terminals.
In order to account for the parity condition in Edenic(G, A), we color the f ix rules of
the tree in the same manner: every f ix rule expands a non-terminal occuring as (20) in the
context introduced by the immediately preceding instance of f ix; it receives the color mi
corresponding to the refined type θi of the occurence to expand. The first f ix rule, which
expands S, receives color 0. Now the usual parity condition for trees is incorporated to
KO f ix (G, A) derivation trees: winning derivation trees are those whose infinite branches all
satisfy the parity condition.
I Theorem 12.
A colorblind strategy σ for Eve is winning in Edenic(G, A) if and only
if π(σ) is a winning derivation tree of KO f ix (G, A).
A derivation tree π of KO f ix (G, A) is winning if and only if Eve’s colorblind strategy
σ(π) is winning in Edenic(G, A).

C.5

Proof of Theorem 4

Theorem 4 is central in this article, as it discloses the comonadic behaviour of the coloring
annotation of the alternating parity automaton. It admits at least three proofs:
one proof consists in a minor and at the same time clarifying alteration of the proof given
by Kobayashi and Ong in the unpublished journal version of their original article,
another more direct proof is based on the equivalence between the game Edenic(G, A)
and of the game Edenicnew (G, A) obtained by playing typing derivations of the Z(A)
type system instead than in KO(A),
the authors are currently writing a third proof formulated in a purely proof-theoretic
language and based on standard techniques in linear logic and semantics, as well as on
the proof by Kobayashi and Ong in the unpublished journal version of their original
article [15] and on the proof by Haddad [11].

Adapting Kobayashi and Ong’s original proof. We start by briefly explaining how the
original proof of soundness given in Kobayashi and Ong’s unpublished journal version of [15]

22

Relational semantics of linear logic and higher-order model-checking

may be very naturally adapted to the comonadic color policy formulated in our paper. The
key idea is to change the definition of the color Ω(C[ ]q ) of a context in the following way:
if C[ ]q = [ ]q , then Ω(C[ ]q ) = ,
if C[ ]q = h α, q 0 i T1 · · · Ti−1 C 0 [ ]q Ti+1 · · · Tn , then
if C 0 [ ]q = [ ]q , then Ω(C[ ]q ) = ,
0
0
0
if C 0 [ ]q = h β, q 00 i T10 · · · Tj−1
C 00 [ ]q Tj+1
· · · Tm
, then Ω(C[ ]q ) = max(Ω(q 00 ), Ω(C 0 [ ]q )).
The definition is written here in the style of Kobayashi and Ong’s proof. However, in
order to understand its true content, one should observe that every tree-context C[ ]q is
either trivial or has a “return state” q 0 defined as the state of the tree automaton labelling
its root h α, q 0 i. The color of the trivial tree-context [ ]q is itself trivial (that is, equal to the
neutral color ) while the color of a non-trivial tree-context C[ ]q is equal to the maximal
color encountered from its return state q 0 (not included) to its hole (not included). This
0
reflects the comonadic nature of our coloring policy, as disclosed in §4. If we write C[ ]qq for
a non-trivial tree-context with return type q 0 , we thus have that the color of a context
0

h α, q 00 i T1 · · · Ti−1 C[ ]qq Ti+1 · · · Tn



0
.
is equal to max Ω (q 0 ) , Ω C[ ]qq
To summarize, the general philosophy of tensorial logic is that the color c = Ω(q) which
labels the state q in Kobayashi and Ong’s approach labels in our case the comonadic box
c which encloses the state q. The definition of Kobayashi and Ong’s function Λ should be
adapted accordingly: in the case (i) of the definition of the rewriting relation  in Section 4.1
of their unpublished journal version of [15], Λ{l 7→ Ω(q)} must be changed to Λ{l 7→ } in
order to reflect the fact that the tree context is trivial in that case. These revised definitions
of Ω and Λ clarify the secretely comonadic principles underlying the proofs of Lemma 4.4
and 4.5 of Kobayashi and Ong’s unpublished journal article, which for that reason can be
easily adapted to our new, comonadic coloring policy. The remaining part of the proof
of soundness (in particular Lemma 4.8) works exactly in the same way in our setting as
in Kobayashi and Ong’s original formulation. This provides a proof of soundness for the
system Zf ix (G, A).

Another proof directly based on parity games. An alternative and simple way to prove
Theorem 4 (soundness and completeness) is to return to the original framework of parity
games, and in particular to the equivalence between Adamic(G, A) and Edenic(G, A) established in Proposition 1. Remember indeed that the parity game Edenic(G, A) is closely
related to the proof-system KO(A). We thus introduce a minor variant of this parity game
called Edenicnew (G, A) adapting Edenic(G, A) to the proof-system Z(A), which plays for
KO(A) the same role as the system Zf ix (G, A) for KO f ix (G, A). It is easy to recast Theorem 12 in this setting, and to show that there is a correspondence between Eve’s colorblind
strategies in the parity game Edenicnew (G, A) and the derivation trees in the type system
Zf ix (G, A). Moreover, this correspondence maps winning strategies to winning derivations,
and conversely. We shall now prove the following equivalence:
I Proposition 2. If G is a productive higher-order recursion scheme, then the parity games
Edenic(G, A) and Edenicnew (G, A) are equivalent, in the sense that a player has a winning
strategy in one of these games if and only if he has a winning strategy in every of these
games.

C. Grellois and P.-A. Melliès

23

We have already established the equivalence between Adamic(G, A) and Edenic(G, A) in
Proposition 1. In order to prove Proposition 2, we observe that there exists a one-to-one
correspondence between KO(A) and Z(A) derivation trees. This implies that there exists
a one-to-one correspondence between Eve’s colorblind strategies in Edenic(G, A) and in
Edenicnew (G, A). The same is true for Adam: his strategies in both games are identical.
In order to establish that the parity games Edenic(G, A) and in Edenicnew (G, A) are
equivalent, there remains to prove that this correspondence preserves the color of infinite
branches. Notice that the productivity of the recursion scheme G excludes the existence of
an infinite branch containing, after a finite prefix, only non-terminals and bound variables on
head positions: indeed, their head reduction would lead to ⊥, which is forbidden by productivity. A consequence is that every infinite branch of a productive recursion scheme G visits
infinitely often a term in head position in an Application rule, so that every such infinite
branch is assigned countably many non-neutral colors in Edenicnew (G, A). Of course, between two such visits to non-neutral colors, the neutral color  is played in Edenicnew (G, A),
whereas the last visited color is repeated in the original game Edenic(G, A). However, since
such repetitions are always of finite length, the maximal color visited infinitely often in
an infinite play of the strategy for Eve (resp. for Adam) in Edenic(G, A) is precisely the
same as the color visited infinitely often in the corresponding strategy for Eve (resp. for
Adam) in Edenicnew (G, A). As a consequence, the correspondence between Edenic(G, A)
and Edenicnew (G, A) preserves the colors of infinite plays and thus transports a winning
strategy for Eve (resp. for Adam) in Edenic(G, A) to a winning strategy for Eve (resp. for
Adam) in Edenicnew (G, A) and conversely. This completes the proof of Proposition 2.
Together with the equivalence between Adamic(G, A) and Edenic(G, A) established in
Proposition 1, this equivalence induces Theorem 4, at least for a productive recursion scheme
G. The soundness and completeness theorem follows indeed for the corresponding theorem
established by Kobayashi and Ong (Theorem 11) for the parity game Adamic(G, A). The
conceptual novelty of course of Theorem 4 is that it reveals the comonadic nature of colors
in higher-order model-checking, and a promising connection of this field with linear logic.

D

Typing terms with colored tensorial logic

The indexed and colored variant T L(Q) of tensorial logic with colors is introduced and
discussed in §4. The main logical rules of the system are formulated below in Figure 5. In
order to simplify their presentation, we choose to write
¬q (A1 , · · · , An )
for the formula of indexed tensorial logic :
¬q (A1 ⊗ · · · ⊗ An )

=

A1 ( · · · ( An ( q.

Similarly, and for the sake of uniformity, we choose to write
¬ (κ1 , · · · , κn )
for the type (or kind) of simply-typed λ-calculus:
κ1 → · · · → κn → ⊥.
Note that, for the sake of simplicity, we prefer to keep implicit the index I, J or K appearing
on the side of each sequent of the logical rules below. The reader interested in the precise
treatment of such indexes will find the detailed treatment in the work by Bucciarelli and
Ehrhard [2, 3] as well as in our companion paper [9].

24

Relational semantics of linear logic and higher-order model-checking

Axiom

Left 

Dereliction

q∈Q
x : q :: ⊥ ` x : q :: ⊥

Γ, x : A :: κ ` M : B :: κ0
Γ, x :  A :: κ ` M : B :: κ0
Γ, x : A :: κ ` M : B :: κ0
Γ, x : [A] :: κ ` M : B :: κ0

Left negation

Right negation

Γ ` M : A :: κ
m Γ ` M : m A :: κ
Γj ` M : Aj :: κ

P

Right m
(∀j ∈ J)

Γ ` M : [Aj | j ∈ J] :: κ
j∈J j

Promotion

Γ1 ` N1 : A1 :: κ1
···
Γn ` Nn : An :: κn
q∈Q
Pn
( i=1 Γi ) , f : ¬q (A1 , · · · , An ) :: ¬ (κ1 , . . . , κn ) ` f N1 · · · Nn : q :: ⊥
Γ, x1 : A1 :: κ1 , . . . , xn : An :: κn ` M : q :: ⊥
q∈Q
Γ ` λx1 · · · λxn . M : ¬q (A1 , . . . , An ) :: ¬ (κ1 , . . . , κn )

Figure 5 Extension of tensorial logic with intersection types and color modalities (main rules)

