Dale Miller

Arnaud Carayol

Panos Rondogiannis

Lars Birkedal
email: birkedal@itu.dk

Marek Czarnecki
email: marek.czarnecki@gmail.com

Hervé Grall

Paul Blain Levy

Matteo Mio

Keiko Nakata

Andrei Romashchenko

Dietmar Berwanger

Martín Escardó

Martin Lange

Richard Mckinley

Dieter Probst

Joshua Sack

Thorsten Altenkirch

' Agostino

Peter Dybjer

Zoltán Ésik

Anna Ingólfsdóttir

Gerhard Jäger

Ralph Matthes

Andrzej Murawski

Damian Niwinski

Luigi Santocanale

Alex Simpson

Jean-Marc Talbot

Tarmo Uustalu

Yde Venema

Igor Walukiewicz

Tony Kučera

Tomáš Brázdil

Jan Schwinghammer

Kristian Støvring

Paweł Waszkiewicz

A Metric Model of Lambda Calculus with Guarded Recursion

Keywords: B, B, ∆ B, ∆ B, B ⊥ initial Fixed Points in Computer

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Fixed Points in Computer Science 2010

Brno, August 21-22, 2010

Structures defined by higher-order recursion schemes

Arnaud Carayol LIGM Université Paris-Est and CNRS 5, boulevard Descartes, Champs-sur-Marne F-77454 Marne-la-Vallée Cedex 2 carayol@univ-mlv.fr

Higher-order recursion schemes are a particular form of typed term rewriting systems. By iterative rewriting from a fixed finite term, an (higher-order) recursion scheme generates at the limit an infinite term. In 2006, Luke Ong has shown that for the infinite terms obtained in this way monadic secondorder logic (MSO) is decidable. As terms defined by recursion schemes encompass most of the known examples of infinite terms having decidable MSO theory, this result has revived the interest for recursion schemes.

In this talk, we will survey results concerning the structures defined by recursion schemes. These structures are essentially graphs which can be defined using MSO logic on the terms generated by recursion schemes. Our main focus will be to assess the expressivity of these structures through alternative characterisations.

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. Fixed points and proof theory:

An extended abstract

Potentially unbounded behavior is available in proof theory via the contraction rule (see Figure 1): when reading this rule from its conclusion to its premise, a formula is duplicated and such duplication can be applied again and again. When contraction is removed, decidability often follows. For example, the multiplicative-additive fragment of linear logic (MALL) does not have contraction (nor weakening) and, as a result, it is decidable whether or not a formula is a theorem. It is possible to given a proof system for propositional intuitionistic logic that does not contain contraction [9]: a naive implementation of that proof system can be a decision procedure for that logic.

Decidable logics, such as MALL and propositional intuitionistic logic, have rather limited applications. For a logic and proof system to find wide ranging applications in, say, computation and deduction, they must allow for potentially infinite behaviors.

Girard designed linear logic to be the result of extending MALL with the exponentials (!, ?): the proof rules of contraction and weakening are allowed only on formulas marked by such exponentials. In this way, potentially infinite behaviors can be mixed with MALL: linear logic becomes undecidable in this way (even the propositional fragment of linear logic is undecidable [12]).

While the addition of the exponentials to MALL is elegant and powerful, the exponentials are not without problems for those working in computational logic. For example, when using (as we will) focused proof systems, the exponentials can cause focusing phases to terminate. Furthermore, exponentials are not canonical: that is, if one allows a "red" version and a "blue" version of both of ! and ?, it is not possible to prove them equivalent (all other connectives of linear logic are canonical in this sense). While there are interesting uses for such non-canonical exponentials (see, for example, the material on subexponentials in [START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF]) one would like to have alternative approaches to potentially infinite behavior in proof systems.

Baelde and Miller have proposed another approach to extending MALL with potentially infinite behavior: in particular, they have added the least and greatest fixed points directly to MALL [6,3]. The resulting logic is surprisingly elegant and expressive: it has been used to describe the logical foundations of a model checker [5] and is being used to design a new theorem proving architecture for the search for proofs involving induction [7]. The development of a focused proof system for MALL plus fixed points has lead to some new proof theory phenomena as well as some new ways to approach the unity of such different topics as computation, model checking, and inductive and co-inductive theorem proving.

This extended abstract will illustrate some of the proof theory of fixed points by concentrating on adding fixed points to classical first-order logic. Parts of this abstract are based on similar material found in [14].

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 9-16

A focused proof system for classical logic

We now consider propositional classical logic over formulas built from ∧, ∨, t, f . Remarkably, we shall not have a need for atomic formulas. Figure 1 contains a one-sided sequent calculus proof systems for this logic. A sequent ∆ contains a multiset of formulas ∆. Besides containing the usual structural rules and identity rules (initial and cut), the logical connectives have two sets of introduction rules. That is, for each logical connective, there is a set of multiplicative rules and a set of additive rules for it. (The set of additive rules for f is empty and the set of additive rules for ∨ contains two rules.) Notice that the rules for the additive conjunction and the multiplicative disjunction are invertible while the rules for the multiplicative conjunction and the additive disjunction are not necessarily invertible.

The cut rule is admissible and the initial rule is admissible for all but atomic formulas. Since we have no atomic formulas, both identity rules can be dropped.

As is well known, the additive rule and the multiplicative rule for the same connective are interadmissible in the presence of the structural rules of contraction and weakening. Another way to state this admissibility statement is the following. Annotate names of the connectives in the inference rules as follows: the invertible rules are annotated as negative ∧ -and ∨ -while the not-necessarily-invertible rules are annotated as positive ∧ + and ∨ + (annotate their units also to be t -, f -, t + , f + ). Given a formula B let B be any polarization of B in which every logical connectives in B is given either a plus or a minus annotation. Then, B is provable (in the unannotated proof system) if and only if B is provable (in the annotated proof system). We shall say that an annotated formula is negative if its top-level logical connective is annotated negatively and is positive if its top-level logical connective is annotated positively. By B ⊥ we shall mean the negation normal form of B: since we have no atomic formulas, negations will not occur within formulas. Notice that the de Morgan dual of ∨ + and ∧ + are, respectively, ∧ -and ∨ -.

If we try to take the construction of proofs literally as a model for performing computation, one is immediately struck by the inappropriateness of sequent calculus rules in Figure 1 for this task: there are just too many ways to build proofs and most of them differ in truly minor ways. One would like to have a tight correspondence between the application of inference rules and "actions" within a computation. An early attempt to provide the sequent calculus with normal forms that corresponded to computation was the work on uniform proofs and backchaining [15] that provided a proof-theoretic foundation for logic programming. It was, however, Andreoli's focused proof system [1] for linear logic that really allowed one to more richly restrict and organize the sequent calculus. The earlier work on uniform proofs was Fixed points and proof theory: An extended abstract Miller Structural rules:

Θ, P ⇑ Γ Θ ⇑ Γ, P Store Θ ⇑ N Θ ⇓ N Release P, Θ ⇓ P P, Θ ⇑ • Focus Negative phase: Θ ⇑ Γ,t - Θ ⇑ Γ, A Θ ⇑ Γ, B Θ ⇑ Γ, A ∧ -B Θ ⇑ Γ Θ ⇑ Γ, f - Θ ⇑ Γ, A, B Θ ⇑ Γ, A ∨ -B Θ ⇑ Γ, A Θ ⇑ Γ, ∀xA
Positive phase: rather limited, both in its range of "focusing behavior" and in the subsets of logic to which it could be applied. Andreoli's result, however, applied to a full and rich logic. Figure 2 presents the focused proof system for annotated propositional classical logic that is derived from the LKF proof system of Liang and Miller [11]. In that figure, P denotes a positive formula, N a negative formula, and Θ consists of positive formulas. The sequents in this proof system are of the form Θ ⇑ Γ and Θ ⇓ B where Θ is a multiset of formulas, Γ is a list of formulas, and B is a formula. The inference rules used in the negative phase are invertible while those in the positive phase are not necessarily invertible. The structural rules contain two rules that allow switching between the two kinds of sequents. Notice also that the Focus rule incorporates the contraction rule.

Θ ⇓ t + Θ ⇓ A Θ ⇓ B Θ ⇓ A ∧ + B Θ ⇓ A i Θ ⇓ A 1 ∨ + A 2 Θ ⇓ A[t/x] Θ ⇓ ∃xA
Theorem 1. LKF is sound and complete for classical logic. More precisely, let B be a first order formula and let B be a polarization of B. Then B is provable in classical logic if and only if there is an LKF proof of • ⇑ B [11].

Notice that polarization does not affect provability but it does affect the shape of possible LKF proofs. Focused proof systems such as LKF allow us to change the size of inference rules with which we work. Let us call individual introduction rules (such as in Figures 1 and2) "micro-rules." An entire phase within a focused proof (the collecting together of only ⇑ sequents or only ⇓ sequent) can be seen as a "macro-rule." In particular, consider the following derivation

Θ, D ⇑ N 1 • • • Θ, D ⇑ N n • • • only ⇓ sequents here • • • Θ, D ⇓ D Θ, D ⇑ •
Here, the selection of the formula D for the focus can be taken as selecting among several macro-rules: this derivation illustrates one such macro-rule: the inference rule with conclusion Θ, D ⇑ • and with n ≥ 0 premises Θ, D ⇑ N 1 , . . . , Θ, D ⇑ N n (where N 1 , . . . , N n are negative formulas). We shall say that this macro-rule is positive. Similarly, there is a corresponding negative macro-rule with conclusion, say, Θ, D ⇑ N i , and with m ≥ 0 premises of the form Θ, D, C ⇑ •, where C is a multiset of positive formulas or negative literals. In this way, focused proofs allow us to view the construction of proofs from conclusions of the form Θ ⇑ • by first attaching a positive macro rule (by focusing on some formula in Θ) and then attaching negative inference rules to the resulting premises until one arrives again to sequents of the form Θ ⇑ •. Such a combination of a positive macro rule below negative macro rules is often called a bipole [2].

Fixed points and proof theory: An extended abstract

∆σ u = v, ∆ † u = v, ∆ ‡ u = u, ∆
The † proviso requires the terms u and v to be unifiable and σ to be their most general unifier. The ‡ proviso requires that the terms s and t are not unifiable. The usual eigenvariable condition holds for y in the ∀ introduction rule. 3 Fixed points and first-order structure

To classical logic we shall now add the two fixed point constructors µ and ν, the two first-order quantifiers ∀ and ∃, and the two comparison relations on first-order terms = and =. Notice that each pair of these connectives forms a de Morgan dual. The connectives µ and ν are really a collection {µ n } n≥0 and {ν n } n≥0 such that the simple type of µ n and of ν n is τ n → τ n , where τ n is i → . . . → i → o (n occurrences of the type i). We shall not write the subscripted arity. Notice that all six of these constants are logical connectives in the sense that they all have introduction rules: furthermore, the identity rules (cut and initial) are admissible. The (unfocused) proof rules for these additional connectives are given in Figure 3.

The rules for equality and its negation are due to Schroeder-Heister [START_REF] Schroeder-Heister | Rules of definitional reflection[END_REF] and Girard [10].

Example 2. Identify the natural numbers as terms involving 0 for zero and s for successor. The following simple logic program defines two predicates on natural numbers.

nat 0 ⊂ true. nat (s X) ⊂ nat X. leq 0 Y ⊂ true. leq (s X) (s Y ) ⊂ leq X Y.

The predicate nat can be written as the fixed point µ(λ pλ x.(x = 0) ∨ + ∃y.(s y) = x ∧ + p y) and binary predicate leq (less-than-or-equal) can be written as the fixed point µ(λ qλ xλ y.(x = 0) ∨ + ∃u∃v.(s u) = x ∧ + (s v) = y ∧ + q u v).

In a similar fashion, any Horn clause specification can be made into fixed point specifications (mutual recursions requires standard encoding techniques). Notice the use of positively annotated logical connectives here.

Following the usual convention of classifying invertible introduction as negative connectives, ∀ and = are negative and their duals ∃ and = are positive. Since the two fixed points are (currently) indistinguishable (they have the same introduction rules), we arbitrarily classify µ as positive and ν as negative. The focused versions of the introduction rules for these connectives is given in Figure 4. Notice now that focusing phases can involve long chains of unfoldings. For example, the fixed points in Example 2 are encoded using entirely positive connectives. Thus, if the focused sequent Θ ⇓ leq m n has a proof, it has a proof that involves exactly one macro-rule. As the following example illustrates, it is now possible to put an arbitrary (Horn clause) computation within a (macro) rule.

Miller Θ ⇓ B[t/x] Θ ⇓ ∃x.B Θ ⇑ Γ, B[y/x] Θ ⇑ Γ, ∀x.B Θ ⇓ u = u Θσ ⇑ Γσ Θ ⇑ Γ, u = v † Θ ⇑ Γ, u = v ‡ Θ ⇑ Γ, B(νB) ū Θ ⇑ Γ, νB ū Θ ⇓ B(µB) ū Θ ⇓ µB ū
Figure 4: Focused inference rules for = and µ. The proviso † and ‡ and the definition of σ are the same as above.

Example 3. Consider proving the positive focused sequent

Θ ⇓ (leq m n ∧ + N 1 ) ∨ + (leq n m ∧ + N 2 ),
where m and n are natural numbers and leq is the fixed point expression displayed above. If both N 1 and N 2 are negative formulas, then there are exactly two possible macro rules with this conclusion: one with premise Θ ⇑ N 1 when m ≤ n and one with premise Θ ⇑ N 2 when n ≤ m (thus, if m = n, either premise is possible). In this sense, a macro inference rule can contain an entire Prolog-style computation.

The following example illustrates that fixed points can be used to describe a typical query from model checking.

Example 4. Assume that first-order terms encode process and action expressions such as are found in CCS. The usual notion of one-step transition can generally be written using a simple, recursive Horn clause program: hence, the ternary relation P A -→ P can be encoded using a purely positive formula. The notion of simulation is then the (greatest) fixed point of the equivalence

sim P Q ≡ ∀P ∀A[P A -→ P ⊃ ∃Q [Q A -→ Q ∧ sim P Q ]].
We can then chose to write the sim relation as the expression

νλ sλ Pλ Q.∀P ∀A[P A -→ P ⊃ ∃Q [Q A -→ Q ∧ s P Q ]]
(Here, we are assuming that the implication B ⊃ C is rendered as B ⊥ ∨ -C in the polarized setting.) Although the body of this definition looks complex, it is, in fact, composed of exactly two "macro connectives" (a bipole). The expression ∀P ∀A[P A -→ P ⊃ •] is a purely negative formula and its "introduction" is invertible: since all possible actions A and continuations P must be computed, there are no choices to be made in building a proof for this expression. On the other hand, focusing on the expression

∃Q [Q A -→ Q ∧ + •]
yields a non-invertible, positive macro rule. In this way, the focused proof system is aligned directly with the structure of the actual (model-checking) problem.

The fact that an entire computation can fit within a macro rule (using purely positive fixed point expressions) provides a great deal of flexibility in designing inference rules. Such flexibility allows inference rules to be designed so that they correspond to an "action" within a given computational system. If one takes seriously using only macro rules (and hiding the details of the micro rules) then placing arbitrary computation within a macro inference rule is probably too much: the term "inference rule" is usually reserved for decidable steps. Thus, some care should be exercised in balancing the complexity of a macro rule with the needs of proof systems to have their correctness be decidable.

Fixed points and proof theory: An extended abstract Miller

Γ, B(µB) ū Γ, µB ū µ Γ, S ū BSx, (Sx) ⊥ Γ, νB ū ν µB ū, ν B ū µν
The variable S denotes a closed term of type τ n , where the arity of ν is n. Also, x is an eigenvariable of the proof. Large macro rules can easily be broken up, if desired, by the use of delays. Within LKF, we can define the delaying operators

∂ + (B) = B ∧ + t + and ∂ -(B) = B ∧ -t -.
Clearly, B, ∂ -(B), and ∂ + (B) are all logically equivalent but ∂ -(B) is always negative and ∂ + (B) is always positive. If one wishes to break a positive macro rule resulting from focusing on a given positive formula into smaller pieces, then one can insert ∂ -(•) into that formula. Similarly, inserting ∂ + (•) can limit the size of a negative macro rule. By inserting many delay operators, a focused proof can be made to emulate an unfocused proof [11].

Induction and co-induction rules

Treating fixed points simply by unfolding is, of course, limited. For example, while it is easy to define fixed points that describe the notions of "natural number", "even", and "odd", it is not possible to prove that every natural number is either even or odd. While one can simply write the appropriate formula stating that theorem, attempts at proofs of it will lead only to potentially infinite unfoldings. What is missing, of course, is induction. To this end, consider the three inference rules displayed in Figure 5 (taken from [3,6]). Notice that the µν rule is the only form of the initial rule that we shall need in this proof system. Here, the negation B of a body B is defined as λ p.λ x.(B(λ x.(p x) ⊥ ) x) ⊥ . A body B is said to be monotonic when for any variables p and t, the negation normal and λ -normal form of Bp t does not contain any negated instance of p. We shall assume that all bodies are monotonic.

Notice that the rule called ν is the rule for co-induction. If we write sequents as two sided, then moving this rule to the left-side as an introduction rule for µ yields the usual induction rule. Thus, induction and co-induction are treated as perfect duals of each other. Proposition 5. The following inference rules are derivable:

P, P ⊥ init Γ, B(νB) ū Γ, νB ū νR
These results are standard, cf. [START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF]. The proof of the second one relies on monotonicity and is obtained by applying the ν rule with B(νB) as the co-invariant. As a result of this proposition, we can replace the inference rules for µ and ν given in Figure 3 with the rules in Figure 5. It is also the case that µ and ν are now canonical. Such canonicity is gained, however, by the rather "high-price" of using an inference rule (the ν rule) that involves a higher-order variable (the invariant).

Baelde [3,4] has proved the (relative) completeness of the focused inference rules in Figure 6 in the context of MALL: his proof involves some rather complex arguments for treating the higher-order nature of the induction/co-induction rule. That proof should, however, lift to the setting described here where classical logic replaces MALL.

Notice that in the ⇑ phase, one chooses between doing (co)induction on νB t and freezing the fixed point expression by moving it to the left of the ⇑. Since such a ν-expression is assigned a negative Fixed points and proof theory: An extended abstract Miller

Γ ⇑ S t, ∆ ⇑ BS x, S x ⊥ Γ ⇑ νB t, ∆ x new Γ, νB t ⇑ ∆ Γ ⇑ νB t, ∆ Γ ⇓ B(µB) x Γ ⇓ µB x νB x ⇓ µB x
Figure 6: Focused proof rules for the fixed point connectives polarity, the Focus rule can never move it from the left of the arrow to the right. Thus, a ν-expression on the left of the ⇑ arrow can only be used to match its dual of the right ⇓ in the (focused version of the) µν rule. For more about these rules for (co)induction, see the Baelde's PhD thesis [3] or the theorem prover based on that work [7].

The unity of computational logic

The proof theory of fixed points offers us a framework for comparing and combining computation, model checking, and theorem proving. The differences between these three activities can be characterized by their different uses of fixed points. Logic programming involves may behavior only, which involves unfolding fixed points and non-deterministically picking a path to a success. On the other hand, both model checking and theorem proving deal with must as well as may behavior. These two differ in that model checkers generally assume finite fixed points (or have specialized methods for handling loops) while (inductive) theorem provers use invariants to characterize possible infinite unfoldings. Given these rough descriptions, it is possible to see rich ways that these activities can fit together into one system (and one logic!) and enhance each other: for example, a theorem prover might prove certain symmetry lemmas (via induction) and these could be used in the model checker to reduce search space. Similarly, tabling within model checkers can be seen as lemma generation in theorem provers [START_REF] Miller | Incorporating tables into proofs[END_REF]. Also, as we have seen, logic programming-style computation can be inserted within the inference rules used in both model checking and theorem proving.

Related work

