{'fraction_non_alphanumeric': 0.03580549725642906, 'fraction_numerical': 0.004248109843983109, 'mean_word_length': 4.330637552230759, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Two Guarded Recursive Powerdomains for Applicative Simulation

Clocked Cubical Type Theory is a new type theory combining the power of guarded recursion with univalence and higher inductive types (HITs). This type theory can be used as a metalanguage for synthetic guarded domain theory in which one can solve guarded recursive type equations, also with negative variable occurrences, and use these to construct models for reasoning about programming languages. Combining this with HITs allows for the use of type constructors familiar from set-theory based approaches to semantics, such as quotients and finite powersets in these models. In this paper we show how to reason about the combination of finite non-determinism and recursion in this type theory. Unlike traditional domain theory which takes an ordering of programs as primitive, synthetic guarded domain theory takes the notion of computation step as primitive in the form of a modal operator. We use this extra intensional information to define two guarded recursive (finite) powerdomain constructions differing in the way non-determinism interacts with the computation steps. As an example application of these we show how to prove applicative similarity a congruence in the cases of may- and must-convergence for the untyped lambda calculus with finite non-determinism. Such results are usually proved using operational reasoning and Howe's method. Here we use an adaptation of a denotational method developed by Pitts in the context of domain theory.


Introduction
Over the past 20 years, step-indexing techniques [4] have become one of the most used tools for constructing operational models of programming languages with combinations of advanced features such as recursive types, polymorphism, concurrency and non-determinism. Often such models are beyond the scope of traditional domain theoretic techniques, and also have the additional benefit of being more elementary. Guarded recursion is an abstract form of step-indexing, in which the explicit steps are replaced by abstract computation steps in the form of a delay modality ⊲. This relieves the user of the bookkeeping involved in explicit step-indexing and reveals the underlying structure that makes these models work in the form of an introduction X → ⊲X , a guarded fixed point combinator of type (⊲X → X ) → X and solutions to guarded recursive domain equations. In its multiclocked version, where the delay modality ⊲ κ is indexed by a clock κ and clocks can be universally quantified, guarded recursion can moreover be used to encode coinductive types in type theory, allowing productivity requirements on these to be encoded in types [6].
Clocked Cubical Type Theory (CCTT) [24] is a type theory combining multiclocked guarded recursion with features from cubical type theory, in particular univalence and higher inductive types (HITs). The latter are a form of inductive types defined not only by constructors, but also by equations. HITs have been used to construct topological spaces such as the circle and the torus in type theory, but can also be used for free structures, such as the free group on a set. In computer science, free structures can be used to form the monads generated by algebraic theories. For example, the finite powerset monad, often used to model finite non-determinism, can be generated by a binary union operation plus axioms of associativity, commutativity, and idempotency, and can therefore be naturally represented as a HIT [8,19].
Combining HITs with guarded recursion provides a powerful metatheory in which one can reason about programming languages and programs. This paper presents a worked example of this. We study the untyped lambda calculus with finite non-determinism, and show how to construct a model of this in CCTT using a guarded recursive type. The model construction takes as parameter a monad T with a union operation ∪ : T X × T X → T X for modelling non-determinism, as well as a step operation step T : ⊲ κ (T X ) → T X , which in combination with the fixed point operator allows us to model recursion.
We present two instantiations for T , corresponding to two different notions of observation on nondeterministic programs. The first describes a notion of non-deterministic computation where all possible branches of a computation are executed in parallel and we can observe all possible values that occur along the way, even if there are diverging branches of the computation. This monad corresponds to may-convergence and can be characterised as being generated by the operations ∪ and step T with no equations between them.
The second instantiation corresponds to a notion of computation where all branches are evaluated in parallel, but partial results are only available when all branches have terminated. This is simply the composition L κ P f of the free monad L κ generated by the step operation and the finite powerset monad P f . It turns out that this composition is not itself a monad, but does have a sequencing operation sufficient for the purposes of this paper. We claim that this composition corresponds to must-convergence.
As an example application of this model, and to substantiate the claim that these constructors correspond to may-and must-convergence, respectively, we apply the model to a classical problem in lambda calculus, namely that of proving that applicative similarity is a congruence. This was first proved by Abramsky [1] for the lazy lambda calculus (without non-determinism) using domain theory and Stone duality, and this method has since been extended to calculi with non-determinism [31]. Here we use a different method due to Pitts [34] who used a domain theoretic model and a relation between syntax and semantics. We extend this proof to non-determinism for both may-and must-equivalence, and adapt it to guarded recursion.
The two instantiations of T mentioned above are what we consider as examples of guarded recursive powerdomains. In classical domain theory [2] a powerdomain is a domain theoretic correspondent to the powerset construction in set theory. A number of different powerdomains exist, each characterising a different notion of observation. One way of characterising the difference between these is in terms of enriched algebraic theories which allow them to be classified in terms of inequations such as x ≤ x ∪ y. In the case of guarded recursion the difference between the two guarded powerdomains studied here can be expressed in terms of equalities describing the interaction between ∪ and step T . This paper can therefore also be read as a first study of the interaction of algebraic effects and guarded recursion.

Synthetic guarded domain theory
Until now most applications of guarded recursion and step-indexing have used these for operational reasoning for programming languages. While these techniques are very useful for proving properties of programs, we believe that there is a need for also developing guarded recursion as a tool for constructing denotational semantics. Denotational methods have the benefit of often being more modular than the operational methods, and often reveal the foundational mathematical building blocks of programming languages. Denotational semantics often inspire new programming constructions or languages, as exemplified in monads [30], runners for computational effects [37,3], homotopy type theory [36], or even guarded recursion itself [10].
Using guarded recursion for denotational semantics has several possible benefits over domain theory. The first is that it appears to be more expressive than domain theory as illustrated by the many uses of step-indexing for advanced programming languages. Another is that step-indexing and guarded recursion by many are considered more elementary tools. A third is that guarded recursion appears to be more amenable to effective formalisation in type theory and proof assistants, although some formalisations of classical domain theory do exist [9,18], and in particular recent progress on such a formalisation in HoTT seems promising [22].
Initial steps towards such a synthetic guarded domain theory were taken by Birkedal, Møgelberg and Paviotti [28,32] who showed how to construct models of the programming languages PCF and FPC modelling recursion in these as guarded recursion, and proving the adequacy of these models entirely in a type theory with guarded recursion. This paper can be viewed as an extension of these works to non-determinism. Perhaps the main disadvantage of guarded recursion compared to domain theory is the intensional nature, allowing the model to distinguish between computations that produce the same result in a different number of steps. The present paper shows that using universal quantification over clocks allows to localise the steps and to prove properties that do not refer to steps, using the models.

Related work
Most proofs of applicative similarity being a congruence use operational arguments [25,26], in particular Howe's method [20]. More recently, an abstract version of Howe's method has been developed [15] to handle languages with algebraic effects in a uniform way. This method uses domain theory to handle recursion. It would be interesting to see if the method described here generalises to a similar uniform method for computational effects, but this requires first developing a theory of algebraic effects in guarded type theory.
Step-indexing and guarded recursion based operational techniques have previously been used for languages with non-determinism. For example, Schwinghammer et al. [35] construct an operational model for reasoning about a typed programming language with recursive types, polymorphism and nondeterminism and use it to prove contextual equivalences of programs. Bizjak et al. [11] show how to construct a similar model using guarded recursion and topos logic. These works use complex operational techniques including ⊤⊤-closure. Our goal is different, namely to develop a theory of denotational semantics in a type theory with guarded recursion.
The above mentioned works on non-determinism [25,26,35,11] study countable non-determinism, rather than finite non-determinism. This is generally considered a harder problem. For example, this forces the step-indexing used by Schwinghammer et al. [35] to be transfinite, whereas the underlying model of the Clocked Cubical Type Theory is based on natural number step-indexing. Likewise, defining powerdomains in domain theory for countable non-determinism is much harder than the finite case [5,17]. We discuss the possibility of extending our approach to countable non-determinism in Section 8.
As described in Section 3, our partiality monad L κ is strongly related to the coinductive partiality monad, and our use of it is similar to previous uses in semantics of recursion [9,12,16]. Interaction trees [39] are a general data structure combining the coinductive partiality monad with computational effects. Our guarded powerdomain monads can perhaps be seen as a form of guarded interaction trees for non-determinism, except that the use of HITs allows us to consider these up to an equational theory.

Overview
The paper is organised as follows: We first recall the basics of Cubical Type Theory in Section 2, in particular path types and higher inductive types. Section 3 then recalls Clocked Cubical Type Theory, the extension of Cubical Type Theory with multiclocked guarded recursion. Section 4 defines the guarded powerdomain for may-convergence and Section 5 presents our proof that applicative may-similarity is a congruence using a denotational model. Section 6 defines a guarded powerdomain for must-convergence, and Section 7 presents our proof that applicative must-similarity is a congruence. We conclude in Section 8.

Cubical type theory
Cubical Type Theory (CTT) [14] is a variant of Homotopy Type Theory (HoTT) [36] based on the cubical model of the univalence axiom, and specifically designed to compute with univalence. It moreover has the benefit of combining more easily with guarded recursion than HoTT, which was the reason for using it as a base for Clocked Cubical Type Theory as we shall describe in Section 3. Reading this paper does not require deep knowledge of CTT, and this section recalls the basic notions from CTT and HoTT that we shall need.
Perhaps the most fundamental difference between CTT and Martin-Löf type theory is that the identity type in the latter is replaced in CTT by a type of paths Path A (x, y) between two elements x, y : A. We will often write the path type infix as x = y, and say that x and y are path equal if there is an element of x = y. Cubical Type Theory represent paths as maps from an abstract interval type I, with endpoints 0 and 1. In particular a lambda abstraction like λ i.t will build a path of type t[0/i] = t [1/i]. This allows more canonical proofs of equality than just reflexivity, and so to give computational content to principles like function extensionality and univalence. Path equality is still substitutive, in the sense that any element of type P(x) can be transported along a path x = y to construct an element of P(y). In the following we will not rely on details about the specific primitives of CTT, which can be found in [14], and [38] for their incarnation in the Agda proof assistant.
Types can be classified according to the complexity of their path equality: We say a type is a mere proposition if any two elements are path equal, and that a type is a homotopy set, or simply a set, if its path equality type is a mere proposition. These predicates can be expressed in the type theory as types isProp(A) and isSet(A) for a type A. Given any universe of types U, we can form a universe of mere propositions Prop whose elements are pairs of an element of U and a proof that it is propositional. For A : Prop we will often write A itself rather than its first projection.
Cubical Type Theory also supports Higher Inductive Types (HITs), which allow to define an inductive type by declaring constructors also for its path equality, rather than only for its elements. For example, the propositional truncation ||A|| of a type A is defined as a higher inductive type with the following constructors This defines the least proposition extending A in the sense that any map f : If B is a set, then such an extension still exists if Π(x y : A). f x = f y [23]. For any two propositions A and B their conjunction A ∧ B is given by the cartesian product A × B, their disjunction A ∨ B by truncating their disjoint union ||A + B||, while the true and false propositions are given by the unit and the empty type. Univalence implies that any two logically equivalent propositions are equal, so associativity and commutativity of disjunction and other such laws hold as path equalities. Given a predicate P : A → Prop, universal quantification ∀a : A.P a is given by the dependent function type Π(a : A).P a, while existential quantification ∃a : A.P a is given by truncating the dependent pair type ||Σa : A.P a|| as generally it will not be propositional otherwise.
As ||Q|| and Q coincide when Q is a proposition, so do ∃a : A.P a and Σa : A.P a when P a uniquely determines a.

Finite Powerset
The finite powerset P f (A) [8,19] of a type is another example of a higher inductive type defined by the following constructors plus two equalities ensuring that P f (A) is a set [24]. Note that we restrict ourselves to non-empty finite powersets. We say that a pair of a type B and a binary operation f : is a set and f is associative, commutative and idempotent. It can then be shown that P f (A) is the free join-semilattice generated by A, and as such maps P f (A) → B which preserve ∪ correspond to maps A → B for any join-semilattice (B, f ). We use this to define the membership predicate x ∈ X , as Prop forms a join-semilattice with disjunction. Membership satisfies the following equations If X : P f (A) we write ∀a ∈ X . Q(a) to mean Π(a : A). a ∈ X → Q(a) and similarly for ∃a ∈ X .Q(a).
The finite powerset also supports the structure of a monad, and in particular, given f : A → P f (B) we write ∪ a∈X f a for the bind operation, defined using the free join-semilattice structure. Given f :

Clocked cubical type theory
Clocked Cubical Type Theory [24] extends Cubical Type Theory with the constructions of Clocked Type Theory [7,27], a type theory with Nakano style guarded recursion, multiple clocks and ticks. This section recalls each of these concepts, but in a simplified form, omitting constructions related to tick irrelevance. The fundamental notion in guarded recursion is that of a time step on a clock. Clocks are introduced as assumptions of the form κ : clock in the context, and time steps are represented as tick assumptions Figure 1: Selected typing rules for Clocked Cubical Type Theory [24]. The telescope TimeLess(Γ ′ ) is composed of the timeless assumptions in Γ ′ , i.e. interval variables and faces (as in Cubical Type Theory) as well as clock variables.
of the form α : κ. The type ⊲ (α : κ).A classifies computations that in the next time step (as represented by the tick α) return elements of A. When α does not appear in A we simply write ⊲ κ A for this type. Elements of ⊲ (α : κ).A are introduced by tick abstraction λ (α : κ).t and eliminated by tick application t [α]. The rules are similar to those for function types, except that tick application requires the eliminated term t not to depend on α, nor any of the variables bound before α. This rules out terms like λ which collapse two steps into one. Interval variables are considered timeless and therefore exempt from this restriction, which is necessary to prove that tick application preserves equalities: In fact, the above map is an equivalence of types, and this extensionality principle is one of the main reasons CTT is used rather than HoTT. One consequence is that ⊲ preserves truncation levels. In particular, and similarly for sets. The delay type allows to safely introduce a fixpoint combinator fix κ of type (⊲ κ A → A) → A and satisfying the path equality fix κ t = t (λ (α :κ).fix κ t) for any t. We can use fix κ to define guarded recursive types, i.e. ones where the recursive occurrences are guarded by ⊲ κ . An example is the partiality monad ). The path equality between this type and its unfolding gives rise to a type equivalence We use now L and step L to denote the two inclusions into L κ A up to the above equivalence.
An element of L κ A represents a possibly non-terminating computation of an element of A. For example, the element ⊥= fix κ (step L ) represents divergence. We say that is the free delay algebra generated by A in the sense that any map The monad structure is then defined with now L as the unit, and multiplication µ L : L κ L κ A → L κ A defined as the unique (delay algebra)-homomorphism extending the identity.
The clock quantification type former ∀κ.A is introduced by clock abstraction, and eliminated by application to a clock. It behaves much like a Π-type, except that clock is not a type, but has a similar status to the interval I. Clock quantification localises guarded recursion on a clock, and in particular supports a map force : ∀κ. ⊲ κ A → ∀κ.A, inverse to λ x. λ κ.λ (α :κ).x [κ], allowing to safely eliminate ⊲ κ .
The main use case for clock quantification is to encode coinductive types. For example ∀κ.L κ A is the final coalgebra for the functor F(X ) = A + X , if A is clock irrelevant, i.e., if the canonical map A → ∀κ.A is an equivalence. The notion of clock irrelevance is closed under all basic type formers as well as inductive types and (under certain restrictions [24]) higher inductive types. In particular, the inductive types used in this paper to represent syntax are all clock irrelevant. This encoding of coinductive types is originally due to Atkey and McBride [6] and presumes the existence of a clock constant κ 0 , which we achieve by just initially assuming κ 0 : clock.
More generally for every (indexed) functor F which commutes with clock quantification we have that ∀κ.fix κ (λ X . F(⊲ (α : κ).X [α])) is the final coalgebra of F, i.e. its coinductive fixpoint [24]. The collection of functors commuting with clock quantification is closed under a long list of constructors including truncations, finite powersets and sum types as expressed in the following type equivalences.

