PaperlayerView exact revision on arXiv

Source-linked AI summary

First steps in synthetic guarded domain theory: step-indexing in the topos of trees

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring

arXiv:1208.3596v2cs.LO

TL;DR

The paper addresses how recursive terms, predicates, and dependent types can be modeled without relying on external step-indexed constructions. It develops guarded recursion in the topos of trees through an internal dependently typed higher-order logic, constructs an internal model of Fµ,ref, and generalizes the model to sheaves over complete Heyting algebras with well-founded bases.

  • Problem

    Recursive functions, relations, and types are central to programming-language semantics, but models with higher-order store commonly involve recursively defined worlds and relations.

  • Method

    The paper uses the topos of trees S and its internal higher-order logic with modal operators on predicates, terms, and types to define guarded recursion and solve dependent recursive type equations.

  • Results

    The topos S models guarded recursion, supports guarded recursive terms and dependent types, and yields an internal synthetic model of Fµ,ref; the results generalize to suitable sheaf topoi.

  • Takeaways & Limitations

    Synthetic guarded domain theory provides an internal setting for constructing step-indexed models of programming languages and program logics.

  • Takeaways & Limitations

    The paper notes that a relevant diagram involving left adjoints does not generally commute because the associated fibred functor does not commute.

Abstract

from arXiv · show

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S. Moreover, we give an axiomatic categorical treatment of models of synthetic guarded domain theory and prove that, for any complete Heyting algebra A with a well-founded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S.

1. Introduction

The paper presents the topos of trees S as a model of guarded recursion with an internal dependently typed higher-order logic. It develops guarded recursive definitions and applies them to programming-language models, while generalizing the framework to sheaves over complete Heyting algebras with well-founded bases.

  • Core setting: The topos S models guarded recursive definitions of functions, relations, and recursive types.This applies the topos of trees to guarded recursion and extends recursive modeling beyond functions and relations.
  • Core setting: S’s internal logic extends many-sorted higher-order logic with modal operators on types and terms.The logic supports semantic models involving recursively defined types and relations, including Fµ,ref with polymorphism, recursive types, and ML-like references.
  • Guarded recursion: Later operators guard recursive predicates and variable sets, making definitions well-founded level by level.For variable sets, the later operator shifts level n + 1 to depend on level n; analogous operators support recursive predicates.
  • Guarded recursion: The internal logic supports mixed-variance recursive type equations and recursive dependent types, including nested guarded recursion.Functorial types are closed under nested recursive types, while all recursion-variable occurrences must remain guarded.
  • Applications: The paper constructs a synthetic model of Fµ,ref entirely inside S and argues that this internal approach simplifies reasoning compared with explicit step-indexed models.The proof of the fundamental theorem is described as much simpler when carried out in S rather than through an external ultrametric-space model.
  • Generalization: The framework generalizes from S to sheaf topoi over complete Heyting algebras with well-founded bases.The paper gives an axiomatic treatment of these models and relates them to earlier work using complete bounded ultrametric spaces.

2. The S Topos

The topos S models guarded recursion through step-indexed variable sets, a later operator, and unique fixed points for contractive morphisms. Its internal logic supports guarded recursive predicates and relations, while locally contractive functors yield recursive domain equations and fixed-point constructions.

  • The topos of trees: S is the presheaf topos Set^ωop, whose objects are families of sets indexed by natural numbers with restriction maps between successive indices.An element at stage n represents data available with at most n time steps for reasoning.
  • The later operator: The later functor ◮ shifts availability by one step: ◮X(1) is singleton and ◮X(n + 1) = X(n), with a natural transformation next_X : X → ◮X.The operator provides the guard used in recursive definitions.
  • Recursive morphisms: S has a fixed-point operator for morphisms contractive in one variable, producing the unique h satisfying f∘⟨h, id_Y⟩ = h.This establishes unique parameterized fixed points for guarded recursive morphisms.
  • Internal logic: The internal logic gives a later modality on predicates with monotonicity, a Löb rule, and distribution over logical connectives, enabling internal fixed-point reasoning.The modality is characterized semantically by shifting a predicate one time step.
  • Recursive predicates and relations: Guarded recursive predicates are well-defined when recursive occurrences are under ✄, and higher-order logic provides recursive guarded relations without special relation syntax.The paper applies this construction to relations such as bounded rewrite reachability.
  • Recursive domain equations: Locally contractive functors have unique recursive-domain solutions, making S algebraically compact and supporting initial-algebra and final-coalgebra constructions.The framework also yields guarded examples such as the stream successor fixed point.

