BRICS RS-01-15 L. Santocanale: A Calculus of Circular Proofs and its Categorical Semantics BRICS

Basic Research in Computer Science

A Calculus of Circular Proofs and its Categorical Semantics

Luigi Santocanale BRICS Report Series RS-01-15 ISSN 0909-0878 May 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Luigi Santocanale.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/15/

A calculus of circular proofs and its categorical semantics

Luigi Santocanale

             luigis@brics.dk

BRICS^{∗}

Abstract

We present a calculus of proofs, the intended models of which are categories with finite products and coproducts, initial algebras and final coalgebras of functors that are recursively constructible out of these operations, that is, μ-bicomplete categories. The calculus satisfies the cut elimination and its main characteristic is that the underlying graph of a proof is allowed to contain a certain amount of cycles. To each proof of the calculus we associate a system of equations which has a meaning in every μ-bicomplete category. We prove that this system admits always a unique solution, and by means of this theorem we define the semantics of the calculus.

Keywords: Initial algebras, final coalgebras. Fixed point calculi, μ-calculi. Bicompletion of categories. Models of interactive computation.

Introduction

The goal of this paper is to present and discuss our first results on free μ-bicomplete categories. A category is said to be μ-bicomplete if every finite set of objects has a product as well as a coproduct, and moreover the initial algebra and the final coalgebra of every definable functor exist.

∗ Basic Research in Computer Science, Centre of the Danish National Research Foundation.

A μ-bicomplete category is said to be free over a set X if it contains X as a subset of objects, and moreover it is canonical^{1} among the μ-bicomplete categories having the same property. Among the motivations to generalize to a categorical setting the results obtained by us on free μ-lattices [San00a, San00b, San00c], is the capability of these algebraic objects to model simple computational situations. Indeed, these results were obtained through an explicit description of free μ-lattices by means of games and strategies. Several authors [NYY92, AJ94, Joy97] have remarked the analogy between games and winning strategies on the one hand, and systems’ specifications and correct programs on the other. Accordingly, we can think of games for free μ-lattices as being bidirectional synchronous communication channels which are recursively constructed from a few primitives: left and right choices, similar to the internal and external choices of CSP [Hoa85], and left and right iterations. The challenging part of our work on free μlattices has been the explicit characterization of the order relation: we declared that S ≤ T, S and T being games for a free μ-lattice, if there exists a winning strategy in a compound game of communication ⟨S, T ⟩ for a player called the Mediator. If S and T are thought of as channels, then such a strategy can be understood as a mediating protocol for letting the left user of the channel S communicate with the right user of T in an asynchronous way. Figure (1) suggests that the games S and T could be sort of telephone lines and the mediating protocol M an answering machine or an operating system. The lattice theoretic point of view, which we have adopted until now, is interested only in the existence of such strategies. The analysis of different strategies is more in the spirit of proof theory [HS86, GTL89], categorical logic [LS88], and the semantics of programming languages [Win93]. We would like to classify all the possible asynchronous communications arising in the situation described above; this is usually achieved by giving an algebra of mediating protocols, that is, a programming language by which to construct them, together with a notion of equivalence between protocols. We suggest that the desired algebra is the one of μ-bicomplete categories, and that two programs should be considered equivalent if they denote the same arrow in every μ-bicomplete category. Motivations behind research on bicompletion of categories [Joy95, Joy97,

1What it means to be canonical can be made precise by introducing morphisms and then stating a universal property analogous to the universal property of the free monoid.

[figure: :; S; :; 1st channel; :; T; :; 2nd channel; mediating protocol; M; hooks; left user; right user]

Figure 1: Games as channels, winning strategies as mediating protocols.

HJ99, CS01] are similar to those of Linear Logic [Gir87, Gir01] and related categorical models [Bar91, CS97]. With respect to these algebraic and logical settings, with μ-bicomplete categories the focus is on initial algebras and final coalgebras of functors; from an operational perspective, the focus is on the modeling of possibly infinite computations. Initial algebras of functors are the categorical counterpart of induction and recursion, they model inductive types [CP90]; on the other hand, final coalgebras are a counterpart of coinduction and corecursion; they are related to bisimilarity, in that they classify the observable behavior of systems [Rut00]. The use of coalgebraic methods is now a well established practice to deal with infinite objects by means of their defining equations [Acz88, ML90]. In this paper we define a logical calculus to describe bounded memory deterministic strategies in a communication game of the form ⟨S, T ⟩, that is, to describe the mediating protocols that use a finite amount of space. We skip here the exact description of the correspondence between the combinatorics of games and the algebra of μ-lattices, and focus on the algebraic meaning of strategies; we remark only that if a communication strategy is translated into a proof, as usual in logics and games, then the result is a paradoxical infinite proof, or, in the case of a bounded memory strategy, a circular proof. Hence, the characteristic of our calculus is that the underlying graph of a proof is allowed to contain a certain amount of cycles. This is a common fact in fixed point theory, for example it appears in the proofs with guarded induction of type theory [Coq94] and in the refutations of the propositional μ-calculus [Wal00]. In order to define the semantics, we proceeds as follows: once the type-terms of the calculus are interpreted in the obvious way by means of products, coproducts, initial algebras and final coalgebras, then the proof-terms are also interpreted in a natural way as systems of equations. The main achievement of this paper, theorem 4.11, states that such systems of equations admit always a unique solution. The semantics of a circular proof with a chosen conclusion is then defined to be the chosen projection of the vector solution. The calculus does not contain an explicit cut rule, it satisfies the cut elimination: two proofs can be composed in a sound way, leading to a proof the interpretation of which is the composition of the interpretations of the two original proofs. However, the calculus is not powerful enough to describe all the arrows of a free μ-bicomplete category, which reflects the fact that there are strategies that use an unbounded amount of memory, nonetheless, are computable. This observation suggests that some kind of step has to be done in order to describe free μ-bicomplete categories; on the other hand, we expect that the ideas and tools presented in this paper will be helpful in future researches. We approach the theory of initial algebras and final coalgebras from fixed point theory [BÉ93] - the two theories are closely related, see for example [Fre91]. From [Lam68], it is known that, in an initial algebra χ : Sx ^{}x of an endofunctor S : 𝒞 ^{}𝒞, the arrow χ is invertible, so that its universal property states the existence and uniqueness of a solution of the equation

f = χ^{−1} · Sf · α ,

for each algebra α : Sa ^{}a. The above equation is rephrased in a more compact way as the fixed point equation

f = χ^{−1} · α_{x}(f) ,

where the natural transformation

α_{x} : 𝒞(x, a) ^{}𝒞(Sx, a)

is obtained from the previous α under the Yoneda correspondence, that is, α_{a}(id_{a}) = α. The next step is to realize that also parameterized fixed points exist whenever the category 𝒞 has products. We prove that, for every natural transformation of the form

α_{x,z,w} : 𝒞(x, T w) × Q(x, z, w) ^{}𝒞(S(x, z), T w) ,

where S : 𝒞 × 𝒵 ^{}𝒞, T : 𝒲 ^{}𝒞 and Q is a parameterized set, covariant in w, contravariant in x and z, there exists a unique solution of the equation

f = χ_{z}^{−1} · α_{x_{z},z,w}(f, q) ,

for each choice of q ∈ Q(x_{z}, z, w). In this case

χ_{z} : S(x_{z}, z) ^{}x_{z}

is the initial algebra of the functor S(x, z), parameterized in the variable z. The existence of parameterized unique fixed points leads to show that circular proofs, whenever interpreted as systems of equations, admit always a unique solution. The paper is organized as follows: we introduce the notation and the key concepts of the theory in section 1. In section 2 we describe the syntactical part of the calculus, defining first the terms and then the proofs. In section 3 we prove the main theorem about the existence and uniqueness of certain parameterized fixed points. In section 4, we use this theorem to define the semantics of the calculus. In section 5, as concluding remarks, we discuss the fact that the calculus is not expressive enough with respect to its intended models and suggest a natural relation with automata theory.

1 Notation and preliminaries

Notation.