A powerdomain for may-convergence
Define the may powerdomain as the unique solution to the guarded recursive equation ) similarly to the definition of L κ A, but in the rest of this paper we will not give such definitions explicitly. The type constructor P κ ♦ comes equipped with the following operations ∪ : where ∪ is inherited from P f and therefore defines a join-semilattice and now ♦ (a) = {inl(a)} step ♦ (a) = {inr(a)} defines a unit and a delay algebra structure. In particular, this means that P κ ♦ (A) can represent diverging computations (⊥ = fix κ (step ♦ )), as well as values. An element of P κ ♦ (A) may also have both converging and diverging branches, as for example {a, ⊥}.
The next lemma states that for a set A, P κ ♦ (A) is the free algebra for the theory combining delay and union with no interaction between the two. Lemma 1. Let A be a set, let B be a set with both a join-semilattice structure and a delay algebra structure, and let f : A → B. Then there is a unique map P κ ♦ (A) → B extending f and commuting with the join-semilattice and delay-algebra structures.
In terms of algebraic theories, P κ ♦ can therefore be seen as generated by the theories of joinsemilattices and delay-algebras with no operations between them. As a special case of the lemma one can define a bind operation mapping a : P κ ♦ (A) and f : A → P κ ♦ B to a >>= f : P κ ♦ B which then equips P κ ♦ with a monad structure with unit given by now ♦ . Bind moreover commutes with these operations as in the following equations