3. Application to Step-Indexing

The paper builds a model of higher-order store and recursive types entirely inside the internal logic of the topos of trees, using guarded recursion where naive definitions fail. Externally, the construction recovers a standard step-indexed model and establishes its operational and typing properties.

  • Language and operational semantics: The example defines the programming language, stores, configurations, typing judgments, and deterministic operational semantics in the internal logic of S.Terms and values are represented syntactically, stores are finite maps from natural numbers to closed values, and configurations pair closed terms with stores.
  • Evaluation: The evaluation predicate gives a guarded, coinductive partial-correctness specification for safety and postconditions.It states that configurations do not lead to errors and that any resulting value-store pair satisfies the postcondition.
  • Interpretation of types: Semantic types and worlds form mutually recursive equations, which the paper solves using guarded variants rather than exact domain equations.The guarded construction uses later in recursive type and reference interpretations so the definitions are well-defined.
  • Fundamental theorem: The fundamental theorem proves that every well-typed term belongs to the computed semantic interpretation at every world.This connects the typing judgment to the internally defined computation and type semantics.
  • External interpretation: Externally, the internal operational semantics agrees with standard semantics, while evaluation becomes a step-indexed partial-correctness property.At index n, evaluation quantifies over reductions of fewer than n steps and checks the postcondition at the remaining index.
  • Discussion: The external interpretation of types is a standard step-indexed model, while the example remains limited to a unary model and deterministic operational semantics.The authors expect adaptations to relational models, local-state models, and nondeterministic languages, with modified evaluation clauses for the latter.

4. Dependent Types

The paper extends the topos of trees’ guarded recursion to dependent types by defining later on slices and establishing fixed-point principles for guarded recursive type equations.

  • Dependent-type semantics: Dependent types in S are interpreted in slice categories, so later must be extended to slices to support guarded dependent type constructors.
  • Slice categories: Slices of S are presheaf categories over forests, enabling a concrete representation of dependent objects and a forest-based definition of later.
  • Fixed points: Contractive morphisms in slices have fixed points, yielding a generalized fixed-point combinator for dependent guarded recursion.
  • Later on slices: The slice functors later_I commute with reindexing up to natural isomorphism, forming a fibred endofunctor with next as a fibred natural transformation.
  • Recursive dependent types: Locally contractive functors in slices admit unique guarded recursive solutions, including parametrized mixed-variance equations and initial dialgebras.
  • Type theory: The guarded dependent type theory adds later, next, functoriality, and contractiveness rules, while nested recursive types require an additional functoriality constant.

5. Relation to metric spaces

The topos of trees relates to bisected complete bounded ultrametric spaces through an adjunction and an equivalence on total objects, with matching notions of contractiveness.

  • Categorical relation: S has an adjunction with bisected ultrametric spaces, restricting to an equivalence between total objects of S and bisected complete bounded ultrametric spaces.
  • Construction: The construction maps an ultrametric space to a presheaf of quotients determined by distance thresholds 2^-n.
  • Contractiveness: Contractiveness in the internal logic of S coincides with metric contractiveness for morphisms between bisected complete bounded ultrametric spaces.
  • Later and metrics: The later operator corresponds to metric scaling by 1/2 for non-empty ultrametric spaces, while S handles the empty-space case without a special construction.

6. General models of guarded recursive terms

The paper axiomatizes models of guarded recursive terms and proves that locally cartesian closed models remain models in every slice, supporting guarded recursion in dependent settings.

  • Axioms: A model of guarded recursive terms consists of finite products, a later endofunctor, next, unique guarded fixed points, and preservation of finite limits.
  • General closure: Later is strong, and the axiomatized structure is closed under taking slices of a locally cartesian closed model.
  • Slice construction: Later on slices is defined using later followed by pullback along next, and it preserves finite limits.
  • Fibred structure: The slice later operators form a fibred endofunctor, with the collection of next morphisms forming a fibred natural transformation.
  • Fixed points in slices: Contractive slice morphisms reduce to contractive global morphisms, so contractive endomorphisms in every slice have unique fixed points.
  • Limitations: The left adjoint to later is not fibred, and later does not generally preserve dependent products, limiting its use as a dependent type operator.
  • Predicates and Löb induction: The later operation on predicates validates Löb induction: ∀p: Prop.(later p → p) → p.