With 𝒮et we shall denote the category of sets and functions; for a function f : A ^{}B we shall use both the notations f_{a} and f(a) for the result of applying f to a. With [n] we shall denote the set {1, …, n}. Composition in categories, say

A ^{f}^{}B ^{g}^{}C ,

will be denoted in two different ways, that is, g ∘ f and f · g. Sometime we shall omit the symbol ∘ and write gf, but we write always the symbol · . We shall use id for identities, ⟨⟩ and pr for tuples and projections, {} and in for cotuples and injections, for every kind of categorical products and coproducts.

Initial algebras of a functor.

Let 𝒞 be a category and S : 𝒞 ^{}𝒞 be an endofunctor. A S-algebra is a pair (c, γ), where c is an object of 𝒞 and γ : Sc ^{}c is an arrow of 𝒞. A morphism of S-algebras f : (c, γ) ^{}(d, δ) is an arrow f : s ^{}d of 𝒞 such that γ · f = Sf · δ. S-algebras and their morphisms form a category 𝒞^{S}. A T -algebra (x, χ) is initial if for each algebra (c, γ) there exists a unique arrow^{!}γ : x ^{}c such that χ·^{!}γ = S^{!}γ·γ. S-coalgebras and their morphisms are defined in the dual way and form a category 𝒞_{S}. We recall that a coalgebra ς : y ^{}Sy is final if for each coalgebra γ : c ^{}Sc there exists a unique arrow ^{!}γ : c ^{}y such that ^{!}γ · ς = γ · S^{!}γ. We explain our conventions concerning variables. Each variable x, y, z, … can be in two states: either it is free, in which case it denotes a projection functor, or it is bounded to some value. As a general rule, we shall use the usual style x, y, z, … for free variables and the typewriter style x, y, z, … for bounded variables. For example, with an equation of the form

x =_{μ} Sx

we shall mean that the denotation of x is the object part of a chosen initial S-algebra, in which case we shall use the corresponding Greek letter χ to denote the arrow part of this S-algebra.

Systems of equations.

Definition 1.1 Let α : C×A ^{}C be an arrow in the functor category 𝒮et^{𝒟} . We shall say that α admits a unique solution if, for each object d of 𝒟 and each a ∈ A_{d}, there exists a unique c ∈ C_{d} such that α_{d}(c, a) = a. If α admits a unique solution we shall denote by α_{d}^{†}(a) such a c ∈ C_{d}. 1.1

Lemma 1.2 If α admits a unique solution, then the collection {α_{d}^{†}}_{d∈Obj(𝒟)} is a natural transformation α^{†} : A ^{}C.

Lemma 1.3 Let α : C × A ^{}C be an arrow of the functor category 𝒮et^{𝒟} and let F : 𝒞 ^{}𝒟 be a functor. If α admits a unique solution, then α_{F} – that is, the arrow 𝒮et^{F} (α) of the category 𝒮et^{𝒞} – admits the unique solution (α^{†})_{F}.

Definition 1.4 A natural system of equations is a tuple ⟨I, C, F, α, β⟩, where • I is a finite indexing set, and for each i ∈ I, F_{i} is a functor from 𝒟

to 𝒮et.

• C ⊆ I is the set of bounded indexes.

• For each c ∈ C, β_{c} ⊆ I and

α_{c} : ∏_{k∈β_{c}} F_{k} ^{}F_{c}

is a natural transformation.

We say that a natural system of equations admits a unique solution if the arrow

∏_{c∈C} F_{c} × ∏_{a∈I\C} F_{a} ^{⟨α_{c}∘pr_{βc}⟩_{c∈C}}^{}∏_{c∈C} F_{c}

admits a unique solution. 1.4

In the following “system” will be synonymous of natural system of equations. We shall represent systems with the usual notation:

{ c = α_{c}(β_{c}) }_{c∈C} .

The Bekič property holds, we state it in the form of a sufficient condition to determine whether a system admits a unique solution.

Proposition 1.5 If the system

{ c = α_{c}(c, α_{d}(c, a), a) }

admits a unique solution, then also the system

\{ \begin{matrix}c & = & α_{c}(c, d, a) \\ d & = & α_{d}(c, a) \end{matrix} \}

admits a unique solution. If the systems

{ d = α_{d}(d, c, a) }
\{ \begin{matrix}c & = & α_{c}(c, d, a) \\ d & = & α_{d}^{†}(c, a) \end{matrix} \}

admit a unique solution, then also the system

\{ \begin{matrix}c & = & α_{c}(c, d, a) \\ d & = & α_{d}(d, c, a) \end{matrix} \}

admits a unique solution.

2 The calculus of circular proofs

2.1 Directed systems of labeled equations

We shall fix a signature Ω and by writing H ∈ Ω_{n}, where n ≥ 0, we shall mean that H is a function symbol from Ω of arity n; we assume that the symbols _{⋀I},_{⋁I} do not belong to Ω, for each finite set I. We let X be a countable set of variables, and let 𝒞 be a category. We form terms as usual.

Definition 2.1 The collection of terms T (𝒞) and the free variables function fv : T (𝒞) ^{}P (X) are defined by induction by the following clauses:

• If x ∈ X, then x ∈ T (𝒞) and fv(x) = {x}.

• If c is an object of 𝒞, then c ∈ T (𝒞) and fv(c) = ∅.

• If I is a finite set and s : I ^{}T (𝒞) is a function, then_{⋀I}s ∈ T (𝒞) and _{⋁I}s ∈ T (𝒞). Moreover fv(_{⋀I}s) = fv(_{⋁I}s) = ⋃_{i∈I} fv(s_{i}).

• If H ∈ Ω_{n} and s : [n] ^{}T (𝒞) is a function, then Hs ∈ T (𝒞) and fv(Hs) = ⋃_{i∈[n]} fv(s_{i}).

For Y ⊆ X, we let T (𝒞, Y) be the collection of terms s ∈ T (𝒞) such that fv(s) ⊆ Y. 2.1

Remark 2.2 Let s : {l, r} ^{}T (𝒞) be a function. In the examples we shall informally use the standard notation s_{l} ∧ s_{r}, s_{l} ∨ s_{r} for ⋀_{{l,r}} s, ⋁_{{l,r}} s, respectively. Similarly, ⊤ stands for _{⋀∅} and ⊥ stands for _{⋁∅}. 2.2

Definition 2.3 A polarized system of equations over 𝒞 is a tuple ⟨X, q, ϵ⟩ where

• X ⊆ X is a finite subset of X, the set of bounded variables.

• q : X ^{}T (𝒞) is a function which associates to each bounded variable its value.

• ϵ : X ^{}{μ, ν} is a labeling of equations.

2.3

We represent a polarized system of equations ⟨X, q, ϵ⟩ with the notation:

{ x =_{ϵ_{x}} q_{x} }_{x∈X} .

Definition 2.4 Let ⟨X, q, ϵ⟩ be a polarized system of equations over 𝒞. The relation → on the set of variables of X is defined as follows:

x → y iff x ∈ X_{S} and y ∈ fv(q_{x}) .

A tuple S = ⟨X_{S}, q_{S}, ϵ_{S}, X_{0,S}⟩ is said to be a directed system over 𝒞 if ⟨X_{S}, q_{S}, ϵ_{S}⟩ is a polarized system of equations and X_{0,S} ⊆ X_{S}; moreover, for each x ∈ X_{S} there exists a unique simple path in the graph ⟨X_{S}, →⟩ from an element r(x) ∈ X_{0,S} to x. That is, the tuple ⟨X_{0,S}, X_{S}, →⟩ is a forest with back edges. If x, y ∈ X_{S}, we shall write x ≤_{S} y if x lies on the simple path from r(y) to y; we shall write x <_{S} y if x ≤_{S} y and x ≠ y. We let

fv(S) = ( ⋃_{x∈X_{S}} fv(q_{x}) ) \ X_{S} ,

and by V(S) we shall denote the collection of finite subsets Y of X such that Y ∩X_{S} = ∅ and fv(S) ⊆ Y. With S(𝒞) we shall denote the collection of directed systems over 𝒞. 2.4