The proof theory of fixed points described here is largely taken from the recent papers of Baelde [3,7]. While Baelde largely considered adding fixed point to MALL, he has also shown how that combination directly treats important subsets of intuitionistic logic. Miller and Saurin [START_REF] Miller | A game semantics for proof search: Preliminary results[END_REF] have also considered fixed points using dialog games which are known to be closely related to focused proof systems. This work builds on earlier work by McDowell, Miller, and Tiu [13,[START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF]. The work on cyclic proofs by, say, Santocanale [19] and Brotherston and Simpson [8], is a related but alternative approach to the treatment of induction within proofs.

Fixed-Point Semantics for Non-Monotonic Formalisms

Panos Rondogiannis Department of Informatics & Telecommunications, University of Athens, Greece prondo@di.uoa.gr

We examine two successful application domains for fixed-point theory, namely (non-monotonic) logic programming and Boolean grammars. We demonstrate that these two areas are quite close, and as a result interesting ideas from one area appear to have interesting counterparts in the other one.

Negation in Logic Programming: We present a recent [START_REF] Rondogiannis | Minimum Model Semantics for Logic Programs with Negation-as-Failure[END_REF] purely model-theoretic characterization of the semantics of logic programs with negation. The new semantics provides a logical basis for the classical well-founded semantics of logic programs [START_REF] Van Gelder | The Well-Founded Semantics for General Logic Programs[END_REF]. The proposed approach uses a truth domain that has an uncountable linearly ordered set of truth values between False (the minimum element) and True (the maximum), with a Zero element in the middle. Under the new semantics, every logic program with negation has a unique minimum model which can be constructed as the least fixed point of the immediate consequence operator of the program. The main benefits of the new construction is that it provides a purely logical characterization of negation-as-failure and a better understanding of the fixed-point semantics of non-monotonic logic programming.

Boolean Grammars: These new grammars [START_REF] Okhotin | Boolean Grammars[END_REF] extend the context-free ones by allowing conjunction and negation in the right hand sides of rules. It has been demonstrated that Boolean grammars can be parsed efficiently and that they can express interesting languages that are not context-free. Despite their simplicity, Boolean grammars proved to be non-trivial from a semantic point of view. In particular, the use of negation makes it difficult to define a simple derivation-style semantics (such as the familiar one for context-free languages). We present the well-founded construction for Boolean grammars [START_REF] Kountouriotis | Well-Founded Semantics for Boolean Grammars[END_REF], which provides the first general solution to the problem of assigning a proper meaning to every Boolean grammar. Our results indicate that many-valued formal language theory is the appropriate mathematical machinery underlying Boolean grammars.

Introduction

Recent work in semantics of programming languages and program logics has suggested that there might be a connection between metric spaces and Nakano's typed lambda calculus with guarded recursive definitions [8]. In this paper we show that is indeed the case by developing a model of Nakano's calculus in a category of metric spaces and by showing that the model is computationally adequate. The latter is done with the use of a logical relation, whose existence is non-trivial because of the presence of recursive types. We define the relation in a novel indexed way, inspired by step-indexed models for operational semantics [2].

For space reasons, we can only briefly hint at some of the motivating applications in semantics:

In [4], Birkedal et al. gave a model of a programming language with recursive types, impredicative polymorphism and general ML-style references. The model is a Kripke model, where the set of worlds is a recursively defined metric space (with the recursion variable in negative position). A simplified variant of the recursive equation can be formulated in a version of Nakano's calculus.

Pottier [9] has recently suggested to use Nakano's calculus as a calculus of kinds in an extension of F ω with recursive kinds, which can serve as a target calculus for a store-passing translation of a language with ML-style references. The model we present here can be extended to a model of F ω with recursive kinds by indexing complete uniform per's over metric spaces.

Hinze [6] has shown, in the context of Haskell streams, how the uniqueness of fixed points of contractive functions in an operational setting can be used for verification. Nakano's calculus can be used to formalize such arguments, and in our model unique fixed points for contractive functions do exist.

For reasoning about imperative interactive programs, Krishnaswami et al. [7] related an efficient imperative implementation to a simple model of functional reactive programming. In current unpublished work by Krishnaswami on extending this to higher-order programs, metric spaces are being used to model the functional reactive programs to capture that all uses of recursion are guarded. A logical relation is used to relate the functional reactive programs and the imperative implementation thereof; that logical relation is defined using ideas that seem similar to those we are using in our logical relation for the adequacy proof in Section 3.

In the remainder of the paper, we present (our version of) Nakano's calculus (Section 2), define the denotational semantics and prove that it is computationally adequate (Section 3), briefly discuss some closely related work (Section 4), and conclude with some comments about future work. In this section we recall the typed lambda calculus of Nakano [8]. It allows certain forms of guarded recursive definitions, and tracks guardedness via a modality in the type system. We shall show that this modality can be understood semantically as a scaling operation of the distances in a metric space. The precise language considered below differs from that presented by Nakano in [8] in that we assume a fixed number of "global" (possibly mutually recursive) datatype declarations. In contrast, Nakano includes equi-recursive types of the form µX.A (subject to some well-formedness conditions that ensure formal contractiveness, and a type equivalence relation).

Γ t : τ τ ≤ σ Γ t : σ Figure 1: Typing rules of Nakano's lambda calculus τ ≤ σ • τ ≤ • σ τ ≤ τ σ ≤ σ τ → σ ≤ τ → σ τ ≤ τ σ ≤ σ τ × σ ≤ τ × σ τ ≤ • τ τ → σ ≤ • τ → • σ • τ → • σ ≤ •(τ → σ ) τ × σ ≤ • τ × • σ • τ × • σ ≤ •(τ × σ )
Syntax and typing. We assume that there is a fixed number of type identifiers ty 1 , . . . , ty n , each associated with a recursive data type equation in the style of Haskell or ML that specifies constructors In i,1 , . . . , In i,k i :

data ty i = In i,1 of τ i,1 | . . . | In i,k i of τ i,k i . (1)
The types τ i,1 , . . . , τ i,k i that appear on the right hand side of (1) are built up from ground types b (for simplicity, we restrict ourselves to Int) and the identifiers ty 1 , . . . , ty n , using product and function space and the unary type constructor '•' (referred to as 'later' modality in recent work on step-indexed semantics [3]). One concrete instance of (1) is a type of infinite sequences of τ's: data seq τ = Cons of τ × seq τ . In general, these declarations need not be monotone, however, and the identifiers ty i may also appear in negative positions. For instance, Nakano [8, Ex. 1] considers the type data u = Fold of u → τ. With this type, the fixed point combinator Y from untyped lambda calculus has type (• τ → τ) → τ; thus, it is not necessary to include a primitive for recursion. Terms and their types are given in Figure 1. The type system uses the subtyping relation defined in Figure 2 (omitting the reflexivity and transitivity rules). Intuitively, the type • τ may be understood as the set of values of type τ that need to be guarded by a constructor. This intuition explains the two rules for typing constructor applications and pattern matching in Figure 1: The application of a constructor lets one remove the outermost modal operator, and it also folds the recursive type. Conversely, the case construct removes a constructor, and the typing rule records this fact by applying the modality to the type of the bound variables. The typing rules for function application and component projections are also generalized to take care of the modal operator. We write Tm(τ) for the set of closed terms of type τ.

Operational semantics and contextual equivalence. The operational semantics consists of the usual (deterministic, call-by-name) reduction rules of lambda calculus with constructor types. One does not reduce under constructors: every term of the form In i, j (t) is a value. We take contextual equivalence as our notion of program equivalence. Formally, we observe the values that terms yield when plugged into closing, base-type valued contexts: Let us write C :

(Γ τ ) (Γ τ) for a context C if Γ C[t]
: τ whenever Γ t : τ . Then t 1 and t 2 are contextually equivalent, written Γ t 1 t 2 : τ, if Γ t 1 : τ and Γ t 2 : τ, and for all C :

(Γ τ) ( / 0 Int) and n ∈ N, C[t 1 ] * → n ⇔ C[t 2 ] * → n.

Denotational Semantics

We give a denotational semantics of types and terms in the category of complete, 1-bounded ultrametric spaces and non-expansive maps between them.

Ultrametric spaces. We briefly recall some basic definitions and results about metric spaces [10]. A 1-bounded ultrametric space (X, d) is a metric space where the distance function d : X × X → R takes values in the closed interval [0, 1] and satisfies the "strong" triangle inequality d(x, y) ≤ max{d(x, z), d(z, y)}. A metric space is complete if every Cauchy sequence has a limit. Because of the use of max in the above inequality, rather than '+' as for the weaker triangle inequality of metric spaces in general, a sequence (x n ) n∈N in an ultrametric space (X, d) is a Cauchy sequence if for every ε > 0 there exists n ∈ N such that d(x k , x k+1 ) ≤ ε for every k ≥ n.

A function f :

X 1 → X 2 between metric spaces (X 1 , d 1 ), (X 2 , d 2 ) is non-expansive if d 2 ( f (x), f (y)) ≤ d 1 (x, y) for all x, y ∈ X 1 . It is contractive if there exists some δ < 1 such that d 2 ( f (x), f (y)) ≤ δ • d 1 (x, y)
for all x, y ∈ X 1 . The complete, 1-bounded, non-empty, ultrametric spaces and non-expansive functions between them form a Cartesian closed category CBUlt ne . Products are given by the set-theoretic product where the distance is the maximum of the componentwise distances. The exponential (X 1 , d 1 ) → (X 2 , d 2 ) has the set of non-expansive functions from (X 1 , d 1 ) to (X 2 , d 2 ) as underlying set, and the distance function is given by d

X 1 →X 2 ( f , g) = sup{d 2 ( f (x), g(x)) | x ∈ X 1 }. A functor F : (CBUlt op ne ) n × CBUlt n ne -→ CBUlt ne is locally non-expansive if d(F( f , g), F( f , g )) ≤ max{d( f 1 , f 1 ), d(g 1 , g 1 ), . . . , d( f n , f n ), d(g n , g n )} for all non-expansive f = ( f 1 , . . . , f n ), f = ( f 1 , . . . , f n ), g = (g 1 , . . . , g n ) and g = (g 1 , . . . g n ). It is locally contractive if there exists some δ < 1 such that d(F( f , g), F( f , g )) ≤ δ • max{d( f 1 , f 1 ), d(g 1 , g 1 ), . . . , d( f n , f n ), d(g n , g n )}.
Note that the factor δ is the same for all hom-sets. By multiplication of the distances of (X, d) with a non-negative shrinking factor δ < 1, one obtains a new ultrametric space, δ • (X, d) = (X, d ) where d (x, y) = δ • d(x, y). By shrinking, a locally non-expansive functor F yields a locally contractive functor

(δ • F)(X,Y ) = δ • (F(X,Y )).
It is well-known that one can solve recursive domain equations in CBUlt ne by an adaptation of the inverse-limit method from classical domain theory:

Theorem 1 (America-Rutten [1]). Let F i : (CBUlt op ne ) n × CBUlt n ne -→ CBUlt ne be locally contractive functors for i = 1, . . . , n. Then there exists a unique (up to isomorphism

) X = (X k , d k ) k ∈ CBUlt n ne such that (X i , d i ) ∼ = F i (X, X) for all i.
The metric spaces we consider below are bisected, meaning that all non-zero distances are of the form 2 -n for some natural number n ≥ 0. When working with bisected metric spaces, the notation x n = y means that d(x, y) ≤ 2 -n . Each relation n = is an equivalence relation because of the ultrametric inequality; we are therefore justified in referring to the relation n = as "n-equality." Since the distance of a bisected metric space is bounded by 1, the relation x 0 = y always holds. Moreover, the n-equalities become finer as n increases, and x = y if x n = y holds for all n. Finally, a function f :

X 1 → X 2 between bisected metric spaces is non-expansive iff x 1 n =x 1 ⇒ f (x 1 ) n = f (x 1 ), and contractive iff x 1 n =x 1 ⇒ f (x 1 ) n+1 = f (x 1 ) for all n.
Denotational semantics of Nakano's lambda calculus. We can now define the interpretation of types and terms in CBUlt ne . More precisely, by induction on the type τ we define locally non-expansive functors F τ : (CBUlt op ne ) n × CBUlt n ne -→ CBUlt ne , by separating positive and negative occurrences of the identifiers ty 1 , . . . , ty n in τ:

F Int (X,Y ) = (Z, d)
, where d is the discrete metric

F ty i (X,Y ) = Y i F τ 1 ×τ 2 (X,Y ) = F τ 1 (X,Y ) × F τ 2 (X,Y ) F τ 1 →τ 2 (X,Y ) = F τ 1 (Y, X) → F τ 2 (X,Y ) F • τ (X,Y ) = 1 2 • F τ (X,Y )
Now consider the functors F i : (CBUlt op ne ) n × CBUlt n ne -→ CBUlt ne for i = 1, . . . , n, defined by

F i (X,Y ) = 1 2 • F τ i,1 (X,Y ) + . . . + 1 2 • F τ i,k i (X,Y ) . (2)
Because of the shrinking factor 1/2 in (2), each F i is in fact locally contractive. Theorem 1 therefore gives a unique fixed point D with ι i : F i (D, D) ∼ = D i for all i. We use D to give the semantics of types:

τ def = F τ (D, D) .
Example 2 (Interpretation of streams). On streams, the semantics yields the "natural" metric. In fact, since seq τ ∼ =1 2 • ( τ × seq τ ) we have 1) .

