Generalised Species of Rigid Resource Terms
Takeshi Tsukada

Kazuyuki AsadaC.-H. Luke Ong

University of Tokyo

University of Tokyo

University of Oxford

Abstract—This paper introduces a variant of the resource
calculus, the rigid resource calculus, in which a permutationof elements in a bag is distinct from but isomorphic to theoriginal bag. It is designed so that the Taylor expansion within it
coincides with the interpretation by generalised species of Fioreet al., which generalises both Joyal’s combinatorial species andGirard’s normal functors, and which can be seen as a proofrelevant extension of the relational model. As an application,
we prove the commutation between computing Böhm trees and(standard) Taylor expansions for a particular nondeterministic
calculus.

I. I NTRODUCTION
Around the same time as the birth of linear logic [20],Girard [21] proposed the normal functor semantics of the λcalculus. In this semantics, a term is interpreted as a formal
power series with set-valued coefficients, i.e., as a functor
X → Set, where the set X is the denotation of a type. Thisidea has subsequently been studied extensively, leading to newmodels of linear logic such as Köthe sequence spaces [11] andfiniteness spaces by Ehrhard [12]; and differential λ-calculus, adifferential calculus for higher-order functions by Ehrhard andRegnier [14]. In a follow-up paper [16], Ehrhard and Regnier
introduced the Taylor expansion of a λ-term as a formal sum(with rational coefficients) of terms of the resource calculus,
which may be viewed as a calculus of linear approximants ofthe λ-terms.
Meanwhile, similarities were noted between Girard’s normal
functors and Joyal’s combinatorial species [25], which arefunctors P → Set, where P is the category of finite cardinals
and bijections; Hasegawa [23], amongst others, investigatedthese connections. There is however an important difference
between the two: the domain of (the power series representation of) a normal functor is any set, by which one can interpreta type; whereas a combinatorial species uses P, which has
non-trivial (iso)morphisms. Unifying them, Fiore et al. [18,19] introduced generalised species of structures between small
categories, whose domains have enough variation to interprettypes and have non-trivial (iso)morphisms. The generalised
species of structures have been proved to form a cartesianclosed bicategory [19], by which one can interpret the λcalculus. It can be seen as a proof-relevant version of (theKleisli category of) the relational model of linear logic.
This paper investigates the connections between these linesof thought. Specifically we introduce a variant of the resource
calculus, which we call the rigid resource calculus, together
with the Taylor expansion of a term that uses this calculus,
978-1-5090-3018-7/17/$31.00

c 2017 IEEEand show that the Taylor expansion coincides with the interpretation of the term by generalised species.
This work, however, did not start as an abstract study ofthe connection. Instead we addressed other, more concrete,
problems, and the generalised species of structures seemedsuitable as a tool to solve the problems, as we shall see below.
In those problems, isomorphisms play a central rôle.
A. Compositional enumeration of reduction sequences
The first problem is related to the semantics of programming
languages with branching constructs, such as nondeterministic,
probabilistic, weighted and quantum programming languages(e.g. [8, 17, 22, 34, 39]). This is an important area of current
interest.
The operational semantics of these calculi seems to sharethe same idea. Consider, for example, a programming language with probabilistic branching. Its operational semantics
is usually defined by the following steps:
1) Define the set of all reduction sequences π : M −→∗ V
where π is the name of this sequence. A program M may
have many reduction sequences.
2) Associate to each reduction sequence π the probability(or weight) w(π), a real number between 0 and 1.
3) The probability of a program M
P being evaluated to avalue V is defined as the sum π:M −→∗ V w(π) of theweights of reduction sequences π resulting in V .
By choosing the weights and the sum appropriately, this framework applies to languages with other branching structures.
For example, for a nondeterministic program, a weight is anelement of the two-valued Boolean algebra and the sum is the
disjunction (i.e. existence of a reduction sequence). We thinkthat this framework applies also to quantum programs though
the structure of weights and the sum are more complicated.
Hence it is natural to develop a denotational model of such alanguage following the above framework, which semanticallyenumerates all reduction sequences and then calculates thesum of the weights. Indeed recent quantitative models ofprobabilistic and quantum languages [8, 17, 34] can be seen
as models of this kind. Our ultimate aim is to give a unified
account for these models.
The key process of the above framework is the enumerationof reduction sequences. For example, the following program
M := (λf.f (f z)) ((λx.x) ⊕ (λy.y))(where ⊕ is nondeterminstic branching and the underlined
expression will be referenced later) always reduces to z but infour different ways in call-by-name; indeedM −→ ((λx.x) ⊕ (λy.y)) ((λx.x) ⊕ (λy.y))z(λf1 f2 .f1 hf2 hzii) h(λx.x)L , (λy.y)R i. The reduction of thiscalculus is deterministic: we should substitute the first element
for the first variable and so on. Now a term of this calculus
represents a unique evaluation of the original program.
There is another problem, though: an evaluation of the original program has many different representations. For example,

and a choice of branch for each occurrence of ⊕ in the righthand-side determines an evaluation of the program. If thewhole program is given as above, there is no difficulty inenumerating the set of all reduction sequences. However we
aim to develop a denotational semantics, which is usually
expected to be compositional. Hence we need a way toenumerate reduction sequences compositionally.
How can we enumerate individual runs compositionally? We
call this problem the Compositional Enumeration Problem(λf1 f2 .f1 hf2 hzii) h(λx.x)L , (λx.x)L i and(λf2 f1 .f1 hf2 hzii) h(λx.x)L , (λx.x)L i

both represent the evaluation of the original program in which
we choose the left branch twice. This suggests to us that anaı̈ve use of lists cannot solve the problem.
Our approach is a hybrid between bags and lists: theconnection between elements in an argument and occurrencesof variables are tracked by lists, but terms that describe thesame connection are identified.
For example, the above terms are identified since both
represent the map given by f1 7→ (λx.x)L and f2 7→ (λx.x)L .
By writing this identification as a relation ∼, we have thefollowing more general law:

B. Key idea: Rigid resource calculus
Let us recall the above example. Observe that every reduction sequence encounters the nondeterministic branch twice,even though there is lexically one occurrence in the original
program. This is because the underlined part is duplicatedduring the evaluation. This suggests to us that a quantitative
approach of linear logic (e.g. [11, 12, 21]) may be useful.
From this observation, it is fairly natural to use the resource
calculus and the Taylor expansion [16]. The resource calculus
is basically the standard λ-calculus except that an argument
is not a term, but a finite multiset of terms, called a bag,which is linear in the sense that each element in a bag must
be used exactly once. Hence the number of elements in a bagcorresponds to the number of calls of the argument. The Taylor
expansion is a technique representing a program as a (formal)
sum of resource terms with real number (or other kinds of)coefficients. For example, the Taylor expansion of the above
program M is1

· (λf.f [f [z]]) [(λx.x)L , (λy.y)R ]

+

(1/2)

· (λf.f [f [z]]) [(λx.x)L , (λx.x)L ]

+

(1/2)

· (λf.f [f [z]]) [(λy.y)R , (λy.y)R ](1)(λx1 . . . xn .t) hu1 , . . . , un i
∼ (λxσ(1) . . . xσ(n) .t) huσ(1) , . . . , uσ(n) i.
It is not trivial to define the relation ∼: for example,(λf.f hz1 , z2 i) hλy1 y2 .ti ∼ (λf.f hz2 , z1 i) hλy2 y1 .ti(2)

since both describe the mapping y1 7→ z1 and y2 7→ z2 .
In order to correctly define ∼, we use an intersection typesystem in which a ∧ b is distinct from but isomorphic to b ∧ a.
Then a permutation σ ∈ Sn induces an isomorphism between
a1 ∧ · · · ∧ an and aσ(1) ∧ · · · ∧ aσ(n) . Key observations are that
an isomorphism acts on terms, e.g., σ maps hu1 , . . . , un i tohuσ(1) , . . . , uσ(n) i and that the desired relation ∼ can naturally
be defined by using the actions of isomorphisms, instead of
permutations. Note that an isomorphism may not merely be a
permutation; the identification in Equation (2) is induced by
an isomorphism that is not just a permutation.
The rigid resource calculus is now defined as a list-based
resource calculus, in which terms are considered modulo ∼.
Rigid resource terms enable us to describe individual runs, andenumeration is given by a variant of the Taylor expansion, therigid Taylor expansion, which is compositional.
A significant advantage of the rigid resource calculus isdeterminism of reduction. It gives us a simple way to compare
the rigid Taylor expansions of a term and its Böhm tree
(Theorem 17).