Example 2.5 Directed systems are (roughly speaking) another representation of μ-terms, they are analogous to the hierarchical systems of equations of [Sei96]. For example, the μ-term μ_{x}.ν_{y}.(x ∧ μ_{z}.(z ∨ y)) is translated into the directed system

⟨ \{ \begin{matrix}x & =_{μ} & y \\ y & =_{ν} & x ∧ z \\ z & =_{μ} & z ∨ y \end{matrix} \} , \{x\} ⟩ .

The forest with back edges is in this case a tree with back edges, since X_{0} = {x} is a singleton, and it is given in the following diagram:

                             [figure: x; y; z]

The ordering is x < y < z. 2.5 Definition 2.6 Let S be a directed system and let F ⊆ X_{S} be an order filter, that is, a subset of X_{S} with the property that if x ∈ F and x ≤_{S} y, then y ∈ F. We define the system S_{F} as follows:

• X_{S_{F}} = F.

• q_{S_{F}} and ϵ_{S_{F}} are the restrictions of q_{S} and ϵ_{S} to F, respectively.

• X_{0,S_{F}} = { y ∈ F | z <_{S} y implies z ∉ F }.

We shall write S_{x} for S_{F}, where F = { y | x <_{S} y }. 2.6

Lemma 2.7 The inequality

fv(S_{x}) ⊆ fv(S) ∪ (x)_{↓_{S}}

holds, where (x)_{↓_{S}} = { y ∈ X_{S} | y ≤_{S} x }.

2.2 Circular proofs

Definition 2.8 Let S, T be two directed systems over 𝒞. The collection R_{S,T} of rule symbols over S, T, with their arity set, is defined by means of the following table:

Rule  Range  Arity
A  [0]
Cf  f is an arrow of 𝒞  [0]
CH  H ∈ Ω_{n}  [n]
L^{⋀I}^{i}

I is a finite set, i ∈ I [1]

R_{⋀I}  I is a finite set  I
L_{⋁I}  I is a finite set  I
R^{⋁I}^{i}

I is a finite set, i ∈ I [1]

Lμx     x ∈ X_{S}, ϵ_{x} = μ  [1]
Ry_{μ}  y ∈ X_{T} , ϵ_{y} = μ  [1]
Lx_{ν}  x ∈ X_{S}, ϵ_{x} = ν  [1]
Rνy     y ∈ X_{T} , ϵ_{y} = ν  [1]
2.8

Definition 2.9 Let S, T be two directed systems over 𝒞. A tuple ⟨G_{0}, λ, ρ, σ⟩, where • G_{0} is a set of vertexes,

• λ : G_{0} ^{}T (𝒞) × T (𝒞) is a labeling of vertexes by sequents,

• ρ : G_{0} ^{}R_{S,T} is a labeling of vertexes by rule symbols over S, T,

• for each g ∈ G, σ_{g} : Arity(ρ(g)) ^{}G_{0} is a successor function,

is said to be well typed over S, T if the following typing constraints hold:

\begin{aligned}& A \\ s ⊢ t \end{aligned}

\begin{aligned}& Cf \\ dom f ⊢ cod f \end{aligned}

{s_{i} ⊢ t_{i}}_{i∈[n]}

                                 CH

Hs ⊢ Ht

\begin{aligned}s_{i} ⊢ t \\ & L_{⋀I} & i \\ _{⋀I}s ⊢ t \end{aligned}  \{s ⊢ t_{i}\}_{i∈I} ; R_{⋀I} ; s ⊢ _{⋀I}t

\{s_{i} ⊢ t\}_{i∈I} ; L_{⋁I} ; _{⋁I}s ⊢ t  \begin{aligned}s ⊢ t_{i} \\ & R_{⋁I} & i \\ s ⊢ _{⋁I}t \end{aligned}

q_{x} ⊢ t ; Lμx ; x ⊢ t  s ⊢ q_{y} ; Ry_{μ} ; s ⊢ y

q_{x} ⊢ t ; Lx_{ν} ; x ⊢ t  s ⊢ q_{y} ; Rνy ; s ⊢ y

Here a typing constraint of the form

{s_{i} ⊢ t_{i}}_{i∈Arity(R)}
R
s ⊢ t

stands for the following implication: for all g ∈ G_{0}, if ρ(g) = R, then λ(g) has the form s ⊢ t and for each i ∈ Arity(R) λ(σ_{g,i}) has the form s_{i} ⊢ t_{i}. 2.9

Definition 2.10 Let P = ⟨G_{0}, λ, ρ, σ⟩ be a tuple which is well typed over S, T. The graph G(P) = ⟨G_{0}, →⟩ has as vertexes the elements of G_{0}, and

g → g′ iff g′ = σ_{g,i} .

for some i ∈ Arity(ρ(g)). 2.10 Definition 2.11 Let P be a tuple well typed over S, T, and let γ_{0} → γ_{1} → … γ_{n} = γ_{0}, n ≥ 1, be a proper cycle of G(P). We let γ_{S}, γ_{T} be the sets

{ x ∈ X_{S} | ∃i ∈ [n] s.t. ρ(γ_{i}) ∈ {Lμx, Lx_{ν}} } ,
{ x ∈ X_{T} | ∃i ∈ [n] s.t. ρ(γ_{i}) ∈ {Rx_{μ}, Rνx} } ,

respectively. 2.11

Remark 2.12 Observe that if γ is a proper cycle of G(P), then either γ_{S} ≠ ∅ or γ_{T} ≠ ∅. If γ_{S} ≠ ∅, then γ_{S} is a strongly connected component of the graph associated to S, hence we can find a minimum element with respect to the order ≤_{S}. A similar remark holds for γ_{T}. 2.12

Definition 2.13 A tuple Π well typed over S, T is said to be a circular proof over S, T, if, for every proper cycle γ of G(Π), either

γ_{S} ≠ ∅ and ϵ(min γ_{S}) = μ ,

or

γ_{T} ≠ ∅ and ϵ(min γ_{T}) = ν .
2.13

Remark 2.14 In the following we shall refer to the first statement as L(γ), and to the second as R(γ), so that a tuple Π, well typed over S, T, is a circular proof over S, T, if, for every proper cycle γ of G(Π), either L(γ) holds, or R(γ) holds. The above condition can be understood as follows: the systems S and T can are a translation of games for free μ-lattices, and a circular proof is meant to describe a bounded memory winning strategy in the compound game ⟨S, T ⟩, which we described in [San00c, San00a, San00b] and recalled in the introduction. As in Blass’ game semantics of Linear Logic [Bla72, Bla92] and in Joyal’s games for communication [Joy97], a player called Mediator has to win either on S or on T. On the other hand, the games S and T are parity games; these games have shown to be a useful tool in the study of Monadic Second Order Logic [GH82] and of Propositional μ-Calculus, a general introduction to them can be found in [Zie98]. Henceforth, the condition L(γ) can be understood as stating the fact that the chosen player of S won’t lose in this game by repeating infinitely often the instructions contained in the cycle γ of its winning strategy. 2.14 Definition 2.15 Let Π = ⟨G_{0}, λ, ρ, σ⟩ be a circular proof over S, T. We say that a vertex g ∈ G_{0} is a conclusion if ρ(g) ≠ A and that it is an assumption if ρ(g) = A. We denote by C_{Π} and A_{Π} the set of conclusions and the set of assumptions of Π, respectively. 2.15

We shall use often the notation s_{g} if g is a vertex of a circular proof and λ(g) = s_{g} ⊢ t for some t ∈ T (𝒞). We shall also use a similar notation t_{g}.

Definition 2.16 Let Π be a circular proof over the directed systems S, T, we define

fv_{l}(Π) = fv(S) ∪ ( ⋃_{g∈G_{0}} fv(s_{g})) \ X_{S} ,
fv_{r}(Π) = fv(T) ∪ ( ⋃_{g∈G_{0}} fv(t_{g})) \ X_{T} .