Applicative may-simulation
The type constructor P κ ♦ should be seen as a guarded recursive powerdomain for may-convergence. Intuitively, this is true because an element of P κ ♦ (A) describes a set of values (of type A) that the computation has returned now, and a set of computations that we can choose to further evaluate, but may also choose not to, if we are only interested in testing if a program may evaluate to a particular value. This should be seen in contrast to the must-powerdomain of Section 6 which will force all branches of a computation tree to be evaluated fully before the result values can be inspected. In this section we substantiate that claim by using P κ ♦ to prove applicative may-similarity a congruence. We start by recalling the untyped lambda calculus with binary non-determinism and the notion of applicative may-similarity. We use informal binding notation here for readability, using the grammar M, N ::= M N | λ λ x.M | M or N for terms. This could for example be implemented more formally as an inductive family using de Bruijn indices. Note the use of λ λ to distinguish it from the meta-level lambda. A value is a closed term of the form λ λ x.M, and we shall use Λ and Val for the types of closed lambda terms and values respectively, which we will assume are sets (and indeed are if formalised using de Bruijn indices). These are moreover clock irrelevant, which can be shown by embedding them into the inductive types of all (also open) terms, and the fact that all inductive types are clock irrelevant [24].
We define two operational semantics. The first one is a big-step operational semantics formulated as a relation ⇓ ♦ : Λ × Val → Prop defined inductively in the standard way One can also similarly define a small-step operational semantics and prove this equivalent to the big-step semantics using standard methods. The second operational semantics is less familiar but has the benefit of being suitable for guarded recursive reasoning. It uses the monad P κ ♦ to model recursion and non-determinism, but since parts of the development in this section will be reused later, we will define the operational semantics relative to a monad T , which can be instantiated to be P κ ♦ . We will assume that T has operations ∪ and step T providing T with a join-semilattice structure as well as a delay-algebra structure satisfying the equations (3) and (4). In fact we shall see later that not all axioms for monads are needed for our developments.
Using this, we define an evaluation function eval : Λ → T (Val) as where pure refers to the unit of the monad T . Note that the match on (λ λ x.M ′ ) in the application case is exhaustive, since values can only be lambda abstractions. To lift this to a big step relation, we will assume given a lifting of T to predicates as follows.