where (·)L and (·)R are the marks indicating the chosen branch(which may or may not be a part of the resource calculus).1
The underlined parts correspond to the underlined part in theoriginal program: they are bags with two elements since theunderlined part of the original program is called twice in every
possible evaluation.
Unfortunately a resource term cannot describe individual
runs. For example, the term (λf.f [f [x]]) [(λx.x)L , (λy.y)R ]reduces to (λx.x)L [(λy.y)R [z]] + (λy.y)R [(λx.x)L [z]],which is the sum of two different evaluations of M . Thisphenomenon stamps from the fact that a resource term does
not specify the connection between elements in a bag andoccurrences of a variable (so we should try all possibilities).
To overcome the problem, we consider a calculus inwhich application arguments are organised into a list (asopposed to bag) and abstraction takes a list of variables as in

C. Reasoning about coefficients of the Taylor expansion
The Taylor expansion of a term is a formal sum of (standard)
resource terms with real number coefficients. The propertiesof its support (i.e. terms with non-zero coefficients) has beenwell-studied, but reasoning about coefficients of the Taylor
expansion is rather difficult. For example, according to [35],it has been open whether the computation of the Böhm
tree commutes with the Taylor expansion in the presence of

1 Here we ignore terms evaluated to 0 such as (λf.f []) [].

2

nondeterminism; the commutation property has been provedfor deterministic (untyped) λ-calculus in [15, 16], and claimed
for System F with weighted branching in [13] (although theproof does not seem to have been published).
The notion of isomorphism appears here as well. Ehrhard
and Regnier [16] proved that, if a resource term t has non-zerocoefficient in the Taylor expansion of a λ-term M (without
nondeterministic branching), the coefficient is 1/m(t) wherem(t) is the order of the isotropy group of t.
Inspired by their observation, we express the coefficients bya groupoid of isomorphisms and its action on rigid resource
terms, in a way reminiscent of the generating series ofcombinatorial species. A resource term can be seen as an orbitof the action, and the coefficient is the ratio of the number of
elements in the orbit to the number of all isomorphims. From
this point of view, the rigid resource calculus may be seen as adeveloped form of the combinatorial concepts studied in [16].
We show that the commutation property holds for thesimply-typed nondeterministic λY-calculus, although coefficients may be infinite.

of linear logic exponentials [7], in the guise of indexedlinear logic, where it was developed in connection with therelational model. We have alluded to the isotropy group in
the coefficient computation of the Taylor expansion of λterms [16]. There are manifestations of the same idea of group
action in game semantics. A key ingredient of the AJM gamemodel [1] is a partial equivalence relation (PER) on strategies,
which enables the formulation of strategies that are “blind to
the Opponent’s thread indexing”. Melliès [31] subsequently
revealed the group-theoretic nature of this PER construction:
he introduced orbital game, which is a reformulation of HOstyle arena games [24] by replacing justification pointers bythread indexing, modulo certain left and right group actions.
Symmetry in a similar spirit can be found in a model ofquantum computation by Pagani et al. [34]. They constructa model of non-linear quantum computation from a linear
model by focusing on morphisms invariant under certain group
action.
There are a number of intersection type systems in theliterature that are non-commutative (in a variety of senses).
Thanks to Kfoury and Wells [27, 28], and Neergaard andMairson [32], and others, it is known that non-commutative,
non-idempotent intersection type systems do not enjoy subject
reduction. Our approach (and notion of rigidity) is different
from the above in a crucial way: two syntactically distinct
intersections that are equal modulo permutation are considered
distinct but isomorphic. This contrasts with, for example, System I [32] which, being “completely” rigid2 , is thus unsoundwith respect to the reduction.
First observed by Kfoury [28], the fruitful relationshipbetween (non-idempotent) intersection types and linearity has
been a recurrent theme in recent years (see e.g. de Carvalho[10], and Bernadet and Lengrand [5]). Building on this is
the idea that intersection type derivations of a λ-term areformally representable by approximants of the term. For
example, Ong and Tsukada [33] presented just such a bijective
correspondence in a non-linear setting. Our rigid resource
calculus may be viewed as a refinement of Mazza’s calculusof approximants3 [30], the derivations of which correspondbijectively to reduction sequences. Another related system isthe type system by Ehrhard et al. [17] for calculating theinterpretation in the probabilistic coherence space model [8].
Following Kfoury [28], many of the above studies use
subject reduction and subject expansion to establish a strong
connection between reductions of a given term and intersection
type derivations (or approximants) of that term. Our approachgives a refinement: we show that the witnessing type of the
reduction (respectively expansion) of a term can always bechosen from among the isomorphic types of the term. This
relates to the phenomenon that, in the AJM game model, theD. Contribution of this paper
The contributions of the paper are as follows.
• Proposal of the rigid resource calculus and the rigid
Taylor expansion. The rigid Taylor expansion is proved tobe sound with respect to Böhm theory, and adequate withrespect to the standard operational semantics. It is also asolution to the Compositional Enumeration Problem.
• Proof of the coincidence of the rigid Taylor expansion ofa term and the interpretation of the term by generalised
species of structures [18, 19]. By this result, we obtain
two different descriptions of the same mathematical object, one is concrete and syntactic and the other is abstract
and categorical.
• Study of the relationship between the rigid and standard
resource calculi. This leads us to a proof of the commutation of normalisation and the standard Taylor expansion
for the simply-typed nondeterministic λY-calculus.
To accomplish the program described in Section I-A, weneed to introduce the notion of weights to generalised speciesof structures. The study of weighted generalised species andthe construction of a model based on it are left for future work(see also Section VII).
E. Related work
In the preamble, we discussed the main ideas that havemotivated our paper. Here we comment on works in theliterature relevant to a number of other key themes.
The computational enumeration problem introduced in thepreceding is concerned with the analysis of reduction sequences of λ-calculus with branching constructs using quantitative semantics. Versions of this problem have been studied
by Danos and Ehrhard [8], and Laird et al. [29], among others.
The notion of symmetry is central to our work. The idea ofconsidering intersection types up to isomorphism was alreadypresent in Bucciarelli and Ehrhard’s work on the semantics

2 Neergaard and Mairson [32] call an intersection operator, ∧, rigid if
idempotency, commutativity nor associativity does not hold.
3 Mazza’s intersection type system is not non-commutative in the senseof Kfoury and others [28, 32]. It follows from the only constraint in his
system—each assumption be used exactly once—that the order of types(and assumptions) is insignificant. Consequently one can implicitly apply theexchange rule to the assumptions.

3

interpretation of a term as a strategy is not preserved by βreduction, but the equivalence class of strategies is.
Our rigid Taylor expansion semantics of the nondeterministic λY-calculus is closely related to two recent categoricalpresentations of the HO/N game model. Tsukada and Asada[37] gave a profunctorial reformulation of HO/N games inwhich plays are graphs: they constructed a pseudofunctor fromthe category of HO/N games to the bicategory of profunctors.
In [39] Tsukada and Ong developed a fully abstract innocent
game model for the simply-typed nondeterministic λ-calculus.
Mathematically a strategy is formalised as a sheaf over anappropriate site of plays. The precise relationships between
the generalised species model and each of the above reformulations of the game model will be developed elsewhere. In adifferent operational direction, Allioux [2] has recently given
an account of the Taylor expansion of algebraic λ-terms basedon a kind of resource-constrained Krivine machine.
Notation: We define [n] := {1, 2, . . . , n} for a natural
number n (so [n] is a set with n elements and [0] is empty).

B. Evaluation
The calculus is call-by-name. The syntax of evaluation
contexts is given by: E ::= [] | E M . The one-step evaluation
relation is given by the following rules:L

E[M1 ⊕ M2 ] ,→1 E[M1 ]0E[(λx.M ) N ] ,→1 E[{N/x}M ]R

E[M1 ⊕ M2 ] ,→1 E[M2 ]E[Y M ] ,→1 E[M (Y M )]where  is the empty sequence. For a sequence π ∈π{ L, 0, R }∗ , we write M ,→ M 0 if there exists an evaluation
d1

d2

dn