Observe that fv_{l}(Π) ∈ V(S) and fv_{r}(Π) ∈ V(T), and that, for g ∈ G_{0}, s_{g} ∈ T (𝒞, X_{S} ∪ fv_{l}(Π)) and t_{g} ∈ T (𝒞, X_{T} ∪ fv_{r}(Π)). 2.16

Definition 2.17 Let Π be a circular proof over S, T, its complexity #Π is the pair of numbers (card C_{Π}, card X_{S} + card X_{T}). 2.17

Remark 2.18 Observe that #Π ∈ ℕ^{2}, and this set comes with the lexicographic order: (n, m) ≤ (n′, m′) if and only if n ≤ n′ and n = n′ implies m ≤ m′. The strict order < arising from the lexicographic order is a well founded relation. Hence, we shall prove properties of circular proofs by induction on #Π, by providing a base case if card C_{Π} = 0 and an induction step if card C_{Π} > 0. 2.18

Definition 2.19 A circular proof Π = ⟨G_{0}, λ, ρ, σ⟩ is said to be strongly connected if, for each pair of conclusions g_{1}, g_{2} ∈ C_{Π}, we can find paths g_{1} →^{∗} g_{2} and g_{2} →^{∗} g_{1} in G(Π). 2.19

We draw examples of circular proofs with a given base point and such that their underlying graph is a tree with back edges. Indeed, we want to remark the analogy with the usual model of a proof as a finite tree and use existing tools for drawing proofs. Hence, we shall draw trees with some of the leaves annotated by a number. With the notation

\begin{aligned}⟩s ⊢ t⟨_{n} & … \\ & & ρ(g) \\ λ(g) \end{aligned} ; \begin{matrix}· \\ · \\ · \end{matrix}

we mean that there is a transition in G(Π) from g to the n-the vetertex g′ on the path from the root to g.

Example 2.20 Let S be the directed system

⟨ \{ \begin{matrix}x & =_{ν} & y \\ y & =_{μ} & x ∧ y \end{matrix} \} , \{x\} ⟩

so that the associated order is x <_{S} y. Let T be the empty system of equations, then

\begin{aligned}⟩y ⊢ ⊥⟨_{2} \\ & L_{⋀\{l,r\}} & r \\ x ∧ y ⊢ ⊥ \end{aligned}

                              Lμy

y ⊢ ⊥

                             Lx_{ν}

x ⊢ ⊥

is a circular proof over S, T. The following is not a circular proof, since it does not satisfy condition of definition 2.13 on cycles:

\begin{aligned}⟩x ⊢ ⊥⟨_{1} \\ & L_{⋀\{l,r\}} & l \\ x ∧ y ⊢ ⊥ \end{aligned}

                               Lμy

y ⊢ ⊥

                             Lx_{ν}

x ⊢ ⊥

Indeed, let γ be the only simple cycle on this graph. R(γ) does not hold, since γ_{T} = ∅. On the other hand L(γ) does not hold, since min γ_{S} = x and ϵ(x) = ν. 2.20 Example 2.21 A more complex example is the following:

\begin{aligned}& R_{⋀∅} \\ ⊤ ⊢ ⊤ \end{aligned} ; R_{⋁\{l,r\}}_{l} ; ⊤ ⊢ ⊤ ∨ x_{1}

          Rx_{1}_{μ}

  ⊤ ⊢ x_{1} R_{⋁{l,r}}_{l}

⊤ ⊢ x_{1} ∨ x_{2}

          Rx_{2}_{μ}

  ⊤ ⊢ x_{2}

\begin{aligned}& R_{⋀∅} \\ ⊤ ⊢ ⊤ \end{aligned} ; R_{⋁\{l,r\}}_{l} ; ⊤ ⊢ ⊤ ∨ x_{1} \begin{aligned}⟩x_{1} ⊢ x_{1}⟨_{10} \\ & R_{⋁\{l,r\}} & r \\ x_{1} ⊢ ⊤ ∨ x_{1} \end{aligned}
L_{⋁{l,r}}
⊤ ∨ x_{1} ⊢ ⊤ ∨ x_{1}

                           Ry_{μ}

               ⊤ ∨ x_{1} ⊢ x_{1}

                         Lμx_{1}

                 x_{1} ⊢ x_{1} R_{⋁{l,r}}_{r}

x_{1} ⊢ ⊤ ∨ x_{1}

                         Rx_{1}_{μ}

                 x_{1} ⊢ x_{1} R_{⋁{l,r}}_{l}

               x_{1} ⊢ x_{1} ∨ x_{2}

⟩x_{2} ⊢ x_{2}⟨_{4} _{R_{⋁{l,r}}_{r}} x_{2} ⊢ x_{1} ∨ x_{2}
L_{⋁{l,r}}

                           x_{1} ∨ x_{2} ⊢ x_{1} ∨ x_{2}
                                         Rx_{1}_{μ}

                             x_{1} ∨ x_{2} ⊢ x_{2}

                                       Lμx

                               x_{2} ⊢ x_{2} R_{⋁{l,r}}_{r}

                             x_{1} ⊢ x_{2} ∨ x_{2}

                                       Rx_{μ}

                               x_{1} ⊢ x_{2}

L_{⋁{l,r}}
⊤ ∨ x_{2} ⊢ x_{2}

This circular proof is over S_{2}, S_{2}, the directed system S_{2} being defined at page 26. 2.21

2.3 Operations on circular proofs

Taking the reachable part.

Let Π = ⟨G_{0}, λ, ρ, σ⟩ be a circular proof and let C ⊆ G_{0}. We define \overline{Π, C} to be the circular proof ⟨H_{0}, λ′, ρ′, σ′⟩, where H_{0} ⊆ G_{0} and g ∈ H_{0} if and only if we can find c ∈ C and a path c →^{∗} g in G(Π); λ′, ρ′, σ′ are the restriction of the analogous functions to H_{0}. If C = \{g\}, then we shall write \overline{Π, g} instead of \overline{Π, \{g\}}. By definition, G(\overline{Π, g}) is a pointed reachable graph.

Addition of new assumptions.

Let Π = ⟨G_{0}, λ, ρ, σ⟩ be a circular proof and let A ⊆ G_{0}. We define Π^{A} to be the circular proof ⟨G_{0}, λ, ρ′, σ⟩, where