5.T (P)(a ∪ b) =T (P)(a) ∧T (P)(b)
Note that a unique such lifting can be defined for P κ ♦ using Lemma 1 since Prop is a set, and ∧ and ⊲ define a join-semilattice and delay-algebra structure on Prop, soT (P) can be defined as the extension of P.
Specialising to T = P κ ♦ we make the following definition. Definition 2. LetT be the lifting of P κ ♦ to predicates, let Q : Val → Prop be a predicate on values and let M : One can then define a more standard big step operational semantics as Intuitively M ⇓ κ ♦ Q means that if M terminates to a value, that value will satisfy Q. In particular, M ⇓ κ ♦ V will hold for any V if M diverges, unlike the statement M ⇓ ♦ V which guarantees termination.
To express the precise relationship between the two semantics, we introduce a predicate of mayconvergence on the powerdomain P κ ♦ . Since termination cannot be expressed as a predicate on guarded recursive types directly, it must be expressed as a predicate on ∀κ.P κ ♦ (−), which captures global behaviour of P κ ♦ [28]. If m : ∀κ.P κ ♦ (A) and a : A define m ⇓ ∀ P ♦ a as the proposition inductively generated by the following introductions This means that these rules should be read as constructors of a HIT which also has propositional truncation operators as a constructor. The relationship between the two semantics can then be expressed as follows. Finally, the next lemma makes the intuition for M ⇓ κ ♦ Q stated above precise. As the notation used in the lemma suggests, κ can appear free in Q κ .