7. General models of guarded recursive types

The paper generalizes guarded recursive type semantics using enriched categories and contractive completeness, reducing mixed-variance recursive equations to fixed-point constructions with initial-algebra and final-coalgebra structure.

  • Generalization: The general theorem extends the concrete results from S to broader enriched models of guarded recursive types.
  • Model definition: General models of guarded recursive types are cartesian closed guarded-term models in which every locally contractive endofunctor has a fixed point up to isomorphism.
  • Existence theorem: The existence theorem applies to E-enriched, contractively complete categories and yields unique guarded solutions for mixed-variance recursive type equations.
  • Universal properties: A fixed point of a locally contractive functor carries both initial-algebra and final-coalgebra structures, making fixed points unique up to isomorphism.
  • Parameterized recursion: The construction produces an enriched fixed-point functor from parameterized locally contractive functors, preserving local contractiveness in the parameters.
  • Mixed variance: For mixed-variance functors, paired fixed points form initial dialgebras, and the two carriers are isomorphic.

8. A class of models of guarded recursion

The section establishes sheaves over complete Heyting algebras with well-founded bases as models of guarded recursive terms and dependent types. It develops the guarded modality, proves fixed-point results, and specializes the construction to the topos of trees and its slices.

  • Guarded recursive dependent types: The same assumptions make Sh(A) a model of guarded recursive dependent types, extending the fixed-point theory from terms to locally contractive enriched functors.The proof uses contractive completeness and establishes fixed points through transfinite approximations whose structure maps become isomorphisms at the relevant stages.
  • Setting: The models considered are sheaves over complete Heyting algebras with well-founded bases, where well-foundedness excludes infinite descending sequences.A basis represents each element as the least upper bound of the basis elements below it.
  • Setting: For a partial order A, sheaves over its ideal completion are equivalent to the corresponding topos of presheaves, Sh(Idl(A)) ≃ bA.This connects the sheaf presentation with the variable-set models used for the topos of trees.
  • Guarded modality: The guarded modality on sheaves is defined by applying the associated sheaf functor to the predecessor reindexing functor, because predecessor reindexing need not preserve sheaves.The modality preserves finite limits and agrees with the previously defined modality on slices of the topos of trees.
  • Guarded recursive terms: Every morphism from the guarded modality of a sheaf to that sheaf has a unique fixed point, obtained by well-founded induction over the basis.The construction yields a compatible family indexed over elements below each a, satisfying the fixed-point equations.
  • Guarded recursive terms: Every slice of Sh(A) is a model of guarded recursive terms when A is a complete Heyting algebra with a well-founded basis.The proof combines completeness of the slices with fixed points for locally contractive functors.

9. Conclusion and Future Work

The paper concludes that sheaves over complete Heyting algebras with well-founded bases provide models for guarded recursive types and terms, including the topos of trees. It identifies broader applications and future work connecting guarded recursion with unguarded recursion, formalization, step-indexing, and predicative models.

  • Conclusion: Sheaves over complete Heyting algebras with well-founded bases provide models for guarded recursive types and terms, including the topos of trees.The internal logic supports synthetic construction of step-indexed models, illustrated by a model of Fµ,ref.
  • Future work: The paper focuses solely on guarded recursion and leaves connections with unguarded recursion, including selectively guarded recursive types, for future work.The authors specifically mention recursive types in which only negative occurrences of the recursion variable might be guarded.
  • Future work: Future work includes formalizing the internal logic in a tool and improving support for isomorphisms involved in recursive type equations.Initial Coq experiments formalized some proofs involving recursively defined relations on recursively defined types.
  • Future work: The authors plan to study synthetic step-indexed models for languages with countable nondeterminism, whose ω1-based indexing motivates general sheaf categories Sh(A).The proposed model naturally lives in sheaves over ω1 rather than only the topos of trees.
  • Future work: Another proposed direction is the study of predicative models of guarded recursive dependent type theory.This would extend prior work on predicative toposes.

Appendix A. More details on the application to step-indexing

The appendix states that the application details are presented within the internal logic of the topos of trees.

  • Scope: The application details in the appendix are to be understood within the internal logic of S.

A.1. Language.

The language used in the application is presented in Figure 1.

  • Language: Figure 1 presents the full language considered in the application.

A.2. Interpretation of types.