ρ′(g) = \{ \begin{matrix}ρ(g) , & g ∈ G_{0} \ A , \\ A , & g ∈ A . \end{matrix} .

We draw this operation as follows:

[figure: {s′ ⊢ t′ \atop s ⊢ t}; Π_{1}; {s′ ⊢ t′ \atop s ⊢ t}; Π_{2}]⇝ [figure: \begin{aligned}& A \\ s ⊢ t \end{aligned}; Π_{1}; s′ ⊢ t′; Π_{2}]

3 A parameterized fixed point theorem

In this section we prove the theorem that enables us to define the semantics of the calculus.

Theorem 3.1 Let 𝒵, 𝒲, 𝒞 be three categories, of which 𝒞 has finite products, and let S, T and Q be functors as follows:

S : 𝒞 × 𝒵  ^{}𝒞
T : 𝒲  ^{}𝒞
Q : 𝒞^{op} × 𝒵^{op} × 𝒲 ^{}𝒮et .

Consider a natural transformation

α_{x,z,w} : 𝒞(x, T w) × Q(x, z, w) ^{}𝒞(S(x, z), T w)

and let (x_{z}, χ_{z}) be a parameterized initial algebra of the functor S(x, z). For each object z of 𝒵, w of 𝒲 and each q ∈ Q(x_{z}, z, w), there exists a unique f : x_{z} ^{}T w which is a solution of the equation

χ_{z} · f = α_{x_{z},z,w}(f, q) .

Before proving the theorem, we observe that the condition that C has products is necessary. Consider the discrete poset {a, b} and the constant function Sx = a, so that a, being the unique fixed point, is the initial S-algebra. In {a, b}, the following implication holds:

x < b ⇒ Sx ≤ b .

Let Q(x, b) be the statement b ≰ x, then the above implication is

x ≤ b ∧ Q(x, b) ⇒ Sx ≤ b

and if the theorem were true also in this case, we would be allowed to deduce

Q(a, b) ⇒ a ≤ b .

Since b ≰ a, then we would deduce that a ≤ b. In the proof we shall use a bimodule notation, that is, for q ∈ Q(x, z, w), we let

(f, g) · q = Q(f, g, id_{w})(q)
q · h = Q(id_{x}, id_{z}, h)(q).

Naturality in x of α leads to the relation

α_{x′,z,w}(h · f, (h, id_{z}) · q)
= S(h, id_{z}) · α_{x,z,w}(f, q)

for h : x′ ^{}x. Proof of theorem 3.1. We show first that the above equation admits a solution. Let z be an object of 𝒵, w be an object of 𝒲 and q ∈ Q(x_{z}, z, w). Consider the two projections pr_{x_{z}}, pr_{T w} from the product x_{z} × T w and observe that (pr_{x_{z}}, id_{z})·q ∈ Q(x_{z} ×T w, z, w). It makes sense to consider the arrow

α_{x_{z}×T w,z,w}(pr_{T w}, (pr_{x_{z}}, id_{z}) · q) : S(x_{z} × T w, z) ^{}T w .

Pair this arrow with

S(pr_{x_{z}}, id_{z}) · χ_{z} : S(x_{z} × T w, z) ^{}x_{z}

to obtain a S(x, z)-algebra (x_{z} × T w, β). Let ^{!}β be the unique morphism of S(x, z)-algebras from the initial one to (x_{z} × T w, β), and observe that

!β · pr_{x_{z}} = id_{x_{z}} ,

since pr_{x_{z}} is a morphism of S(x, z)-algebras. Let

f = ^{!}β · pr_{T w} : x_{z}  ^{}T w ,

then the relation χ_{z} · f = α_{x_{z},z,w}(f, q) holds:

χ_{z} · f = χ_{z} ·^{!}β · pr_{T w}
= S(^{!}β, id_{z}) · β · pr_{T w}
= S(^{!}β, id_{z}) · α_{x_{z}×T w,z,w}(pr_{T w}, (pr_{x_{z}}, id_{z}) · q)
= α_{x_{z},z,w}(^{!}β · pr_{T w}, (^{!}β, id_{z}) · (pr_{x_{z}}, id_{z}) · q)
= α_{x_{z},z,w}(f, (^{!}β · pr_{x_{z}}, id_{z}) · q)
= α_{x_{z},z,w}(f, q) .

On the other hand, suppose that χ_{z} · f = α_{x_{z},z,w}(f, q), and let

γ = ⟨id_{x_{z}}, f⟩ : x_{z}  ^{}x_{z} × T w .

We shall show that

χ_{z} · γ = S(γ, id_{z}) · β ,

and, as a consequence, we shall deduce that γ = ^{!}β and that f = γ · pr_{T w} = ^{!}β · pr_{T w}. Indeed, we have:

χ_{z} · γ · pr_{x_{z}} = χ_{z}
= S(γ · pr_{x_{z}}, id_{z}) · χ_{z}
= S(γ, id_{z}) · S(pr_{x_{z}}, id_{z}) · χ_{z}
= S(γ, id_{z}) · β · pr_{x_{z}} ,

and

χ_{z} · γ · pr_{T w} = χ_{z} · f
= α_{x_{z},z,w}(f, q)
= α_{x_{z},z,w}(γ · pr_{T w}, (γ · pr_{x_{z}}, id_{z}) · q)
= S(γ, id_{z}) · α_{x_{z}×T w,z,w}(pr_{T w}, (pr_{x_{z}}, id_{z}) · q)
= S(γ, id_{z}) · β · pr_{T w} .
□

As in 1.2, unique solutions of the above equation make up a natural transformation

β_{z,w} : Q(x_{z}, z, w) ^{}C(x_{z}, T w) .

A similar dual technique has been used in [AAV00, Mos00] to prove the universal property of iteration monads. The full dual statement, which we need to prove theorem 4.11, is as follows:

Theorem 3.2 Let 𝒵, 𝒲, 𝒞 be three categories, of which 𝒞 has finite coproducts, and let S, T and Q be functors as follows:

S : 𝒵  ^{}𝒞
T : 𝒞 × 𝒲  ^{}𝒞
Q : 𝒵^{op} × 𝒞 × 𝒲 ^{}𝒮et .

Consider a natural transformation

α_{z,y,w} : 𝒞(Sz, y) × Q(z, y, w) ^{}𝒞(Sz, T (y, w))

and let (y_{w}, ς_{w}) be a parameterized final coalgebra of the functor T (y, w). For each object z of 𝒵, w of 𝒲 and each q ∈ Q(z, y_{w}, w), there exists a unique f : Sz ^{}y_{w} which is a solution of the equation

f · ς_{w} = α_{z,y_{w},w}(f, q) .

4 Semantics of the calculus

4.1 Semantics of systems, μ-bicomplete categories

Definition 4.1 Let 𝒞 be a category, a functor S : 𝒞^{{x}∪J} ^{}𝒞 is said to admit initial algebras if, for each object z of C^{J}, an initial algebra of the functor S(x, z) exists. Observe that if R : 𝒞^{I} ^{}𝒞^{J} is a functor and S : 𝒞^{{x}∪J} ^{}𝒞 admits initial algebras, then also the functor

S ∘ (id_{𝒞} × R) : 𝒞^{{x}∪I} ^{}𝒞

admits initial algebras. A choice of initial algebras is a correspondence (x, χ) which assigns to each pair (S, z), where S : 𝒞^{{x}∪J} ^{}𝒞 admits initial algebras and z is an object of 𝒞^{J}, an initial algebra χ_{z} : S(x_{z}, z) ^{}x_{z}. We shall require that a choice of initial algebras is stable under substitution, that is, if χ_{z} : S(x_{z}, z) ^{}x_{z} is the initial algebra associated to the pair (S, z), then χ_{Ru} : S(x_{Ru}, Ru) ^{}x_{Ru} is the initial algebra associated to the pair (S ∘ (id_{𝒞} × R), u). A choice of final coalgebras is defined in a similar way. 4.1 Definition 4.2 An Ω-model is a pair ⟨𝒞, I⟩ where 𝒞 is a category with a given choice of finite products, finite coproducts, initial algebras and final coalgebras, and I is an interpretation of the signature, that is, a correspondence which assigns a functor I(H) : 𝒞^{n} ^{}𝒞 to each symbol H ∈ Ω_{n}, for each n ≥ 0. 4.2

Remark 4.3 We can avoid the use of choices if we allow uniqueness up to unique natural isomorphism in proposition 4.4. To easy the notation, we shall write simply H : 𝒞^{n} ^{}𝒞 for I(H) : 𝒞^{n} ^{}𝒞 and say that 𝒞 is an Ω-model. 4.3

To understand properly the next proposition, recall from [ML98, V.3] that if 𝒞 has products (coproducts), then a functor category 𝒞^{J} has products (coproducts), which are calculated pointwise. Hence, a choice of products (coproducts) gives rise to a choice of products (coproducts) in the category 𝒞^{J}. In a similar way, a choice of initial algebras (final coalgebras) determines, for each functor S : C^{{x}∪J} ^{}C admitting initial algebras, a unique extension of the collection of objects {x_{z}}_{z∈Obj(C^{J})} to a functor x : C^{J} ^{}C such that χ_{z} is a natural transformation from S(x_{z}, z) to x_{z}.

Proposition 4.4 Let 𝒞 be an Ω-model, let S ∈ S(𝒞) and Z ∈ V(S). There exists at most one correspondence ∥−∥_{S}^{Z}, defined on T (𝒞, X_{S} ∪ Z), with the following properties:

• For each s ∈ T (𝒞, X_{S} ∪ Z), ∥s∥_{S}^{Z} is a functor 𝒞^{Z} ^{}𝒞.

• For each z ∈ Z, ∥z∥_{S}^{Z} is the projection functor on the z component.

• For each object c of 𝒞, ∥c∥_{S}^{Z} = c, a constant functor.

• If s : I ^{}T (𝒞, X_{S}∪Z), then ∥⋀_{I} s∥_{S}^{Z} = ∏_{i∈I} ∥s_{i}∥_{S}^{Z} and ∥⋁_{I} s∥_{S}^{Z} = ∐_{i∈I} ∥s_{i}∥_{S}^{Z}.

• If H ∈ Ω_{n} and s : [n] ^{}T (𝒞, X_{S} ∪ Z), then ∥Hs∥_{S}^{Z} = H ∘ ⟨∥s_{i}∥_{S}^{Z}⟩_{i∈[n]}.

• If the equation x =_{μ} q_{x} belongs to S, then ∥x∥_{S}^{Z} is the chosen initial algebra of the functor

∥q_{x}∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[ x , ∥y∥_{S}^{Z}/y]_{y<_{S}x}

where [ x , ∥y∥_{S}^{Z}/y]_{y<_{S}x} is the functor

id_{C^{{x}}} × ⟨∥y∥_{S}^{Z}, id_{C^{Z}}⟩_{y<_{S}x}
: 𝒞^{{x}∪Z} ^{}𝒞^{(x)_{↓_{S}} ∪Z} .

• If the equation x =_{ν} q_{x} belongs to S, then ∥x∥_{S}^{Z} is the chosen final coalgebra of the above functor.

Observe that the relation (x)_{↓_{S}} ∪ Z ∈ V(S_{x}) follows from lemma 2.7. In the following lemma, (x)_{↑_{S}} ⊆ X is the principal order filter generated by

x.

Lemma 4.5 Let 𝒞 be an Ω-model, let S ∈ S(𝒞) and let Z ∈ V(S). If a correspondence ∥−∥_{S}^{Z} with the above properties exists, then

∥s∥_{S}^{Z} = ∥s∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[ ∥y∥_{S}^{Z}/y]_{y≤_{S}x}

holds, for every s ∈ T (𝒞) such that fv(s) ⊆ fv(S) ∪ (x)_{↓_{S}} ∪ (x)_{↑_{S}}. In particular ∥q_{x}∥_{S}^{Z} is equal to

∥q_{x}∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[ ∥x∥_{S}^{Z}/x , ∥y∥_{S}^{Z}/y ,]_{y<_{S}x} .

The only obstacle to the existence of such a correspondence is that the desired initial algebras and final coalgebras could not exist. The following proposition gives an inductive method to verify whether we can find such a correspondence.

Proposition 4.6 Let 𝒞 be an Ω-model, let S ∈ S(𝒞) and Z ∈ V(S). Suppose that for each variable x ∈ X_{0,S} the following conditions hold:

• A correspondence ∥−∥_{S_{x}}^{{x}∪Z} with the above properties exists.

• If the equation x =_{μ} q_{x} belongs to S, then an initial algebra of the functor ∥q_{x}∥_{S_{x}}^{{x}∪Z} exists.

• If the equation x =_{ν} q_{x} belongs to S, then a final coalgebra of the functor ∥q_{x}∥_{S_{x}}^{{x}∪Z} exists.

Then also a correspondence ∥−∥_{S}^{Z} with the above properties exists.

This justifies the following definition.

Definition 4.7 An Ω-model 𝒞 is said to be μ-bicomplete if, for each directed system S ∈ S(𝒞) and Z ∈ V(S), there exists exactly one correspondence ∥−∥_{S}^{Z} with the above properties. 4.7

Example 4.8 Every complete lattice L with an interpretation of the signature Ω is a μ-bicomplete Ω model. If Ω is the empty signature, then a lattice L is μ-bicomplete if and only if it is a μ-lattice [San00b]. 4.8

Example 4.9 Let λ > ω be a regular cardinal and consider the space of λ-accessible functors of the form S : 𝒮et^{J} ^{}𝒮et for some finite set J; that is, those functors that preserve λ-directed colimits, cf. [AR94]. This space contains constant functors and projections, and it is closed under substitution, finite products and coproducts. Parameterized initial algebras and final coalgebras exist, cf. [AK79, Bar93] and the respective induced functors are again λ-accessible. Therefore, if for each H ∈ Ω_{n} I(H) : 𝒮et^{n} ^{}𝒮et is a λ-accessible functor, then ⟨𝒮et, I⟩ is a μbicomplete Ω-model. The same arguments is still true, if we substitute 𝒮et with an arbitrary locally λ-presentable category. 4.9

4.2 Semantics of circular proofs

We shall suppose in the following that 𝒞 is a μ-bicomplete Ω-model.

Definition 4.10 Let Π = ⟨G_{0}, λ, ρ, σ⟩ be a circular proof over S, T ∈ S(𝒞), let Z = fv_{l}(Π) and and W = fv_{r}(Π). The natural system of equations ∥Π∥ is the tuple

⟨G_{0}, C_{Π}, 𝒞_{S,T} , ∥ρ(−)∥, β⟩ ,

where

• The indexing set is G_{0}, the set of vertexes of Π. The set of bounded indexes is C_{Π}, i.e. those g ∈ G_{0} such that ρ(g) ≠ A.

• If λ(g) = s ⊢ t, recall that ∥s∥_{S}^{Z} : 𝒞^{Z}  ^{}𝒞 and ∥t∥_{T}^{W} : 𝒞^{W}  ^{}𝒞.

Therefore we let 𝒞_{S,T} (g) be the functor

𝒞(∥s∥_{S}^{Z}, ∥t∥_{T}^{W}) : (𝒞^{Z})^{op} × 𝒞^{W}  ^{}𝒮et .

• If ρ(g) ≠ A, then we let

β_{g} = { σ_{g,i} | i ∈ Arity(ρ(g)) } ,

• ∥ρ(−)∥ has the form

∥ρ(g)∥(σ_{g,i})_{i∈Arity(ρ(g))} ,

where

∥Cf∥ = f
∥CH∥(h_{i})_{i∈[n]} = H(h_{1}, …, h_{n})
∥L_{⋀I}_{i}∥(h) = pr_{i} · h
∥R_{⋀I}∥(h_{i})_{i∈I} = ⟨h_{i}⟩_{i∈I}
∥L_{⋁I}∥(h_{i})_{i∈I} = {h_{i}}_{i∈I}
∥R_{⋁I}_{i}∥(h) = h · in_{i}
∥Lμx∥(h) = χ^{−1} · h
∥Rx_{μ}∥(h) = h · χ
∥Ly_{ν}∥(h) = ς · h
∥Rνy∥(h) = h · ς^{−1}

Above, χ is the arrow part of the choice of initial algebras of the functor ∥q_{x}∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}, respectively ∥q_{x}∥_{T_{x}}^{(x)_{↓_{T}} ∪W}, and ς is the arrow part of the chosen final coalgebra of the similar functorial expression. 4.10