Applicative may-similarity
We now recall the notion of applicative similarity, as originally studied by Abramsky [1] for the pure lambda calculus and adapt it to finite non-determinism in the case of may-convergence. Say that a relation R on closed terms is an applicative may-simulation if MRN and M ⇓ ♦ λ λ x.M ′ implies Applicative may-similarity is the greatest applicative may-simulation. We define this by universally quantifying a clock in a guarded recursive definition. First define The statement M ≤ κ ♦ N should be read as stating that if M terminates, then also N terminates, and moreover, applying the resulting terms to the same value results in the related results later. Note the asymmetry in the use of operational semantics: The evaluation of M uses the guarded operational semantics which ensures that if M diverges, then M ≤ κ ♦ N is true. On the other hand, once M converges to a value, N must also converge, and expressing this requires the inductive operational semantics. The delay in the definition of ≤ κ Val ensures well-definedness: unfolding the definition of ≤ κ ♦ in ≤ κ Val gives a guarded recursive definition.
Applicative similarity is extended to open terms by defining M ≤ κ ♦ N to mean Mσ ≤ κ ♦ Nσ for all substitutions σ mapping all free variables in M and N to values. Finally, we localise the steps in the definition of M ≤ κ ♦ N by universally quantifying κ and thereby pass to a coinductive type: We now proceed to prove that applicative may-similarity is a congruence. Most proofs of this use syntactic arguments, but here we use a semantic method developed by Pitts [34] in the context of domain theory, which we adapt to guarded recursion. As a first step we construct a denotational semantics of the untyped lambda calculus.