sequence M = M0 ,→1 M1 ,→1 · · · ,→1 Mn = M 0 and
π = d1 d2 . . . dn (where n ≥ 0). The length of π is the numberof β- and ⊕-rules in the sequence; evaluation of Y is notπrecorded in π. Evaluation preserves η-longness: if M ,→ M 0
and M is η-long, then M 0 is also η-long.
C. Compositional Enumeration Problem
Sections III and IV address the following problem.
Problem. Give a compositional semantics of the λnd Ycalculus such that the interpretation of a term x1 : o, . . . , xn :o ` M : o can be seen as the set of all its evaluation sequences.

II. P ROBLEM S ETTING
This section defines a problem addressed in (the first partof) this paper. The problem is compositional enumeration of
all possible evaluations of a given nondeterministic term of acertain type. We choose the simplest calculus to illustrate theideas of our approach; and we claim that our idea is applicableto PCF and the (untyped) λ-calculus, for example.
Further, the problem is a guide, which serves to justify andexplain the design of the syntactic development in Sections III
and IV, from which generalised species naturally arise.

Here the set of evaluation sequences means something likeπ
{ (π, xi ) | M ,→ xi }, although it is not necessarily exactly
the same. A satisfactory information on the set depends on
the purpose. For example, if we aim to model a language withprobabilistic binary branching which chooses each branch withprobability 1/2, the number of L and R in π is important butthat of 0 is not. For another example, if the language has aweighted branching (α M ) ⊕ (β N ) where weights α and β
are taken from a given ring, we need additional informationof weights for each L and R symbols.
We would like to emphasise that solving the above problem
is not the ultimate goal of our development. We are looking fora good way to solve the problem, which would be applicable toother settings, which would be useful in proving an interesting
result, and which would provide us with new insights. The
solution presented in Sections III and IV is justified by a strong
semantics background studied in Section V.

A. The target language: Nondeterministic λY-calculus
The target language is the λnd Y-calculus, the simply-typed
λY-calculus with nondeterministic branching. The syntax ofsimple types is A, B ::= o | A → B where o is the unique
atomic type. The syntax of terms is given by the following
grammar:M, N := x | λxA .M | M M | YA M | M ⊕A M.
Here YA is the fixed-point operator of type (A → A) → A
and M ⊕A N is the nondeterministic branching where M and
N are terms of type A. We identify α-equivalent terms. Typeannotations are often omitted.
A simple type environment Γ is a finite sequence of typebindings of the form x : A. The typing rules are fairly
straightforward.
A term M is η-long if every application in M is fullyapplied and every variable as well as Y occur with its
arguments. Formally it is defined by the following grammar:

D. Full reduction and Böhm tree
Directly reasoning about the set of evaluation sequences isa bit messy. This subsection introduces another operationalsemantics, in which the set of all evaluation sequences in theprevious subsection are put into the result (i.e. its Böhm tree).
The (full) reduction relation has the form M −→ M 0 . It isdefined by the following base cases(λx.M ) N −→ {N/x}M

R ::= λx1 .λx2 . . . . λxn .Q | R ⊕ R0

Y M −→ M (Y M )Q ::= x R1 . . . Rn | R0 R1 . . . Rn | Y R1 . . . Rn | Q ⊕ Q(M1 ⊕ M2 ) N −→ (M1 N ) ⊕ (M2 N )where n ≥ 0 and the type of Q must be o. Every term can betransformed into an η-long form in the obvious way. Hence we
can assume without loss of generality that a term is in η-longform. This assumption simplifies the statements of lemmas andtheorems, and will be used often (but always explicitly).

and the context rule: M −→ M 0 implies C[M ] −→ C[M 0 ]for every context C. Notice that, unlike the evaluation relation,no branch of a nondeterministic choice is discarded.
We write −→∗ for the reflexive and transitive closure of−→. The standard technique shows that −→∗ is confluent.

0

4

Basically the “normal form” of the reduction relation contains information on all evaluations. Since both the length of
the reduction sequence as well as the size of the resulting“term” can be infinite, we need an auxiliary definition toformalise this idea.
The finite canonical form is defined by the following syntax:
S ::= λx1 .λx2 . . . . λxn .T

but isomorphic. In other words, while we do not allow implicit
use of commutation, we allow explicit commutation.
Remark 3. The indexed syntax of rigid intersection types isreminiscent of the indexed linear logic of Bucciarelli andEhrhard [7]. The development in Sections III and IV can beseen as a proof-relevant variant of [7], although there is adifference even in the proof-irrelevant setting. For example,
indices of rigid intersection types do not affect provability ofa judgement. A detailed comparison is left for future work.

T ::= ⊥ | T ⊕ T 0 | x S1 . . . Sn

where the type of T must be o. It is basically an η-long termin β-normal form except for the additional constant ⊥ for thediverging term of type o. We write FCF for the set of finite
canonical forms. The set of finite canonical forms (of a giventype) forms a poset with the least element λx1 . . . . λxn .⊥ andthe order v defined as the least partial order such that C[⊥] v
C[T ] for every context C and term T with C[T ] ∈ FCF.
One can compare a λnd Y-term with a finite canonicalform in a similar way because the constructors of finite
canonical forms (except for ⊥) can be regarded as those of thecalculus. We write T C M for the relation consisting of pairsC[⊥, . . . , ⊥] C C[M1 , . . . , Mn ] for every multi-hole context
C and terms M1 , . . . , Mn such that C[⊥, . . . , ⊥] ∈ FCF andC[M1 , . . . , Mn ] is a λnd Y-term.
A Böhm tree is an order ideal4 of finite canonical forms
with respect to v. Given a λnd Y-term M in η-long form, itsBöhm tree BT (M ) is defined by

A. Rigid refinement intersection types
The rigid intersection types are basically the same as
the standard nonidempotent intersection types except that anintersection is no longer a finite multiset of types but a finite
sequence. We write ha1 , . . . , an i for a sequence. Then thesyntax is given by:a, b ::= ? | θ ( bwhere n ≥ 0. The sequence ha1 , . . . , an i is also written as
hai ii∈[n] , or simply as h~ai if the length is unimportant. The
sequence ha1 , . . . , an i means the intersection type a1 ∧· · ·∧an .
The refinement relation a C A is defined by:?Co

There is, of course, a tight relationship between the evaluation and reduction. Let ¯· : { L, R, 0 }∗ → { L, R }∗ be themap that erases 0. For π̄ ∈ { L, R }∗ , we define Cπ̄ byCLπ̄ := Cπ̄ ⊕ ⊥θ C !A b C B
θ (bCA→B∀i ∈ [n]. ai C A
hai ii∈[n] C !A

Here A → B is identified with !A ( B, where ! and ( arethe exponential modality and linear implication of linear logic.
We write JAK := {a | aCA} for the set of all refinement typesof the simple type A.

BT (M ) := {T ∈ FCF | ∃M 0 . M −→∗ M 0 B T }.

C := []

θ ::= ha1 , . . . , an i

B. Type isomorphisms

and CRπ̄ := ⊥ ⊕ Cπ̄ .

Although the type ha, bi is not identical to hb, ai, they areclearly closely related. Relating these types is also motivatedby an observation that a non-commutative intersection typesystem does not enjoy subject reduction [27, Remark 2.9].5
We consider these types isomorphic.
Let a1 and a2 be rigid intersection types (not necessarily
refinements of simple types). We write ϕ : a1 ∼= a2 to meanthat a1 and a2 are isomorphic, of which ϕ is a witness (or aproof ). This relation is defined by the rules below:ψ : θ0 ∼
ϕ: b∼
=θ
= b0
∼
∼
id? : ? = ?
(ψ ( ϕ) : (θ ( b) = (θ0 ( b0 )Proposition 1. For every x1 : o, . . . , xn : o ` M : o in ηπlong form, the map ¯· is a bijection from { π | M ,→ xi } to{ π̄ | Cπ̄ [xi ] ∈ BT (M ) } for every i ∈ [n].
Remark 2. Proposition 1 together with certain properties on
BT (·) shows that the Böhm tree interpretation can be asolution to the problem in Section II-C. This is, however,unsatisfactory for us. For example, this solution is quite
syntactic rather than semantic and ⊕ in this solution is neither
commutative nor associative. Recall that to solve the problem
in Section II-C is not our ultimate goal, rather we aim to
use the problem as a guide of our development that provides
us with a syntactic description of the generalised species ofstructures [18, 19].

∀i ∈ [n]. ϕi : ai ∼= a0σ(i)(σ, hϕi ii∈[n] ) : hai ii∈[n] ∼= ha0i ii∈[n]σ ∈ SnThis section introduces types with non-idempotent andnon-commutative intersection which we call rigid refinement
intersection types (cf. [32]). The key difference from theexisting work on non-commutative intersection types (such as[28, 30, 32]) is that we consider the types a∧b and b∧a distinct