We shall represent the system ∥Π∥ with the more compact notation

C_{Π} = ∥Π∥(C_{Π}, A_{Π}) .

Theorem 4.11 The system ∥Π∥ admits a unique (natural) solution

∥Π∥^{†} : ∏_{g∈A_{Π}} C_{S,T} (g) ^{}∏_{g∈C_{Π}} C_{S,T} (g) .

Proof. The proof is by induction on #Π. To begin with, observe that if

card C_{Π} = 0 ,

then the result is obviously true, and that if

card C_{Π} > 0 ,

then a proof is either strongly connected or not. Therefore, if it is possible to argue as follows.

Suppose Π is not strongly connected: let g_{1}, g_{2} ∈ C_{Π} and suppose that there is no path from g_{1} to g_{2}. Let Π_{1} = \overline{Π, g_{1}} and Π_{2} = Π^{C_{Π_{1}}}. Hence, we decompose ∥Π∥ as

\{ \begin{matrix}C_{Π_{1}} & = & ∥Π_{1}∥(C_{Π_{1}}, A_{Π_{1}}) \\ C_{Π_{2}} & = & ∥Π_{2}∥(C_{Π_{2}}, C_{Π_{1}}, A_{Π}) \end{matrix} \}

Since g_{1} is a conclusion of Π_{1}, g_{1} is not a conclusion of Π_{2}, and therefore card C_{Π_{2}} < card C_{Π}; and since g_{2} ∈ C_{Π} \ C_{Π_{1}} we have C_{Π_{1}} < card C_{Π}. By the induction hypothesis ∥Π_{1}∥, ∥Π_{2}∥ admit a unique solution in the proper categories of functors from (𝒞^{fv_{l}(Π_{j})})^{op} ×𝒞^{fv_{r}(Π_{j})} for j = 1, 2. Since fv_{i}(Π_{j}) ⊆ fv_{i}(Π) for i ∈ {l, r} and j = 1, 2, then we conclude that the above circular proofs admit also a unique solution in the category of functors from (𝒞^{fv_{l}(Π)})^{op} × 𝒞^{fv_{r}(Π)}, by 1.3. We conclude that also ∥Π∥ admits a unique solution, using the Bekič lemma. We shall therefore assume that Π is strongly connected. In this case we can find a cycle γ which visits every g ∈ C_{Π}. Suppose that this cycle satisfies L(γ) – a dual argument can be carried out if only the statement R(γ) is satisfied – and let x = min γ_{S}. We can also suppose that each assumption of Π is reachable from an element g ∈ C_{Π}, hence from any element of C_{Π}, since the unique solution of this system depends only on the proof \overline{Π, C_{Π}}. It follows that if λ(g) = s_{g} ⊢ t_{g}, then fv(s_{g}) ⊆ fv(S) ∪ (x)_{↓_{S}} ∪ (x)_{↑_{S}}. Let