Denotational semantics
Like the operational semantics, the denotational semantics is parametrised by a monad T equipped with a join-semilattice structure and a delay algebra structure, satisfying (3) and (4). Closed terms will be interpreted as elements of the type D κ defined by the following equations.
Here the definition of SVal κ should be read as a guarded recursive definition, and states that semantic values can be considered effectful computations on semantic values, but that this unfolding takes a single computation step. Define a semantic application · : and using this we define the operational semantics − κ : Λ(n) → (SVal κ ) n → D κ where Λ(n) is the set of terms with at most n free variables, as Note that the interpretation of values factor through pure : Theorem 1 (Soundness). T ( − κ Val )(eval M) = M κ We now specialise T to P κ ♦ for the following notation and corollary. If Q : A → Prop and m : P κ ♦ A, we shall use the infix notation m ↓ κ ♦ Q forT Qm, whereT is the lifting of P κ ♦ . Corollary 1. The statements M κ ↓ κ ♦ Q and M ⇓ κ ♦ Q • − κ Val are equivalent.

Relating syntax and semantics
We now construct a relation between syntax and semantics that will allow us to use the model to reason about the operational semantics. The relation is similar to the one constructed by Pitts [34] in the setting of domain theory, but whereas Pitts must provide a technical argument for the existence of the relation, which is far from obvious in the domain theoretic setting, in our setting the relation exists simply by guarded recursion.
In this section we specialise the model from the general monad T to P κ ♦ , and define two relations, one on values and one on general terms as follows This is well-defined, because unfolding the definition of κ in the definition of κ Val gives a guarded recursive definition of κ Val . If ρ : (SVal κ ) n and σ : Val n write ρ κ Val σ to mean ρ 1 Lemma 4 (Fundamental lemma). If ρ κ Val σ then M κ ρ κ Mσ . The fundamental lemma is proved by induction on M. Using this, one can prove the following correspondence between κ and ≤ ♦ Lemma 5. If M and N are closed terms then M ≤ ♦ N is equivalent to ∀κ. M κ κ N.
The left to right direction is proved by showing that κ is upward closed in its second argument. The other direction is proved using guarded recursion. Note that as a consequence of Lemma 4 and 5 it follows that ≤ ♦ is a reflexive relation.