The interpretation maps programming-language types to semantic objects indexed by worlds and type environments. It defines products, sums, references, polymorphism, recursive types, computations, and states within this framework.

  • Type interpretation: Type interpretations are defined by induction as functions over type environments and worlds.The environment records interpretations for free type variables, while worlds index semantic values.
  • Type interpretation: Products and sums combine component interpretations pointwise at each world.Products contain pairs of component values; sums contain tagged left or right values.
  • Type interpretation: Reference types contain locations whose stored functions yield later-guarded values of the interpreted type at all future worlds.The reference interpretation requires the location to belong to the world domain and satisfy the stated condition for every extension.
  • Type interpretation: Universal types quantify over all semantic types and future worlds, requiring computations to inhabit the instantiated body.The interpretation includes polymorphic abstractions satisfying the body condition for every type and world extension.
  • Type interpretation: Recursive types are interpreted using a fixed point over later-guarded unfoldings.A recursive value is represented by fold applied to a value satisfying the body under the recursive interpretation.
  • Computations and states: The computation and state operations provide the semantic treatment of effectful terms and stores.The supplied definitions use computations indexed by worlds and states drawn from each world.

A.3. Soundness and the fundamental theorem.

The section defines semantic validity and proves the fundamental theorem by establishing semantic counterparts for the typing rules. Auxiliary properties of the computation operator support the proof, including the reference-introduction case.

  • Semantic validity: Semantic validity requires every well-typed term substitution to inhabit the interpretation of its type at each world.The condition ranges over worlds, type environments, and semantic environments for the typing context.
  • Fundamental theorem: The fundamental theorem is proved by showing semantic counterparts for all typing rules.The proof is organized around key cases and relies on auxiliary properties of computations.
  • Computation lemmas: The relation ν ⊸w ξ characterizes evaluation contexts that preserve membership from ν to ξ at every world extension.For every future world and value in ν, plugging the value into the context produces an element of ξ.
  • Computation lemmas: Lemma A.1 establishes value inclusion in computations and closure under evaluation-context composition.These two properties are used to transport semantic membership through computation proofs.
  • Reference introduction: The reference-introduction case concludes that typing t as τ entails typing ref t as ref τ.The proof applies Lemma A.1 to show that the reference constructor preserves the semantic interpretation.

A.4. Case “allocation”:

The allocation case proves that reference creation preserves semantic typing. The argument allocates a fresh location, extends the world with its semantic type, and verifies the resulting store state.

  • Allocation: If t has type τ, then ref t has type ref τ under semantic validity.The proof starts from the semantic membership of t and applies the computation-context lemma to the reference constructor.
  • Allocation: Allocation chooses the smallest location absent from the current store and steps to a store extended with the allocated value.The operational step introduces a fresh location l and updates the store with v.
  • Allocation: The proof extends the world with a function interpreting the allocated location as the later-guarded interpretation of τ.The new world is defined by updating w1 at l with lam([[τ]]ϕ).
  • Allocation: The updated store satisfies the world-state condition because the fresh location has the allocated value’s type and existing locations remain valid by monotonicity.The argument separately checks the fresh location and all pre-existing locations.

A.5. Case “lookup”:

The lookup and related store-operation cases establish semantic soundness for dereferencing, assignment, and recursive-type unfolding. The section culminates in type safety for closed well-typed programs evaluated from the empty store.

  • Lookup: Lookup evaluates a reference by retrieving the value stored at its location and proving that the result belongs to the corresponding computation interpretation.The proof uses the reference semantic condition and the state invariant for worlds.
  • Lookup: The state invariant ensures that every location in a world has a stored value belonging to its associated semantic type.For the looked-up location, this invariant yields the required semantic membership after the operational lookup step.
  • Assignment: Assignment is shown sound by combining the computation lemma twice: once for the reference target and once for the assigned value.The proof establishes that updating the store preserves the world-state condition and returns the unit value.
  • Assignment: The assignment proof preserves store validity because the target location’s semantic type matches the assigned value’s interpretation.The location remains associated with the same type function, while the updated value satisfies that type at the current world.
  • Recursive types: Unfolding a recursive value is sound because fold/unfold reduces operationally to the body value, whose guarded semantic membership follows from the recursive-type interpretation.The proof uses the fixed-point interpretation of recursive types and the later modality to establish computation membership.
  • Type safety: A well-typed closed term evaluates successfully from the empty store under the trivial postcondition.This type-safety corollary follows from the fundamental theorem and the empty world.
Loading 1208.3596v2…