A = { g ∈ G_{0} | ρ(g) = Lμx } ,

and Π_{2} = Π^{A}. Recall that, if g ∈ A, then there exists a unique vertex g′ such that g → g′ is a transition of G(Π); we shall denote Sg such vertex, and let t_{g} ∈ T (𝒞) be such that λ(g) = x ⊢ t_{g} and λ(Sg) = q_{x} ⊢ t_{g}. If we let ∥Lμx∥ be the system

{ g = ∥Lμx∥(Sg) }_{g∈A} ,

we obtain a decomposition of ∥Π∥ as

\{ \begin{matrix}A & = & ∥Lμx∥(C_{Π_{2}}, A, A_{Π}) \\ C_{Π_{2}} & = & ∥Π_{2}∥(C_{Π_{2}}, A, A_{Π}) \end{matrix} \} .

By construction, in Π_{2} there are no rules of the form Lμx, hence we can free all bounded variables y ≤_{S} x from S and let the circular proof Π_{2} be over the directed systems S_{x} and T. Since card X_{S_{x}} < card X_{S}, by the induction hypothesis the system ∥Π_{2}∥ admits a unique natural solution ∥Π_{2}∥_{x}^{†} over S_{x}, T; if we apply back the substitution functor [ ∥y∥_{S}^{Z}/y]_{y≤_{S}x}, we see that ∥Π_{2}∥ admits the unique solution ∥Π_{2}∥_{[∥y∥_{S}^{Z}/y]_{y≤_{S} x}}^{†} over S, T, by the remark 1.3 and lemma 4.5. Thus, we have reduced existence and uniqueness of a solution of ∥Π∥, to existence and uniqueness of a solution of

A = ∥Lμx∥(A, ∥Π_{2}∥_{[∥y∥_{S}^{Z}/y]_{y≤_{S} x}}^{†}(A, A_{Π}), A_{Π}) ,

as usual, from the Bekič lemma. This system has the form

{ g = χ−1 ; z⃗ · α_{∥x∥_{S}^{Z} z⃗,z⃗,w⃗}^{g}(A, A^{Π}) }_{g∈A}

where for each g ∈ G