d seq τ (s 1 s 2 . . . , s 1 s 2 . . . ) ≤ 2 -n ⇔ d τ (s 1 , s 1 ) ≤ 2 -(n-1) ∧ d seq τ (s 2 s 3 . . . , s 2 s 3 . . . ) ≤ 2 -(n-
In particular, because of the discrete metric on Int , for seq Int this means s n = s holds if s 1 = s 1 , . . . , s n-1 = s n-1 , i.e., if the common prefix of s and s has at least length n -1, and s = s if s i = s i for all i ∈ N.

For each subtyping derivation ∆ of a judgement τ ≤ σ we define a corresponding coercion function, i.e., a non-expansive function ∆ : τ → σ . First note that, for each of the 5 subtyping axioms τ ≤ σ in Figure 2 (as well as the reflexivity axiom), the underlying sets of τ and σ are equal. Thus we can define ∆ as the identity on the underlying sets, and it is easy to check that ∆ is in fact non-expansive. 1 If ∆ is obtained from ∆ 1 and ∆ 2 by an application of the transitivity rule, then ∆ is defined as the composition of ∆ 1 and ∆ 2 . Finally, for each of the 3 structural rules in Figure 2, we use the functorial property of the respective type constructor to define ∆ from the coercions of the subderivations. It follows by induction that the coercion determined from any derivation ∆ of τ ≤ σ is the identity on the underlying set of τ , and hence independent of ∆.

A Metric Model of Lambda Calculus with Guarded Recursion Birkedal et al.

Each term x 1 :τ 1 , . . . , x n :τ n t : τ denotes a non-expansive function

t : τ 1 × . . . × τ n → τ
which is defined by induction on the typing derivation. The cases of lambda abstraction, application, pairing and projections are given in terms of the cartesian closed structure on CBUlt ne . From the definition of the type interpretation it follows that ι i is an isomorphism between 1 2 • τ i,1 + . . . + 1 2 • τ i,k i and ty i . Together with the injections from • τ i, j = 1 2 • τ i, j into the sum, this isomorphism is used to interpret the constructors and pattern matching of the calculus:

In i, j (t) ( a) = (ι i • in j • t )( a) and case t of In i,1 (x 1 ) ⇒ t 1 | . . . | In i,k i (x k i ) ⇒ t k i ( a) = t j ( a, a)
where ι -1 i ( t ( a)) = in j (a) for some 1 ≤ j ≤ k i and a ∈ τ i, j . We obtain a model that is sound:

Theorem 3 (Soundness). If / 0 t : τ and t 1 → t 2 then t 1 = t 2 in τ .
Remark 4 (Recursive definitions). In [8] Nakano shows that the fixed point combinator Y from untyped lambda calculus can be represented by λ f .∆ f (Fold(∆ f )) where ∆ f = λ x. f (case x of Fold(y) ⇒ y x) and the data type data u = Fold of u → τ is assumed, and that this term has type (• τ → τ) → τ. Note that in the above interpretation, where the modality is interpreted by scaling the distances by 1/2, the type • τ → τ denotes the set of all non-expansive functions 1 2 • τ → τ , or equivalently (by the bisectedness of τ ) the contractive functions on τ . Such functions have a unique fixed point in τ by the Banach fixed point theorem, and we can show that Y indeed returns this fixed point since f

( Y f ) = Y f .
As an alternative to this coding, we could introduce a recursion operator rec : (• τ → τ) → τ for each τ as a primitive, with reduction rule rec t → t (rec t), and use the above observation for its interpretation.

Computational adequacy. We now relate the interpretation of lambda terms in the metric model and their operational behaviour. In particular, we prove that the semantics is sound for reasoning about contextual equivalence: if two terms have the same denotation then they are contextually equivalent.

The general idea of the adequacy proof is standard: the universal quantification over contexts prevents a direct inductive proof, so we use the compositionality of the denotational semantics and construct a (Kripke) logical relation between semantics and syntax. More precisely, we consider the family (R k τ ) k τ of relations indexed by types τ and natural numbers k, where R k τ ⊆ τ × Tm(τ) is given by:

n R k Int t ⇔ t * → n (a 1 , a 2 ) R k τ 1 ×τ 2 t ⇔ a 1 R k τ 1 proj 1 (t) ∧ a 2 R k τ 2 proj 2 (t) f R k τ 1 →τ 2 t ⇔ ∀ j, a 1 ,t 1 . j ≤ k ∧ a 1 R j τ 1 t 1 ⇒ f a 1 R j τ 2 t t 1 a R k • τ t ⇔ k > 0 ⇒ a R k-1 τ t a R k ty i t ⇔ ∃a ,t . a = (ι i • in j )(a ) ∧ t * → In i, j (t ) ∧ a R k • τ i, j t
Note that it is the natural number index which lets us define the relations R k τ inductively in the presence of recursive types ty i . We prove the 'fundamental property' by induction on typing derivations: → n, and with a symmetric argument the claim t 1 = t 2 ⇒ Γ t 1 t 2 : τ follows. Apart from using the semantics directly to reason about contextual equivalence, we can also use computational adequacy to derive more abstract proof principles from it. For instance, by the characterization of the metric on seq Int given in Example 2 and the fact that there are closed terms get n : seq Int → • n Int that yield the n-th element of a sequence, we obtain a variant of Bird and Wadler's take lemma: if get n t 1 and get n t 2 reduce to the same value, for each n ∈ N, then / 0 t 1 t 2 : seq Int . Similarly, we can exploit the uniqueness of fixed points of contractive equations also in the operational setting: if there exists a closed term f : • τ → τ such that f t 1 and t 1 are convertible, and also f t 2 and t 2 are convertible, then / 0 t 1 t 2 : τ. See, for instance, Hinze's article [6] for numerous applications of such a unique fixed point principle phrased in the context of Haskell streams, and Pottier's work [9] for a similar application to establish type equivalences in the context of F ω with recursive kinds.

Proposition 5. If Γ t : τ, k ∈ N,

Related Work

Metric semantics of PCF. Escardó [5] presents a metric model of PCF. One can, almost,2 factor his interpretation of PCF into two parts: (1) a syntactic translation from PCF to Nakano's calculus, extended with constants for integer operations and a booleans, and (2) the metric interpretation of Nakano's calculus presented here. The basic idea of the syntactic translation is that a potentially divergent PCF term of integer type is translated into a term of the recursive type Int s = Done of Int | Next of Int s . After evaluating such a term, one either obtains an actual integer answer, Done(n), or a new term that one can evaluate in the hope of eventually getting an integer answer. PCF function types are translated to function types. Now, for all types τ that are used to interpret PCF types, one defines a term delay : • τ → τ; this term is used to define the fixed-point combinator of PCF in terms of the fixed-point combinator of our calculus (Remark 4). See Escardó for more details. Intuitively, the idea is that unfolding a recursive definition takes a "computation step," which will be visible as an extra Next in the final answer of type Int s . Escardó shows an adequacy result which implies that the semantics of a PCF term does indeed match the number of unfoldings of the fixed-point combinator; the same information can be obtained from our adequacy proof using the definition of the logical relation on recursive types. Escardó gives two adequacy proofs, the first of which uses a Kripke logical relation as in our adequacy proof.

Since Escardó considers PCF, he does not treat recursively defined types, as we do here.

Conclusion and Future Work

We have presented a computationally adequate metric model of lambda calculus with guarded recursion. It complements Nakano's realizability interpretations [8], and it explains the modality in terms of scaling. We conjecture that an adaptation of the present model can be used to give a model for focusing proof systems with recursive types [11].

Introduction

Reasoning about higher-order stateful programs is notoriously difficult, and often involves the need to track aliasing information. A particular line of work that addresses this point are substructural type systems with regions, capabilities and singleton types [1,7,8]. In this context, Pottier [9] presented the anti-frame rule as a proof rule for hiding local state. It states that (the description of) a piece of mutable state that is local to a procedure can be removed from the procedure's external interface (expressed in the type system). The benefits of hiding local state include simpler interface specifications, simpler reasoning about client code, and fewer restrictions on the procedure's use because of potential aliasing. Thus, in combination with frame rules that allow the irrelevant parts of the state to be hidden during verification, the anti-frame rule provides an important ingredient for modular reasoning about programs.

Soundness of the frame and anti-frame rules is subtle, and relies on properties of the programming language. Pottier [9] sketched a proof for the anti-frame rule by a progress and preservation argument, resting on assumptions about the existence of certain recursively defined types. Subsequently, Schwinghammer et al. [12] investigated the semantic foundations of the anti-frame rule by identifying sufficient conditions for its soundness, and by instantiating their general setup to prove soundness for a separation logic variant of the rule. The latter was done by giving a Kripke model where assertions are indexed over recursively defined worlds. The recursive domain equation involved functions that should be monotonic with respect to an order relation that is specified using the isomorphism of the solution itself and an operator on the recursively defined worlds. This means that the standard existence theorems do not appear to apply, and thence we had to give the solution by a laborious explicit inverse-limit construction [12].

Here we explore an alternative approach, which consists of two steps. First, we consider a recursive metric space domain equation without any monotonicity requirement, for which we obtain a solution by appealing to a standard existence theorem. Second, we carve out a suitable subset of what might be called hereditarily monotonic functions. We show how to define this recursively specified subset. The resulting subset of monotonic functions is, however, not a solution to the original recursive domain equation; hence we verify that the semantic constructions used to justify the anti-frame rule in [12] suitably restrict to the recursively defined subset of hereditarily monotonic functions. In summa, this results in a considerably simpler model construction than the earlier one in loc. cit.

In the next section we give a brief overview of Charguéraud and Pottier's type and capability system [7,9] with higher-order frame and anti-frame rules. Section 3 summarizes some background on ultrametric spaces and presents the construction of a set of hereditarily monotonic recursive worlds. Following recent work by Birkedal et al. [4], we work with step-indexed heap relations based on the operational semantics of the calculus. The worlds thus constructed are then used (Section 4) to give a model of the type and capability system. For space reasons, many details are relegated to an online technical appendix.

A Calculus of Capabilities

Syntax and operational semantics. We consider a standard call-by-value, higher-order language with general references, sum and product types, and polymorphic and recursive types. For concreteness, the following grammar gives the syntax of values and expressions, keeping close to the notation of [7,9]:

v ::= x | () | inj i v | (v 1 , v 2 ) | fun f (x)=t | l t ::= v | (vt) | case(v 1 , v 2 , v) | proj i v | ref v | get v | set v
Here, the term fun f (x)=t stands for the recursive procedure f with body t. The operational semantics is given by a relation They extend the value types by a type of references, and also include all types of the form ∃ σ .τ * C which describe the final value and heap that result from the evaluation of an expression. Arrow types (which are value types) have the form χ 1 → χ 2 and thus, like the pre-and post-conditions of a triple in Hoare logic, make explicit which part of the heap is accessed and modified when a procedure is called. We also allow recursive capabilities, value types, and memory types, resp., provided the recursive definition is (formally) contractive, i.e., the recursion must go through a type constructor such as →.

(t | h) -→ (t | h ) between configurations
Frame and anti-frame rules. Each of the syntactic categories is equipped with an invariant extension operation, • ⊗C. Intuitively, this operation conjoins C to the domain and codomain of every arrow type that occurs within its left hand argument, which means that the capability C is preserved by all procedures of this type. This intuition is made precise by regarding capabilities and types modulo a structural equivalence which subsumes the "distribution axioms" for ⊗ that are used to express generic higherorder frame rules [6]. Two key cases of the structural equivalence are the distribution axioms for arrow types, (χ

1 → χ 2 ) ⊗ C = (χ 1 ⊗ C * C) → (χ 2 ⊗ C * C), and for successive extensions, (χ ⊗ C 1 ) ⊗ C 2 = χ ⊗ (C 1 •C 2 ) where the derived operation C 1 •C 2 abbreviates the conjunction (C 1 ⊗C 2 ) * C 2 .
There are two typing judgements, x 1 :τ 1 , . . . , x n :τ n v : τ for values, and x 1 :χ 1 , . . . , x n :χ n t : χ for expressions. The latter is similar to a Hoare triple where (the separating conjunction of) χ 1 , . . . , χ n serves as a precondition and χ as a postcondition. This view provides some intuition for the following "shallow" and "deep" frame rules, and for the (roughly dual) anti-frame rule:

[SF] Γ t : χ Γ * C t : χ * C [DF] Γ t : χ (Γ ⊗C) * C t : (χ ⊗C) * C [AF] Γ ⊗C t : (χ ⊗C) * C Γ t : χ (1)
As in separation logic, the frame rules can be used to add a capability C (which might assert the existence of an integer reference, say) as an invariant to a specification Γ t : χ, which is useful for local reasoning.

The difference between the shallow variant [SF] and the deep variant [DF] is that the former adds C only on the top-level, whereas the latter also extends all arrow types nested inside Γ and χ, via • ⊗C. While the frame rules can be used to reason about certain forms of information hiding [6], the anti-frame rule expresses a hiding principle more directly: the capability C can be removed from the specification if C is an invariant that is established by t, expressed by • * C, and guaranteed to hold whenever control passes from t to the context and back, expressed by • ⊗C.

Hereditarily Monotonic Recursive Worlds

Intuitively, capabilities describe heaps. A key idea of the model that we present next is that capabilities (as well as types and type contexts) are parameterized by invariants -this will make it easy to interpret the invariant extension operation ⊗, as in [11,12]. But, as the frame and anti-frame rules in (1) indicate, invariants can be arbitrary capabilities again. Thus, we are led to consider a Kripke model where the worlds are recursively defined: to a first approximation, we need a solution to the equation

W = W → Pred(Heap) . (2)
In fact, we will also need to consider a preorder on W and ensure that the interpretation of capabilities and types is monotonic. We will find a solution to a suitable variant of (2) using ultrametric spaces.

Ultrametric spaces. We recall some basic definitions and results about ultrametric spaces; for a less condensed introduction to ultrametric spaces we refer to [13]. A 1-bounded ultrametric space (X, d) is a metric space where the distance function d : X × X → R takes values in the closed interval [0, 1] and satisfies the "strong" triangle inequality d(x, y) ≤ max{d(x, z), d(z, y)}. A metric space is complete if every Cauchy sequence has a limit. A function f :

X 1 → X 2 between metric spaces (X 1 , d 1 ), (X 2 , d 2 ) is non-expansive if d 2 ( f (x), f (y)) ≤ d 1 (x, y) for all x, y ∈ X 1 . It is contractive if there exists some δ < 1 such that d 2 ( f (x), f (y)) ≤ δ • d 1 (x, y) for all x, y ∈ X 1 . By multiplication of the distances of (X, d) with a non- negative factor δ < 1, one obtains a new ultrametric space, δ • (X, d) = (X, d ) where d (x, y) = δ • d(x, y).
The complete, 1-bounded, non-empty, ultrametric spaces and non-expansive functions between them form a Cartesian closed category CBUlt ne . Products are given by the set-theoretic product where the distance is the maximum of the componentwise distances. The exponential

(X 1 , d 1 ) → (X 2 , d 2 ) has the set of non-expansive functions from (X 1 , d 1 ) to (X 2 , d 2 )
as underlying set, and the distance function is given by d Uniform predicates, worlds and world extension. Let (A, ) be a partially ordered set. An upwards closed, uniform predicate on A is a subset p ⊆ N × A that is downwards closed in the first and upwards closed in the second component: if (k, a) ∈ p, j ≤ k and a b, then ( j, b) ∈ p. We write UPred(A) for the set of all upwards closed, uniform predicates on A, and we define p

X 1 →X 2 ( f , g) = sup{d 2 ( f (x), g(x)) | x ∈ X 1 }. The notation x n = y means that d(x, y) ≤ 2 -n . Each relation n = is
[k] = {( j, a) | j < k}. Note that p [k] ∈ UPred(A). We equip UPred(A) with the distance function d(p, q) = inf{2 -n | p [n] = q [n] }, which makes (UPred(A), d) an object of CBUlt ne .
In our model, we use UPred(A) with the following concrete instances for the partial order (A, ): (1) heaps (Heap, ), where h h iff h = h • h 0 for some h 0 #h, (2) values (Val, ), where u v iff u = v, and (3) stateful values (Val × Heap, ), where (u, h) (v, h ) iff u = v and h h . We also use variants of the latter two instances where the set Val is replaced by the set of value substitutions, Env, and by the set of closed expressions, Exp. On UPred(Heap), ordered by subset inclusion, we have a complete Heyting BI algebra structure [3]. Below we only need the separating conjunction and its unit I, given by

p 1 * p 2 = {(k, h) | ∃h 1 , h 2 . h = h 1 •h 2 ∧ (k, h 1 ) ∈ p 1 ∧ (k, h 2 ) ∈ p 2 } and I = N × Heap .
It is well-known that one can solve recursive domain equations in CBUlt ne by an adaptation of the inverse-limit method from classical domain theory [2]. In particular, with regard to (2) above:

Theorem 1. There exists a unique (up to isomorphism) (X, d) ∈ CBUlt ne s.t. ι : 1 2 •X → UPred(Heap) ∼ = X.
Using the pointwise lifting of separating conjunction to 1/2•X → UPred(Heap) we define a composition operation on X, which reflects the syntactic abbreviation

C 1 •C 2 = C 1 ⊗C 2 * C 2 of conjoining C 1 and
C 2 and additionally applying an invariant extension to C 1 . Formally, • : X × X → X is a non-expansive operation that for all p, q, x ∈ X satisfies

ι -1 (p • q)(x) = ι -1 (p)(q • x) * ι -1 (q)(x) ,
and which can be defined by an easy application of Banach's fixed point theorem as in [11]. One can show that this operation is associative and has a left and right unit given by emp = ι(λ w.I); thus (X, •, emp) is a monoid in CBUlt ne . Using • we define an extension operation ⊗ :

Y (1/2•X) × X → Y (1/2•X) for any Y ∈ CBUlt ne by ( f ⊗ x)(x ) = f (x • x ).
Without going into details, let us remark that this operation is the semantic counterpart to the syntactic invariant extension, and thus plays a key role in explaining the frame and anti-frame rules. However, for Pottier's anti-frame rule we also need to ensure that specifications are not invalidated by invariant extension. This requirement is stated via monotonicity, as we discuss next.

Relations on ultrametric spaces and hereditarily monotonic worlds. As a conseqence of the fact that • defines a monoid structure on X there is an induced preorder on X:

x y ⇔ ∃x 0 . y = x • x 0 .
For modelling the anti-frame rule, we aim for a set of worlds similar to X ∼ = 1/2 • X → UPred(Heap) but where the function space consists of the non-expansive functions that are additionally monotonic, with respect to the order induced by • on X and with respect to set inclusion on UPred(Heap):

(W, ) ∼ = 1 2 • (W, ) → mon (UAdm, ⊆) . (3)
Because the definition of the order (induced by •) already uses the isomorphism between left-hand and right-hand side, and because the right-hand side depends on the order for the monotonic function space, the standard existence theorems for solutions of recursive domain equations do not appear to apply to (3).

Previously we have constructed a solution to this equation explicitly as inverse limit of a suitable chain of approximations [12]. We show in the following that we can alternatively carve out from X a suitable subset of what we call hereditarily monotonic functions. This subset needs to be defined recursively.

Let R be the collection of all non-empty and closed relations R ⊆ X. Given R ∈ R, we define

R [n] def = {y | ∃x ∈ X. x n = y ∧ x ∈ R} . Thus, R [n] is the set of all points within distance 2 -n of R. Note that R [n] ∈ R. In fact, R ⊆ R [n]
by the reflexivity of n-equivalence, and if (y k ) k∈N is a sequence in R . We make some further observations that follow from the properties of n-equality on X.

First, R ⊆ S implies R [n] ⊆ S [n]
for any R, S ∈ R. Moreover, using the fact that the n-equalities become increasingly finer it follows that (R

[m] ) [n] = R [min(m,n)] for all m, n ∈ N, so in particular each (•) [n] is a closure operation on R. As a consequence, we have R ⊆ . . . ⊆ R [n] ⊆ . . . ⊆ R [1] ⊆ R [0] . By the 1-boundedness of X, R [0] = X for all R ∈ R. Finally, R = S if and only if R [n] = S [n] for all n ∈ N. Proposition 2. Let d : R × R → R be defined by d(R, S) = inf {2 -n | R [n] = S [n] }. Then (R, d) is a com- plete, 1-bounded, non-empty ultrametric space. The limit of a Cauchy chain (R n ) n∈N with d(R n , R n+1 ) ≤ 2 -n is given by n (R n ) [n]
, and in particular R = n R [n] for any R ∈ R.

We will now define the set of hereditarily monotonic functions W as a recursive predicate on X. Let the function Φ on subsets of X be given by Φ

(R) = {ι(p) | ∀x, x 0 ∈ R. p(x) ⊆ p(x • x 0 )}. If R ∈ R then Φ(R)
is non-empty and closed (i.e., Φ restricts to a function on R), and Φ is contractive. By Proposition 2 and the Banach theorem we can now define W as the (uniquely determined) fixed point of Φ and obtain

w ∈ W ⇔ ∃p. w = ι(p) ∧ ∀w, w 0 ∈ W. p(w) ⊆ p(w • w 0 ) .
Note that W thus constructed does not quite satisfy (3). We do not have an isomorphism between W and the non-expansive and monotonic functions from W (viewed as an ultrametric space itself), but rather between W and all functions from X that restrict to monotonic functions whenever applied to hereditarily monotonic arguments. Keeping this in mind, we abuse notation and write

1 2 •W → mon UPred(A) def = {p : 1 2 • X → UPred(A) | ∀w 1 , w 2 ∈ W. p(w 1 ) ⊆ p(w 1 • w 2 )} .
Then, for our particular application of interest, we also have to ensure that all the operations restrict appropriately. First, by induction we show that for all n ∈ N, if

w 1 , w 2 ∈ W then w 1 • w 2 ∈ W [n]
, and this entails that the composition operation • restricts to W . In turn, this means that the ⊗ operator restricts accordingly: if w ∈ W and p is in 1 2 •W → mon UPred(A) then so is p ⊗ w.

Possible World Semantics of Capabilities

We define semantic domains for the capabilities and types of the calculus described in Section 2,

Cap = 1 2 •W → mon UPred(Heap) VT = 1 2 •W → mon UPred(Val) MT = 1 2 •W → mon UPred(Val × Heap) ,
so that p ∈ Cap if and only if ι(p) ∈ W. Next, we define operations on the semantic domains that correspond to the syntactic type and capability constructors. The most interesting of these is the one for arrow types. Given

p, q ∈ 1/2 • X → UPred(Val × Heap), p → q in 1 2 • X → UPred(Val) is defined by (p → q)(x) def = {(k, fun f (y)=t) | ∀ j < k. ∀w ∈ W. ∀r ∈ UPred(Heap). ∀( j, (v, h)) ∈ p(x • w) * ι -1 (x • w)(emp) * r. ( j, (t[ f :=fun f (y)=t, y:=v], h)) ∈ E (q)(x • w) * r} , (4)
where E (q) is the extension of a world-indexed, uniform predicate on Val × Heap to one on Exp × Heap.

It is here where the index is linked to the operational semantics: (k, (t, h)) ∈ E (q)(x) iff for all j ≤ k,t , h ,

(t | h) -→ j (t | h ) ∧ (t | h ) irreducible ⇒ (k-j, (t , h )) ∈ w ∈W q(x • w ) * ι -1 (x • w )(emp) .
Definition (4) realizes the key ideas of our model as follows. First, the universal quantification over w ∈ W and subsequent use of the world x • w builds in monotonicity, and intuitively means that p → q is parametric in (and hence preserves) invariants that have been added by the procedure's context. In particular, (4) states that procedure application preserves this invariant, when viewed as the predicate ι -1 (x • w)(emp). By also conjoining r as an invariant we "bake in" the first-order frame property, which results in a subtyping axiom χ 1 → χ 2 ≤ χ 1 * C → χ 2 * C in the type system. The existential quantification over w , in the definition of E , allows us to absorb a part of the local heap description into the world. Finally, the quantification over indices j < k in (4) achieves that (p → q)(x) is uniform. There are two explanations why we require that j be strictly less than k. Technically, the use of ι -1 (x • w) in the definition "undoes" the scaling by 1/2, and j < k is needed to ensure the non-expansiveness of p → q as a function 1/2 • X → UPred(Val). Moreover, it lets us prove the typing rule for recursive functions by induction on k. Intuitively, the use of j < k for the arguments suffices since application consumes a step. All these constructors restrict to Cap, VT and MT, respectively. With their help it becomes straightforward to define the interpretation of capabilities and types, and to verify that the type equivalences hold with respect to this interpretation. The semantics of typing judgements is defined in analogy to (4), but also universally quantifying over worlds and indices, and it validates the typing rules of the calculus.

Conclusion and Future Work

To justify proof rules that take advantage of hidden state, like the frame and anti-frame rules, one needs semantic models that adequately capture this aspect of programming languages. In this paper, we have described the construction of a suitable possible worlds model where the worlds are given by a recursively defined predicate on a recursively defined metric space. In contrast to a similar model [12] which involved a tedious explicit inverse-limit construction, the present approach uses standard existence and fixed point theorems. We believe that this method provides a realistic approach to study frame and antiframe rules in the presence of other programming language features, and to investigate the soundness of generalizations of these rules that have recently proposed by Pottier [10].

Basic notions

Researchers of the modal µ calculus were widely investigating classes of formulae which reach their fixpoints relatively fast, that is in a finite number of steps (bounded formulae) or in no more than ω steps (constructive formulae). Some interesting remarks about those classes of formulae can be found in Gaëlle Fontaine's paper [1]. In this paper we analize how fast, in general, may modal µ formulae reach their least fixpoints.

Along this paper we work with the following definition.

Definition 1. We say that a modal µ formula reaches its fixpoint in α steps in a variable x if and only if α is the least ordinal such that for all models M and all valuations τ, ϕ α+1 M ,τ (∅) = ϕ α M ,τ (∅) holds. We will denote this fact by O x (ϕ) = α.

Our investigation is motivated by a question asked by Damian Niwiński whether there exists a formula which reaches its fixpoint in ω + 1 steps and, in a broader sense, whether it is possible to control the number of interations of formulae above ω. As a response for this question Mikołaj Bojańczyk conjectured that the formula (3x ∧ 2p 1 ∧ p 1 ) ∨ (2x ∧ 2p 1 ∧ ¬p 1 ) ∨ 2⊥ reaches its fixpoint in exactly ω + 1 steps. We prove this conjecture is true and make an observation on the sense of appearances of propositional variable p 1 in this formula. This consideration lets us to think of p 1 as a fuse, which melts while 2 is used, and which prohibits adding new points afterwards. Adding more fuses allows us to pass through more limit ordinals. Those propositional variables may be considered also as a finite one-way counter which, however, increases its size linearly 1 -in the sense of length of the formula -while increasing its capacity. Therefore our approach can not be extended to a construction of formulae fixing at ω 2 or further. Now we recall some basic notions. The syntax of modal µ calculus is an extension of modal logic with the construction µx.ϕ bounding an individual variable x, that can be applied to formulae in which every occurrence of x is in range of a positive number of negations. Semantics for this construction is the following: µx.ϕ M ,τ = {A ⊆ |M | : ϕ M ,τ[x:=A] ⊆ A}. One can observe that this, indeed, is the least fixpoint of the map ϕ :

P(|M |) → P(|M |) such that ϕ(A) = ϕ M ,τ[x:=A] .
We will omit subscripts, if it is clear from the context, which model and valuation we work with.

It is easy to see that to some formulae ϕ we can not assign any ordinal number α such that O x (ϕ) = α. It means that there are arbitrary large ordinal numbers α and models in which those formulae reach their fixpoints in more than α steps. Certainly the easiest example of such a formula is 2x. There is a folklore way of assigning the tree to an ordinal number. To 0 we assign just one point -the root of the tree. For a successor α + 1 we add to the preexisting tree for α one more point, which is to be a new root, and attach to it simply the previous one. For a limit ordinal λ we also take a new point, which is to be a new root, but we attach to it all the roots of the trees constructed before i.e. for α < λ . A straightforward transfinite induction argument leads us to conclusion that the formula 2x reaches its fixpoint in a model assigned to λ in exactly λ + 1 steps, for every limit ordinal λ . Therefore there is no ordinal that bounds the number of iterations of 2x in every model -we denote it by O x (2x) = ∞.

Before proceeding to the infinite case we introduce easy examples of formulae reaching their fixpoints in finite numbers of steps.

For n ∈ ω let us consider formulae

ϕ n = 2x ∧ 2 n+1 ⊥. Note that for k ≤ l there is 2 k ⊥ ∧ 2 l ⊥ ≡ 2 k (2 l-k ⊥ ∧ ⊥) ≡ 2 k ⊥ and 2 k ⊥ ∨ 2 l ⊥ ≡ 2 l ⊥.
Therefore, for each n ∈ ω, every model and valuation

ϕ n+1 n (∅) = n+1 i=0 (2 i+1 ⊥ ∧ 2 n+1 ⊥) = 2 n+1 ⊥ ∧ n+1 i=0 2 i+1 ⊥ = 2 n+1 ⊥ ∧2 n+2 ⊥ = 2 n+1 ⊥ = ϕ n n (∅)
. This gives us the upper bound for the number of iterations needed by ϕ n to reach its fixpoint. To prove that it is also the lower bound, consider the trees assigned to finite ordinals from previous paragraph.

Fuses -controlling the number of interations

Let us introduce sets of fuses: for n > 0 and 0

≤ i ≤ n let C n i = ¬p 1 ∧ • • • ∧ ¬p i ∧ p i+1 ∧ • • • ∧ p n . One can treat C n i as different colors as it is obvious that for every n > 0 if i = j, then C n i ∧C n j ≡ ⊥.
We now proceed to the general construction2 of formulae reaching their fixpoints in α steps for ω ≤ α < ω 2 .

ψ ω•n = n-1 i=0 (3x ∧C n i ∧ 2C n i ) ∨ n-2 i=0 (2x ∧C n i+1 ∧ 2C n i ), ψ ω•n+m = ψ ω•n ∨ m-1 i=0 (2x ∧ i j=0 2 j C n n ∧ 2 i+1 C n n-1 ), ϕ ω•n+m = ψ ω•n+m ∨ 2 ⊥ .
Note that ϕ ω+1 is exactly the formula which, according to Mikołaj Bojańczyk's conjecture, reaches its fixpoint in ω + 1 steps. We now show the key lemma of the paper.

Lemma 1. Let k > 0, α, β such that ω • k ≤ α, β < ω 2 , let M = (M, R,V ) be a model and let τ be a valuation. Then for every a ∈ M, if a |= p k and a ∈ ϕ β α (∅), then a ∈ ϕ ω•k α (∅).
Proof. Fix M = (M, R,V ), τ and a ∈ M. We proceed by induction on β . The base step for β = ω • k is trivial as we have:

∀k > 0∀ω • k ≤ α < ω 2 [(a |= p k ∧ a ∈ ϕ ω•k α (∅)) ⇒ a ∈ ϕ ω•k α (∅)]
. The limit step is obvious as well: Let λ be a limit ordinal and for each ordinal number So it remains to prove the successor case: Let β = γ + 1, then the induction hypothesis is of the form:

β < λ , ∀k > 0∀ω • k ≤ α < ω 2 [(a |= p k ∧ a ∈ ϕ β α (∅)) ⇒ a ∈ ϕ ω•k α (∅)] holds. Fix k > 0 and α such that ω • k ≤ α < ω
∀k > 0∀ω • k ≤ α < ω 2 [(a |= p k ∧ a ∈ ϕ γ α (∅)) ⇒ a ∈ ϕ ω•k α (∅)]. We need to show that ∀k > 0∀ω • k ≤ α < ω 2 [(a |= p k ∧ a ∈ ϕ γ+1 α (∅)) ⇒ a ∈ ϕ ω•k α (∅)]. Fix k > 0 and let α = ω • n + m, for n ≥ k and m ∈ ω. Let us assume that a |= p k and a ∈ ϕ β α (∅). Since β = γ + 1 we have a ∈ ϕ α (ϕ γ α (∅))
. By the definition of ϕ α , one of the following cases must hold:

• a |= 2 ⊥ -then a ∈ ϕ 0 α (∅) ⊆ ϕ ω•k α (∅), • a |= C n l ∧ 2C n l for some l < k -since a |= p k ,
(∅). Because ω • (l + 1) is a limit ordinal, there exists s ∈ ω such that t ∈ ϕ ω•l+s α (∅). Therefore a ∈ ϕ ω•l+s+1 α (∅) ⊆ ϕ ω•(l+1) α (∅) ⊆ ϕ ω•k α (∅), • a |= C n l+1 ∧ 2C n l for some l < k -1 -since a |= p k ,
(∅). Thus a ∈ ϕ ω•(l+1)+1 α (∅) ⊆ ϕ ω•k α (∅) since l < k -1,
• In other cases, namely:

a |= m-1 i=0 (2x ∧ i j=0 2 j C n n ∧ 2 i+1 C n n-1
), a |= C n n which means a |= ¬p i for i = 1, . . . , n, but this is a contradiction since k ≤ n and we assumed that a |= p k . This ends the proof of lemma 1.

Lemma 1 shows us how the fuses work. If a point in which p i is true is in the least fixpoint of ϕ α , it has to be added relatively fast, that is in at most ω • i steps. After that number of iterations the fuse p i melts and no more points in which p i is true may be added to the fixpoint. That is a global view on fuses, but we can also think about fuses locally. Let us consider the following example:

ϕ ω•2+3 = (3x ∧C 2 0 ∧ 2C 2 0 ) ∨ (3x ∧C 2 1 ∧ 2C 2 1 ) ∨ (2x ∧C 2 1 ∧ 2C 2 0 )∨ ∨ (2x ∧C 2 2 ∧ 2C 2 1 ) ∨ (2x ∧C 2 2 ∧ 2C 2 2 ∧ 2 2 C 2 1 )∨ ∨ (2x ∧C 2 2 ∧ 2C 2 2 ∧ 2 2 C 2 2 ∧ 2 3 C 2 1 )
We recall that

C 2 0 = p 1 ∧ p 2 , C 2 1 = ¬p 1 ∧ p 2 and C 2 2 = ¬p 1 ∧ ¬p 2 .
We can restrict our considerations to models that are trees. In every tree, in the first step all the leaves are added i.e. ϕ 0 ω•2+3 (∅) = 2⊥ . Now, there are four different types of points in the model: those that satisfy p 1 ∧ p 2 , p 1 ∧ ¬p 2 , ¬p 1 ∧ p 2 and ¬p 1 ∧ ¬p 2 . If a point is of the first type and was added to the fixpoint in some iteration, then its parent will be added in the next iteration just in two cases -if it and all its children satisfy p 1 and

p 2 (3x ∧ C 2 0 ∧ 2C 2 0 )
or if all its children were already added to the fixpoint and it satisfies ¬p 1 and p 2 (2x ∧C 2 1 ∧ 2C 2 0 ). In the second case the fuse p 1 melted which says that ancestors of this point will never be added via 2x ∧C 2 1 ∧ 2C 2 0 . This melted fuse p 1 represents one use of the 2. The second type of points are not very interesting as the parents of such points will never be added while iterating ϕ ω•2+3 -the second fuse is melted and the first is not while no disjunct in the formula satisfy such configuration. The third type of points is similar to the first one, but since they satisfy ¬p 1 and p 2 there is one less 2 to use while trying to add their parents to the fixpoint. And again when 2x ∧C 2 2 ∧ 2C 2 1 is used to add a parent of a point, a fuse p 2 melts and the parent added that way and its ancestors that are in the fixpoint do not satisfy p 2 . In such case this was again the use of 2 which might have let us pass the limit ordinalnamely ω • 2. The forth type of points -those which may be added to the fixpoint after melting the last fuse have nothing to do with fuses anymore -the formula is constructed in such way to ensure that there will be just m -1 more essential iterations after melting the last fuse.

We now state the main theorem of the paper.

Theorem 1. For every ordinal number α such that ω ≤ α < ω 2 , in every model M and every valuation τ, ϕ α+1 α (∅) = ϕ α α (∅) holds. Proof. The inclusion ⊇ is obvious by the monotonicity of ϕ α in x. We show the other inclusion. Let α = ω • n + m, for n > 0 and m ∈ ω. Fix a model M = (M, R,V ), valuation τ, and assume that a ∈ ϕ α+1 α (∅). We show that a ∈ ϕ α α (∅). If there exists i ≤ n such that a |= p i , then, by lemma 1 we know that a ∈ ϕ ω

•i α (∅) ⊆ ϕ ω•n+m α (∅) = ϕ α α (∅), since a ∈ ϕ α+1 α (∅).
Let us now assume that for i = 1, . . . , n, a |= ¬p i holds. Since a ∈ ϕ α (ϕ α α (∅)), then by the definition of ϕ α , m > 0 and one of the following cases must hold:

• a |= 2 ⊥ -then trivially a ∈ ϕ α α (∅). • a |= i j=0 2 j C n n ∧ 2 i+1 C n n-1
, for some i = 0, . . . , m -1 and for every t such that aRt, t ∈ ϕ α α (∅). We proceed by induction on i to show that if

a |= i j=0 2 j C n n ∧ 2 i+1 C n n-1 , then a ∈ ϕ ω•n+i+1 α (∅).
For the base step let us assume that i = 0. Then for all t such that aRt, t |= C n n-1 holds. Therefore t |= p n and by lemma 1,

t ∈ ϕ ω•n α (∅). Thus a ∈ ϕ ω•n+1 α (∅). Suppose now that for 0 ≤ i < k ≤ m if a |= i j=0 2 j C n n ∧ 2 i+1 C n n-1 , then a ∈ ϕ ω•n+i+1 α (∅).
We show that for i = k this implication holds as well. Suppose that

a |= k j=0 2 j C n n ∧ 2 k+1 C n n-1 then for every t such that aRt, t |= k-1 j=0 2 j C n n ∧ 2 k C n n-1 holds. Therefore, by the induction hypothesis t ∈ ϕ ω•n+k α (∅), and thus a ∈ ϕ ω•n+k+1 α (∅). Hence, for every such case a ∈ ϕ ω•n+m α (∅) = ϕ α α (∅).
• In other cases, namely when a |= n-1 i=0 (3x

∧C n i ∧ 2C n i ) ∨ n-2 i=0 (2x ∧C n i+1 ∧ 2C n i ) also a |= C n+1 i
holds, for some i = 1, . . . n -1. This means that a |= p n which is a contradiction, since we assumed that a |= ¬p n .

This ends the proof.

By theorem 1 for all ordinal numbers α such that ω ≤ α < ω 2 the least fixpoint of ϕ α is reached in at most α steps. Now it is sufficient to show that for each formula ϕ α there is a model such that ϕ α reaches its least fixpoint in this model in exactly α steps.

Theorem 2. For every ordinal number α such that ω ≤ α < ω 2 there is a model, in which ϕ α reaches its least fixpoint in α steps.

Proof. Let us recall the assignment of the trees to ordinal numbers sketched in the end of the previous section, where we show that O x (2x) = ∞. To 0 we assign just one point -the root of the tree. For a successor α + 1 we add to the preexisting tree for α one more point, which is to be a new root, and attach to it simply the previous one. We change a limit step a bit: for a limit ordinal λ = ω • n we also take a new point, which is to be a new root, but we attach to it just the roots of the trees ω • (n -1), ω • (n -1) + 1, . . . . Now we need to augment models assigned to the ordinal numbers α < ω 2 to models over Prop = {p 1 , p 2 , . . . }. Let n > 0, m ∈ ω, and α = ω • n + m and let V ω•n+m satisfy: r ω•n+m ∈ V (p i ) if and only if i > n, where r ω•n+m is the root of the corresponding model. The idea is to start with the model M 0 whose root satisfies every p i , for i > 0. When passing the successor step -the new root satisfies the same propositional variables as the previous one. Finally, for the limit step -if i is the least number for which all p i are satisfied, in every point of models below, then the root of the limit model satisfies exactly p j for j > i (it does not satisfy p i anymore). Violating the intuition, let us denote a model for an ordinal α < ω 2 by M α+1 . This construction works up to ω 2 and gives us models M α , for each nonlimit ordinal α. By simple induction on α such that ω ≤ α < ω 2 we see that the formula ϕ α reaches its least fixpoint M α+1 -{r α+1 } in the model M α+1 in exactly α steps.

Corollary 1. Let α < ω 2 . Then O x (ϕ α ) = α holds.
The question whether there are formulae that reach their fixpoints in at least ω 2 iterations remains an open problem. Note that the formulae ϕ α introduced in this paper are all basic modal formulae -we did not use the fixpoint operator in their construction. There may be some more complicated formulae which would allow us to control the number of iterations above ω 2 . There also is a possibility to use fuses in the construction of such formulae, but this would require having a single formula that behaves as an infinite one-way counter at least in some big models 3 allowing us to count the number of uses of 2 up to ω.

One can answer the following questions in order to extend the subject:

• Is there a basic modal logic formula which reaches its fixpoint in at least ω 2 ?

• Is there a modal µ calculus formula which reaches its fixpoint in at least ω 2 ?

• Is there a single formula behaving as an ω-counter at least in big enough models allowing us to count 2 uses up to ω?

Proving fixed points

Hervé Grall Research Team Ascola (EMN-INRIA, LINA)

Ecole des mines de Nantes, France hgrall@mines-nantes.fr

Abstract

We propose a method to characterize the fixed points described in Tarski's theorem for complete lattices. The method is deductive: the least and greatest fixed points are "proved" in some inference system defined from deduction rules. We also apply the method to two other fixed point theorems, a generalization of Tarski's theorem to chain-complete posets and Bourbaki-Witt's theorem. Finally, we compare the method with the traditional iterative method resorting to ordinals and the original impredicative method used by Tarski.

We are interested in fixed points of maps defined over partially ordered sets (abbreviated as posets). Consider Tarski's fixed point theorem. Asserting the existence of fixed points under certain conditions, it is proved according to one of these two methods. In the impredicative method, the fixed points are characterized by a property (expressing extremality) using a quantification over a domain that includes the fixed point itself. In the iterative method, the fixed points are iteratively computed by using a transfinite induction. The impredicative method corresponds to a logical specification that is essentially not constructive 1 . As for the iterative method, it seems to be more constructive, in that it corresponds to an iteration. However, first, it assumes the machinery of ordinals and second, it therefore requires a specific computation for limit ordinals, the next value being then computed from an infinite set of preceding values.

Is there a proof method that not only is not impredicative, but also does not resort to ordinals? In this paper, we positively answer by proposing an alternative method, where fixed points are (inductively) proved in inference systems: this is a deductive method. It corresponds to a proof construction, using forward chaining for deduction rules, as used in logic programming, for instance in Datalog, a query language for deductive databases.

The paper is organized as follows. After recalling Tarski's theorem, the first section deals with inference systems, and their interpretations, either inductive or coinductive. In the second section, we introduce the deductive method, and apply it to different fixed point theorems: Tarski's theorem, its generalization to chain-complete posets and Bourbaki-Witt's theorem. Finally, we compare the deductive method with the iterative and impredicative methods. Note that the proofs presented here are just sketched: an extended version, available online2 , provides the details.

Induction and Coinduction for Inference Systems

Generally speaking, following Aczel's classical presentation [1], an inference system over a set U of judgments is a set of deduction rules. A deduction rule is an ordered pair (A, c), where A ⊆ U is the set of premises or antecedents and c ∈ U is the conclusion. A rule is usually written as follows:

A . c
Its intuitive interpretation is that the judgment c can be deduced from the set of judgments A.

Fixed Point Approach. The first way to assign a definitional meaning to an inference system is to consider the fixed points of the associated inference operator.

Indeed there exists a canonical Galois connection between the set of inference systems over U ordered by inclusion and the set of isotone (order-preserving) maps from 2 U to 2 U ordered point-wise. If Φ is an inference system over U , then the associated operator ϕ : 2 U → 2 U is defined as follows:

ϕ(S) = {c ∈ U | ∃ A ⊆ S . (A, c) ∈ Φ}.
The application of ϕ to S gives the conclusions that can be inferred in one step from S by using the inference rules: ϕ is thus called the inference operator associated to the system Φ. For instance, if S is the empty set, then ϕ(S) is the set of the axioms of the inference system, in other words the conclusions of the rules without premises. Conversely, given an isotone operator ϕ : 2 U → 2 U , the inference system containing all the rules (A, c), with c ∈ ϕ(A), and only these rules, belongs to the inverse image of ϕ: this is the greatest element of the inverse image of ϕ.

Let Φ be an inference system and ϕ its associated inference operator. Since the powerset 2 U is a complete lattice, by applying Tarski's fixed point theorem [9, p. 286], we obtain that the inference operator ϕ possesses both a least fixed point and a greatest fixed point.

We recall here Tarski's fixed point theorem, with two proof sketches following the impredicative and the iterative methods respectively.

Theorem 1 (Tarski). Let (E , ≤) be a complete lattice. Let η : E → E be an isotone map over E . Then η has a least fixed point lfp η and a greatest fixed point gfp η.

Impredicative method. The proof uses the following characterization:

lfp η = ∧{x ∈ E | η(x) ≤ x} and gfp η = ∨{x ∈ E | x ≤ η(x)},
defining the least and greatest fixed points as the smallest η-closed set and the greatest η-consistent set respectively. It can be found in original Tarski's paper [9].

Iterative method. The proof uses the following characterization:

lfp η = α ∆ α (η) and gfp η = α ∇ α (η).
where the sequences (∆ α (η)) α and (∇ α (η)) α are defined over ordinals as follows:

∆ α (η) = η( β |β <α ∆ β (η)) and ∇ α (η) = η( β |β <α ∇ β (η)).
It can be found in Cousot's article [5], for instance, with a slight variant in the definition of the sequences.

Deductive Method. In contrast with the fixed point approach, the deductive method starts from the proofs admissible in an inference system. These proofs are represented as trees, called proof trees. These are trees whose nodes are labeled with judgments in U and such that for all nodes n, the label c of n and the labels A of the sons of n correspond to an inference rule (A, c) in Φ. The conclusion of a proof is the label of its root node. A proof d is well-founded if it has no infinite branch; d is ill-founded otherwise.

Note that an ill-founded proof is always infinite. A well-founded proof is finite if and only if it only uses rules with a finite set of premises.

In the deductive method, the inductive interpretation of the inference system Φ is the set ∆(Φ) of the conclusions of the well-founded proofs, while the coinductive interpretation is the set ∇(Φ) of the conclusions of all the proofs, ill-founded or well-founded. The following theorem shows that the interpretations defined using fixed points and using proofs coincide.

Theorem 2 (Inductive and coinductive interpretations). Let Φ be an inference system and ϕ the associated inference operator. Then:

lfp ϕ = ∆(Φ) and gfp ϕ = ∇(Φ).
Proof. It is easy to show that ∆(Φ) and ∇(Φ) are a η-closed set and a η-consistent set respectively. In the reverse direction, given a η-closed set, an induction over well-founded proofs shows that any conclusion of a well-founded proof belongs to the η-closed set; given a η-consistent set, a system of guarded recursive equations over proof trees can be defined, generating as solution a valuation mapping each judgment in the η-consistent set to a proof tree with conclusion this judgment. By Tarski's theorem, we deduce lfp ϕ = ∆(Φ) and ∇(Φ) = gfp ϕ.

Details for the proof can be found in Leroy and author's article [7,Th. 1], where some bibliographic references are also given.

Generalization of the Deductive Method

Theorem 2 asserts that the least and greatest fixed points of an isotone map over a powerset, a particular complete lattice, can also be defined as the inductive and coinductive interpretations of an inference system. We first generalize to any complete lattice, and then to more powerful fixed point theorems.

Tarski's Theorem Revisited. Given an isotone map η over a complete lattice (E , ≤), how can we define an inference system Φ over E , or equivalently an inference operator ϕ : 2 E → 2 E , whose inductive and coinductive interpretations produce the least and greatest fixed points of η?

A first attempt, defining ϕ(S) as the image of S with η, trivially fails, since the least fixed point would be the empty set. However, a well-known result [4, Th. I.5.3] allows a complete lattice to be embedded in its powerset. Indeed, let γ : 2 E → {≤ x | x ∈ E } be the closure operator from the powerset of E to the set {≤ x | x ∈ E } of principal order ideals defined as follows: γ(S) =≤ (∨ S) 3 . Let δ : {≤ x | x ∈ E } → 2 E be its adjoint embedding: δ (≤ x) =≤ x. Now, the isomorphism ι from E to {≤ x | x ∈ E } is defined as follows: ι(x) =≤ x. Finally, thanks to the embedding via a closure operator, we can associate to the map η the operator ϕ : 2 E → 2 E , equal to δ • ι • η • ι -1 • γ : we have ϕ(S) =≤ η(∨ S). It turns out that this operator has the intended properties with respect to fixed points. It suffices to use the associated inference system to get the following theorem, which we prove using the deductive method.

Theorem 3 (Tarski revisited). Let (E , ≤) be a complete lattice. Let η : E → E be an isotone map over E . Consider the inference system Φ over E containing all the rules, and only these rules, of the following form: S s S ⊆ E , s ≤ η(∨ S) .

Then:

≤ (lfp η) = ∆(Φ) and ≤ (gfp η) = ∇(Φ).
Proof. It is easy to show that the inference operator ϕ associated to Φ is equal to δ

• ι • η • ι -1 • γ,
with the preceding notation. As ≤ (lfp η) = lfp ϕ and ≤ (gfp η) = gfp ϕ, we can conclude by applying Theorem 2.

Proving fixed points

Grall

Two Other Fixed Point Theorems. The deductive characterization of fixed points is still pertinent when we consider two other well-known fixed point theorems, where the assumptions for the poset and the map are weakened.

A poset is chain-complete if any chain, including the empty chain, has a least upper bound4 . Tarski's theorem can be extended to chain-complete posets, as shown for instance by Markowsky [8,Th. 9]. We again resort to the preceding inference system to characterize the least fixed point, with two restrictions: we only consider chains as premises and greatest judgments as conclusions.

Theorem 4 (Fixed point theorem for chain-complete poset). Let (E , ≤) be a chain-complete poset and η : E → E an isotone map. Let Φ be the inference system over E containing all the rules, and only these rules, of the following form: C

η(∨C) C ⊆ E ,C chain .
Then η has a least fixed point lfp η satisfying:

≤ (lfp η) = ≤ ∆(Φ).
Proof. We first show that ∆(Φ) is a chain, precisely that for any x 1 and any x 2 in ∆(Φ), we have x 1 ≤ x 2 or x 2 ≤ x 1 . We proceed by induction over well-founded proofs. Consider a well-founded proof ended with the rule (C 1 , η(∨C 1 ). Assume as inductive hypothesis that for any y 1 ∈ C 1 and any y 2 ∈ ∆(Φ), we have y 1 ≤ y 2 or y 2 ≤ y 1 . Let x 2 be in ∆(Φ). There exists a chain C 2 included in ∆(Φ) such that x 2 = η(∨C 2 ).

There are two cases. First, assume ∃ y

1 ∈ C 1 . ∀ y 2 ∈ C 2 . y 2 ≤ y 1 .
We therefore have, for some y 1 in C 1 and for all y 2 in C 2 : y 2 ≤ y 1 , y 2 ≤ ∨C 1 and ∨C 2 ≤ ∨C 1 . We deduce by monotony x 2 ≤ η(∨C 1 ).

Second, assume ∀ y 1 ∈ C 1 . ∃ y 2 ∈ C 2 . ¬(y 2 ≤ y 1 ). We therefore have, for all y 1 in C 1 and some dependent point y 2 in C 2 : y 1 ≤ y 2 (inductive hypothesis), y 1 ≤ ∨C 2 and ∨C 1 ≤ ∨C 2 . We deduce by monotony η(∨C 1 ) ≤ x 2 .

Since ∆(Φ) is a chain, ∆(Φ), η(∨ ∆(Φ)) is a rule. We have η(∨ ∆(Φ)) ∈ ∆(Φ), hence η(∨ ∆(Φ)) ≤ ∨ ∆(Φ) and then η 2 (∨ ∆(Φ)) ≤ η(∨ ∆(Φ)) by monotony. Assume x is η-closed: η(x) ≤ x. It is easy to show by induction over well-founded proofs that x is an upper bound of ∆(Φ). We deduce that first ∨ ∆(Φ) ≤ η(∨ ∆(Φ)) and second ∨ ∆(Φ) is the least fixed point of η.

Finally ≤ (lfp η) = ≤ ∆(Φ) since ∨ ∆(Φ) ∈ ∆(Φ).
Actually, as shown by Markowsky [8, Th. 9], the preceding theorem can be considered as a corollary of Bourbaki-Witt's theorem [3]. We also give a proof of this theorem by using the same inference system as in Theorem 4.

Theorem 5 (Bourbaki-Witt). Let E be a chain-complete poset and η : E → E an expansive5 map. Let Φ be the inference system over E containing all the rules, and only these rules, of the following form:

C η(∨C) C ⊆ E ,C chain .
Then η has a fixed point fp η satisfying:

≤ (fp η) = ≤ ∆(Φ).
Proving fixed points

Grall

Proof. We show that ∆(Φ) is a chain, which allows to conclude. Indeed, if ∆(Φ) is a chain, the inference rule ∆(Φ), η(∨ ∆(Φ)) belongs to Φ. From η(∨ ∆(Φ)) ∈ ∆(Φ), we deduce η(∨ ∆(Φ)) ≤ ∨ ∆(Φ). Since η is expansive, we deduce that ∨ ∆(Φ) is a fixpoint of η. Moreover, ∨ ∆(Φ) belongs to ∆(Φ). Therefore ≤ ∆(Φ) = ≤ (∨ ∆(Φ)).

To show that ∆(Φ) is a chain, we introduce the notion of useful proofs. A well-founded proof, say ended by the rule (C, η(∨C)), is said useful if for any well-founded proof, say ended by the rule (D, η(∨ D)), we have:

(∨ D < ∨C) ⇒ (η(∨ D) ≤ ∨C).
Two crucial properties about usefulness can be asserted. First, for any useful proof ended by (C, η(∨C)) and any well-founded proof ended by (D, η(∨ D)), we have either η(∨C) = η(∨ D), η(∨C) ≤ ∨ D or η(∨ D) ≤ ∨C. Second, all well-founded proofs are useful.

Thanks to these properties, it is easy to conclude that ∆(Φ) is a chain. Indeed, let x 1 and x 2 be in ∆(Φ). There exists two well-founded proofs, respectively ended by (C 1 , η(∨C 1 )) and (C 2 , η(∨C 2 )), such that x 1 = η(∨C 1 ) and x 2 = η(∨C 2 ). Since the former proof is useful, we have by applying the first property either

x 1 = x 2 , x 1 ≤ ∨C 2 or x 2 ≤ ∨C 1 . Since η is expansive, we deduce x 1 ≤ x 2 or x 2 ≤ x 1 .
The two properties about usefulness can be proved by induction over well-founded proofs. The arguments used are standard, since the notion of useful proofs comes from the notion of extreme points, used in the proof of the Bourbaki-Witt's theorem following the impredicative method: see for instance the proof in Lang's book [6, pp. 881-884].

Comparison of the Methods. Tarski's theorem and its two extensions to chain-complete posets are usually proved with the iterative method or the impredicative method, two methods that are not clearly connected. We now suggest that the deductive method allows these two methods to be connected.

First, to each inference system Φ used in Theorems 3, 4 and 5, we can associate an inference operator ϕ over 2 E . Thus, the inductive interpretation ∆(Φ) of Φ can also be defined as the smallest ϕ-closed set, as expressed in Theorems 1 and 2. It turns out that the definition of a ϕ-closed set is very akin to the definition of an admissible set, as found in the standard proof of Bourbaki-Witt's theorem following the impredicative method [6, pp. 881-884].

Second, the deductive method can be considered as an abstraction of the iterative method: it abstracts away from the iterative process involved in proof construction. The following proposition precisely describes their relationship in the case of Tarski's theorem. The height of a well-founded proof tree d is defined as follows: it is the least ordinal greater than the height of each immediate proof sub-tree of d. Given an inference system Φ over E and an ordinal α, we say that x ∈ E has complexity α if there is a well-founded proof of x with height less or equal to α. We denote by ∆ α (Φ) the set of all x with complexity α.

Proposition 1. Let (E , ≤) be a complete lattice and η : E → E an isotone map over E . Consider the transfinite sequence (∆ α (η)) α defined as follows:

∆ α (η) = η( β |β <α ∆ β (η)).
Consider the inference system Φ containing all the rules, and only these rules, of the following form: S s S ⊆ E , s ≤ η(∨ S) .

Then, for any ordinal α: ≤ ∆ α (η) = ∆ α (Φ). Proof. By transfinite induction.

An analogous proposition holds for the two other fixed point theorems.

Conclusion

We have presented a method to characterize the fixed points described in fixed point theorems for complete lattices and chain-complete posets. The method is deductive: the fixed points are "proved" in some inference system. The techniques used in the proofs of these theorems is consistent with the method: they are based on induction over well-founded proofs. Finally, we have sketched a comparison between the deductive method and the two traditional methods, impredicative and iterative. In brief, given an inference system, the impredicative method essentially corresponds to the characterization à la Tarski using the inference operator associated to the inference system, whereas the iterative method corresponds to an iterative construction of the well-founded proofs in the inference system. The connection that we have suggested deserves a further exploration, which we reserve to future work.

We have already experienced the deductive method in a work about coinductive operational semantics [7]. It turns out that the method is well-suited to the proof assistant Coq, which uses a calculus of inductive and coinductive constructions, an extension of type theory. The fixed points were expressed through inference systems and defined over powerset lattices. A motivation of the present work was to extend the method to fixed points defined in Coq over complete lattices or chain-complete posets. The iterative method resorts to ordinals, which are rarely used in Coq. Indeed, either they require to encode set theory, which is expensive, or they are implemented as constructive ordinals, which is restrictive. As for the impredicative method, it does not really fit with the calculus of inductive and coinductive constructions. Thus, the deductive method is a good candidate. A major problem to be solved is the use of classical logic. First, since the fixed points defined may have a non-terminating behavior, for instance when the fixed point is a function possibly divergent, adding classical logic axioms to the constructive logic of Coq is needed. In the same way, in the preceding proofs of the fixed point theorems, we have used the law of excluded middle. Second, as explained in the recent proposal of Bertot and Komendantsky [2], the addition of classical logic axioms should allow not only to reason about a fixed point with a terminating or non-terminating behavior, but also to extract a program computing the fixed point from the proof that the fixed point satisfies its specification, following the Curry-Howard correspondence.

Introduction

Recursion is an important programming language feature that provides a fixpoint of an endofunction. But an endofunction may have many fixpoints, so an important question in semantics is to determine which is the one calculated by recursion. For example, for both the may-testing and must-testing preorders, recursion calculates the least pre-fixed point. (In the case of must-testing, we must assume the calculus uses erratic rather than ambiguous nondeterminism, see e.g. [START_REF] S B Lassen | Relational Reasoning about Functions and Nondeterminism[END_REF].)

What if we work modulo bisimilarity? We provide a characterization of the fixpoint calculated by recursion as follows. First calculate the least pre-fixed point up to similarity. Within this equivalence class, calculate the least pre-fixed point up to 2-nested similarity. Iterate this procedure through all the countable ordinals and it converges on a single point: the "nesting fixpoint". This is the one that recursion calculates.

In Sect. 2 we introduce the general notions of nested simulation and nesting fixpoints. We illustrate them in Sect. 3 with the process calculus CCS.

Notation

• We write ω 1 for the least uncountable ordinal.

• For any sets X,Y, Z and relations R ⊆ X ×Y and R ⊆ Y × Z, we write R; R for the composite.

• For any sets X and Y , we write X Y for the set of partial functions from X to Y with finite domain.

• For any set X with preorder , and any ∩ -equivalence class U, we write

↓ (U) def = {x ∈ X | ∃y ∈ X. x y} = {x ∈ X | ∀y ∈ X. x y}

Transition systems and ω 1 -nested preorders

We first recall the basic notions of transition systems. Definition 1. Let Act be a set of actions, and let S = (X, →) be an Act-labelled transition system, i.e. a set X together with a relation → ⊆ X × Act × X.

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 47-52 1. For each x ∈ X and a ∈ Act, we write succ a (P)

def = {Q ∈ Prog | P → a Q}
If this set is always countable, S is said to be image-countable.

2. A relation R ⊆ X × X is
• a simulation on S when for all (x, x ) ∈ R and a ∈ Act, if y ∈ succ a (x) then there exists y ∈ succ a (x ) such that (x , y ) ∈ R.

• a bisimulation on S when both R and its converse are simulations.

3. The greatest bisimulation is called bisimilarity. It is an equivalence relation and written .

4. Let be a preorder on X. A relation R ⊆ X × X is

• a simulation up to on the right when for all (x, x ) ∈ R and a ∈ Act, if y ∈ succ a (x) then there exists y ∈ succ a (x ) such that (x , y ) ∈ (R; )

• a simulation up to when for all (x, x ) ∈ R and a ∈ Act, if y ∈ succ a (x) then there exists y ∈ succ a (x ) such that (x , y ) ∈ ( ; R; ) Definition 2.

[GV92] Let Act be a set, and let S = (X, →) be an Act-labelled transition system. For each ordinal α, we shall define a preorder α , known as α-nested similarity, with the property that any simulation contained in α is also contained in α . We define α to be (α = β + 1) the greatest simulation contained in β , or equivalently the greatest simulation contained in β ∩ β (α a limit ordinal) the intersection of β over all β < α.

Lemma 1. [GV92]

Let Act be a set, and let (X, →) be an Act-labelled transition system.

1. Let β be an ordinal. If R is a simulation up to β +1 contained in β , then R is contained in β +1 .

2. α contains bisimilarity, for each ordinal α.

3. If (X, →) is image-countable, then ω 1 is bisimilarity.

We are thus led to the following abstract notion.

Definition 3. Let X be a set. An ω 1 -nested preorder on X is a sequence of preorders ( α ) α ω 1 such that

• ( α+1 ) ⊆ ( α ) ∩ ( α ), for each α < ω 1 • ( γ ) = α<γ ( α ), for each limit ordinal γ ω 1
It follows that

• ( 0 ) is the indiscrete relation • α β ω 1 implies ( β ) ⊆ ( α ) • α < β ω 1 implies ( β ) ⊆ ( α )
• ( α ) is an equivalence relation, for each limit ordinal α ω 1 .

In particular, ω 1 is an equivalence relation, which we write ≡.

Definition 4. Let Act be a set, and let S = (X, →) be an Act-labelled transition system. We write A(S ) for the ω 1 -nested preordered set (X, ( α ) α ω 1 ).

Definition 5. Let A = (X, ( α ) α ω 1 and B = (Y, ( α )) α ω 1 be ω 1 -nested preordered sets. A monotone function A f / / B is a function X f / / Y such that, for every α ω 1 (or equivalently: every

successor ordinal α < ω 1 ), if x ⊆ α A x then f (x) ⊆ α B f (x )
. Now we come to our key definition. Definition 6. Let A = (X, ( α ) α ω 1 be an ω 1 -nested preordered set, and let f be a monotone endofunction on A. We shall define a decreasing sequence of subsets (U f α ) α ω 1 of X such that U f α either is empty or satisfies the following conditions:

• U f α is an equivalence class of α ∩ α
• f restricts to an endofunction on U f α and hence on ↓ α (U f α )

• if x ∈ ↓ α (U f α ) and f (x) α x then x ∈ U f α .
We define U f α to be

(α = β + 1) the set of α-least elements of {x ∈ U f β | f (x) α x} = {x ∈ ↓ β (U f β ) | f (x) α x}
(α a limit ordinal) the intersection of U f β over all β < α.

The elements of U f ω 1 are called nesting fixpoints of f .

Note that nesting fixpoints are fixpoints up to ≡ and unique up to ≡. But some monotone endofunctions f do not have a nesting fixpoint-i.e. U f ω 1 is empty.

CCS and Bisimilarity

Our thesis is that a recursive program in a transition system S is is a nesting fixpoint of the monotone endofunction on A(S ) given by the recursion body. To illustrate this, we consider the calculus CCS [START_REF] Milner | Communication and Concurrency[END_REF], over a fixed set Act of actions.

As CCS is untyped, a context Γ is merely a list of distinct identifers. The syntax is given inductively by the rules in Fig. 1. We write Prog for the set of programs, i.e. closed terms, which forms an Actlabelled transition system with transition relation → defined inductively by the rules in Fig. 2. This system is easily shown to be image-countable, and we call it CCS.

Our version of CCS includes parallel composition of any countable arity I, with synchronization described by a relation V saying when finitely many actions performed by the constituent processes may cause an action in the combined process. In [START_REF] Milner | Communication and Concurrency[END_REF], Act is given by a disjoint union

{a | a ∈ Σ} ∪ {a | a ∈ Σ} ∪ {τ}
where Σ is a set of synchronization actions. The parallel composition, hiding and renaming operators provided there are subsumed by our parallel composition as follows.

Levy

Γ P a ∈ Act Γ a.P Γ P i (∀i ∈ I) I countable Γ ∑ i∈I P i Γ, x P Γ rec x. P x ∈ Γ Γ x Γ P i (∀i ∈ I) I countable, V ⊆ (I fin Act) × Act Γ V i∈I P i Figure 1: Syntax of CCS a.P → a P P î → a Q î ∈ I ∑ i∈I P i → a Q P[rec x. P/x] → a Q rec x. P → a Q P i → b(i) Q i (∀i ∈ dom b) (b, a) ∈ V V i∈I P i → a V i∈I Q i (if i ∈ dom b) P i (otherwise)
Figure 2: Operational Semantics (Transitions) of CCS

• We express P | Q as V {0 → P, 1 → Q}, with V given by {({0 → a, 1 → a}, τ) | a ∈ Σ} ∪ {({0 → a, 1 → a}, τ) | a ∈ Σ} ∪ {({0 → a}, a) | a ∈ Act} ∪ {({1 → a}, a) | a ∈ Act} • Let f : Σ → Σ be a function. We express P[ f ] as V {0 → P}, with V given by {({0 → a}, f (a)) | a ∈ Σ} ∪ {({0 → a}, f (a)) | a ∈ Σ} ∪ {(0 → τ, τ)}
• Let L ⊆ Σ be a subset. We express P\L as V {0 → P}, with V given by

{({0 → a}, a) | a ∈ Σ \ L} ∪ {({0 → a}, a) | a ∈ Σ \ L} ∪ {(0 → τ, τ)}
The "synchronization algebras" of [START_REF] Winskel | Models for concurrency[END_REF] are likewise expressible. As explained in [START_REF] Milner | Communication and Concurrency[END_REF], we could also incorporate into the language countably mutual recursion. We have not done so, but our results would go through without difficulty.

The following operations on programs are called the basic operations: P → a.P for any a ∈ Act

(P i ) i∈I → ∑ i∈I P i for any countable I (P i ) i∈I → V i∈I P i
for any countable I and V ⊆ (I fin Act) × Act Proposition 1. The basic operations preserve α-nested similarity, for every ordinal α, and hence preserves bisimilarity.

Proof. Straightforward induction on α. Preservation of bisimilarity may also be proved directly.

Lemma 2. Let R be a simulation on CCS. Then the relation

{(M[P/x], M[P /x]) | (P, P ) ∈ R, x M}
is also a simulation.

Proof. We want to show that if M[P/x] → a Q, then for all P such that (P,

P ) ∈ R we have (R, R ) ∈ R and x N such that Q = N[R/x] and M[P /x] → a N[R /x].
We proceed by induction on →. We omit the details.

Proposition 2. (Definable functions are monotone) Let x M be a term. Then the endofunction on Prog

P → M[P/x]
preserves α-similarity, for every ordinal α, and hence preserves bisimilarity.

Proof. By induction on α using Lemma 2. Preservation of bisimilarity also follows directly from Lemma 2.

Lemma 3. Let be a preorder on Prog that is a simulation and preserved by the basic operations. Let Proof. We have to show that rec x. M is in U f α for each α ω 1 . The case where α is a limit ordinal is trivial, so suppose α = β + 1. Since rec x.M ∈ U f β we have

↓ β (U f β ) = {P ∈ Prog | P β rec x. M}
We need to show that rec x. M is an β +1 -least element of

{P ∈ ↓ β (U f β ) | f (P) α P} = {P ∈ Prog | P β rec x. M ∧ M[P/x] α P} It is an element because M[rec x. M/x] rec x. M. Suppose P is another element. Then {(N[rec x. M/x], N[P/x]) | x N}
is contained in β and, by Lemma 3, is a simulation up to α on the right. Lemma 1(1) tells us that it is contained in α , so rec x. M α P as required. This result may also be proved using Howe's method [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF][START_REF] Levy | Infinitary Howe's method[END_REF].

Conclusions and Further Work

The present paper was greatly inspired by the denotational semantics in [START_REF] Roscoe | Seeing beyond divergence[END_REF], where recursion is interpreted by a "reflected" fixpoint calculated in two steps. The quotient of CCS by bisimilarity is an image-countable transition system S in which bisimilarity is discrete. (It can also be described as a final coalgebra [START_REF] Turi | On the foundations of final coalgebra semantics[END_REF].) Therefore nesting fixpoints in A(S ) are genuine fixpoints and unique. This almost provides a denotational semantics, except that some monotone endofunctions do not have a nesting fixpoint. Perhaps restricting to the exploratory functions of [START_REF] Blain | Exploratory functions on nondeterministic strategies, up to lower bisimilarity[END_REF] would be fruitful, as these are all definable in a sufficiently rich calculus.

In [START_REF] Abramsky | A domain equation for bisimulation[END_REF] a domain theoretic model is provided that captures bisimilarity between processes without divergences. For general processes it induces a more subtle preorder.

The results of this paper may be adapted to lower (i.e. divergence-insensitive) applicative bisimulation [START_REF] Abramsky | The lazy λ -calculus[END_REF] in nondeterministic λ -calculus. However, in this instance Howe's method is stronger because it shows applicative bisimilarity to be preserved not only by recursion (Corollary 1) but also by application.

The Equivalence of Game and Denotational Semantics for the Probabilistic µ-Calculus

Matteo Mio LFCS, School of Informatics, University of Edinburgh M.Mio@sms.ed.ac.uk

Introduction

The modal µ-calculus L µ [7] is a very expressive logic obtained by extending classical propositional modal logic with least and greatest fixed point operators. The logic L µ has been extensively studied as it provides a very powerful tool for expressing properties of labeled transition systems [14]. Encodings of many important temporal logics such as LTL, CTL and CTL * into L µ [1], provided evidence for the very high expressive power of the calculus. A precise expressivity result was given in [6], where the authors showed that every formula of monadic second order logic over transition systems which does not distinguish between bisimilar models is equivalent to a formula of L µ . The logic L µ has a simple denotational interpretation [14] and an elegant proof theory [15]. However it is often very difficult to intuitively grasp the denotational meaning of a L µ formula as the nesting of fixed point operators can induce very complicated properties. To alleviate this problem, another complementary semantics for the logic L µ , based on two player (parity) games, has been studied in [3,14]. The two semantics have been proven to coincide and this allows us to pick the most convenient viewpoint when reasoning about the logic L µ . One of the main properties of the games used to give semantics to L µ formulae is the so called positional determinacy which asserts that both Players can play optimally in a given game-configuration without knowing the history of the previously played moves.

In the last decade, a lot of research has focused on the study of reactive systems that exhibit some kind of probabilistic behavior, and logics for expressing their properties. Segala systems [13] are a natural generalization of labeled transition systems to the probabilistic scenario. Given a countable set of labels L, a Segala System is a pair P, { a -→} a∈L where P is a countable set of states and, for each a ∈ L, a -→ ⊆ P × D(P) is the a-accessibility relation, where D(P) is the set of probability distributions over P.

The transition relation models the dynamics of the processes: (p, d) ∈ a -→ means that the process p can perform the atomic action a ∈ L and then behave like the process q with probability d(q). The probabilistic modal µ-calculus pL µ , introduced in [12,5,2], is a generalization of L µ designed for expressing properties of Segala systems. This logic was originally named quantitative µ-calculus, but since other µ-calculus-like logics, designed for expressing properties of non-probabilistic systems, have been given the same name (e.g. [4]), we adopt the probabilistic adjective. The denotational semantics for the logic pL µ of [12,2], interprets every formula F as a map F : P → [0, 1], which assigns to each process p a degree of truth. Actually, in [5] three different possible denotational semantics for pL µ (including the one of [12,2]) have been proposed as there there is no, a priori, good reason to prefer one in favour of the others. In [9,10], the authors introduce a game semantics for the logic pL µ . This semantics, given in term of two player stochastic (parity) games, is the natural generalization of the two player (non stochastic) game semantics for the logic L µ ; the key difference being that in the configuration p, a F (respectively p, [a] F ) Player 1 (respectively Player 2) choses a a-successor of p, i.e. a distribution d such that (p, d) ∈ a -→, and the next configuration q, F is then reached with probability d(q). This semantics Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 53-59 Mio allows one to interpret formulae as expressing, for each process p, the (limit) probability of the property specified by the formula to hold in the state p. This game semantics suggests a very clear operational interpretation for the logical connectives of the logic which, a posteriori, justifies the denotational interpretation of [12,2]. In [10,9], the authors proved the equivalence of the denotational and game semantics for pL µ only for finite models. The proof crucially depends on positional determinacy which does not hold, in general, for the infinite pL µ stochastic parity games generated by infinite models. The general result, i.e. the equivalence of the game and denotational semantics for arbitrary infinite models, has been left open. In this workshop paper we show that the equivalence indeed holds for arbitrary infinite models, thus strengthening the connection between denotational and game semantics. Our contribution consists in adapting the technique introduced in [4], where the authors used it to prove a similar result for a µcalculus-like logic designed to express quantitative properties of (non-probabilistic) labeled transition systems. While this is not a difficult adaption, the result seems worth noticing since the question has been open in literature since [9]. Moreover the differences between the games considered in [4] and pL µ stochastic games, e.g. the fact that Markov chains are the outcomes of the games rather than just infinite paths, make this result not immediate from [4].

The rest of the paper is organized as follows: in section 2 we define the syntax of the logic pL µ and the class of models given by Segala systems; in section 3 we define the denotational semantics of pL µ as in [12,2]; in section 4 we define the class of parity games that are going to be used to give game semantics to the logic; in section 5 we define the game semantics of pL µ in terms of two player stochastic parity games; in section 6 we state the main theorem which asserts the equivalence of the denotational and game semantics. An extended version of this paper with detailed proofs is available at [11].

The Probabilistic Modal µ-Calculus

Given a set Var of propositional variables ranged over by the letters X,Y, Z and a set of labels L ranged over by the letters a, b, c, the formulae of the logic are defined by the following grammar:

F, G ::= X | a F | [a] F | F ∨ G | F ∧ G | µX.F | νX.F
We assume the usual notions of free and bound variables. A formula is closed if it has no free variables. Definition 2.1 (Subformulae). We define the function Sub(F) by case analysis on F as follows:

Sub(X) def = {X} Sub(F 1 ∧ F 2 ) def = {F 1 ∧ F 2 } ∪ Sub(F 1 ) ∪ Sub(F 2 ) Sub([a] F) def = {[a] F} ∪ Sub(F) Sub(νX.F) def = {νX.F} ∪ Sub(F)
The cases for the connectives ∨, a and µX are defined as for their duals. We say that G is a subformula of F if G ∈ Sub(F). Definition 2.2 (Normal Formula). A formula F is normal if

• Whenever 1 X 1 and 2 X 2 , with 1 , 2 ∈ {µ, ν}, are two different occurrences of binders in F then

X 1 = X 2 .
• No occurrence of a free variable X is also used in a binder X in F.

Every formula can be put in normal form by standard α-renaming of the bound variables. We only consider formulae F in normal form. A bound variable X in F is called a µ-variable (respectively a Mio ν-variable) if it is bound in F by a µ (respectively ν) operator.

Definition 2.3 (Variables subsumption). Given a normal formula

F such that 1 X 1 .F 1 , 2 X 2 .F 2 ∈ Sub(F), we say that the variable X 1 subsumes X 2 in F if 2 X 2 .F 2 ∈ Sub(F 1 ).
The formulae of the logic pL µ are interpreted over the class of models given by Segala systems. 3 Denotational Semantics Given a Segala system P, { a -→} a∈L we denote by (P → [0, 1]) and by (D(P) → [0, 1]) the complete lattice of functions from P and from D(P) respectively, to the real interval [0, 1] with the component-wise order. Given a function f ∈ (P → [0, 1]), we denote by f ∈ (D(P) → [0, 1]) the lifted function defined as follows:

f def = λ d. ∑ p∈supp(d) d(p) • f (p) . A function ρ : Var → (P → [0, 1]
) is called an interpretation of the variables. Given a function f ∈ (P → [0, 1]) we denote by ρ[ f /X] the interpretation that assigns f to the variable X, and ρ(Y ) to all other variables Y . Fix a Segala System P, { a -→} a∈L and an interpretation ρ, the denotational semantics F ρ : P → [0, 1] of the pL µ formula F, under the interpretation ρ, is defined by structural induction on F as follows:

X ρ = ρ(X) G ∨ H ρ = G ρ H ρ G ∧ H ρ = G ρ H ρ a G ρ = λ p. { G ρ (d) | p a -→ d} [a] H ρ = λ p. { H ρ (d) | p a -→ d} µX.G ρ = lfp of the functional λ f .( G ρ[ f /X] ) νX.H ρ = gfp of the functional λ f .( H ρ[ f /X] )
Since the interpretation assigned to every pL µ operator is monotone, the existence of the least and greatest fixed points is guaranteed by the Knaster-Tarski theorem. Moreover the least and the greatest fixed point can be computed inductively:

µX.G ρ = α µX.G α ρ and νX.G ρ = α νX.G α ρ where µX.G α ρ def =      G ρ[λ p.0/X] G ρ[ µX.G α-1 ρ /X] G ρ[ β <α µX.G β ρ /X] νX.G α ρ def =      G ρ[λ p.1/X] for α = 0 G ρ[ νX.G α-1 ρ /X] for α successor ordinal. G ρ[ β <α νX.G β ρ /X]
for α limit ordinal.

Two Player Stochastic Parity Games

A turn-based Stochastic Game Arena (or just a 2 1 2 Game Arena) is a tuple A = (S, E), {S 1 , S 2 , S P }, π where (S, E) is a directed graph with countable set of states S and successor function E : S → 2 S ; the sets S 1 , S 2 , S P are a partition of S and π : S P → D(S) is called the probabilistic transition function. For every state s ∈ S, E(s) is the (possibly infinite) set of successors of s. We require that for all s ∈ S P , E(s) = supp(π(s)) = / 0. We denote by S t the set of terminal states, i.e. those s ∈ S such that E(s) = / 0.

Mio

The states in S 1 are Player 1 states; the states in S 2 are Player 2 states; the states in S P are probabilistic, or Player P, states. At a state s ∈ S 1 (respectively s ∈ S 2 ), if s ∈ S t Player 1 (respectively Player 2) chooses a successor from the set E(s); if s ∈ S t the game ends. At a state s ∈ S P , a successor state is chosen probabilistically according to the distribution π(s).

A finite path s in A is a finite sequence s 0 , ..., s n of states in S such that for every 0 < i ≤ n, s i ∈ E(s i-1

). An infinite path s in A is an infinite sequence of states {s i } i∈N such that for every i > 0, s i ∈ E(s i-1 ).

We denote by P ω and P <ω the sets of infinite paths and finite paths in A respectively. Given a finite path s ∈ P <ω we denote by last( s) the last state s ∈ S of s. We denote by P <ω 1 , P <ω 2 and P <ω P the sets of finite paths having last state in S 1 , S 2 and S P respectively. We also denote by P t the set of finite paths ending in a terminal state, i.e. the set of paths s such that E(last( s)) = / 0; the paths in P t are called terminated paths. We denote by P the set P ω ∪ P t and we refer to this set as the set of the possible Plays in A. Given a finite path s ∈ P <ω , we denote by O s the set of all plays having s as prefix. We consider the standard topology on P , where the basis for the open sets is given by the cones in G, i.e. the sets O s for s ∈ P <ω .

As usual in Game Theory, Players' moves are determined by strategies. A (full memory) deterministic strategy σ 1 for Player 1 in the Game Arena A is defined as usual as a function σ 1 :

P <ω 1 → S ∪ {•} such that σ 1 ( s) ∈ E(last(s)) if E(last( s)) = / 0 and σ 1 ( s) = • otherwise.
Similarly a strategy σ 2 for Player 2 is defined as a function σ 2 :

P <ω 2 → S ∪ {•}.
A pair σ 1 , σ 2 of strategies, one for each player, is called a strategy profile and determines the behaviors of both players. Fix a strategy profile σ 1 , σ 2 and an initial state s ∈ S we denote by M s σ 1 ,σ 2 the Markov Chain obtained by pruning A, starting from s, accordingly with σ 1 and σ 2 . We often refer to this Markov Chain as the Markov Play generated by the strategy profile σ 1 , σ 2 from s ∈ S. Each Markov Play M s σ 1 ,σ 2 has an associated probability measure on the set P of plays in A, which we denote by M s σ 1 ,σ 2 . The probability measure M s σ 1 ,σ 2 is defined as usual as the unique probability measure which assigns to every basic open set O s the multiplication of all the probabilities associated with the probabilistic transitions in s.

A priority assignment P (of rank n ∈ N) for the arena A is a function assigning a natural number in {0, ..., n} to every state in S, i.e. P : S → {0, ..., n}. Given a priority assignment P of any rank, and an infinite path s = {s i } i∈N , we denote by P( s) the greatest natural number appearing infinitely often in the infinite sequence {P(s i )} i∈N . A reward assignment B for the arena A is a function assigning a value in the real interval [0, 1] to each terminal state s ∈ S t , i.e. B : S t → [0, 1]. A pair P, B of a priority assignment P and a reward assignment B for the arena A, determines a unique measurable function Φ P,B : P → [0, 1] defined as follows:

Φ P,B ( s) =    B(last( s)) if s ∈ P t 0 if s ∈ P ω and P( s) is even 1 if s ∈ P ω and P( s) is odd
The value Φ P,B ( s) should be understood as the payoff assigned to Player 1 when s is the outcome of the game. The payoff function Φ P,B is called the Parity payoff determined by P, B . We say that Φ P,B has rank n if P has rank n. We often omit the subscript P, B in Φ P,B if the context is clear enough. Note that, since the priority assigned by P to the terminal states s ∈ S t does not affect the induced payoff function, we can assume, without any loss of generality, that P(s) = 0 for any terminal state s ∈ S t . From now on we assume that this condition holds for every priority assignment P.

A Two Player Stochastic Parity Game G is a tuple G = A, P, B of a 2 1 2 Game Arena A, a priority assignment P and a B assignment for the arena A. Given a Parity game G = A, P, B , a state s ∈ S and a Mio strategy profile σ 1 , σ 2 , we denote by with M s σ 1 ,σ 2 (Φ P,B ) the value defined as:

P Φ P,B dM s σ 1 ,σ 2
which corresponds to the expected payoff for Player 1 when the game starts in the state s and Player 1 and Player 2 follow the strategies σ 1 and σ 2 respectively. We denote by Val 1 (G ) : S → [0, 1] and Val 2 (G ) : S → [0, 1] the functions defined as follows:

Val 1 (G )(s) = σ 1 σ 2 M s σ 1 ,σ 2 (Φ) Val 2 (G )(s) = σ 2 σ 1 M s σ 1 ,σ 2 (Φ).
Val 1 (G )(s) represents the limit (expected) payoff that Player 1 can get, when the game begins in s, by choosing his strategy σ 1 first and then letting Player 2 pick an appropriate counter strategy σ 2 . Similarly Val 2 (G )(s) represents the limit (expected) payoff that Player 1 can get, when the game begins in s, by first letting Player 2 choose a strategy σ 2 and then picking an appropriate counter strategy σ 1 . Clearly Val 1 (G )(s) ≤ Val 2 (G )(s) for every s ∈ S. Theorem 4.1 (Determinacy [8]). For every Two Player Stochastic Parity Game G = A, P, B the following equality holds:

∀s ∈ S, Val 1 (G )(s) = Val 2 (G )(s).
Intuitively the determinacy Theorem states that the players do not get any advantage by letting the opponent choose his strategy first. We just write V(G ) for the value function of the Game defined as Val 1 (G ) = Val 2 (G ). As a corollary of the Determinacy theorem we have the following Lemma: Lemma 4.2 (ε-optimal strategies). Given a Two Player Stochastic Parity Game G = A, P, B , for every ε > 0 the following assertions hold:

• there exists a strategy σ ε 1 for Player 1 such that for every s ∈ S,

σ 2 M s σ ε 1 ,σ 2 (Φ) > V(G )(s) -ε.
• there exists a strategy σ ε 2 for Player 2 such that for every s ∈ S,

σ 1 M s σ 1 ,σ ε 2 (Φ) < V(G )(s) + ε.

Game Semantics

Fix a Segala System P, { a -→} a∈L , a formula F and an interpretation ρ : Var → (P → [0, 1]) of the variables, we denote by G F ρ the parity game A, P, B formally defined as described below. The state space of the arena A = (S, E), {S 1 , S 2 , S P }, π , is the set S = P ∪ D(P) × Sub(F) of pairs of states p ∈ P or distributions d ∈ D(P) and subformulae G ∈ Sub(F); the transition relation E is defined as

E( d, G ) = { p, G | p ∈ supp(d)} for every d ∈ D(P); E( p, G
) is defined by case analysis on the outermost connective of G as follows:

1. if G = X, with X free in F, then E( p, G ) = / 0. 2. if G = X, with X bound in F by the subformula X.H, with ∈ {µ, ν}, then E( p, G ) = { p, X.H }. 3. if G = X.H, with ∈ {µ, ν}, then E( p, G ) = { p, H }. 4. if G = a H or G = [a] H then E( p, G ) = { d, H | p a -→ d}. 5. if G = H ∨ H or G = H ∧ H then E( p, G ) = { p, H , p, H }
The partition {S 1 , S 2 , S P } is defined as follows: every state p, G with G's main connective in { a , ∨, µX} or with G = X where X is a µ-variable, is in S 1 ; dually every state p, G with G's main connective in {[a] , ∧, νX} or with G = X where X is a ν-variable, is in S 2 . Finally every state d, G is in S P . The terminal states p, X , with X free in F, are in S 1 by convention. The probability transition function π : S P → S is defined as π( d, G )( p, G ) = d(p). The priority assignment P is defined as usual in µ-calculus model checking games [14]: the priority assigned to the states p, X , with X a µ-variable is even; dually the priority assigned to the states p, X , with X a ν-variable is odd. Moreover P( p, X ) > P( p , X ) if X subsumes X in F. All other states get priority 0. The reward assigment B is defined as B( p, X ) = ρ(X)(p) for every terminal state p, X with X free in F. All other terminal states in G F ρ are either of the form p, a H or p, [a] H . The reward assignment B is defined on these terminal states as follows: B( p, a H ) = 0 and B( p, [a] H ) = 1. Fix a Segala system P, { a -→} a∈L , the game semantics of the formula F under the interpretation ρ, is the function

F ρ : P → [0, 1] defined as F ρ def = λ p.V(G F ρ )( p, F ).
6 Equivalence of Denotational and Game Semantics for pL µ

We are now ready to give the main theorem which states that given any Segala system P, { a -→} a∈L , the denotational and game semantics of any pL µ formula coincide. Theorem 6.1. Given a Segala system P, { a -→} a∈L , for every pL µ formula F and interpretation ρ for the variables, the following equality holds: F ρ = F ρ .

Denotational semantics for lazy initialization of letrec black holes as exceptions rather than divergence

Keiko Nakata Institute of Cybernetics at Tallinn University of Technology

Abstract

We present a denotational semantics for a simply typed call-by-need letrec calculus, which distinguishes direct cycles, such as let rec x = x in x and let rec x = y and y = x + 1 in x, and looping recursion, such as let rec f = λ x. f x in f 0. In this semantics the former denote an exception whereas the latter denotes divergence.

The distinction is motivated by "lazy evaluation" as implemented in OCaml via lazy/force and Racket (formerly PLT Scheme) via delay/force: when a delayed variable is dereferenced for the first time, it is first pre-initialized to an exception-raising thunk and is updated afterward by the value obtained by evaluating the expression bound to the variable. Any attempt to dereference the variable during the initialization raises an exception rather than diverges. This way, lazy evaluation provides a useful measure to initialize recursive bindings by exploring a successful initialization order of the bindings at runtime and by signaling an exception when there is no such order. It is also used for the initialization semantics of the object system in the F# programming language.

The denotational semantics is proved adequate with respect to a referential operational semantics.

Introduction

Lazy evaluation is a well-known technique in practice to initialize recursive bindings. OCaml [6] and Racket (formerly PLT Scheme) [4], provide language constructs, lazy/force and delay/force operators respectively, to support lazy evaluation atop call-by-value languages with arbitrary side-effects. Their implementations are quite simple: when a delayed variable is dereferenced for the first time, it is first pre-initialized to an exception-raising thunk and is updated afterward by the value obtained by evaluating the expression bound to the variable. Any attempt to dereference the variable during the initialization raises an exception rather than diverges. In other words, lazy evaluation as implemented in OCaml and Racket distinguishes direct cycles 1 , which we call "black holes", such as let rec x = x in x and let rec x = y and y = x + 1 in x, and looping recursion, such as let rec f = λ x. f x in f 0. The former raise an exception, whereas the latter diverges.

Lazy evaluation provides a useful measure to initialize recursive bindings by exploring a successful initialization order of the bindings at runtime and by signaling an exception when there is no such order. In [12], Syme advocates the use of lazy evaluation for initializing mutually recursive bindings in MLlike languages to permit a wider range of recursive bindings 2 . Flexibility in handling recursive bindings is particularly important for these languages to interface with external abstract libraries such as GUI APIs. Syme's proposal can be implemented using OCaml's lazy/force operators and it underlies the initialization semantics of the object system in F# [13].

There is a gap between lazy evaluation, as outlined above, and conventional models for lazy, or call-by-need, computation as found in the literature. Traditionally call-by-need is understood as an economical implementation of call-by-name, which does not distinguish black holes and looping recursion but typically interprets both uniformly as "undefined". The gap becomes evident when a programming language supports exception handling, as both OCaml and Racket do -one can catch exceptions but Nakata Expressions M, N ::

= n | x | λ x.M | M N | let rec x 1 be M 1 , . . . , x n be M n in M | • Results V ::= n | λ x.M | • Types τ ::= nat | τ 1 → τ 2 Figure 1: Syntax of λ letrec n : nat x : type(x) • : τ x : τ 1 M : τ 2 λ x.M : τ 1 → τ 2 M : τ 1 → τ 2 N : τ 1 M N : τ 2 x 1 : τ 1 . . . x n : τ n M 1 : τ 1 . . . M n : τ n N : τ let rec x 1 be M 1 , . . . , x n be M n in N : τ Figure 2:
Typing rules cannot catch divergence. Indeed catching exceptions due to black holes is perfectly acceptable, or could be even desired, in practice; it is just like catching null-pointer exceptions due to object initialization failure in object-oriented languages.

In this paper we present a denotational semantics, which matches the lazy evaluation as implemented in OCaml and Racket and used in F#'s object initialization. In this semantics, direct cycles denote exceptions whereas looping recursion denotes divergence. The key observation is to think of lazy evaluation as a most successful initialization strategy of recursive bindings: the initialization succeeds if and only if there is a non-circular order in which the bindings can be initialized. The operational semantics searches such an order by on-demand computation. The denotational semantics searches such one intuitively by initializing recursive bindings in parallel and choosing the most successful result as the denotation.

The denotational semantics, proved adequate with respect to a referential operational semantics, is the main contribution of the paper.

Syntax and operational semantics

The syntax of our simply typed letrec calculus, λ letrec , is given in figure 1. An expression is either a natural number n ∈ N, variable x, abstraction λ x.M, application M N, letrec let rec x 1 be M 1 , . . . , x n be M n in M, or black hole •, which represents an exception. Results are natural numbers, abstraction and black holes. A type is either a base type, nat, or a function type of shape τ 1 → τ 2 . To simplify the calculus, we assume each variable x is associated with a unique type, given, e.g., type(x). Typing rules are found in figure 2, which are all straightforward.

In figure 3, we present the natural semantics. The natural semantics is identical to that given in our previous work [8], which is very much inspired by Launchbury's [5] and Sestoft's [10]. Heaps, ranged over by metavariables Ψ and Φ, are finite mappings from variables to expressions. We write x 1 → M 1 , . . . , x n → M n to denote a heap whose domain is {x 1 , . . . , x n }, and which maps

x i 's to M i 's. The notation Ψ[x 1 → M 1 , . . . , x n → M n ] denotes mapping extension. Precisely, Ψ[x 1 → M 1 , . . . x n → M n ](x i ) = M i and Ψ[x 1 → M 1 , . . . x n → M n
](y) = Ψ(y) when y = x i for any i in 1, . . . , n. We write Ψ[x → M] to denote a single extension of Ψ with M at x. In rule Letrec, M i 's and N denote expressions obtained from M i 's and N by substituting x i 's for x i 's, respectively. We may abbreviate Ψ M where Ψ is an empty mapping, i.e., the domain of Ψ is empty, to M.

The judgment Ψ M ⇓ Φ V expresses that an expression M in an initial heap Ψ evaluates to a result V with the heap being Φ. In Variable rule, the heap Ψ is updated to map x to • while the expression bound to x is evaluated. For instance, let rec x be x in x ⇓ x → • • is deduced. This way, an attempt to dereference a variable which is under "initialization" results in a black hole. Error β rule propagates black holes. Other rules are self-explanatory. In figure 4 we present the derivation for the expression let rec x be f x, f be λ y.y in x. We deliberately chose a black hole producing expression.

Result Ψ V ⇓ Ψ V Application Ψ M 1 ⇓ Φ λ x.N Φ[x → M 2 ] N[x /x] ⇓ Ψ V x fresh Ψ M 1 M 2 ⇓ Ψ V Variable Ψ[x → •] Ψ(x) ⇓ Φ V Ψ x ⇓ Φ[x → V ] V Letrec Ψ[x 1 → M 1 , . . . , x n → M n ] N ⇓ Φ V x 1 , . . . , x n fresh Ψ let rec x 1 be M 1 , . . . , x n be M n in N ⇓ Φ V Error β Ψ M 1 ⇓ Φ • Ψ M 1 M 2 ⇓ Φ • Figure 3: Natural semantics x → •, f → • λ y.y ⇓ x → •, f → • λ y.y x → •, f → λ y.y f ⇓ x → •, f → λ y.y λ y.y x → •, f → λ y.y, y → • • ⇓ x → •, f → λ y.y, y → • • x → •, f → λ y.y, y → • x ⇓ x → •, f → λ y.y, y → • • x → •, f → λ y.y, y → x y ⇓ x → •, f → λ y.y, y → • • x → •, f → λ y.y f x ⇓ x → •, f → λ y.y, y → • • x → f x , f → λ y.y x ⇓ x → •, f → λ y.y, y → • • let rec x be f x, f be λ y.y in x ⇓ x → •, f → λ y.y, y → • •

Denotational semantics

We proceed to the denotational semantics. An expression M of type τ denotes an element of (V τ +Err τ ) ⊥ , where (•) ⊥ is lifting and Err τ is a singleton, whose only element is • τ . V τ denotes proper values of type τ and is defined by induction on τ:

V nat = N V τ 0 →τ 1 = [(V τ 0 + Err τ 0 ) ⊥ → (V τ 1 + Err τ 1 ) ⊥ ]
We omit injections for both the lifting and the sum. A metavariable ϕ ranges over proper function values, i.e., elements of V τ 0 →τ 1 for some τ 0 and τ 1 . For d ∈ (V τ 0 →τ 1 + Err τ 0 →τ 1 ) ⊥ and d ∈ (V τ 0 + Err τ 0 ) ⊥ , application of d to d is defined by

d(d ) = ⊥ τ 1 when d = ⊥ τ 0 →τ 1 • τ 1 when d = • τ 0 →τ 1 ϕ(d ) when d = ϕ
semantics assigns a bottom element to both black holes and looping recursion; the distinction of the two is at the heart of our work.

Ariola and Klop [3] studied equational theories of cyclic lambda calculi by means of cyclic lambda graphs and observed that having non-restricted substitution leads to non-confluence. Ariola and Blom [1] and Schmidt-Schauß et al. [9] use infinite lambda terms to reason about call-by-need letrec; it is not obvious if their techniques can be adapted so that black holes are distinguished from divergence.

Viewing black holes as exceptions is not new. For instance, Moggi and Sabry's monadic operational semantics for value recursion signals a monadic error when a black hole is encountered [7]. The idea seems to be ascribed to the backpatching semantics of Scheme [11].

Conclusion

We have presented a denotational semantics for lazy initialization of letrec. The semantics interprets direct cycles, called black holes, as exceptions, which fits lazy evaluation as implemented in OCaml and Racket and which underlies the initialization semantics of F#'s object system. We think signaling an exception for these "non-sense recursion" is natural and useful in practice; we believe it is also natural in theory.

Fixed Point Argument and Tilings without Long Range Order

Andrei Romashchenko LIF de Marseille (CNRS & Univ. Aix-Marseille) on leave from IITP RAS of Moscow andrei.romashchenko@lif.univ-mrs.fr

Abstract

Tiling is a classic model of combinatorial structure, whose global properties are determined by simple local rules. In this paper we construct tilings with some specific properties, using selfreferential argument originating in Kleene's recursion theorem. This methods proves to be very effective though the initial problems under consideration are purely combinatorial and do not refer explicitly to any questions of computability.

More specifically, we investigate the problem of long range order formulated by C. Radin: whether one can determine by local rules such tilings on the plane in which we loose all information while traveling between distant areas. We present a partial answer to Radin's question by constructing a tile set τ = τ 0 τ 1 (i.e., all tiles in τ are divided into two disjoint classes of 0-tiles and 1-tiles) such that every τ-tiling of the plane corresponds to some configuration in {0, 1} Z 2 , where there is no long range order.

Introduction

In this paper we call by tile a unit square with colored sides. Given a finite set of tiles we consider tilings, i.e., coverings of the plane by copies of these tiles such that colors match (adjacent sides of every two neighbor tiles must have the same color in both squares).

For example, for a tile set that consists of two tiles (the first one has black lower and left side and white top and right sides, and the second one has the opposite colors) only the checkerboard tilings are possible.

More formally, we consider a finite set C of colors. A tile is a quadruple of colors (assigned to its four sides), i.e., an element of C 4 . A tile set is a subset τ ⊂ C 4 . Respectively, a tiling of the plane with tiles from τ (τ-tiling) is a mapping U : Z 2 → τ that respects the color matching condition.

A tiling U is periodic if it has a period, i.e., a non-zero vector T ∈ Z 2 such that U(x + T ) = U(x) for all x ∈ Z 2 . For example, for the checkerboard tiling in the example above the vertical and horizontal unit shifts are periods.

Intuitively it seems that a periodic tiling has an extremely simple structure. It is not surprising that some local rules enforce simple and regular periodic configurations. On the contrary, what is rather unexpected, is the fact that some tile sets do imply much more complex global structures. The first result of this kind was proven by Berger in [2]: Theorem 1. There exists a tile set τ such that τ-tilings exist and all of them are aperiodic (such tilings are called aperiodic).

Berger's theorem shows that very simple local rules (matching rules for some finite set of colored tiles) can imply rather nontrivial global structure. Later it was shown that a tile set can enforce even much more sophisticated structures than just aperiodic configurations. For example, in [4] there was constructed a tile set whose tilings have maximal "density of information" (more precisely, Kolmogorov complexity of each N × N-square in a tiling must have Kolmogorov complexity Ω(N)).

Charles Radin in [11] noticed that there exist another natural angle of the intuitive idea of "regular configuration". A global configuration looks regular if it has long range order, i.e., there is dependency even between very far remote tiles. For example, in a periodic tiling U every two tiles U(x) and U(x + T ) must be equal to each other if T is a multiple of the minimal period (thus, T can be arbitrarily large).

Following [11], we define a notion of long range order in a more general way. Let τ be a tile sets and P be some subset of τ. For a τ-tiling U we denote by ν(P) the frequency of tiles from P in U. More precisely, for each positive integer N we count in U the fraction of tiles from P in N-neighborhood of the point (0, 0). We define ν(P) as the limit of these fractions as N tends to infinity. Note that (a) this limit exists not for all tilings; (b) if this limit exists, it does not change under shifts of the tiling. We restrict our attention to tilings in which this limit exists for each P ⊂ τ. Similarly, for subsets P, Q ⊂ τ and a translation t ∈ Z 2 we denote by ν(P t -→ Q) the limit fraction of points x ∈ Z 2 such that U(x) ∈ P and U(x + t) ∈ Q. We say that a tiling does not have long range order if probabilities of occurrences of tiles at distant sites are in some sence 'almost independent'. More precisely, we say that a τ-tiling U does not have long range order if for all P, Q ⊂ τ

lim |t|→∞ |ν(P t - → Q) -ν(P) • ν(Q)| = 0 ( * )
where |t| is the usual Euclidean norm of vector t.

The following question was formulated by C. Radin in [11]: Does exist a tile set τ such that some τ-tilings exists and all τ-tilings do not have long range order? Obviously, such tilings must be aperiodic. However this requirement is much stronger than aperiodicity. In particular, the classic constructions of aperiodic tilings (e.g., [10,1]) do not satisfy (*). In fact, (*) looks rather counterintuitive: we look for a local rule which guarantees that tiling must look globally "irregular" in some sense.

To the best of our knowledge, this question of Radin remains open. We believe that tilings without long range order can be obtained from self-similar tile set constructions based on the fixed-point argument. In this paper we explain the main ideas of this technique and prove a weaker version of the main conjecture:

Theorem 2 (main result). There exists a tile set τ that can be split into two disjoint parts τ = P Q so that (a) τ-tilings exist, and (b) for each τ-tiling (*) is true.

Since τ = P Q, we can correspond to each τ-tiling U a configuration in U ∈ {0, 1} Z 2 : we let U (x) = 0 if U(x) ∈ P and U (x) = 1 if U(x) ∈ Q. Theorem 2 claims that to each τ-tiling there corresponds a configuration U satisfying (*). In other words, the local rules of τ admit tilings such that the natural projection π : τ Z 2 → {0, 1} Z 2 maps each τ-tiling to a configuration that does not have long range order.

In the rest of this paper we explain the idea of the fixed-point construction of tilings and give a sketch of the proof of Theorem 2.

Fixed point construction of a tiling

First we present a construction of an aperiodic tile set that is based on Kleene's fixed-point construction. This argument is similar to J. von Neumann self-reproducing automata [9]; very similar ideas were also used by P. Gács in the context of error-correcting computations [7]. This type of argument was used in [5] to construct tilings with some specific properties. Flexibility of this construction allows us to construct a tile set that is not only aperiodic but satisfies the claim of Theorem 2. We believe that the same technique can help answer the question of C. Radin in the most general form.

Macro-tiles

Let us fix some tile set τ and some integer N > 1. We call by a macro-tile any N × N square tiled by τ-tiles. Neighbor tiles in this square must match (adjacent sides must have equal colors); there is no constraints for colors on the boarder line of this square. Thus, every side of a macro-tile carries a sequence of N colors. We call this sequence of colors a macro-color.

Let ρ be a set of τ-macro-tiles. We say that τ simulates ρ if (a) at least one τ-tilings exist, and (b) for each τ-tiling there exists a unique grid of vertical and horizontal lines that cuts this tiling into N × N macro-tiles from ρ. For example, let a set ρ consist of exactly one macro-tile (that has the same macro-colors on all four sides) is simulated by some tile set τ. The tile set τ consists of N 2 tiles indexed by pairs (i, j) of integers modulo N. A tile from τ has colors on its sides as shown on Fig. 1. The macro-tile in ρ has colors (0, 0), . . . , (0, N -1) and (0, 0), . . . , (N -1, 0) on its borders (Fig. 2).

(i + 1, j) (i, j) (i, j) (i, j + 1)
If a tile set τ simulates some set ρ of τ-macro-tiles with zoom factor N > 1 and ρ is isomorphic to τ, then the set τ is called self-similar. We call by an isomorphism between τ and ρ some bijection that respects the relations "one tile can be placed on the right of another one" and "one tile can be placed on the top of another one". For the sake of brevity we say that a tile set τ simulates a tile set ρ when τ simulates some set of macro tiles ρ isomorphic to ρ. So, a self-similar tile set simulates itself.

(0, 0) (0, 0) (0, N -1) (0, 0) (N -1, 0) (0, 0) (0, N -1) (N -1, 0) N Figure 2: Macro-tile of size N × N
The idea of self-similarity was used (sometimes implicitly) in most constructions of aperiodic tile sets. Probably only the constructions in [8,3] are the exceptions. The proof is based on a simple lemma: Lemma 1 (folklore). A self-similar tile set τ has only aperiodic tilings.

Thus, to prove that aperiodic tile set exits, it is enough to construct a selfsimilar tile set. We show how to construct such a tile set using the idea of Kleene's fixed-point theorem. To this end, we first explain how to simulate a given tile set by embedding computations (e.g., a Turing machine) in a tiling.

Simulating a tile set

We start with an informal discussion. Assume that we have a tile set ρ whose colors can be encoded as k-bit strings (i.e., C ⊂ B k ) and the set of tiles ρ ⊂ C 4 is presented as a predicate R(c 1 , c 2 , c 3 , c 4 ). Assume that we have some Turing machine R that computes R. Now we show how to simulate ρ using some other tile set τ.

Our construction extends the example on Fig. 2. We keep the coordinate system modulo N embedded into tiles of τ. These coordinates guarantee that all τ-tilings can be uniquely cut into blocks of size N × N and every tile "knows" its position in the block. In addition to the coordinate system, now each tile in τ carries supplementary colors on its sides. On the border of a macro-tile only two supplementary colors (e.g., 0 and 1) are allowed. So the macro-color encodes a string of N bits, where N is the size of macrotiles. We assume that N ≥ k and let k bits in the middle of macro-tile sides represent colors from C. All other bits on the sides are zeros (this is a restriction on the tile set: each tile knows its coordinates so it also knows whether non-zero supplementary colors are allowed). Now we introduce additional restrictions on tiles in τ that guarantee that the macro-colors on sides of each macro-tile satisfy the relation R. To this end we ensure that bits from the macro-tile sides are transferred to the central part of the tile where the checking computation of R is simulated.

For this "information transmission" we fix which tiles in a macro-tile form "wires". This choice can be done in any reasonable way; we may even assume that wires do not cross each other. We require that tiles along each of these wires carries equal bits on two sides (so one bit value of is transmitted along a wire); again it is easy to organize since each tile knows its coordinates.

To check that the property R is true for a quadruple of macro-colors, we require that the central part of a macro-tile represents a time-space diagram of R's computation. Embedding of a space-time diagram in a tiling is a standard trick. We require that horizontal rows represent configurations of the tape of the Turing machine, time goes upwards. We require that computation terminates in an accepting state: if not, the tiling cannot be formed.

To make this construction work, the size of macro-tile should be large enough: we need enough space for k bits to propagate and enough time and space to perform accepting computation of R.

In this construction the number of supplementary colors depends on the machine R. The more states it has, the more colors are needed in the computation zone. To get rid of this dependency, we replace the ad hoc machine R by a fixed universal Turing machine U that runs a program simulating R. Talking about the universal Turing machine, we may require that the tape has an additional read-only layer. Each cell of this layer carries one bit that is not changed during the computation; these bits are used as a program for the universal machine (Fig. 3). So in the computation zone the columns carry unchanged bits, and the tile set restrictions guarantee that these bits form the program for U , and the central zone represents the protocol of an accepting computation for that program. In this way we get a tile set τ that simulates ρ with zoom factor N using O(N 2 ) tiles.

Simulating itself

We already know how to simulate a given tile set ρ (represented as a program for the universal Turing machine) by another tile set τ with a large enough zoom factor N. Now we want τ to be isomorphic to ρ itself. Here we use a construction that follows the fixed-point argument from Kleene's recursion theorem. Recall the construction from Section 2.2. Note that most rules of τ do not depend at all on the program for R. They deal only with information transfer along the wires, the vertical propagation of unchanged program bits, and the space-time diagram for the universal Turing machine in the computation zone. We make these rules a part of ρ's definition, and get a program which checks that macro-tiles behave like τ-tiles in this respect.

The only remaining part of the rules for τ is the hardwired program. We must guarantee that macrotiles carry the same program as τ-tiles do. Hence, our program for the universal Turing machine needs to access the bits of its own text. This self-referential action is quite legal. Indeed, the program is written on the tape, and the machine can read it (this argument is the key idea of the standard proof of Kleene's recursion theorem). The program checks that if a macro-tile belongs to the first line of the computation zone, this macro-tile carries the correct bit of the program. Now we choose N. We need it to be large enough so the described above computations can fit in the computation zone. The used computations are rather simple. They all are polynomial in the input size, i.e., of size O(log N). So for large N it easily fits in O(N) available space and time. This finishes the basic construction of a self-similar aperiodic tile set. This construction together with Lemma 1 is already enough to get Theorem 1. However to prove Theorem 2 we need to extend our self-referential technique.

Variable zoom factor

In our basic construction the macro-tiles of all levels are of the same size: each of them contained N × N macro-tiles of the previous level for some constant zoom factor N. It is not enough to achieve our main result, since we will need to host arbitrarily long computations in high-level macro-tiles. So we need an increasing sequence of zoom factors N 0 , N 1 , N 2 , . . .; macro-tiles of the first level are blocks of N 0 × N 0 tiles; macro-tiles of the second level are blocks of N 1 × N 1 macro-tiles of level 1 (and have size of level k inside the N k × N k -matrix XOR of the two random bits corresponding to its row and column. Now consider any 1 × N k row of k-level macro-tiles in the constructed macro-tile of level k + 1 (this "row" is a rectangle of size (N 0 • . . . • N k-1 ) × (N 0 • . . . • N k ) paved by τ-tiles), and consider the shift of this row by vector t. It is not hard to check (with standard Chernoff bounds) that with very high probability this shift "changes" assigned bits for approximately 50% of all tiles in the block. The typical deviation of the fraction of "changed" bits from 50% is very small and can be bounded by 1/k. Technically the deviation of this frequency is greater than 1/k only with probability at most e -Ω(N k /poly(k)) • poly(N k ). (Remark: this bound requires the assumption N k-1 N k . For the lack of space we skip the calculations.) Probability of large deviations remains very small even when we sum up it for all rows in a (k + 1)-level macro-tile (i.e., multiply it by N k ).

Thus, we proved probabilistically that the required distribution of k-level macro-tiles inside a (k + 1)level macro-tile exists. How to enforce such a coloring by local rules? First of all, we can guarantee that this distributions are the same (or exactly opposite) in every two neighboring (k + 1)-level macrotiles (in our construction the choice of the distribution of 0-and 1-tiles in a (k + 1)-level macro-tile is determined by only O(N k ) bit parameters; so this information can be passed through the borderline of neighboring macro-tiles of size N k × N k ). It remains to guarantee that the valid distribution of k-level macro-tiles indeed implies that shifts t such that N 0 N 1 . . . N k-1 ≤ |t| < N 0 N 1 . . . N k changes about 50% of "auxiliary bits" inside every (k + 1)-level macro-tile. To this end, the computational zone of each (k + 2)level macro-tile checks the required property is true. We have enough room for this computation since N k+1 N k . To run this computation we need to deliver to the computational zone of every (k + 2)-level macro-tile the auxiliary bits assigned to its subordinate macro-tiles of lower levels. This can be done by the bit propagation technique from [6]. Since the complete argument is rather technical, we have to skip detail for the lack of space.

Further research

We see two main avenues for the subsequent work. First, we believe that our technique is suitable to answer the question of C. Radin in the most general setting. Another intriguing question is how to implement the fixed-point construction of a tile set with a smaller size of a tile set. In the present argument the number of different tiles in a tile set is about several millions. It would be interesting to obtain a similar construction with hundreds or even dozens of tiles. This probably requires involving other programming model, supporting more succinct programming style than Turing machines.

A note on strong dinaturality, initial algebras and uniform parameterized fixpoint operators 1 Introduction

I present a Yoneda-like lemma relating strongly dinatural (a.k.a. Barr dinatural) transformations and initial functor-algebras. It is very basic, but I do not know whether it has appeared in the literature. I have found it quite useful: it can be used, for example, to prove the validity of some Mendler-style structured recursion schemes for initial algebras or recursive coalgebras [12,14] and to prove properties of Church representations of inductive types [9,5]. Here, I use it to reprove some known results [7,10] about existence and unique existence of uniform parameterized fixpoint operators, exploiting that uniformity is a strong dinaturality condition. I would not dare to claim that the proofs become simpler, but they obtain a structure that nicely localizes the invocations of the various initial and bifree algebra existence assumptions made.

Strong dinaturality and a Yoneda lemma for initial algebras

Dinatural transformations [2] and strongly dinatural (a.k.a. Barr dinatural) transformations [7,8] are two generalizations of natural transformations from (covariant) functors to mixed-variant functors that have components only defined for the diagonal of the domain. We recall the definitions, starting with dinaturality.

Definition 1 (Dinaturality). A dinatural transformation between H, K ∈ C op × C → E is given by, for any X ∈ |C|, a map Θ X ∈ E(H(X, X), K(X, X)) such that, for any f ∈ C(X, X ), the following hexagon commutes in E:

H(X, X) Θ X / / K(X, X) K(X, f ) ) ) S S S S S S H(X , X) H( f ,X) 5 5 k k k k k k H(X , f ) ) ) S S S S S S K(X, X ) H(X , X ) Θ X / / K(X , X ) K( f ,X ) 5 5 k k k k k k
Dinatural transformations are used, for example, in the definitions of coend and end. A coend is an initial cowedge, where a cowedge is given by an object and an accompanying dinatural transformation (just as a colimit is defined as an initial cocone, a cocone being an object with a natural transformation).

Dinatural transformations do not generally compose and so do not give a category. Strongly dinatural transformations do not suffer from this shortcoming.

Uustalu

Freyd [3,4], Mulry [7], Simpson and Plotkin [10] etc. Hyland and Hasegawa [6] showed that (uniform) Conway operators are equivalent to (uniform) traces (definable in general monoidal categories, not just categories with finite products).

We will closely follow the account of Simpson and Plotkin [10]. First we recall the definitions of parameterized fixpoint operators, parameterized Conway operators and uniformity.

We assume given a category D with finite products.

Definition 3 (Parameterized fixpoint-like operator). A parameterized fixpoint-like operator on D is given by, for any X,Y ∈ |D|, a function fix X,Y ∈ D(X ×Y,Y ) → D(X,Y ).

Definition 4 (Parameterized fixpoint operator). A parameterized fixpoint operator on D is a parameterized fixpoint-like operator fix on D such that

• for any f ∈ D(X, X ) and k ∈ D(X ×Y,Y ), fix (k • ( f × id Y )) = fix k • f (naturality); • for any k ∈ D(X ×Y,Y ), fix k = k • id X , fix k (parameterized fixpoint property).
Definition 5 (Conway operator). A Conway operator on D is a parameterized fixpoint operator fix on D with the further properties that

• for any f ∈ D(X ×Y,Y ) and h ∈ D(X ×Y ,Y ), f • id X , fix (h • fst, f ) = fix ( f • fst, h ) (param- eterized dinaturality); • for any k ∈ D((X ×Y ) ×Y,Y ), fix (k • id X×Y , snd X,Y ) = fix (fix k) (diagonal property).
Parameterized dinaturality implies the parameterized fixpoint property, so for Conway operators the latter condition is redundant.

For our final definition, we assume we also have a category C with finite products and the same objects as D together with an identity-on-objects functor J ∈ C → D preserving the finite products of C strictly. We call the maps of D in the image of J pure. Definition 6 (Uniformity). A parameterized fixpoint-like operator fix on D is said to be uniform wrt. J, if

• for any f ∈ C(Y,Y ), k ∈ D(X × Y,Y ) and k ∈ D(X × Y ,Y ), J f • k = k • (id X × J f ) implies J f • fix k = fix k .
(In the terminology of iteration theories [1], naturality is parameter identity, parameterized fixpoint property is fixpoint identity, parameterized dinaturality is composition identity and diagonal property is double dagger identity. Finally, uniformity corresponds to the functoriality condition.)

We now focus on the special case of D arising as the coKleisli category of a comonad (D, ε, (-) † )1 on C with J the right adjoint in its coKleisli splitting. The prototypical well-behaved situation here has C = df Cppo ⊥ , D = df (-) ⊥ and D ∼ = Cppo, where Cppo stands for the category of ω-complete pointed partial orders and ω-continuous functions, Cppo ⊥ is as Cppo but has as maps only the strict (bottompreserving) maps of Cppo and (-) ⊥ is the lifting endofunctor. More generally, the lifting comonad can be replaced with any comonad on Cppo ⊥ that has its underlying functor Cppo-enriched.

In terms of the "base" category C, a parameterized fixpoint-like operator is now, for any X,Y ∈ |C|, a function fix X,Y ∈ C(D (X ×Y ),Y ) → C(D X,Y ). The various optional additional conditions specialize into the following:

Uustalu • for any f ∈ C(D X, X ) and k ∈ C(D(X ×Y ),Y ), fix (k • f • D fst, ε Y • D snd † ) = fix k • f † (nat- urality); • for any k ∈ C(D (X ×Y ),Y ), fix k = k • ε X , fix k † (parameterized fixpoint property); • for any f ∈ C(D (X ×Y ),Y ) and h ∈ C(D (X ×Y ),Y ), f • ε X , fix (h • ε X • D fst, f † ) † = fix ( f • ε X • D fst, h † ) (parameterized dinaturality); • for any k ∈ C(D ((X ×Y ) ×Y ),Y ), fix (k • D id X×Y , snd X,Y ) = fix (fix k) (diagonal property); • for any f ∈ C(Y,Y ), k ∈ C(D (X ×Y ),Y ) and k ∈ C(D (X ×Y ),Y ), f •k = k •D (id X × f ) implies f • fix k = fix k (uniformity).
(Notice that here, id and • refer to identity and composition in C rather than in D, differently from what they meant above.) Crucially for us, the uniformity condition asserts nothing else than strong dinaturality of fix X,Y in Y , i.e., that fix X,-∈ [C, Set] sd (C(D (X × -), -), C(D X, -))-an observation first made by Mulry [7].

From Proposition 1, we immediately get:

Corollary 1. If every functor D(X × -) ∈ C → C has an initial algebra, then a uniform wrt. J parameterized fixpoint-like operator fix on D is the same as, for any X ∈ |C|, a map fix X ∈ C(DX, µ(D (X ×-))).

The bijection is given by fix

X = df fix X,µ(D (X×-) in D (X×-) and, for k ∈ C(D(X × Y ),Y ), fix X,Y k = df fold D (X×-),Y k • fix X .
It is not difficult to strengthen this corollary to the following characterization of uniform parameterized fixpoint operators (one has to verify that the conditions are pairwise equivalent): Proposition 2. If every functor D (X × -) ∈ C → C has an initial algebra, then a uniform wrt. J parameterized fixpoint operator fix on D is the same as, for any X ∈ |C|, a map fix X ∈ C(DX, µ(D (X × -))) such that

• for any f ∈ C(D X, X ), µ( f • D fst, ε -• D snd † ) • fix X = fix X • f † ("naturality");

• for any X ∈ |C|, fix X = in D (X×-) • ε X , fix X † ("parameterized fixpoint property").

Recall that a bifree algebra is an initial algebra that is at the same time also a final coalgebra. The following is nearly immediate from the proposition we just stated.

Proposition 3 ([10, Proposition 6.5]). If every functor D(X × -) ∈ C → C has a bifree algebra, then D has a unique uniform wrt. J parameterized fixpoint operator.

Proof. Just observe that the parameterized fixpoint property can be rewritten as in -1

D (X×-) • fix X = D (X × fix X ) • ε X , id D X
† , which stipulates that fix X (if existing) must be a coalgebra map between (D X, ε X , id D X † ) and (µ(D (X × -)), in -1 D (X×-) ). As the latter is a final coalgebra, there is exactly one such map. This map turns out to also satisfy the required naturality condition.

Uniform Conway operators can be analyzed similarly. Here we need the existence of further initial algebras to replace conditions on fix with conditions on fix. When these initial algebras are also final coalgebras, we have a unique uniform Conway operator. Proposition 4. If all functors D (X × -), D (X × D (X × -)), D ((X × -) × -) ∈ C → C have initial algebras, then a uniform wrt. J Conway operator on D is the same as, for any X ∈ |C|, a map fix X ∈ C(DX, µ(D (X × -))) satisfying the conditions of Proposition 2, but also the following conditions:

• for any X ∈ |C|, in • ε X , fold ( ε X • D fst, in † ) • fix † = fold (in • ε X • D fst, id † ) • fix
∈ C(DX, µ(D (X × D (X × -)))) ("parameterized dinaturality");

• for any X ∈ |C|, fold (in • D id, snd ) • fix = fold (fold in • fix) • fix ∈ C(DX, µ(D ((X × -) × -))) "diagonal property").

Proposition 5 ([10, Theorem 3]). If all functors D (X ×-), D (X ×D (X ×-)), D ((X ×-)×-) ∈ C → C have bifree algebras, then D has a unique uniform wrt. J Conway operator.

Uniform guarded recursion operators

A similar treatment is possible for guarded recursion operators (we have previously considered some aspects for the dual situation of guarded iteration [13]). Here, the prototypical example is given by cofree recursive comonads on endofunctors on Set, such as the nonempty list comonad defined by DX = df µ(X × (1 + (-))

).

An ideal comonad on a category C with finite products is a comonad given by DX = df X × D 0 X, ε As soon as all functors X × D 0 (X × -) have initial algebras, having a uniform guarded recursion operator rec becomes equivalent to having, for any X ∈ |C|, a map rec X ∈ C(D X, µ (X × D 0 (X × -)) such that rec = in • (fst × id) • ε, rec † .

A uniform guarded recursion operator exists uniquely, e.g., whenever D is the cofree recursive comonad on an endofunctor H on C, in which case D X ∼ = µ (X × H (-)) ∼ = X × µ (H (X × -)).

Conclusion

I find it intruiging that the use of the Yoneda-like lemma stages the invocations of the initial algebra resp. bifree algebra existence assumptions: the initial algebra existence assumptions ensure the possibility of reducing the existence of a parameterized fixpoint operator to the existence of a family of maps to initial algebras; the bifree algebra existence assumptions ensure that such a family of maps exists uniquely.

I would like to learn more about the relationship of strong dinaturality and models of parametric polymorphism.

Introduction

Banach's and Knaster-Tarski's fixed point theorems have constructive proofs. In the first part of this paper we show that more is true: both statements are instances of a single theorem. As we shall see, in both cases the fixed point of a given map f : X → X is found by examining its generalized direct image f * on a suitably constructed directed-complete poset. Since f * is always order-preserving, regardless of the properties of f , we can apply the well-known theorem that an order-preserving map on a pointed dcpo has the least fixed point; remarkably, as shown by D. Pataraia [12], this statement has a fully constructive proof, formalizable in higher-order intuitionistic logic (in 2003 it found an entry to the compendium on continuous lattices and domains [7], where it is presented as a set of exercises). Hence we are going to use Pataraia's construction to simultaneously prove Banach's and Knaster-Tarski's theorems.

In the second part of this paper we show that Caristi's [3] theorem is precisely the metric analogue of the Bourbaki-Witt theorem. Again, both results are instances of a single statement, but this time we do not use any external help in the proof -it is the Bourbaki-Witt construction that proves the unifying theorem. Now, it has recently been discovered by A. Bauer [1] that the Bourbaki-Witt theorem can never be demonstrated by a fully constructive argument. In what follows we are going to use Bauer's insight to show that unless a proof of Caristi's theorem substantially rely on the symmetry axiom of the metric, then it cannot be accepted intuitionistically.

A construction of fixed points for order-preserving maps on dcpos

Since we will refer to details of Pataraia's proof, we shall start with a concise description of his construction.

Recall that a map f : P → P on a poset P is expanding if x f x, for all x. We say that an orderpreserving expanding map is inflationary. A dcpo is a poset P where each directed set has a supremum. A poset is pointed, if it has the least element, usually denoted as ⊥. Now, suppose f is order-preserving on a pointed dcpo P. Following Pataraia's line of thought, we look for subsets of P that (a) contain ⊥, (b) are closed under f , and (c) are directed-complete. Clearly Y := {x ∈ P | x f x} is one of them. Let C be the intersection of all sets with (a)-(c). Therefore, f : C → C is inflationary. Now, the set E(C) of all inflationary maps on C, ordered pointwise, is directed-complete, and -and this is the crux of the construction -it is itself a directed set. The reason is that for g, h ∈ E(C), we have g, h g • h. Hence

The setup

The fundamental reason why we can treat both order and metric fixpoint theorems from a unified perspective is that both structures are examples of quantale-enriched categories [11]. Consequently, we will work with distances that do not posses all flexibility of metrics. This is of course the price that must be paid for generality of the setup.

Our primary object of investigation is thus a set X together with a distance into [0, ∞] that satisfies: (a) X(x, y) = X(y, x) = 0 iff x = y, (b) X(x, y) + X(y, z) X(x, z), for all x, y, z ∈ X. In the literature on the subject a set X as above is known as a generalized metric space (gms) [2].

Any gms carries an intrinsic partial order: x X y iff 0 = X(x, y). It is crucial to observe that if the distance map X(-, -) takes only two values: 0 and ∞, then the gms X is a partial order. We will say: "a gms X is a poset" precisely when its distance map takes values in 2 := {0, ∞}.

Taking into account absence of symmetry, every gms X has its dual, denoted X op . Note also that [0, ∞] itself is a gms with [0, ∞](x, y) = yx, whereis the (extended) substraction truncated at zero.

A map f : X → Y is non-expansive if X(x, y) Y ( f x, f y) for all x, y ∈ X.

The set all non-expansive maps of type X op → [0, ∞] will be denoted X, to distinguish it from the set [0, ∞] X of all maps of the same type. The former plays a crucial role in our paper: it is a gms when equipped with the usual sup-distance X(φ , ψ) := sup z∈x (ψz -φ z). Since X(φ , ψ) + f * (φ )(y) inf x∈X (ψx +Y (y, f x)) = f * (ψ)(y), we get X(φ , ψ) Y ( f * (φ ), f * (ψ)), i.e. f * is non-expansive. The map f * can be interpreted as a generalized direct image of f , see Sect. 2.6 of [13]. For example if X and Y are posets (i.e. gmses with distances into 2), then f * is a lower closure of the direct image of f . It is perhaps helpful for the reader if we issue a warning here: a non-expansive map in a gms may not be continuous. For example, if X and Y are posets, non-expansiveness means order-preserving, while continuous means directed-sup preserving, which is a stronger property.

The generalized direct image of a function

Completeness of gmses

Consider an operation J that assigns to every gms X a subset J X of elements of X in such a way that (a) each J X contains all yx for all x ∈ X (where yx := X(-, x)); (b) each J X contains all f * (φ ) for φ ∈ J Y and a non-expansive f : Y → X. We say that elements of J X are ideals on X. Observe that J X with the distance inherited from X is in fact a subgms of X. Now we say that X is J -complete if there exists a non-expansive map S : J X → X, called supremum, with ∀φ ∈ J X ∀x ∈ X X(Sφ , x) = X(φ , yx).

The importance of the above notion of completeness lies in the fact that certain choices of J capture completeness of metric spaces and directed-completeness of posets at the same time, as will be shown on examples below. Since ε is arbitrary, sup n≥N X(y, T n x 0 ) T * (φ )(y). This holds for any N ∈ ω and y ∈ X, therefore φ T * (φ ).

For the converse, let y, z ∈ X, m ∈ ω and n ≥ m. Then X(y, T z) + X(z, T n x 0 ) X(y, T z) + X(T z, T n+1 x 0 ) X(y, T n+1 x 0 ) and thus X(y, T z) + φ z φ y. Consequently, T * (φ ) X φ . Theorem 3.4 (Banach). A contraction on an A-complete gms has a unique fixed point.

Proof. Let X be A-complete and T : X → X be contractive. Then for any x 0 ∈ X, (T n x 0 ) n∈N is a forward Cauchy sequence. Hence by Lemma 3.3, there exists φ ∈ AX that is fixed under T * . Now Theorem 3.1 applies and we get a fixed point of T . Since T is a contraction, any choice of x 0 leads to the same Sφ ∈ X. Hence the fixed point of T is unique.

Knaster-Tarski's fixed point theorem

Now J X = X. It is well-known that that any (•)-complete X is a complete lattice in the intrinsic order, and hence (•) is admissible.

It is actually a metric version of Knaster-Tarski's theorem that we are going to prove. We recover the original statement exactly when X is a poset. Theorem 3.5 (Knaster-Tarski). A non-expansive map T : X → X on an (•)-complete gms has the least and the greatest fixed point. Proof. Let ⊥, be the least and the top elements of X, respectively. By proofs of Lemmata 3.2, 3.3, φ z := inf m∈ω sup n≥m X(z, T n (⊥)) is an ideal on X with supremum n∈ω T n (⊥). Moreover, φ is a fixed point of T * . By Theorem 3.1, there exists a fixed point of T , which is least above n∈ω T n (⊥), and hence least above ⊥ as well.

Since T is non-expansive on X iff it is non-expansive on X op , the same construction applied to X op in place of X produces the least fixed point of T in X op , i.e. the greatest fixed point of X.

A pattern for Caristi's and Bourbaki-Witt's fixed point theorems

It is known from [6] that any complete metric space X can be embedded onto the set of maximal elements of a continuous dcpo BX := { x, r | x ∈ X, ∞ > r 0} ⊆ X, where x, r (z) := X(z, x) + r, and x, r BX y, s iff x, r X y, s iff r X(x, y) + s. In [9] it has been shown that X is an A-complete gms iff (BX, BX ) is a dcpo. We will use this knowledge in proving a generalized version of Caristi's fixed point theorem.

Theorem 4.1. Let X be an A-complete gms and let ϕ : X → [0, ∞) be a lower semicontinuous function. Suppose T : X → X is an arbitrary mapping which satisfies ϕ(x) X(x, T x) + ϕ(T x) for each x ∈ X. Then T has a fixed point.

Proof. Let Z be a subgms of BX consisting of elements of the form x, ϕ(x) for x ∈ X. Hence x, ϕ(x) Z y, ϕ(y) iff ϕ(x) X(x, y) + ϕ(y). Moreover ϕ is lower semicontinuous iff it preserves directed suprema with respect to the order Z . All this means that (Z, Z ) is a subdcpo of (BX, BX ).

By assumption, T : Z → Z, defined as T ( x, ϕ(x) ) := T x, ϕ(T x) is expanding. Therefore we use the Bourbaki-Witt argument (that can be found in [10]) to conclude that T : Z → Z has a fixed point. That is: z, ϕ(z) = T z, ϕ(T z) for some z ∈ X. Therefore, z = T z, as required.

Note that when X is a poset and ϕ is constant, then Thm. 4.1 becomes the Bourbaki-Witt theorem for dcpos. On the other hand, since any complete metric space is A-complete, we have: Theorem 4.2 (Caristi). Let X be a complete metric space and let ϕ : X → [0, ∞) be a lower semicontinuous function. Suppose T : X → X is an arbitrary mapping which satisfies ϕ(x) X(x, T x) + ϕ(T x) for each x ∈ X. Then T has a fixed point.

We conclude the paper with recalling a result of A. Bauer [1] who proved that in the effective topos, there is a chain-complete lattice with an inflationary map that does not have a fixed point. As a consequence the Bourbaki-Witt theorem for chain-complete lattices (or -equivalently [4] -for dcpos) cannot have a proof in higher-order intuitionistic logic. For us, this means that Theorem 4.1 has no constructive proof. Moreover, if the original Caristi theorem for metric spaces had a constructive proof that does not rely on symmetry of the distance, nor on the assumption that X(x, y) < ∞ for all x, y ∈ X -see e.g. [8], [5] for proofs that neither use Zorn's lemma nor symmetry -then it would be a valid proof of our Theorem 4.1, and hence of the Bourbaki-Witt construction, which is impossible.

Taking into account the observations above we conjecture that symmetry plays no role in the argument, and therefore no proof of Caristi's theorem is constructively valid, but we are unable to prove this at the moment. One way to support our claim would be a construction, for every complete metric space X, of a non-symmetric A-complete quasi-metric on X with equivalent fixed-point properties; such a quasi-metric could perhaps be found by a deeper analysis of these existing proofs of Caristi's theorem that do not invoke equivalents of Zorn's lemma.

Figure 1 :

 1 Figure 1: Proof rules for propositional classical logic

Figure 2 :

 2 Figure 2: The focused proof system LKF for classical logic.

Figure 3 :

 3 Figure 3: Introduction rules for = and µ.

Figure 5 :

 5 Figure 5: Inference rules for induction and co-induction.

Figure 2

 2 Figure 2: Subtyping

  an equivalence relation because of the ultrametric inequality; we refer to the relation n = as "n-equality." Since the distances are bounded by 1, x 0 = y always holds, and the n-equalities become finer as n increases. If x n = y holds for all n then x = y.

  [n] with limit y then d(y k , y) ≤ 2 -n for some k, i.e., y k n = y. So there exists x ∈ X with x ∈ R and x n = y k , and hence x n = y which gives lim n y n ∈ R[n]

  2 and assume that a |= p k and a ∈ ϕ λ α (∅). By definition of λ -th iteration of ϕ α : ϕ λ α (∅) = β <λ ϕ β α (∅), therefore there exists β < λ such that a ∈ ϕ β α (∅). Hence, by the induction hypothesis, a ∈ ϕ ω•k α (∅).

xProposition 3 .

 3 M and P ∈ Prog be such that M[P/x] P. Then the relation {(N[rec x. M/y], N[P/y]) | y N} is a simulation up to on the right. Proof. We want to show that if N[rec x. M/y] → a Q then there exists y R and Q ∈ Prog such that Q = R[rec x. M/y] and N[P/y] → a Q and R[N/y] Q . We proceed by induction on →. • Suppose that N = y. Then M[rec x. M/x] → a Q and applying the inductive hypothesis gives y R and Q ∈ Prog such that Q = R[rec x. M/y] and M[P/x] → a Q and R[N/y] Q . Since M[P/x] P and is a simulation we have P → a Q and Q Q , giving R[N/y] Q .• The other cases are trivial. Let x M be a term. Then rec x. M is a nesting fixpoint of the monotone endofunction f : P → M[P/x] on A(CCS).

Corollary 1 .

 1 Let x M, M be terms such that M[P/x] M [P/x] for all programs P. Then rec x. M rec x. M .

Definition 2 . 4 .

 24 A Segala system is a pair P, { a -→} a∈L where P is a countable set of states and for each a ∈ L, a -→ ⊆ P × D(P) is the transition relation where D(P) is the set of all probability distribution over P. Given a probability distribution d ∈ D(P) we denote by supp(d) the support of d defined as the set {p ∈ P | d(p) > 0}.

Figure 4 :

 4 Figure 4: The derivation for let rec x be f x, f be λ y.y in x

Figure 1 :

 1 Figure 1: Basic tiles

Figure 3 :

 3 Figure 3: Scheme of a macro-tile

  X = df fst ∈ C(DX, X), for any k ∈ C(DX,Y ), k † = df k, k ‡ • snd ∈ C(DX, DY ) where D 0 is an endofunctor on C and, for any X,Y ∈ |C|, (-) ‡ X,Y ∈ C(DX,Y ) → C(D 0 X, D 0 Y ). A guarded recursion operator for an ideal comonad is, for any X,Y ∈ |C|, a unique function rec X,Y ∈ C(X × D 0 (X × Y ),Y ) → C(D X,Y ) satisfying the guarded recursion equation rec k = k • (fst × id) • ε, rec k †and possibly further properties.

  E(C) has a top element m : C → C. Consequently, f • m = m, and thus f (m(⊥)) = m(⊥), i.e. m(⊥) ∈ C is a fixed point of f . If x ∈ P is some other fixed point of f , then ↓x := {y ∈ P | y x} satisfies (a)-(c), hence C ⊆ ↓x and consequently, m(⊥) x.

  Let f : X → Y be any non-expansive map. Consider f * : X → Y given by f * (φ )(y) := inf x∈X (φ x +Y (y, f x)).

Table of Contents

 of Invited Talks Arnaud Carayol, Structures Defined by Higher-Order Recursion Schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Dale Miller, Fixed Points and Proof Theory: An Extended Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Panos Rondogiannis, Fixed-Point Semantics for Non-Monotonic Formalisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  By induction on the derivation of Γ t : τ. The proof uses the closure of the relations under the operational semantics, the downwards closure (Kripke monotonicity) in k, and the closure under the coercions determined by the subtyping relation.→ n for some n ∈ N, then C[t 2 ] = C[t 1 ] = nfollows from the assumption t 1 = t 2 and Theorem 3. By Proposition 5, C[t 2 ] R k Int C[t 2 ], and therefore n R k Int C[t 2 ] holds. But by definition this means C[t 2 ] *

	and a i R k τ i t i for all x i :τ i in Γ, then t ( a) R k τ t[ x:= t]. Proof sketch. Now adequacy is easily proved. In fact, given Γ t 1 : τ, Γ t 2 : τ and C : (Γ τ) and C[t 1 ]	( / 0 Int),

*

  and there exists t such that aRt and t ∈ ϕ

	Therefore t |= C n l which implies t |= p l+1 . By the induction hypothesis, since t ∈ ϕ t |= p l+1 , we know that t ∈ ϕ ω•(l+1) α	γ α (∅). α (∅) and γ

  and for all t if aRt, then t ∈ ϕ

γ α (∅). Fix such t, then t |= C n l and therefore t |= p l+1 , so by the induction hypothesis t ∈ ϕ ω•(l+1) α

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp.[19][START_REF] Schroeder-Heister | Rules of definitional reflection[END_REF][START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF][22][23][24][25]

Birkedal et al.Γ, x:τ x : τ Γ n : Int Γ, x:τ t : σ Γ λ x:τ.t : τ → σ Γ t 1 : • n (τ → σ ) Γ t 2 : • n τ Γ t 1 t 2 : • n σ Γ t 1 : τ 1 Γ t 2 : τ 2 Γ (t 1 ,t 2 ) : τ 1 × τ 2 Γ t : • n (τ 1 × τ 2 ) Γ proj i (t) : • n τ i • Γ t : • τ Γ t : τ Γ t : •τ i, j Γ In i, j (t) : ty i Γ t : ty i Γ, x 1 :•τ i,1 t 1 : τ . . . Γ, x i k :•τ i,k i t k i : τ Γ case t of In i,1 (x 1 ) ⇒ t 1 | . . . | In i,k i (x k i ) ⇒ t k i : τ

Note however that even though the underlying sets are the same, the inclusion of •(τ → σ ) into • τ → • σ fails to be non-expansive. Thus we cannot have•(τ → σ ) ≤ • τ → • σ in general.

Due to the syntactic restrictions on recursive types in our variant of Nakano's calculus, the metrics on PCF ground types (and hence on all types) differ slightly in our model and Escardó's model.

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 27-33

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 35-391 This can be improved to a logarithmic growth, but with a drawback on clearness of the reasoning, thus we will work with the linear fuses.

I would like to thank Michał Skrzypczak for showing me an idea how to present those formulae in a clearer way.

Such models that there is a formula which reaches its fixpoint in those models in at least ω 2 .

In a common sense: we do not specifically refer here to constructive mathematics.

Downloadable from http://hal.archives-ouvertes.fr/.

Here, and in the following, given x ∈ E , we denote by ≤ x the principal order ideal {y ∈ E | y ≤ x}. Likewise, if X ⊆ E , we denote by ≤ X the union x∈X (≤ x).

A chain-complete poset has therefore a bottom element, ∨ / 0.

A map η : E → E is expansive (also inflationary, progressive) if any point is η-consistent: ∀ x ∈ E . x ≤ η(x).

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 61-67 1 Direct cycles are also known as provable divergence.2 In ML, the right-hand side of recursive bindings is restricted to be syntactic values.

We use the lambda notation to express (mathematical) functions on domains.

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 69-75

Luigi Santocanale (ed.): Fixed Points in Computer Science 2010, pp. 77-82

We write (-) † for the coKleisli extension operation of a comonad.

Acknowledgments: I wish to thank David Baelde and the anonymous reviewers of this abstract for their comments.

Acknowledgments I thank Matthias Felleisen and Olivier Danvy for valuable exchanges, Eijiro Sumii, Makoto Tatsuta, Masahito Hasegawa, Yukiyoshi Kameyama and Yasuhiko Minamide for discussions.

This research was supported by the Estonian Centre of Excellence in Computer Science, EXCS, funded by the European Regional Development Fund, and the Estonian Science Foundation grant no. 6940.

Acknowledgment I thank my anonymous referees for useful remarks. This research was supported by the Estonian Science Foundation under grant no. 6940.

The author is supported by grant number N206 3761 37 funded by Polish Ministry of Science and Higher Education.

Nakata

where An environment, ρ, is a function from variables to denotations, which respects types, i.e., ρ(x) ∈ (V τ + Err τ ) ⊥ where x : τ. The least environment, ρ ⊥ , maps all variables to bottom elements.

The semantic function [[M : τ]] ρ assigns a denotation to a typing derivation M : τ under an environment ρ and is defined in figure 5 by induction on the derivation 3 . µ stands for the least fixed point operator. ρ[x 1 → d 1 , . . . , x n → d n ] stands for extension of ρ with d i 's at x i 's. For d, d ∈ (V τ + Err τ ) ⊥ , the notation d • d abbreviates ((λ y.λ x.x) * (d))(d ). The semantic function, being defined using only continuous operations, is continuous and mostly standard (c.f., [14]) except for letrec. The denotation of let rec x 1 be M τ 1 1 , . . . , x n be M τ n n in N : τ is defined with the help of a semantic function for (typed) heaps. The function

ρ takes three parameters, a heap x 1 → M τ 1 1 , . . . , x n → M τ n n , an environment ρ and a natural number m, and returns an environment. It is defined by induction on m, with semantic functions for M i : τ i 's given by the outer induction.

We compute the denotation of a heap Ψ = x 1 → M τ 1 1 , . . . , x n → M τ n n under an environment ρ as follows. Let ρ m = {{Ψ}} (m) ρ . The variables x i 's are first pre-initialized to black holes, that is,

] ρ 0 of M i : τ i for each i under the initial environment ρ 0 , so that we take the fixed-point semantics for the recursive bindings whose initialization was successful. That is,

where

Indeed it follows from lemmata 3.1 and 3.2 below that this is equivalent to defining

Generally, ρ m+1 is given by taking the fixedpoint semantics for the recursive bindings whose initialization is successful under the environment ρ m ; i.e., ρ m+1 = µρ .ρ[x 1 → d 1 , . . . , x n → d n ] where

Nakata

This process is iterated for n times, where n is the length of the heap Ψ. The number of the iteration is justified, as it converges by then:

Adequacy

The denotational semantics is adequate with respect to the natural semantics. An important fact, to be stated in lemma 3.4, is that, as we iteratively compute denotations of (typed) heaps Ψ under an environment ρ, we reach a fixed point:

We define a relation < < τ ⊆ (V τ + Err τ ) ⊥ × (V τ + Err τ ) ⊥ by induction on τ:

Then a relation < < on environments is defined such that ρ < < ρ iff for any x, ρ(x) < < τ ρ (x) where x : τ. It captures a relationship between (intermediate) denotations of a heap at different iterations (see lemma 3.2 below).

.

Lemma 3.3. For any x 1 : τ 1 , . . . , x n : τ n , M 1 : τ 1 , . . . , M n : τ n , m and ρ, {{x

.

The natural semantics is correct with respect to the denotational semantics in that evaluations preserve the denotations of expressions.

Proposition 3.1. For any typed expression

Moreover an expression evaluates to a result if and only if its denotation is non-bottom.

Related work

The natural semantics used in the paper is very much inspired by those of Launchbury [5] and Sestoft [10]. Ariola and Felleisen gave a reduction semantics for λ letrec [2], which is proved equivalent to our natural semantics [8]. Our denotational semantics is also influenced by Launchbury's, except that his

However, all these macro-tiles (of all levels) still carry the same program in their computation zone. The difference between their behavior is caused by the input data on the tape: each macro-tiles "knows" its level since it is provided as a sequence of bits on its tape. Then this level k may be used to compute N k which is then used as a modulus for coordinates in the father macro-tile.

We must ensure that this information is correct. We need two properties: (a) all macro-tiles of the same level have the same idea about their level, and (b) these ideas are consistent between levels (each father is one level higher than its sons). To achieve these properties we involve additional features in our macro-tiles. Since each macro-tile knows its position inside the father, so it knows whether the father should keep some bits of his level information in that macro-tile. If yes, the macro-tile checks that this information is correct. Each macro-tile checks only one bit of the level information, but with brothers' help they check all the bits in their father's memory.

Also we should check that the level information fits into the tiles, and the computation required to compute N k from k also fits into level k tile. This means that log k, log N k and the time needed to compute N k from k should be much less than N k-1 (since the computation zone is some fraction of N k-1 ). So N k should not grow very slow (e.g., N k = log k is too slow), should not grow very fast (e.g., N k = 2 N k-1 is too fast) and should not be too hard to compute. All these restriction still leave us a lot of freedom. E.g., N k can be proportional to √ k, to k, to 2 k , etc. In the next section we assume that N k = 2 C k from some large enough constant C. Now computational zones of macro-tiles increase on each next level, so we can embed there computations of increasing sizes into the macro-tiles.

Sketch of the proof of Theorem 2

In our basic construction every tile knows its coordinates in the macro-tile and some additional information needed to arrange 'wires' and simulate calculations of the universal Turing machine. Now in addition to this basic structure each tile keeps one auxiliary bit of information. Formally it means that the set of all tiles is split into two parts: τ = τ 0 τ 1 . These bits (assigned to all tiles of a tiling) will make a configuration in {0, 1} Z 2 that satisifies (*). Similarly, we assign an auxiliarely bit to each macro-tile (i.e., on each level we will have 0-type or 1-type macro-tiles).

On each level k, we allow exactly two different valid distributions of auxiliary bits in a k-level macrotiles; these two distributions will be opposite to each other (one is the "reversed image" of the other one).

For each k-level macro-tile the choice between these two possible distributions of subordinate "auxiliary bits" is determined by the "auxiliary bit" assigned to this macro-tile itself. The two valid distributions of auxiliary bits inside a k-level macro-tile are defined inductively: first we chose two valid distributions of 0-tiles and 1-tiles in a 1-level macro-tile of size N 0 × N 0 (there will be exactly 50% of 0-tiles and 50% of 1-tiles in a macro-tile of level 1); then we define two valid distributions of 1-level macro-tile in a 2-level macro-tile (which is an N 1 × N 1 -matrix of 1-level macro-tiles), etc.

The distribution of auxiliary bits inside of a k-level macro-tile should be chosen in such a way that for every shift t such that N

so, it tend to 0 as k tends to infinity). The fact that such configurations of auxiliary bits exist, follows from a simple probabilistic argument. In what follows, we explain this argument in some detail.

Assume we already fixed valid distributions of 0-tiles and 1-tiles in all macro-tiles of level up to k. Now we decide how to distribute k-level macro-tiles of type 0 and 1 inside a matrix of size N k × N k , which makes a (k + 1)-level macro-tile. Let us draw independent random bits for each row and each column of a (k + 1)-level macro-tile (i.e., we need 2N k random bits), and assign to each macro-tile of Uustalu Definition 2 (Strong dinaturality). A strongly dinatural transformation between H, K ∈ C op × C → E is given by, for any X ∈ |C|, a map Θ X ∈ E(H(X, X), K(X, X)) such that, for any map f ∈ C(X, X ) and any span (W, p, p ) on (X, X ), if the square in the following diagram commutes in E, then so does the hexagon:

If E is a category with pullbacks such as, e.g., Set, one can equivalently require that, for every map f ∈ C(X, X ), the outer hexagon of the above diagram commutes for (W, p, p ) the chosen pullback of the cospan (H(X, X ), H(X, f ), H( f , X )).

We write [C, E] sd for the category of mixed-variant functors from C to E and strongly dinatural transformations.

Any strongly dinatural transformation is also dinatural, but the converse does not hold in general. This note is centered around the following observation, which I have not noticed published (I have mentioned it in an unpublished talk abstract [11] ten years ago, and also in a paper on the recursion scheme from the cofree recursive comonad [14]). Please be so kind and tell me, if you know of a reference where it might appear. It is a kind of a Yoneda lemma for strongly dinatural transformations and initial algebras.

Proposition 1 (Yoneda lemma for initial algebras). Let C be a locally small category, F ∈ C → C a functor with an initial algebra (which we denote (µ F, in F ) and K ∈ C → Set a functor (whose padding into a mixed-variant functor we denote also by K). Then

in fact, a set too). This isomorphism is natural in F (to the extent that initial algebras exist in C).

A strongly dinatural transformation between C(F-, -) and K is given by, for any X, a map Θ X ∈ C(FX, X) → K X, such that, for any X, X , φ ∈ C(F X, X), φ ∈ C(F X , X ), f ∈ C(X, X ), f •φ = φ •F f (i.e., f being an F-algebra map from between (X, φ ) and (X , φ )) implies

We denote the natural isomorphism by i F . It is defined as follows: for

where fold F,X denotes the unique algebra map from (µ F, in F ) to (X, k).

An important special case is when KX = df C(1, X). We get that

This is closely related to Church representations of inductive types. Remember that, in System F, we represent µ F by ∀X. (F X ⇒ X) ⇒ X). Needless to say, for final coalgebras, a dual proposition is true; I refrain from spelling it out here.

Uniform parameterized fixpoint operators

We now turn to parameterized fixpoint-like operators and uniformity. The dependencies between different axiomatiozations and sufficient conditions for existence have been studied by Bloom and Ésik [1],

3 A pattern for Banach's and Knaster-Tarski's theorems A class J of ideals is admissible if each J -complete X is directed-complete with respect to the intrinsic order X introduced in Sect. 2.

Theorem 3.1. Fix an admissible class of ideals J . Let T : X → X be a non-expansive map on an Jcomplete gms X. Suppose that there exists φ ∈ J X, which is a fixed point of T * . Then T has a fixed point, which is the least fixed point of T above Sφ .

Proof. Since X is complete, Sφ exists. By Prop. 2.5. of [13], non-expansiveness of T yields S(T * (φ )) X T (Sφ ), hence Sφ X T (Sφ ). We can now follow steps of Pataraia's construction, the only difference being that instead of ⊥, we use Sφ . Thus T has a fixed point, which is of the form m(Sφ ) for some m : C → C. Recall that C ⊆ X is the smallest set closed under T and directed lubs that contains Sφ . Suppose now that x 1 is also fixed by T , and that Sφ x 1 . Being the lower cone of a fixed point, ↓x 1 is closed under T and directed lubs. As a consequence m(Sφ ) ∈ C ⊆ ↓x 1 .

We will now demonstrate that Thm. 3.1 offers a pattern for generalizing and proving both of the classic fixed point theorems.

Banach's fixed point theorem

A first example of an admissible class of ideals is J = A, where by definition φ ∈ AX if and only if φ x := inf i∈I sup j≥i X(x, x j ) for some forward Cauchy net (x i ) i∈I [2] (recall that a net

It can be shown that a metric space X is A-complete iff it is complete in the usual sense. On the other hand, if X is a poset, then X is A-complete iff it is a dcpo. Lemma 3.2. A is admissible. Proof. Suppose (x i ) i∈I is X -directed. Define φ := inf i∈I sup j≥i X(-, x j ). Since X is A-complete, the supremum Sφ ∈ X exists, and now will show that it is the least upper bound of (x i ) i∈I .

Let k ∈ I. Firstly observe φ (x k ) sup j≥k X(x k , x j ) = 0. Therefore 0 = φ (x k ) = X(yx k , φ ) X(x k , Sφ ), whence x k X Sφ . On the other hand take any upper-bound u ∈ X of (x i ) i∈I . Then 0 = X(x k , u) for all k ∈ I, and consequently 0 = inf k sup j≥k X(yx k , yu) = X(φ , yu) = X(Sφ , u), i.e. Sφ X u. Lemma 3.3. Let T : X → X be a non-expansive map on an A-complete gms X. Suppose that there exists x 0 ∈ X such that (T n x 0 ) n∈ω is a forward Cauchy sequence. Then there is φ ∈ AX such that φ = T * (φ ).

Proof. Define an ideal on X by φ := inf m∈ω sup n≥m X(-, T n x 0 ). Let us first show that φ X T * φ . Fix N ∈ ω, y ∈ X and choose ε > 0 such that ε > sup n≥N X(y, T n x 0 ). Then there is δ > 0 with ε > sup n≥N X(y, T n x 0 ) + δ . Use Cauchyness to get M ≥ N such that for all i ≥ M, δ > X(T M x 0 , T i x 0 ). Hence δ sup i≥M X(T M x 0 , T i x 0 ). Consequently, ε > sup Author Index