A powerdomain for must-convergence
We now introduce our powerdomain construction P κ for must-convergence. This should have an inclusion now : A → P κ (A), a join-semilattice structure ∪ and a delay algebra structure step . However, when considering must-convergence, a term M or N diverges if M diverges even if N converges. To enforce that in our powerdomain we use equations to enforce parallel evaluation of subcomputations and stating that terminating values are postponed until all subcomputations have been evaluated fully: These equations (together with the derivable symmetric version of (6)) allow steps to bubble up the syntax tree, to a normal form consisting of a (possibly infinite) sequence of computation steps followed by a finite set of values. Following this intuition we define This has the benefit over, say a HIT given by the equations above, of giving direct access to the set of possible values returned by a computation that must converge. By definition P κ carries a delay-algebra structure, and the inclusion of A into P κ (A) can be defined as The join-semilattice can be defined by guarded recursion using the equations (5), (6), the symmetrisation of (6) and A natural question is whether P κ defines a monad. Since it is the composite of two monads, it is sufficient that there is a distributive law of monads, and indeed a natural candidate is easily defined as However, this only defines a distributive law of the monad P f over L κ considered as a functor, not a monad. Proposition 2. Of the four diagrams for distributive laws over monads: all but the last commute. A counterexample to the last is {step L (λ (α : κ).now L (now L x)), now L (step L λ (β : κ).now L x)} which is mapped by the lower composite to step L (λ (α : κ).now L {x})) and by the upper to step L λ (α : κ).step L λ (β : κ).now L {x}. Note that these only differ by a finite number of computation steps, i.e., are equal up to weak bisimilarity. We conjecture that this is generally true and that P κ is a monad up to weak bisimilarity.
As a consequence, using ζ to define the multiplication of P κ does not define a monad. Nevertheless, it does define a bind operation. Lemma 6. The bind operation induced by ζ maps f : A → P κ (B) and a : P κ (A) to a >>= L λ X . ∪ x∈X f (x) and satisfies the equations (now (a) >>= f ) = f (a) and (a >>=now ) = a, and moreover defines a homomorphism of delay-algebras as well as join-semilattices in a. It does not satisfy the associativity axiom.
Since the associativity axiom is not used in our development, the proofs done in the previous section for a general monad T carry over to this case, as we shall see.

Applicative must-simulation
We now show how our techniques from the may-convergence case apply to show that applicative mustsimilarity is a congruence also in the case of must-convergence. First we set up the operational semantics. In the case of the standard big-step semantics, define the predicate ⇓ ⊆ Λ × P f (Val) as The judgement M ⇓ X states that M must converge and that the possible values that it can converge to is X . The evaluation function eval : Λ → P κ (Val) is defined by specialising the general definition given in Section 5. We also define a relation M ⇓ κ Q stating that if M terminates, it will terminate to a set of values satisfying Q : P f (Val) → Prop. Note that Q is a predicate on sets of values, rather than values themselves (as was the case for M ⇓ κ ♦ Q). This allows us to express properties e.g. by existential quantification over outcome values, as needed e.g. in the definition of must-similarity below. To define M ⇓ κ Q, consider first a liftingL κ Q of predicates Q : A → Prop to L κ A defined aŝ and note that this also satisfies items 1 and 4 of Definition The relationship between these two operational semantics is similar to the one between ⇓ ♦ and ⇓ κ ♦ . First define, for m : ∀κ.L κ A and a : A a termination predicate m ⇓ ∀ a as an inductive family in Prop like so: Say that a relation R on closed terms is an applicative must-simulation if MRN implies Define M ≤ κ N by guarded recursion to be This is extended to open terms by defining M ≤ κ N to mean Mσ ≤ κ Nσ for all substitutions σ mapping all free variables in M and N to closed terms. Write M ≤ N for ∀κ.M ≤ κ N.
Also in the case of the denotational semantics the general case described in Section 5.2 specialises to P κ . None of the proofs or constructions rely on associativity of the bind operation, so also the soundness result holds. For our applications of the denotational semantics, however, we need a variant of Corollary 1 which applies to predicates on sets of values rather than on values themselves. This uses an infix notation m ↓ κ Q forL κ Q(m).