α^{g} = \{ \begin{matrix}∥Π_{2}∥_{[x,∥y∥_{S}^{Z}/y]_{y<_{S} x}}^{†} · pr_{Sg} , & Sg ∈ C_{Π_{2}} \\ pr_{Sg} , & otherwise . \end{matrix}

Let

S(x, z⃗) = ∥q_{x}∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[x, ∥y∥_{S}^{Z}/y]_{y<_{S}x}
: 𝒞 × 𝒞^{Z} ^{}𝒞 ,
T w⃗ = ∏_{g∈A} ∥t_{g}∥_{T}^{W} : 𝒞^{W}  ^{}𝒞 ,

and let Q(x, z⃗, w⃗) be

∏_{a∈A_{Π}} 𝒞( ∥s_{a}∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[x, ∥y∥_{S}^{Z}/y]_{y<_{S}x} , ∥t_{a}∥_{T}^{W} )

: 𝒞^{op} × (𝒞^{Z})^{op} × 𝒞^{W} ^{}𝒮et .

Observe that for g ∈ A the domain of α^{g} is

∏_{a∈A} 𝒞(x, ∥t_{a}∥_{T}^{W}) × Q(x, z⃗, w⃗) ,

since ∥x∥_{S_{x}}^{(x)_{↓_{S}} ∪Z}[x, ∥y∥_{S}^{Z}/y]_{y<_{S}x} is equal to the projection functor on x, where its codomain is 𝒞(S(x, z⃗), ∥t_{g}∥_{T}^{W}). If we let α_{x} = ⟨α_{x}^{g}⟩_{g∈A}, under natural isomorphism, we have

α_{x,z⃗,w⃗} : C(x, T w⃗) × Q(x, z⃗, w⃗) ^{}C(S(x, z⃗), T w⃗)

and therefore, the existence and uniqueness of a solution of the previous system follows from 3.1. □

5 Conclusions and future work

The calculus presented in this paper satisfies the cut elimination, in a sound way. This can be made precise as follows.

Definition 5.1 A pointed circular proof is a pair ⟨Π, g_{0}⟩, where Π = ⟨G, λ, ρ, σ⟩ is a circular proof and g_{0} ∈ G_{0}. We call g_{0} the conclusion of ⟨Π, g_{0}⟩ and say that this pair is a proof of s ⊢ t if λ(g_{0}) = s ⊢ t. We say that a pointed circular proof ⟨Π, g_{0}⟩ is reachable if the pointed graph ⟨G(Π), g_{0}⟩ is reachable. 5.1

A pair (s, S), where S ∈ S(𝒞) and s ∈ T (𝒞), is said to be closed if fv(S) = ∅ and fv(s) ⊆ X_{S}. By writing

Π_{g_{0}} : (s, S) ^{}(t, T)

we mean that Π_{g_{0}} = ⟨Π, g_{0}⟩ is a reachable pointed circular proof over S, T such that λ(g_{0}) = s ⊢ t and moreover that A_{Π} = ∅ and (s, S), (t, T) are closed pairs. If fv(S) = ∅ and fv(s) ⊆ X_{S}, then ∥s∥_{S}^{∅} : 𝒞^{∅} ^{}𝒞 can be identified with an object of 𝒞. Hence, if Π_{g_{0}} : (s, S) ^{}(t, T), then

∥Π_{g_{0}}∥ : ∏_{g∈∅} 𝒞_{S,T} (g) ^{}𝒞(∥s∥_{S}^{∅}, ∥t∥_{T}^{∅})

can be identified with an arrow from ∥s∥_{S}^{∅} to ∥t∥_{T}^{∅}.

Definition 5.2 For Π_{g_{0}} : (s, S) ^{}(t, T), we let ∥Π_{g_{0}}∥ be ∥Π∥^{†} · pr_{g_{0}}. 5.2

Proposition 5.3 Let Π_{g_{0}} : (s, S) ^{}(t, T) and Γ_{h_{0}} : (t, T) ^{}(u, U) be pointed circular proofs. There is an algorithm to construct a pointed circular proofs Π_{g_{0}}; Γ_{h_{0}} : (s, S) ^{}(u, U) with the property that ∥Π_{g_{0}}; Γ_{h_{0}}∥ = ∥Π_{g_{0}}∥; ∥Γ_{h_{0}}∥.

The construction is analogous to the usual cut elimination procedure and allows to consider circular proofs as algorithms. For example, let S_{n} be the system

⟨ { x_{n} =_{μ} x_{n−1} ∨ x_{n} ⋮ x_{1} =_{μ} ⊤ ∨ x_{1} } , {x_{n}}⟩ .

The interpretation ∥x_{n}∥_{S_{n}}^{∅} in the category 𝒮et is ℕ^{n}, the n-power of the set of natural numbers; moreover every tuple of natural numbers (k_{n}, …, k_{1}) can be coded as a pointed reachable circular proof from (⊤, ∅) to (x_{n}, S_{n}). If Π_{g} is a circular proof from (x_{n}, S_{n}) to (x_{m}, S_{m}), it is possible to apply the cut elimination procedure, to calculate the result of ∥Π_{g}∥. The proposed calculus is not complete enough to describe all the arrows in a free μ-bicomplete category. Indeed the diagonal Δ : ℕ ^{}ℕ^{2} arises as the unique algebra morphism from the initial one to the algebra ⟨⟨0, 0⟩, s × s⟩ : 1 + ℕ^{2} ^{}ℕ^{2}, which is definable in the calculus being the interpretation of the proof of example 2.21 (here s is the successor function).

Proposition 5.4 There is no pointed reachable circular proof Π_{g} : (x_{1}, S_{1}) ^{}(x_{2}, S_{2}) such that ∥Π_{g}∥ is the diagonal.

The above result is analogous to the well known fact that the set of words { a^{n}b^{n} | n ≥ 0 } is not recognizable and indeed the computation which arises under the cut elimination is similar to computation with automata. The above result shows that the ideas presented in this paper and the syntax of the calculus have to be generalized in order to describe free μ-bicomplete categories. However, it seems likely that the calculus presented here describes all the computations requiring bounded space.

References

[AAV00] P. Aczel, J. Adámek, and J. Velebil. Iteration monads.

        Preprint, available at http://math.feld.cvut.cz/velebil/,

November 2000.

[Acz88] P. Aczel. Non-well-founded sets. Stanford University Center for the Study of Language and Information, Stanford, CA, 1988.

[AJ94] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59(2):543–574, 1994.

[AK79] J. Adámek and V. Koubek. Least fixed point of a functor. J. Comput. System Sci., 19(2):163–178, 1979.

[AR94] J. Adámek and J. Rosický. Locally presentable and accessible categories. Cambridge University Press, Cambridge, 1994.

[Bar91] M. Barr. ∗-autonomous categories and linear logic. Math. Structures Comput. Sci., 1(2):159–178, 1991.

[Bar93] M. Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 114(2):299–315, 1993.

[BÉ93] S. L. Bloom and Z. Ésik. Iteration theories. Springer-Verlag, Berlin, 1993. The equational logic of iterative processes.

[Bla72] A. Blass. Degrees of indeterminacy of games. Fund. Math., 77(2):151–166, 1972.

[Bla92] A. Blass. A game semantics for linear logic. Ann. Pure Appl. Logic, 56(1-3):183–220, 1992.

[Coq94] T. Coquand. Infinite objects in type theory. In Types for proofs and programs (Nijmegen, 1993), pages 62–78. Springer, Berlin, 1994.

[CP90] T. Coquand and C. Paulin. Inductively defined types. In COLOG-88 (Tallinn, 1988), pages 50–66. Springer, Berlin, 1990.

[CS97] J.R.B. Cockett and R.A.G. Seely. Weakly distributive categories. J. Pure Appl. Algebra, 114(2):133–173, 1997.

[CS01] J.R.B. Cockett and R.A.G. Seely. Finite sum-product logic. Theory and Applications of Categories, 8:63–99, 2001.

[Fre91] P. Freyd. Algebraically complete categories. In Category theory (Como, 1990), pages 95–104. Springer, Berlin, 1991.

[GH82] Y. Gurevich and L. Harrington. Trees, automata, and games. In Proc. 14th ACM Symp. on the Theory of Computation, pages 60–65, 1982.

[Gir87] J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50(1):101, 1987.

[Gir01] J.-Y. Girard. Locus solum. To appear in Math. Struct. in Comp. Science, january 2001.

[GTL89] J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and types. Cambridge University Press, Cambridge, 1989.

[HJ99] H. Hu and A. Joyal. Coherence completions of categories. Theoret. Comput. Sci., 227(1-2):153–184, 1999. Linear logic, I (Tokyo, 1996).

[Hoa85] C.A.R. Hoare. Communicating sequential processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985. With a foreword by Edsger W. Dijkstra.

[HS86] J.R. Hindley and J.P. Seldin. Introduction to combinators and λ-calculus. Cambridge University Press, Cambridge, 1986.

[Joy95] A. Joyal. Free bicomplete categories. C. R. Math. Rep. Acad. Sci. Canada, 17(5):219–224, 1995.

[Joy97] A. Joyal. Free lattices, communication, and money games. In Logic and scientific methods, pages 29–68, 1997. Proceedings of the 10th international congress of logic, methodology and philosophy of science, Florence, Italy, August 19–25, 1995.

[Lam68] J. Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151–161, 1968.

[LS88] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, Cambridge, 1988. Reprint of the 1986 original.

[ML90] P. Martin-Löf. Mathematics of infinity. In COLOG-88 (Tallinn, 1988), pages 146–197. Springer, Berlin, 1990.

[ML98] S. Mac Lane. Categories for the working mathematician. Springer-Verlag, New York, second edition, 1998.

[Mos00] L. S. Moss. Parametric corecursion. Preprint, available at

http://math.indiana.edu/home/moss/, 2000.

[NYY92] A. Nerode, A. Yakhnis, and V. Yakhnis. Concurrent programs as strategies in games. In Logic from computer science (Berkeley, CA, 1989), pages 405–479. Springer, New York, 1992.

[Rut00] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3–80, 2000. Modern algebra and its applications (Nashville, TN, 1996).

[San00a] L. Santocanale. The alternation hierarchy for the theory of μlattices. Technical report, BRICS, November 2000. Submitted for a special issue of Theory and Applications of Categories, in occasion of CT2000.

[San00b] L. Santocanale. Free μ-lattices. Technical report, BRICS, November 2000. To appear in a special issue of the Journal of Pure and Applied Algebra, in occasion of Category Theory 99.

[San00c] L. Santocanale. Sur les μ-treillis libres. PhD thesis, Université du Québec à Montréal, July 2000.

[Sei96] H. Seidl. Fast and simple nested fixpoints. Inform. Process. Lett., 59(6):303–308, 1996.

[Wal00] I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Inform. and Comput., 157(1-2):142– 182, 2000. LICS 1995 (San Diego, CA).

[Win93] G. Winskel. The formal semantics of programming languages. MIT Press, Cambridge, MA, 1993. An introduction.

[Zie98] W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci., 200(1-2):135–183, 1998.

Recent BRICS Report Series Publications

RS-01-15 Luigi Santocanale. A Calculus of Circular Proofs and its Categorical Semantics. May 2001. 30 pp.

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From Hierarichcal

Timed Automata to Uppaal. March 2001.

RS-01-10 Daniel Fridlender and Mia Indrika. Do we Need Dependent Types? March 2001. 6 pp. Appears in Journal of Functional Programming, 10(4):409–415, 2000. Superseeds BRICS Report RS-98-38.

RS-01-9 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. Static Validation of Dynamically Generated HTML. February 2001. 18 pp.

RS-01-8 Ulrik Frendrup and Jesper Nyholm Jensen. Checking for Open Bisimilarity in the π-Calculus. February 2001. 61 pp.

RS-01-7 Gregory Gutin, Khee Meng Koh, Eng Guan Tay, and Anders Yeo. On the Number of Quasi-Kernels in Digraphs. January 2001. 11 pp.

RS-01-6 Gregory Gutin, Anders Yeo, and Alexey Zverovich. Traveling Salesman Should not be Greedy: Domination Analysis of Greedy-Type Heuristics for the TSP. January 2001. 7 pp.

RS-01-5 Thomas S. Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear Parametric Model Checking of Timed Automata. January 2001. 44 pp. To appear in Margaria and Yi, editors, Tools and Algorithms for The Construction and Analysis of Systems: 7th International Conference, TACAS ’01 Proceedings, LNCS, 2001.