Here id? is a constant witnessing that the type ? is (obviously)isomorphic to ?. The rules are fairly straightforward; we note
contravariance of the position of θ in θ ( b.
As expected, type isomorphism is an equivalence relation.
Reflexivitiy is witnessed by ida and idθ defined by idθ(b :=idθ ( idb and idhai ii∈[n] := (id[n] , hidai ii∈[n] ). Transitivity
is witnessed by the composition operation ◦A such that ϕ1 :4 Given a poset (P, ≤), an order ideal is a subset X ⊆ P that is downward
closed (i.e. x ≤ y and y ∈ X implies x ∈ X) and directed (i.e., for every
x, y ∈ X, there exists z ∈ X such that x ≤ z and y ≤ z).

5 Although the remark in [27] is about system I, in which ∧ is noncommutative and non-associative, it directly applies to an intersection typesystem with non-commutative but associative ∧.

III. G ROUPOID OF R IGID R EFINEMENT T YPES

5

a1 ∼
= a3 , which= a3 implies (ϕ2 ◦ ϕ1 ) : a1 ∼= a2 and ϕ2 : a2 ∼can be defined by id? ◦o id? := id? and

IV. R IGID R ESOURCE C ALCULUS
This section introduces the rigid resource calculus, bywhich one can describe individual runs of a term. It is a variantof the resource calculus in the sense of [16], a variant whichuses lists instead of bags. The key notion is the equivalence
relation ∼ on terms, which identifies terms describing the samerun, where the groupoid structure of refinement types plays animportant rôle.

(ψ2 ( ϕ2 ) ◦ (ψ1 ( ϕ1 ) := (ψ1 ◦ ψ2 ) ( (ϕ2 ◦ ϕ1 )(σ2 , hϕ2j ij ) ◦ (σ1 , hϕ1i ii ) := (σ2 σ1 , hϕ2σ1 (i) ◦ ϕ1i ii )where we omit the ranges of i and j which must be thesame. Symmetry is proved by the inverse operation (·)−1defining by id−1:= id? , (ψ ( ϕ)−1 := ψ −1 ( ϕ−1 and?
−1∼(σ, hϕi ii∈[n] ) := (σ −1 , hϕ−1
σ −1 (j) ij∈[n] ). Then ϕ : a1 = a2
−1
−1
−1
∼
implies ϕ : a2 = a1 and ϕ ◦ ϕ = ϕ ◦ ϕ = id.
By these data, the refinement types of a simple type A
form a groupoid (i.e. a category in which every morphism isinvertible), whose objects are rigid refinement types aCA andmorphisms from a to b are type isomorphisms ϕ : a ∼= b. We
write this groupoid as JAK. The groupoid J!AK whose objectis θ C !A is defined in the same way.
We abbreviate (σ, hidai ii ) to σ and (id, hϕi ii ) to hϕi ii .

A. Rigid resource raw terms
Rigid resource raw terms are defined by:t, u := x | λ~x.t | t µ | t ⊕ • | • ⊕ t(formally each variable is annotated by a rigid intersection
type, which is omitted above). Here • is a place holder for theunused part of branching and ~x is a (possibly empty) sequenceof variables. Rigid resource terms appearing in the sequel arealways linear, i.e. each variable appears exactly once.
A rigid resource term shall be used to describe a reduction
sequence of a λnd Y-term.6 For example, t ⊕ • means thatthe left-branch should be chosen here; since the right branch
is irrelevant in this case, a rigid resource raw term simply
ignores it.
A rigid type environment Ξ is a finite sequence of typebindings of the form x : a. We stipulate that a rigid typeenvironment contains each variable at most once. We write
Ξ1 , Ξ2 for the concatenation. For sequences ~x = x1 , . . . , xn
and ~a = a1 , . . . , an , we write ~x : ~a for x1 : a1 , . . . , xn : an .
A type judgement is of the form Ξ ` t : a or Ξ ` µ : h~ai.
The typing rules are listed in Fig. 1. It is worth noting that theorder of type bindings in a type environment does not affectthe derivability of a judgement by the exchange rule. This rulecan be seen as a weaker version of type-isomorphism rules;
the relationship to general rules is the topic of Section IV-D.
In the sequel, we shall consider only typed rigid resource
terms, i.e. rigid resource terms associated with derivable typing
judgements Ξ ` t : a (or Ξ ` µ : θ). The notion of η-longforms is defined in a similar way to the λnd Y-calculus . The
associated judgements are often left implicit.
We can give an evaluation relation for rigid resource raw
terms. Evaluation contexts are given by: E ::= [] | E µ.

C. Categorical definition
The groupoid JAK of rigid refinement intersection types
and isomorphisms has a simple categorical definition. Thisis, indeed, the interpretation of simple types by generalised
species of structures [18, 19].
We start from an auxiliary definition. Let C be a small
category. We define a category P C as follows. An objectof P C is a (possibly empty) finite sequence hCi ii∈[n] ofobjects in C. A morphism from hCi ii∈[n] to hDi ii∈[m] is atuple (σ, hfi ii∈[n] ) where σ : [n] → [m] is a bijection andfi : Ci → Dσ(i) is a morphism in C (for all i ∈ [n]). Notethat there is no morphism if n 6= m. Composition is given by(σ2 , hgj ij∈[n] ) ◦ (σ1 , hfi ii∈[n] ) := (σ2 ◦ σ1 , hgσ1 (i) ◦ fi ii∈[n] ).
The groupoids JAK are given by induction on the structureof simple types A. For the base case, JoK is the set {?}, i.e. acategory with a single object ? and no morphism other than
the identity. For the inductive steps, we have
JA → BK = J!AKop × JBKµ := hu1 , . . . , un i

J!AK = P JAK.

This resembles the interpretation of types in the relationalmodel: we just replace a set with a groupoid and the finite
multiset comonad with P.

LR

E[t ⊕ •] ,→ E[t]E[• ⊕ t] ,→ E[t]0

E[(λ~x.s) hu1 , . . . , un i] ,→ E[{u1 /x1 , . . . , un /xn }s].
D. Isomorphisms of type environmentsπ

As before, we write s ,→ s0 if there exists a sequence s =d1d2dns0 ,→ s1 ,→ · · · ,→ sn = s0 and π = d1 d2 . . . dn (where n ≥0). Evaluation of a rigid resource raw term is deterministic.
We give a (full) reduction semantics for rigid resource terms.
It is defined by the base cases

A type environment is a sequence of type bindings of theform x : a (such that a is a refinement of the simple typeof x). Here a variable can appear many times in a sequence.
The refinement relation and the isomorphisms can be naturally
extended to intersection type environments:(λx1 . . . xn .t) hu1 , . . . , un i −→ {u1 /x1 , . . . , un /xn }t∀(x : a) ∈ Θ. ∃(x : A) ∈ Γ. a C A
ΘCΓ(t ⊕ •) µ −→ (t µ) ⊕ •σ ∈ Sn∀i ∈ [n]. xi = yσ(i) and ϕi : ai ∼= bσ(i).
(σ, hϕi ii∈[n] ) : (x1 : a1 , . . . , xn : an ) ∼=Γ (y1 : b1 , . . . , yn : bn )(• ⊕ t) µ −→ • ⊕ (t µ).

6 Here is another point of view: each term constructor corresponds to atyping rule of an intersection type system. See also Remarks 8 and 13.

6x:a`x:aΞ`t:aΞ`t⊕•:aΞ, x1 : a1 , . . . , xn : an ` t : bΞ ` λx1 . . . xn .t : ha1 , . . . , an i ( bΞ`t:aΞ`•⊕t:aΞ1 ` t : θ ( bΞ2 ` µ : θΞ1 , Ξ2 ` t µ : b∀i ∈ [n]. Ξi ` ui : ai
Ξ1 , . . . , Ξn ` hui ii∈[n] : hai ii∈[n]x1 : a1 , . . . , xn : an ` t : b
σ ∈ Snxσ(1) : aσ(1) , . . . , xσ(n) : aσ(n) ` t : b

Fig. 1. The typing rules for rigid resource terms (Environment permutation for lists µ is omitted.)

The reduction relation is strongly normalising because of thelinearity of rigid resource raw terms. We write nf(t) for thenormal form of t. Furthermore it is confluent since there isno critical pair. Unlike the standard resource calculus, thereduction relation is deterministic (or, reduction does not
introduce formal sums).

Remark 8. Corollaries 5 and 7 suggest existence of a soundand complete intersection type system defined as follows. A
judgement of the type system is of the form x1 : a1 , . . . , xn :an ` M : b (where xi and xj can be the same even wheni 6= j). This judgement is derivable if there exists t such thaty1 : a1 , . . . , yn : an ` t : b and y1 C x1 , . . . , yn C xn ` t C M .
This “type system” is sound and complete by Corollaries 5 and7. Indeed it is the type system corresponding to the relationalmodel of linear logic (see, e.g., [10]). From this point of view,a rigid resource term is a representation of a derivation of anintersection type system.

B. Rigid term approximation of λnd Y-terms
A variable refinement X is a sequence of the form x1 C
y1 , . . . , xn C yn such that xi 6= xj if i 6= j. The variables
x1 , . . . , xn are those of rigid resource terms and y1 , . . . , yn arethose of the λnd Y-calculus. For sequences ~x and ~y of variablesof the same length, ~x C~y denotes the variable refinement x1 C
y1 , . . . , xn C yn . Let rng(X) := {y | (x C y) ∈ X}.
An approximation judgement has the form X ` t C M , andvalid judgements are defined by the rules in Fig. 2.

D. Action of type isomorphisms
The goal of this subsection is to avoid the redundancy
described at the end of the previous subsection. The idea
is to introduce an equivalence relation ∼ relating terms that
represent the same evaluation.
Basically redundancy arises from application of the same
permutation to both the variable list and the argument list. For
example, the term

C. Representation of reduction sequences
A rigid raw term t C M gives an evaluation of M . The
only nontrivial case is M = E[N1 ⊕ N2 ] as other cases are
deterministic. Then t C M implies t = E 0 [u ⊕ •] or E 0 [• ⊕ u];
we choose the left-branch for the former case and the rightbranch for the latter.
πt := (λx1 . . . xn .t) hu1 , . . . , un irepresents the same evaluation ast0 := (λxσ(1) . . . xσ(n) .t) huσ(1) , . . . , uσ(n) i.

πLemma 4. Assume X ` t C M . If t ,→ t0 , then M ,→ M 0
and X ` t0 C M 0 for some M 0 .

A difficulty comes from the fact that the corresponding
variable and argument lists are not necessarily syntacticallyadjacent. Consider, for example,

Corollary 5. Let x1 : o, . . . , xn : o ` M : o. If y Cxi ` tCM
and y : ? ` t : ?, then t represents a unique evaluationππsequence of M ,→ xi , i.e., t ,→ y.

(λf.f hz1 , z2 i) hλy1 y2 .ti

Furthermore every evaluation of a λnd Y-term has a representation by a rigid resource term.
πand(λf.f hz2 , z1 i) hλy2 y1 .tithat are reduced to, respectively,(λy1 y2 .t) hz1 , z2 iπLemma 6. Assume X ` t0 C M 0 . If M ,→ M 0 , then t ,→ t0
and X ` t C M for some t.

and(λy2 y1 .t) hz2 , z1 i.

To correctly handle such a complex case, we use typeisomorphisms and their action on rigid resource terms.
We do not have the type isomorphism rule in the above
type system. For example, Θ ` ht1 , . . . , tn i : ha1 , . . . , an idoes not imply Θ ` ht1 , . . . , tn i : haσ(1) , . . . , aσ(n) i, although
σ : ha1 , . . . , an i ∼= haσ(1) , . . . , aσ(n) i.
However, applying the same permutation σ to the list ofterms gives a valid judgement. For example, in the above case,
we have Θ ` htσ(1) , . . . , tσ(n) i : haσ(1) , . . . , aσ(n) i.
By generalising this idea, it is natural to expect that, given arigid resource term Ξ ` t : a and a type isomorphism ϕ : a0 ∼=a, we obtain another rigid resource term t0 by “applying” ϕand we have Ξ ` t0 : a0 . Indeed it is the case provided that theterm is η-long. We write such t0 as t[ϕ] and call the operation(−)[ϕ] the (right) action of ϕ.

πCorollary 7. Let x1 : o, . . . , xn : o ` M : o and M ,→ xi .
There exists t such that y C xi ` t C M , xi : ? ` t : ? andπt ,→ y.
However there is a problem as mentioned around (1) inπSection I-B: some evaluation M ,→ xi has more than one
rigid resource raw term representation. For example, consider
M = (λf.f (f z)) ((λx.x) ⊕ (λy.y))t1 = (λf1 f2 .f1 hf2 hzii) h((λx.x) ⊕ •), (• ⊕ (λy.y))it2 = (λf2 f1 .f1 hf2 hzii) h(• ⊕ (λy.y)), ((λx.x) ⊕ •)i.
0L0R0

Then both t1 and t2 represent M ,−−−−→ z.

7xCy `xCy

X, x1 C y, . . . , xn C y ` t C My∈/ rng(X)X ` (λx1 . . . xn .t) C (λy.M )X1 ` t C M
X2 ` µ C (Y M )X1 , X2 ` (t µ) C (Y M )X ` t C M1
X ` (t ⊕ •) C (M1 ⊕ M2 )∀i ∈ [n]. Xi ` ti C M
X1 , . . . , Xn ` hti ii∈[n] C M

X1 ` t C M
X2 ` µ C N
X1 , X2 ` (t µ) C M N
X ` t C M2
X ` (• ⊕ t) C (M1 ⊕ M2 )x1 C y1 , . . . , xn C yn ` t C M
σ ∈ Snxσ(1) C yσ(1) , . . . , xσ(n) C yσ(n) ` t C M

Fig. 2. Rigid approximation relation (Permutation of variable refinements for lists is omitted.)

The action (−)[ϕ] of an isomorphism to terms is definedby the rules in Fig. 3. It is defined by mutual induction with{[ϕ]/x}(−), which describes the action of the isomorphism ϕ
to environments. We have the following derived rules:Ξ, x : b ` t : a
ϕ:b∼
Ξ`t:a
ϕ : a0 ∼
= b0
=a
.
0
0
Ξ ` t[ϕ] : a
Ξ, x : b ` {[ϕ]/x}t : a

From this point of view, a rigid resource term (i.e. an equivalence class modulo ∼) is an equivalence class of derivations
modulo natural commutations such as∆, x : ~a ` M : b∆ ` λx.M : h~ai ( b (id ( ϕ) : (h~ai ( b0 ) ∼= (h~ai ( b)∆ ` λx.M : h~ai ( b0

Example 9. Let σ = (1 2) ∈ S2 and a := h?, ?i ( ?.
Then (σ ( id) : a ∼= a. Let ϕ be this isomorphismand Θ ` λy2 y1 .u0 : a be a rigid resource raw term inη-long form. Let u := λy2 y1 .u0 . By applying ϕ to u,
we obtain u[ϕ] = λy1 y2 .u0 . Consider another isomorphism(hϕi ( id) : (hai ( ?) ∼= (hai ( ?). Consider z1 : ?, z2 :? ` λf.f hz1 , z2 i : hai ( ?, which we write as t. By applying(hϕi ( id) to t, we obtain t[hϕi ( id] = λf.f hz2 , z1 i.

←→∆, x : ~a ` M : b
ϕ : b0 ∼=b∆, x : ~a ` M : b0
∆ ` λx.M : h~ai ( b0.

The notions and operations defined for rigid resource terms
are well-defined for the equivalence classes et. For example,Ξ ` t : a and t ∼ t0 implies Ξ ` t0 : a, and
π 0
π 0
0
0
• t1 ∼ t2 and t1 ,→ t1 implies t2 ,→ t2 with t1 ∼ t2 .

•We have the following result as expected.

Lemma 10. For every term t in η-long form, we have

Theorem 14. Let x1 : o, . . . , xn : o ` M : o and assumeπ
M ,→ xi for some i. Then there exists t unique up to ∼ suchπthat y C xi ` t C M and t ,→ y.

{[ϕi ]/xi }i (t[ψ]) = ({[ϕi ]/xi }i t)[ψ](t[ψ1 ])[ψ2 ] = t[ψ1 ◦ ψ2 ]1{[ϕi ]/xi }i ({[ϕ2i ]/xi }i t) = {[ϕ1i ◦ ϕ2i ]/xi }i tprovided the type isomorphisms are of the appropriate types.

E. Rigid Taylor expansion

Remark 11. A type isomorphism ϕ : a ∼=A a0 induces a rigid
resource term, which we write as ` [ϕ] : a0 → a by abuse ofnotation, such that ` [ϕ] C ηA (λy.y) where ηA (λy.y) is theη-long form of λy.y. The action of a type isomorphism ϕto Θ ` t : a0 can be seen as the application of the term [ϕ] tot, followed by the reduction of redex related to [ϕ].
Now we define ∼ as the least congruence that satisfies

Let us fix an infinite sequence z1 , z2 , . . . , zn , . . . of distinct
variables. We write ~z for a prefix of this sequence.
Definition 15. Let Γ ` M : A be a λnd Y-term in η-longform. Define, for ∆ = (~z : ~b) C Γ and a C A,
JM K(∆, a) := {et | ~z C ~x ` t C M and ~z : ~b ` t : a}We call JM K the rigid Taylor expansion of M . We write (∆ `et : a) ∈ JM K to mean et ∈ JM K(∆, a).

t0 (µ1 [ϕ1 ]) . . . (µn [ϕn ])∼ (t0 [ϕ1 ( · · · ( ϕn ( id]) µ1 . . . µn

Theorem 14 shows that the rigid Taylor expansion JM K canbe seen as an enumeration of evaluation sequences, which canbe defined by induction on M and is thus compositional. This
aspect is further studied in the next section.
Recall the groupoid JAK of refinement types and isomorphims, defined in Section III-C. By the action of an isomorphism on a rigid resource term, the rigid Taylor expansion
becomes a functor.

for every η-long rigid resource terms t0 , µ1 , . . . , µn and typeisomorphisms ϕ1 , . . . , ϕn of appropriate types. We write et for
the equivalence class of ∼ to which t belongs.
Example 12. Let ϕ and a be those defined in Example 9.
We have (λf.f hz1 , z2 i) hλy1 y2 .ti ∼ (λf.f hz2 , z1 i) hλy2 y1 .ti
from(λf.f hz1 , z2 i) hλy1 y2 .ti = (λf.f hz1 , z2 i) (hλy2 y1 .ti[ϕ])Theorem 16. Let Γ ` M : A be a λnd Y-term in η-long form.
(λf.f hz2 , z1 i) hλy2 y1 .ti = ((λf.f hz1 , z2 i)[ϕ ( id]) hλy2 y1 .ti. Then JM K is a functor PJΓK × JAKop → Set.
The rigid Taylor expansion is sound with respect to theBöhm theory. Let Γ ` T : A be a Böhm tree (i.e. an order

Remark 13. Recall that a rigid resource raw-term can be seen
as a derivation of an intersection type system (Remark 8).

8hti ii∈[n] [σ] := htσ(j) ij∈[n](λx1 . . . xn .t)[id ( ϕ] := λx1 . . . xn .(t[ϕ])hti ii∈[n] [hϕi ii∈[n] ] := hti [ϕi ]ii∈[n](λx1 . . . xn .t)[σ ( id] := λxσ−1 (1) . . . xσ−1 (n) .t{[ψ]/x}(x µ1 . . . µn ) := x (µ1 [ϕ1 ]) . . . (µn [ϕn ])(λx1 . . . xn .t)[hϕi ii∈[n] ( id] := λx1 . . . xn .({[ϕi ]/xi }i∈[n] t)(t ⊕ •)[ϕ] := (t[ϕ]) ⊕ •(• ⊕ t)[ϕ] := • ⊕ (t[ϕ])(where ψ = ϕ1 ( . . . ( ϕn ( id? )Fig. 3. Action of isomorphisms on rigid raw terms. Other isomorphims are decomposed into the above ones. The definition of {[ϕ]/x}(−) is the same as
the standard substitution except for the above case.

ideal of the finite canonical forms Γ ` T : A). We define JT K
by, given ∆ = (~z : ~b) C Γ and a C A,

B. Generalised species of structures
Given small categories A and B, a (A, B)-species of structures [18, 19] is defined as a functor PA × B op → Set, i.e. a
profunctor PA →−7 B.
There is a bicategory whose 0-cell is a small category
and whose 1-cell is an (A, B)-species. The identity species
IA : PA →−7 A is defined by IA (θ, a) := PA(hai, θ). The
composition of (A, B)-species of structures f and (B, C)species of structures g is defined as follows. Given (A, B)−7 PB
species of the structures f : PA →−7 B, its lifting f ] : PA →is defined by the following coend:

JT K(∆, a) := {et | ~z : ~b ` t : a and ∃T ∈ T . ~z C ~x ` t C T }.
Theorem 17. The family of functions
JM K(Θ, a) → JBT(M )K(Θ, a) : e
t 7→ nf(et)
defines a natural isomorphism JM K ∼= JBT(M )K. Thus therigid Taylor expansion J−K is sound with respect to the Böhmtheory.

f ] (θ, hb1 , . . . , bk i)
Z (θi )i∈k ∈(PA)k  Y:=f (θi , bi ) × PA(θ1 · · · θk , θ)

V. G ENERALISED S PECIES OF S TRUCTURES
This section shows that the rigid Taylor expansion of a
λnd Y-term is equivalent to its interpretation in the bicategory ESP (for espèces de structures [25, 26]) of generalised
species of structures by Fiore et al. [19], which is a proofrelevant extension of the relational model Rel! . We first review
the generalised species of structures and its cartesian closed
structure and then compare it with the rigid Taylor expansion.

i∈[k]where θ1 · · · θk is the concatenation of lists. Then g ◦ f isdefined as the composition gf ] as profunctors. The 2-cells arenatural transformations. We write this bicategory as ESP.
Remark 18. Fiore et al. [19] showed that ESP can be seenas the coKleisli bicategory of a pseudo-comonad P on the
bicategory Prof of profunctors; the action of P to 0-cells is
the same as P. There is a formal similarity to the constructionof the relational model Rel! , which is the coKleisli categoryof the finite multiset comonad !.

A. Profunctor
We introduce the bicategory Prof of profunctors (or distributors; see e.g. [3, 4] and [6, § 7.7]), which can be regarded
as a proof-relevant extension of the category Rel of sets andrelations.
Given small categories A and B, a profunctor from A to
B is a functor f : A × B op → Set. This is an extension ofrelations: a relation R ⊆ Y × Z can be seen as a profunctorfR between sets (i.e. categories with no morphism except for
the identities) such that fR (y, z) is either singleton or empty
depending on whether (y, z) ∈ R. We write f : A →−7 B if f
is a profunctor from A to B.
Let f : A −→7 B and g : B →−7 C be profunctors. A
morphism ϕ : b → b0 in B acts on elements in f (a, b0 ) by
y 7→ f (a, ϕ)(y) ∈ f (a, b) and in g(b, c) by z 7→ g(ϕ, c)(z) ∈g(b0 , c), which we write y[ϕ] and {ϕ}z, respectively. The
composite gf is defined bya(gf )(a, c) :=(f (a, b) × g(b, c))/∼(3)

C. Cartesian closed structure
The bicategory ESP is cartesian closed [19].
d Given small categories Ai (i ∈ [n]),` the cartesian product
A
in
ESP
is
the
coproductii∈[n]i∈[n] Ai as categories.
d
For an object a ∈ Ai , the corresponding object of j∈[n] Aj
is written as ιi (a). For→
7 Ai (i ∈ [n]), the tuplingd gi : PB −hg1 , . . . , gn i : PB −→7
Aisdefined byii∈[n]hg1 , . . . , gn i(b, ιi (a)) := gi (b, a).
d
The projection πi : P( j∈[n] Aj ) →−7 Ai is given by(
Ai (a, a0 ) if u = hιi (a0 )i
πi (u, a) :=∅otherwise.
Given small categories B and C, we define C B := PB op ×C.
Given g : P(A u B) →−7 C, we define ΛB (g) : PA →−7 C B byb∈BΛB (g)(ha1 , . . . , an i, (hb1 , . . . , bm i, c))where ∼ is the least equivalence relation that contains(y, {ϕ}z) ∼ (y[ϕ], z) for every morphism ϕ in B.

:= g(hι1 (a1 ), . . . , ι1 (an ), ι2 (b1 ), . . . , ι2 (bm )i, c).

9The evaluation map evalB,C : P(C B u B) →−7 C is defined by((PB op × C)((u2 , c), d0 ) if u1 = hd0 i
evalB,C (u, c) :=∅otherwise

A. Preliminary: The resource calculus and Taylor expansions
The syntax of simple terms and simple bags is given by:v, w ::= x | λx.v | v ξ

where, for u ∈ P(A1 u A2 ), ui ∈ PAi (i = 1, 2) is thesubsequence consisting of objects from the ith component.

ξ ::= [v1 , . . . , vn ]where n ≥ 0 and [. . . ] is a finite multiset. A term is a (possibly
infinite) formal sum of simple terms with coefficients in R+ ,where R+ := {x ∈ R | x ≥ 0}. A simple term can appear(possibly infinitely) many times in a term. See, e.g., [16] fora more detailed definition.

D. Interpretation
Types are interpreted as groupoids of rigid refinement types.
So JoK is the category with one object ? and one morphism,
J!AK := PJAK and JA → BK := J!AKop × JBK.
The interpretation of terms is the standard one for the λcalculus fragment (i.e. x, λx.M and M N ). The interpretationof the nondeterministic branching is the disjoint union

Remark 21. Given
P a set D and a countable set I, we identify
a formal sum i∈I ri di whereri ∈ R+ and di ∈ D withP
a mapping (d ∈ D) 7→ ( i∈I,di =d ri ) ∈ R+ ∪ {∞}. The
equality of formal sums is that of the associated mappings.

JM ⊕ N KESP (Θ, a) := JM KESP (Θ, a) + JN KESP (Θ, a).

We shall consider only simply-typed resource terms. The
typing rules are the standard ones: for example, [v1 , . . . , vn ]has type A if vi has type A for every i ∈ [n]. The notion of
η-long form is defined in the straightforward way.
The reduction is defined as follows. If t has n free occurrences of x, we haveX
(λx.t) [u1 , . . . , un ] −→{uσ(1) /x1 , . . . , uσ(n) /xn }t

ESP
We write YA
for the rigid Taylor expansion of (the η-long7

form of) f : A → A ` Y f : A. Now the interpretation
JY M KESP of Γ ` Y M : A is defined as the composite
ESP
JY M KESP := YA◦ JM KESP .

We show that the ESP interpretation JM KESP is isomorphic
to the rigid Taylor expansion JM K. As we have seen in
Theorem 16, JM K is a generalised species of structures. The
key lemma is that the composition as ESP can be seen
as substitution followed by the rigid Taylor expansion. The
equivalence relation ∼ in the composition of profunctors(Equation (3)) coincides with that of the resource calculus.

σ∈Snwhere x1 , . . . , xn are the names of the free occurrences of x
in t. If the number of free occurrence of x in t is not n, thenthe above term is reduced to the empty sum.
Intermediate representations (or simply representations) of
simple terms and bags are the same as simple terms and bags
except that (i) simple terms have new constructors v ⊕ • and• ⊕ v, and (ii) elements of each bag are linearly ordered(i.e. a bag ξ is represented by a list). A representation v
induces a simple term |v| obtained by forgetting the branching
information (i.e. |v ⊕ •| = | • ⊕v| = |v|) and the order of
elements in a bag. Representations are used as an intermediate
data structure during the Taylor expansion.
Figure 4 defines the approximation relation v J M , wherev ranges over representations, and M over λnd Y-terms. We
define the function w(−) byLemma 19. Let x1 : A1 , . . . , xk : Ak ` M : B and Γ ` Ni :Ai (i ∈ [k]). Then there is a natural isomorphism
JM K ◦ hJN1 K, . . . , JNk Ki ∼= J{N1 /x1 , . . . , Nk /xk }M K.

Theorem 20. For every term Γ ` M : A, the ESP interpretation is naturally isomorphic to the rigid Taylor expansion:
JM K ∼= JM KESP : PJΓKop × JAK → Set.

Proof. (Sketch) By induction on the structure of M using
ESP◦ JM KESP ∼Lemma 19. For example, JY M KESP = YA=
JY f K ◦ JM K ∼= J{M/f } (Y f )K = JY M K. A key observationis that evalJBK,JCK is equivalent to the rigid Taylor expansionof (the η-long form of) f : B → C, x : B ` f x : C.

w(λx.v) = w(v ⊕ •) = w(• ⊕ v) = w(v)Y
w(v ξ) = w(v) × w(ξ) w([v1 , . . . , vn ]) = n! ×w(vi ).

w(x) = 1

VI. R EASONING ABOUT STANDARD RESOURCE TERMS
This section studies the rigid Taylor expansion of standard
resource terms—in which application arguments are bags
(i.e. finite multisets)—and compares the rigid and standard
Taylor expansions. As an application, we show the commutation between computing Böhm trees and Taylor expansions
for the λnd Y-calculus (although some coefficients may be ∞).
The proof is an extension of the combinatorial arguments in[16] showing the commutation property of the deterministic
case. In this subsection, resource terms always mean standard
resource terms, and rigid terms are always called rigid.

i∈[n]Definition 22. The Taylor expansion of a λnd Y-term M is
M ∗ :=

X
vJM

1
|v|
w(v)

where v ranges over representations.
It is not difficult to see that this coincides with the standard
definition. The definition can be easily extended to Böhm trees.
The above formal sum may not converge for Böhm trees.

7 There is another definition of Y ESP that does not relies on the rigid
A

Taylor expansion. We omit it because of the space limitation.

10

vJM
vJM
ξJN
v J M1v J M2x J x λx.v J λx.Mvξ J M Nv ⊕ • J M1 ⊕ M2 • ⊕ v J M1 ⊕ M2

∀i ∈ [n]. vi J N[v1 , . . . , vn ] J N

vJM
ξ J YMvξ J YM

Fig. 4. Approximation relation

This interpretation is sound with respect to the reduction of
the resource term. Similarly to the case of λnd Y, a marked
rigid resource term ue◦ C v resolves nondeterminism by, in thiscase, a mapping from elements in a bag to occurrences of avariable.

B. Marked rigid resource terms
Interestingly, in order to describe the rigid Taylor expansion(or the ESP interpretation) of a standard resource term, weneed to use a variant of rigid resource calculus that we callthe marked rigid resource calculus. This reflects a difference
between the symmetries associated to the standard resource
calculus and the symmetries associated to the λY-calculus:
see Remark 23.
In the new syntax, a list is annotated with a permutation:µ := ht1 , . . . , tn iσ where σ ∈ Sn . This annotation σ does
not affect the operational semantics, which simply ignoresσ, but the action of a type isomorphism. Consider the list
µ = h(λx.x), (λy.y)i in the old syntax, whose elements are
identical (as we identify α-equivalent terms), and a = h?i (?. Let ϕ : ha, ai ∼= ha, ai be the type isomorphism swapping
the elements. Then [ϕ]µ = hλy.y, λx.xi = µ (using αconversion), so µ is a fixed-point of [ϕ](−). In other words theold syntax cannot notice if the elements were really swapped.
The aim of the new syntax is to detect such swapping:[ϕ](h(λx.x), (λy.y)iid ) is defined as h(λy.y), (λx.x)iσ (whereσ swaps 1 and 2), which has a different annotation.
We use (−)◦ to express that it is marked. For example, amarked rigid resource raw term is written as u◦ .

Lemma
24. Let v be a resource term and assume that nf(v) =
P
w
.
Then
there exists a natural isomorphism
k
k
a
∼
=
Jwk K(∆, a)α∆,a : JvK(∆, a) −→ksuch that α∆,a (es◦ ) = ιk (eu◦ ) implies nf(es◦ ) = ue◦ . Here ιk is
the k-th injection.
Let (|−|)X be the map from rigid resource terms to standard
resource terms, which replaces a list hu1 , . . . , un i with abag [(|u1 |)X , . . . , (|un |)X ], an abstraction λx1 . . . xn .t withλy.(|t|)X,x1 Cy,...,xn Cy and a variable x with y s.t. (xCy) ∈ X.
We write #iso(∆, a) for the number of isomorphisms, i.e. thenumber of elements in {(ψ, ϕ) | ψ : ∆ ∼= ∆0 and ϕ : a ∼= a0 }.
Lemma 25. Let v be a resource term in normal form.
X1(|eu◦ |)~zC~xv =#iso((~x : ~b), a)(~x:~b`eu◦ :a)∈JvK

Proof. (Sketch) This follows from the following observations:(i) if v is normal, JvK has a single orbit (i.e. any marked rigid
approximations in JvK are related by an isomorphism) and (ii)isomorphisms (except for the identity) do not have a fixedpoint because of the annotations on ue◦ .

Remark 23. The necessity of the marks can be intuitively understood as follows. The marks are needed because a resource
term distinguishes different occurrences of the same term ina bag. For example, consider (λf.f [f [z]]) [λx.x, λx.x]. Thisis reduced to (λx.x)[(λx.x)[z]] + (λx.x)[(λx.x)[z]]. The one
is obtained by substituting the left occurrence of λx.x to theleft occurrence of f , and the other is by the left occurrenceof λx.x to the right occurrence of f ; here we distinguish theoccurrences of λx.x.

The next result follows from Lemmas 24 and 25.
Corollary 26. For every simple resource term v,
X1nf(v) =(|nf(eu◦ )|)~zC~x .
#iso((~x : ~b), a)(~x:~b`eu◦ :a)∈JvK

C. ESP interpretation of standard resource terms

D. Reasoning about the standard Taylor expansion
The following lemma is an explicit computation of the
Taylor expansion of the Böhm tree of a given term.

Let v be a representation of a resource term in η-long form
with no ⊕. As before, we write ~z for a prefix of a fixed infinite
sequence z1 , z2 , . . .. The rigid Taylor expansion JvK of v isdefined by the rules in Fig. 5 andLemma 27.

JvK(∆, a) := { et◦ | ~z C ~x ` t◦ C v and ~z : ~b ` t◦ : a }BT (M )

where ∆ = (~z : ~b). This is a generalised species by the actionof isomorphisms to rigid resource terms defined in Section IV.

∗

=

1

X
(~
x:~b`et:a)∈JBT (M )K#iso((~x : ~b), a)(|et|)~zC~x

Proof. The claim is essentially the same as [16, Lemma 13]
because the action of an isomorphism on rigid terms in normal
form is a combination of swapping of variable occurrences andpermutation of lists.

It is obvious to see that the permutation of elements induces
a natural isomorphism: if v and v 0 represent the same resource
term, then JvK ∼= Jv 0 K. So J·K is well-defined for resource
terms (provided that we do not refer to the annotations; it
is possible to check if the two annotations are equivalent,since the equivalence of annotations is preserved by the natural
isomorphism mentioned above).

The next theorem follows from Corollary 26, Lemma 27 andTheorem 17 with a careful calculation; the proof is omitted
because of the page limit.
∗

Theorem 28. nf(M ∗ ) = BT (M ) .

11

yCx`yCx

X, ~y C x ` t◦ C v x ∈/X◦X ` λ~y .t C λx.v

X1 ` t◦ C v X2 ` µ◦ C ξσ ∈ Sn∀i ∈ [n]. Xi ` t◦i C vσ(i)X1 , X2 ` t◦ µ◦ C v ξ
X1 , . . . , Xn ` ht◦1 , . . . , t◦n iσ C [v1 , . . . , vn ]Fig. 5. The rules of the rigid Taylor expansion of the standard resource terms. Exchange rule of the assumptions in X is omitted.

VII. F UTURE WORK[15] ——, “Böhm trees, krivine’s machine and the taylor expansion oflambda-terms,” in CiE, ser. Lecture Notes in Computer Science,
A. Beckmann, U. Berger, B. Löwe, and J. V. Tucker, Eds., vol. 3988.
Springer, 2006, pp. 186–197. I-C[16] ——, “Uniformity and the Taylor expansion of ordinary lambda-terms,”
Theoretical Computer Science, vol. 403, no. 2-3, pp. 347–372, 2008. I,
I-B, I-C, I-E, IV, VI, VI-A, VI-D
[17] T. Ehrhard, C. Tasson, and M. Pagani, “Probabilistic coherence spaces
are fully abstract for probabilistic PCF,” in POPL, 2014, pp. 309–320.
I-A, I-A, I-E, VII[18] M. P. Fiore, “Mathematical models of computational and combinatorial
structures,” in FoSSaCS, 2005, pp. 25–46. I, I-D, 2, III-C, V-B[19] M. P. Fiore, N. Gambino, J. M. E. Hyland, and G. Winskel, “Thecartesian closed bicategory of generalised species of structures,” J.
London Math. Soc., vol. 77, pp. 203–220, 2008. I, I-D, 2, III-C, V,
V-B, 18, V-C[20] J. Girard, “Linear logic,” Theor. Comput. Sci., vol. 50, pp. 1–102, 1987.
I[21] ——, “Normal functors, power series and λ-calculus,” Ann. Pure Appl.
Logic, vol. 37, no. 2, pp. 129–177, 1988. I, I-B[22] R. Harmer and G. McCusker, “A fully abstract game semantics for finite
nondeterminism,” in LICS. IEEE Comput. Soc, 1999, pp. 422–430. I-A[23] R. Hasegawa, “Two applications of analytic functors,” TheoreticalComputer Science, vol. 272, no. 1-2, pp. 113–175, 2002. I[24] J. M. E. Hyland and C.-H. L. Ong, “On full abstraction for PCF: I, II,
and III,” Info. & Comp., vol. 163, no. 2, pp. 285–408, 2000. I-E[25] A. Joyal, “Une théorie combinatoire des séries formelles,” Adv. Math.,
vol. 42, p. 182, 1981. I, V
[26] ——, “Foncteurs analytiques et espèces de structures,” in CombinatoireÉnumérative. Springer, 1986, pp. 126–159. V[27] A. Kfoury and J. Wells, “Principality and type inference for intersection
types using expansion variables,” TCS, vol. 311, no. 1-3, pp. 1–70, 2004.
I-E, III-B, 5[28] A. J. Kfoury, “A linearization of the lambda-calculus and consequences,”
J. Logic & Comp., vol. 10, no. 3, pp. 411–436, 2000. I-E, 3, III[29] J. Laird, G. Manzonetto, G. McCusker, and M. Pagani, “Weighted
relational models of typed lambda-calculi,” in LICS, 2013, pp. 301–310.
I-E[30] D. Mazza, “Affine approximations and intersection types,” 2016, contributed talk, ITRS 2016. I-E, III[31] P.-A. Melliès, “Asynchronous games 1: Uniformity by group invariance,”
2003, unpublished manuscript. I-E[32] P. M. Neergaard and H. G. Mairson, “Types, potency, and idempotency:
why nonlinearity and amnesia make a type system work,” in ICFP,C. Okasaki and K. Fisher, Eds. ACM, 2004, pp. 138–149. I-E, 2, 3,
III[33] C.-H. L. Ong and T. Tsukada, “Two-level game semantics, intersection
types, and recursion schemes,” in ICALP, 2012, pp. 325–336. I-E[34] M. Pagani, P. Selinger, and B. Valiron, “Applying quantitative semantics
to higher-order quantum computing,” in POPL, 2014, pp. 647–658. I-A,
I-A, I-E, VII[35] M. Pagani, C. Tasson, and L. Vaux, “Strong normalizability as afiniteness structure via the Taylor expansion of λ-terms,” in FoSSaCS,
2016, pp. 408–423. I-C[36] P. Selinger and B. Valiron, “On a fully abstract model for a quantum
linear functional language: (extended abstract),” Electr. Notes Theor.
Comput. Sci., vol. 210, pp. 123–137, 2008. VII[37] T. Tsukada and K. Asada, “Strategies in HO/N games as profunctors,”
2016, contributed talk, GaLoP Workshop. I-E[38] T. Tsukada and C.-H. L. Ong, “Innocent strategies are sheaves over plays- deterministic, non-deterministic and probabilistic innocence,” CoRR,
vol. abs/1409.2764, 2014. VII[39] ——, “Nondeterminism in game semantics via sheaves,” in LICS, 2015.
I-A, I-E

For future work, we aim to develop a theory of “weighted
generalised species”. For example, an R-weighted generalised
species, where R is the ring of real numbers, is a generalised
species f : PA×B op → Set together with the weight function
wa,b : f (a, b) → R (a ∈ PA, b ∈ B) that is preserved by theaction of morphisms in PA and B. It is natural to expectthat a probabilistic programming language can be modelled
by using R-weighted generalised species, where the weightfunction associates a run of a program to its probability, andthis idea is a reminiscent of the existing models (e.g. [8, 9, 17,38]). Furthermore we think that any SMCC can be used as
the domain of weights. In fact, the rigid Taylor expansion canbe seen as generalised species with weights from the linear
λ-calculus and this observation suggests to us the possibilityof replacing the rigid resource terms by morphisms of thechosen SMCC. We are interested in the SMCC CPM [36]and conjecture that CPM-weighted generalised species serve
as a model of a quantum programming language, which should
be closely related to [34].
Acknowledgement
The authors are grateful to Marcelo Fiore for insightfulcomments. They would also like to thank the anonymous
reviewers for their helpful and constructive comments. This
work was supported by JSPS KAKENHI Grant Numbers
JP15H05706 and JP16K16004, and EPSRC EP/M023974/1.
R EFERENCES[1] S. Abramsky, R. Jagadeesan, and P. Malacaria, “Full abstraction for
PCF,” Inf. Comput., vol. 163, no. 2, pp. 409–470, 2000. I-E[2] A. Allioux, “Krivine machine and Taylor expansion in a non-uniform
setting,” in LINEARITY, 2016, pp. 24–32. I-E[3] J. Bénabou, “Les distributeurs,” Tech. Rep. 33, 1973. V-A[4] ——, “Distributors at work,” 2000, course notes, TU Darmstadt. V-A[5] A. Bernadet and S. Lengrand, “Non-idempotent intersection types andstrong normalisation,” LMCS, vol. 9, no. 4, 2013. I-E[6] F. Borceux, Handbook of Categorical Algebra I. CUP, 1994. V-A[7] A. Bucciarelli and T. Ehrhard, “On phase semantics and denotationalsemantics: the exponentials,” Ann. Pure Appl. Logic, vol. 109, no. 3,
pp. 205–241, 2001. I-E, 3[8] V. Danos and T. Ehrhard, “Probabilistic coherence spaces as a model ofhigher-order probabilistic computation,” Inf. Comput., vol. 209, no. 6,
pp. 966–991, 2011. I-A, I-A, I-E, VII[9] V. Danos and R. S. Harmer, “Probabilistic game semantics,” ACM
Trans. Comp. Logic, vol. 3, no. 3, pp. 359–382, 2002. VII[10] D. de Carvalho, “Execution time of lambda-terms via denotationalsemantics and intersection types,” CoRR, vol. abs/0905.4251, 2009. I-E,
8[11] T. Ehrhard, “On Köthe sequence spaces and linear logic,” Mathematical
Structures in Computer Science, vol. 12, no. 5, pp. 579–623, 2002. I,
I-B[12] ——, “Finiteness spaces,” Mathematical Structures in Computer Science, vol. 15, no. 4, pp. 615–646, 2005. I, I-B[13] ——, “A finiteness structure on resource terms,” in LICS, 2010, pp.
402–410. I-C[14] T. Ehrhard and L. Regnier, “The differential lambda-calculus,” Theoretical Computer Science, vol. 309, no. 1-3, pp. 1–41, 2003. I

12