Relating syntax and semantics
As in the case of may-convergence we now construct a relation between syntax and semantics. To simplify syntax we introduce the lifting of a relation R : X ×Y → Prop to a relation on powersets P f (R) : We define two relations between syntax and semantics by mutual guarded recursion (overwriting notation from Section 5.3): If ρ : (SVal κ ) n and σ : Val n write ρ κ σ to mean ρ 1 κ σ 1 ∧ . . . ∧ ρ n κ σ n .
The proof of Lemma 9 is by induction on M. In particular the case of application requires some work, and relies on the fact that P f respects the monad structure of P f in the sense that if f : X → P f (X ′ ) and g : Y → P f (Y ′ ) map pairs related in R : X ×Y → Prop to pairs related in P f (S), then the extensions f : P f (X ) → P f (X ′ ) and g : P f (Y ) → P f (Y ′ ) map pairs related in P f (R) to pairs related in P f (S). Similarly to the case of may-convergence, this implies that applicative may-similarity is a reflexive relation. From this it follows that it is a congruence exactly as in the proof of Theorem 2.

Conclusion
The constructions of this paper illustrate how the combination of guarded recursion with higher inductive types and univalence in Clocked Cubical Type Theory gives an expressive type theory for reasoning about programming languages. In particular, this combination allows arguments known from domain theory involving constructions such as recursive types to be represented in type theory. Moreover, the abstract setting of synthetic guarded domain theory allows for these tools to be used in a much more elementary setting, far from the mathematical complexity of domain theory. This is particularly clear in the construction of the relation ≤ κ ♦ which in ordinary domain theory requires a non-trivial existence argument [34,33]. It also appears in our definitions of the guarded powerdomains, which we define much more directly than the standard constructions in domain theory [2].
It is unfortunate that the bind rule for P κ is not associative. As mentioned, this does not affect our constructions, and we conjecture that it is associative up to weak bisimilarity, and that this is enough for most purposes. We believe the reason for the failure of associativity is that the equality (6) is not algebraic in the sense that it only applies when one side is a value. One way to avoid this is to replace (5) and (6)  which means that to evaluate x ∪ y takes as many steps as the sum of steps used to evaluate x and y respectively, rather than the maximum. In particular, this means that idempotency is lost (but may hold up to weak bisimilarity) and one essentially works with finite multisets rather than the standard powerset.
Future work includes extending to the case of countable non-determinism. This could use the countable powerset functor, which is also definable as a HIT [13]. We believe that the case of may-convergence generalises directly to the countable case, but in the case of must-convergence the definition of ∪ as used here requires deciding if all branches of a computation terminates. We believe this is a symptom of a much more fundamental problem, namely that the partiality monad of guarded recursion describes termination in finite steps, whereas the must-convergence predicate for countable non-determinism requires more steps to reach a fixed point. Bizjak et al. [11] observe a similar problem in the operational setting and solve it using a combination of ⊤⊤-lifting and transfinite induction in the underlying step-indexing model. It would be interesting to see if such an approach also applies to type theory.
Finally, it would be interesting to develop a general theory of combinations of algebraic effects such as state, exceptions, and non-determinism (as studied here) with guarded recursion. The domain theoretic counterparts of these effects are usually described algebraically using order-enriched theories [21], but as we have seen here, in the setting of guarded recursion the intensional information of the individual steps allows us to describe the interaction of these effects with recursion in terms of ordinary equations. This theory could then give rise to a notion of guarded interaction trees [39] which would allow also equations between computations across steps as well as guarded recursive definitions.