{'fraction_non_alphanumeric': 0.04997142396576738, 'fraction_numerical': 0.009188294084028195, 'mean_word_length': 3.8393730941068007, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Denotational semantics of recursive types in synthetic guarded domain theory

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques. Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for FPC, the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.


Introduction
Recent years have seen great advances in formalisation of mathematics in type theory, in particular with the development of homotopy type theory [Uni13]. Such formalisations are an important step towards machine assisted verification of mathematical proofs. Rather than adapting classical set theory-based mathematics to type theory, new synthetic approaches sometimes offer simpler and clearer presentations in type theory. As an example of the synthetic approach, consider synthetic homotopy theory [Uni13], which formalises homotopy theory in type theory, not by formalising a topological space as a type with structure, but rather by thinking of types as topological spaces directly. Particular spaces such as the circle can then be constructed as types using higher inductive types. Synthetic homotopy theory can be formally related to classical homotopy theory via the simplicial sets interpretation of homotopy type theory [KL12], interpreting types essentially as topological spaces.
Just like any other branch of mathematics, domain theory and denotational semantics for programming languages with recursion should be formalised in type theory and, as was the case of homotopy theory, synthetic approaches can provide clearer and more abstract proofs. In the case of domain theory, the synthetic approach means treating types as domains, rather than constructing domains internally in type theory as types with an order relation. The result of this should be a considerable simplification of denotational semantics when expressed in type theory. For example, function types of a higher-order object language can be modelled simply as the function types of type theory, rather than as some type of Scott continuous maps. To model recursion, some form of fixed point construction must be added to type theory, but, as is well known, an unrestricted fixed point combinator makes the logical reading of type theory inconsistent.

Synthetic guarded domain theory
In this paper we follow the approach of guarded recursion [Nak00], which introduces a new type constructor ⊲, pronounced "later". Elements of ⊲A are to be thought of as elements of type A available only one time step from now, and the introduction form next : A → ⊲A makes anything available now, also available later. The fixed point operator has type fix : (⊲A → A) → A and maps an f to a fixed point of f • next. Guarded recursion also assumes solutions to all guarded recursive type equations, i.e., equations where all occurences of the type variable are under a ⊲, as for example in the equation used to define the lifting monad L below, but guarded recursive equations can also have negative or even non-functorial occurences. One application of guarded recursion is for programming with coinductive types. This requires a notion of clocks used to index delays. For example, if κ is a clock and A is a type then ⊲ κ A is a type. If κ is a clock variable not free in A and LA ∼ = A + ⊲ κ LA, then κ can be universally quantified in LA to give the type ∀κ.LA which can be shown to be a coinductive solution to ∀κ.LA ∼ = A + ∀κ.LA. Almost everything we do in this paper uses a single implicit clock variable and all uses of ⊲ should be thought of as indexed by this clock. More details can be found in Section 2.
Recent work has shown how guarded recursion can be used to construct syntactic models and operational reasoning principles for (also combinations of) advanced programming language features including general references, recursive types, countable nondeterminism and concurrency [Bir+12; BBM14;SB14]. These models often require solving recursive domain equations which are beyond the reach of domain theoretic methods. When viewing these syntactic models through the topos of trees model of guarded recursion [Bir+12] one recovers step-indexing [AM01], a technique for sidestepping recursive domain equations by indexing the interpretation of types by numbers, counting the number of unfoldings of the equation. Thus guarded recursion can be more accurately described as synthetic step-indexing. Indeed, guarded recursion provides a type system for constructing step-indexed models, in which the type equations sidestepped by step-indexing can be solved using guarded recursive types.
This work is part of a programme of developing denotational semantics using guarded recursion with the expectation that this will not only be simpler to formalise in type theory than the classical domain theoretic semantics, but also generalise to languages with advanced features for which step-indexing has been used for operational reasoning.
This programme was initiated in previous work [PMB15], in which a model of PCF (simply typed lambda calculus with fixed points) was developed in Guarded Dependent Type Theory (GDTT) [Biz+16] an extensional type theory with guarded recursive types and terms. By aligning the fixpoint unfoldings of PCF with the steps of the metalanguage (represented by ⊲), we proved a computational adequacy result for the model inside type theory. Guarded recursive types were used both in the denotational semantics (to define a lifting monad) and in the proof of computational adequacy. Likewise, the fixed point operator fix of GDTT was used both to model fixed points of PCF and as a proof principle.

Contributions
Here we extend our previous work in two ways. First we extend the denotational semantics and adequacy proof to languages with recursive types. Secondly, we define a relation capturing extensionally equal elements in the model.
More precisely, we consider the language FPC (simply typed lambda calculus extended with general recursive types) with a call-by-name operational semantics. Working internally in GDTT this language can be given a denotational semantics in the synthetic style discussed above. In particular, function types of FPC are interpreted simply as the function types of GDTT. Base types are interpreted using the lifting monad L satisfying the isomorphism (1). In particular the unit type of FPC is interpreted as L1 isomorphic to 1 + ⊲L1, so that denotationally, a program of this type is either a value now, or a delayed computation. Recursive types are modelled as guarded recursive types satisfying the isomorphism µα.σ ∼ = ⊲ σ[µα.σ/α] (in the case of closed types). This means that the introduction rule for recursive types (folding a term) can be interpreted as next. To interpret unfolding of terms of recursive types we construct, for every FPC type σ a map θ σ : ⊲ σ → σ, and interpret unfolding as θ σ[µα.σ/α] . As a consequence, folding followed by unfolding is interpreted as the map δ σ[µα.σ/α] defined as θ σ[µα.σ/α] • next. This composition is not the identity, rather the denotational semantics counts the number of fold-unfold reductions needed to evaluate a term to a value.
Thus, to state a precise soundness theorem, the operational semantics also needs to count the fold-unfold reductions. To do this, we define a judgement M → k * N to mean that M reduces to N in a sequence of reductions containing exactly k fold-unfold reductions, and an equivalent big-step semantics M ⇓ k v. One might hope to formulate an adequacy theorem stating that for M of type 1, M ⇓ k (where is the introduction form for 1) if and only if M = δ k . Unfortunately this is not true. For example, if M ⇓ 2 the type M ⇓ 1 is empty, but the identity type M = δ 1 is equivalent to ⊲0, a non-standard truth value different from 0. To state an exact correspondence between the operational and denotational semantics we use the guarded transitive closure of the small-step semantics which synchronises the steps of FPC with those of GDTT. This is defined as M ⇒ k+1 N if M → 0 * M ′ , M ′ → 1 M ′′ and ⊲(M ′′ ⇒ k N ), where M ′ → 1 M ′′ is a fold-unfold reduction in an evaluation context.
The adequacy theorem states that M ⇒ k if and only if M = δ k . We prove this working inside GDTT, and the proof shows an interesting aspect of guarded domain theory: It uses a logical relation between syntax and semantics defined by induction over the structure of types. The case of recursive types requires a solution to a recursive type equation. In the setting of classical domain theory, the existence of this solution requires a separate argument [Pit96], but here it is simply a guarded recursive type.
The second contribution is a relation capturing extensionally equal elements in the model. As mentioned above, the denotational semantics distinguishes between computations computing the same value in a different number of steps. In this paper we construct a relation on the denotational semantics of each type relating elements extensionally equal elements, i.e., elements that compute the same value in a different number of steps. This relation is defined on the global interpretation of types σ gl defined from σ by quantifying over the implicit clock variable (see Section 1.1 above). This is necessary, because, as can be seen from the denotational semantics of guarded recursion, any relation on 1 relating to δ n for any n will also necessarily relate non-termination to . On the other hand, it is possible to define such a relation on 1 gl which is the coinductive solution to 1 gl ∼ = 1 + 1 gl . This is then lifted to function types in the usual way for logical relations: Two functions are related it they map related elements to related elements, and to recursive types using a solution to a guarded recursive type equation. We prove a soundness result for this relation stating that if the (global) denotation of two terms are related, then the terms are contextually equivalent.
Finally we show that it is possible to execute the denotational semantics. Of course, FPC is a non-total programming language, so to run FPC programs in type theory, these must be given a time-out to ensure termination. We demonstrate the technique in the case of boolean typed programs and show that the denotation of a program executes to true with a time-out of n steps if and only if the program evaluates to true in less than n steps in the operational semantics.
All constructions and proofs are carried out working informally in GDTT. This work illustrates the strength of GDTT , and indeed influenced the design of the type theory.

Related work
Escardó constructs a model of PCF using a category of ultrametric spaces [Esc99]. Since this category can be seen as a subcategory of the topos of trees [Bir+12], our previous work on PCF is a synthetic version of Escardó's model. Escardó's model also distinguishes between computations computing the same value in a different number of steps, and captures extensional behaviour using a logical relation similar to the one constructed here. Escardó however, does not consider recursive types. Although Escardó's model was useful for intuitions, the synthetic construction in type theory presented here is very different, in particular the proof of adequacy, which here is formulated in guarded dependent type theory.
Synthetic approaches to domain theory have been developed based on a wide range of models dating back to [Hyl91;Ros86]. Indeed, the internal languages of these models can be used to construct models of FPC and prove computational adequacy [Sim02]. A more axiomatic approach was developed in Reus's work [Reu96] where an axiomatisation of domain theory is postulated a priori inside the Extended Calculus of Constructions.
There has also been work on (non-synthetic) adaptations of domain theory to type theory [BKV09; Ben+10; Doc14]. However, due to the mistmatch between set-theory and type theory "some of the proofs and constructions are much more complex than they would classically and one does sometimes have to pay attention to which of two classicallyequivalent forms of definition one works with" [BKV09]. More recently Altenkirch et al. [ADK17] have shown how to encode the free pointed ω-cpo as a quotient inductiveinductive types (QIIT). This looks like a more promising direction for domain theory in type theory, but this has not yet been developed to models of programming languages.
The lifting monad used in this paper is a guarded recursive variant of Capretta's delay monad [Cap05] considered by among others [BKV09; Ben+10; Dan12; CUV15; ADK17; Vel17]. The monad D(A) is coinductively generated by the constructors now : A → D(A) and later : D(A) → D(A). As reported by Danielsson [Dan12], working with the partiality monad requires convincing Agda of productivity of coinductive definitions using workarounds. In this paper productivity is ensured by the type system for guarded recursion.
In the delay monad, two computations of type D(A) can be distinguished by their number of steps. To address this issue, Capretta also defines a weak bisimulation on this monad, similar to the one defined in Definition 6.2, and proves the combination of the delay monad with the weak bisimulation is a monad using setoids. Chapman et al. [CUV15;Vel17] avoid using setoids, but they crucially rely on proposition extensionality and the axiom of countable choice. Altenkirch et al. [ADK17] show that under the assumption of countable choice, their free pointed ω-cpo construction is equivalent to quotiented delay monad of Chapman et al. We work crucially with the non-quotiented delay monad when defining the denotational semantics, since the steps are necessary for guarded recursion. This is an extended version of a conference publication [MP16]. A number of proofs that were omitted from the previous version due to space restrictions have been included in this version. There is also a slight difference in approach: the conference version defined a big-step operational semantics equivalent to the guarded transitive closure of the smallstep operational semantics of Figure 2 below. This operational semantics synchronises the steps of FPC with those of the meta-language, and capturing this in a big-step semantics was quite tricky. Here, instead, we define a simpler big-step operational semantics and prove this equivalent to the "global" small-step semantics (Lemma 3.2). The results on executing the denotational semantics presented in Section 7 are also new.
Since this work was carried out, the extensional type theory GDTT that we work in in this paper has been extended in two directions towards intensionality and implementation. The first direction is Guarded Cubical Type Theory [Bir+16], extending the fragment of GDTT without universal quantification over clocks with constructions from Cubical Type Theory [Coh+16]. Guarded Cubical Type Theory even has a prototype implementation. The other direction is Clocked Type Theory [BGM17], a variant of the fragment of GDTT without identity types in which delayed substitutions (Section 5.1) are encoded using a new notion of ticks on a clock. Clocked Type Theory has a strongly normalising reduction semantics. Since neither theory is complete, we stick to GDTT as our type theory for this paper.
The paper is organized as follows. Section 2 gives a brief introduction to the most important concepts of GDTT. More advanced constructions of the type theory are introduced as needed. Section 3 defines the encoding of FPC and its operational semantics in GDTT. The denotational semantics is defined and soundness is proved in Section 4. Computational adequacy is proved in Section 5, and the relation capturing extensional equivalence is defined in Section 6. Section 7 shows how to execute the denotational semantics of boolean programs. We conclude and discuss future work in Section 8.

Guarded recursion
In this paper we work informally within a type theory with dependent types, inductive types and guarded recursion. Although inductive types are not mentioned in [Biz+16] the ones used here can be safely added -as they can be modelled in the topos of trees model -and so the arguments of this paper can be formalised in Guarded Dependent Type Theory (GDTT) [Biz+16]. We start by recalling some core features of this theory, but postpone delayed substitutions to Section 5.1 since these are not needed for the moment.
When working in type theory, we use ≡ for judgemental equality of types and terms and = for propositional equality (sometimes = A when we want to be explicit about the type). We also use = for (external) set theoretical equality.
The core of guarded recursion consists of the type constructor ⊲ and the fixed point (2) both introduced in Section 1.1. Elements of type ⊲A are intuitively elements of type A available one time step from now. To illustrate the power of the fixed point operator, consider a type of guarded streams Str g satisfying This is a guarded recursive type in the sense that the recursion variable appears under a ⊲, and its elements are to be thought of as streams, whose head is immediately available and whose tails take one time step to compute. The fixed point operator can be used to define guarded streams by recursion. For example, the constant stream of a number n can be defined as fix(λx. n, x ), where the type isomorphism (3) is left implicit. Note that the type of the fixed point operator prevents us from defining elements like fix(λx.x), which are not productive, in the sense that any element of the stream can be computed in finite time. In fact, the type ⊲ Str g → Str g precisely captures productive recursive stream definitions.
The type constructor ⊲ is an applicative functor in the sense of [MP08], which means that there is a "later application" ⊛ : ⊲(A → B) → ⊲A → ⊲B written infix, satisfying among other axioms (see also [BM13]). In particular, ⊲ extends to a functor mapping f : A → B to λx : ⊲A. next(f ) ⊛ x. Moreover, the ⊲ operator distributes over the identity type as follows Guarded dependent type theory comes with universes in the style of Tarski. In this paper, we will just use a single universe U. Readers familiar with [Biz+16] should think of this as U κ , but since we work with a unique clock κ, we will omit the subscript. The universe comes with codes for type operations, including + : U × U → U for binary sum types, codes for dependent sums and products, and ⊲ : ⊲U → U satisfying where we use El(A) for the type corresponding to an element A : U. The type of ⊲ allows us to solve recursive type equations using the fixed point combinator. For example, if A is small, i.e., has a code A in U, the type equation (1) can be solved by computing a code of LA as and then by taking the elements using El. More precisely, defining LA as El( L A), LA unfolds to El( +( A, ⊲(next( L A)))) which is equal to A + El( ⊲(next( L A))) which is equal to A + ⊲LA. In this paper, we will only apply the monad L to small types A.
To ease presentation, we will usually not distinguish between types and type operations on the one hand, and their codes on the other. We will still refer use the notation ⊲ : ⊲U → U, but write ⊲ for the composition ⊲ • next. We generally leave El implicit.

The topos of trees model
The topos S of trees is the category of presheaves over ω, the first infinite ordinal. The category S models guarded recursion [Bir+12] and provides useful intuitions, and so we briefly recall it.
A closed type is modelled as an object of the topos of trees, i.e., as a family of sets X(n) indexed by natural numbers together with restriction maps r X n : X(n + 1) → X(n) as in the following diagram A term of type Y in context x : X, for X, Y closed types, is modelled as a morphism in S, i.e., as a family of functions f i : X(i) → Y (i) obeying the naturality condition The ⊲ type operator is modelled as an endofunctor in S such that ⊲X(1) = 1, ⊲X(n + 1) = X(n). Intuitively, X(n) is the nth approximation for computations of type X, thus X(n) describes the type X as it looks if we have n computational steps to reason about it.
Using the proposition-as-types principle, types like ⊲ 3 0 are non-standard truth values. Following the intuition that ⊲ 3 0(n) is the type ⊲ 3 0 as it looks, if we have n steps to reason about it, ⊲ 3 0 is the truth value of propositions that appear true for 3 computation steps, but then are falsified after 4. In fact, in the model, (⊲ 3 0)(3) equals 1, but (⊲ 3 0)(4) equals 0 zero as depicted by the following diagram The global elements of a closed type X is the set of morphisms from the constant object 1 to X in S. This can be thought of as the limit of the sequence of (8) as a diagram in Set. This construction gives us the global view of a type as it allows us to observe all the computation at once. For example, the global elements of ⊲X correspond to those of X simply by discarding the first component. Note that objects can have equal sets of global elements without being isomorphic. In particular 0 and ⊲ n 0 are not isomorphic.
For guarded recursive type equations, X(n) describes the nth unfolding of the type equation. For example, fixing an object A, the unique solution to (1) is LA(n) = 1 + A(1) + · · · + A(n) with restriction maps defined using the restriction maps of A. In particular, if A is a constant presheaf, i.e., A(n) = X for some fixed X and r A n identities, then we can think of LA(n) as {0, . . . , n − 1} × X + {⊥} with restriction map given by r n (⊥) = ⊥, r n (n, x) = ⊥ and r n (i, x) = (i, x) for i < n. The set of global elements of LA is then isomorphic to N × X + {⊥}. In particular, if X = 1, the set of global elements isω, the natural numbers extended with a point at infinity.
The global elements of LA, correspond to the elements of Capretta's partiality monad [Cap05] L gl defined as the coinductive solution to the type equation Similarly, the type of Str g can be modelled as Str g (n) = N n × 1. Note that if these products associate to the right, we can even model (3) as an identity. The restriction maps of this type are projections, and the global elements of this type correspond to streams in the usual sense.

Universal quantification over clocks
The type of guarded streams Str g mentioned above, is not the usual coinductive type of streams. For example, a term t : Str g in context x : Str g is a causal function of streams, i.e., one where the n first elements of the output depend only on the n first elements of the input. This can be seen e.g. in the topos of trees model, where such a term is modelled by a family of maps f n : N n × 1 → N n × 1 commuting with projections. Causality is crucial to the encoding of productivity in types mentioned above.
On the other hand, a closed term t : Str g is modelled by a global element of Str g and thus corresponds to a real stream of numbers. Likewise, if t : Str g only depends on a variable x : N, then t denotes a map from the set of natural numbers to that of streams, because the context is modelled as the constant topos of trees object N, with restriction maps being identities. More generally, say a context is independent of time if it is modelled as a constant object, i.e, one where all restriction maps are isomorphisms. The denotation of a term t : Str g in a context Γ independent of time, corresponds to a map from Γ(1) to the set of streams.
The idea of independence of time can be captured syntactically using a notion of clocks, and universal quantification over these [AM13]. We now briefly recall this as implemented in GDTT, referring to [Biz+16] for details.
In GDTT all types and terms are typed in a clock context, i.e., a finite set of names of clocks. For each clock κ, there is a type constructor ⊲ κ , a fixed point combinator, and so on. Each clock carries its own notion of time, and the idea of a context being independent of time mentioned above, can be captured as a clock not appearing in a context.
If A is a type in a context where κ does not appear, one can form the type ∀κ.A, binding κ. This construction behaves in many ways similarly to polymorphic quantification over types in System F. There is an associated binding introduction form Λκ.(−) (applicable to terms where κ does not appear free in the context), and elimination form t[κ ′ ] having type A[κ ′ /κ] whenever t : ∀κ.A.
Semantically, a closed type in the empty clock variable context is modelled by a set, and a type in a context of a single clock is modelled as an object in the topos of trees. In the latter case, universal quantification over the single clock is modelled by taking the set of global elements. As we saw above, these sets correspond to coinductive types, and this also holds in the type theory: If Str g is the type of streams guarded on clock κ, i.e., satisfies Str g ∼ = N × ⊲ κ Str g , then one can prove [AM13; Møg14] that the type ∀κ. Str g behaves as a coinductive type of streams. Similarly, if LA ∼ = A + ⊲ κ LA, and κ is not free in A, then ∀κ.LA is a coinductive solution to X ∼ = A + X. This isomorphism arises as a composite of isomorphisms the components of which we recall below. Using these encodings one can use guarded recursion to program with coinductive types in such a way that typing guarantees produc-tivity. We refer to [BM15] for a full model of guarded recursion with clocks, in particular for how to model types with more than one free clock variable. The isomorphism (14) arises from a general type isomorphism ∀κ.⊲ κ A ∼ = ∀κ.A holding for all A. The direction from right to left is induced by next κ : A → ⊲ κ A. For the direction from left to right, a form of elimination for ⊲ κ is needed, but note that an unrestricted such of type ⊲ κ A → A in combination with fixed points makes the type system inconsistent. Instead GDTT allows for a restricted elimination rule for ⊲ κ : If t is of type ⊲ κ A in a context where κ does not appear free, then prev κ.t has type ∀κ.A. Using prev κ. we can define a term force: The term force can be proved to be an isomorphism by the axioms The other direction is given by application to a clock constant κ 0 , which we assume exists. These can be proved to be inverses of each other using the clock irrelevance axiom, which states that if t : ∀κ.A and κ does not appear free in A, then t[κ ′ ] ≡ t[κ ′′ ] for all κ ′ and κ ′′ . Using force and the isomorphism ∀κ.0 ∼ = 0, one can prove that ∀κ.⊲ n κ 0 is isomorphic to 0, reflecting the fact that there are no global elements of ⊲ n 0 in the model, as mentioned earlier. We refer to [Biz+16] for details.
The isomorphism (12)  If π 1 (x[κ 0 ]) = inl(⋆), note that for any κ, using the clock irrelevance axiom is similar. In fact, this construction generalises to an isomorphism valid whenever κ is not free in A.
Finally we note the following extensionality rule for quantification over clocks.
In most of this paper we will work in a setting of a unique implicit clock κ, and simply write ⊲ for ⊲ κ to avoid cluttering all definitions and calculations with clocks.
For the proof of computational adequacy we will need one more construction from GDTT: The delayed substitutions. These will be recalled in Section 5.1.

FPC
This section defines the syntax, typing judgements and operational semantics of FPC. These are inductive types in guarded type theory, but, as mentioned earlier, we work informally in type theory, and in particular remain agnostic with respect to choice of representation of syntax with binding.
The typing judgements of FPC are defined in an entirely standard way. The grammar for terms of FPC L, M, N : should be read as an inductive type of terms in the standard way. Likewise the grammars for types and contexts and the typing judgements defined in Figure 1 should be read as defining inductive types in type theory, allowing us to do proofs by induction over e.g. typing judgements.
We denote by Type FPC , Term FPC and Value FPC the types of closed FPC types and terms, and values of FPC and by OTerm FPC the type of all (also open) terms. By a value we mean a closed term matching the grammar v ::

Operational semantics
Figure 2 defines a big-step and a small-step operational semantics for FPC, as well as two transitive closures of the latter. All these definitions should be read as inductive types. Since the denotational semantics of FPC is intensional, counting reduction steps, it is necessary to also count the steps in the operational semantics in order to state the soundness and adequacy theorems precisely. More precisely, the semantics counts the number of unfold-fold reductions in the same fashion in which Escardó counted fix-point reduction for PCF.
The statement where M is a term, k a natural number, and v a value, should be read as 'M evaluates in k steps to a value v. We can define more standard big-step evaluation predicates as follows We note that the semantics is trivially deterministic.
Well formed types Typing rules Of the two transitive closures of the small-step semantics defined in Figure 2 the first is a standard one, equivalent to the big-step operational semantics. The second is a guarded version which synchronises the steps of FPC with those of the metalogic. This is needed for the statement of the soundness and adequacy theorems, and also allows for guarded recursion to be used in the proofs of these. The next lemma states the relationship between the big-step semantics and the two transitive closures of the small-step semantics Lemma 3.2. Let M and N be FPC terms, v a value and k a natural number. Then The opposite implication does not hold, as we shall see in the examples below.
Proof. The first statement is a essentially a textbook result on operational semantics, and we omit the proof.
For the second statement the proof from left to right is by induction on M → k * N . The case of M = N is trivial, so consider the case when M → k M ′ and M ′ → m * N . When  The right to left implication is proved by induction on k. When k = 0 the clock κ is not free in M ⇒ k N and so ∀κ.

Examples
As an example of a recursive FPC type, one can encode the natural numbers as Using this definition we can define the term ifz of PCF. If L is a term of type nat and M ,N are terms of type σ define ifz as On the other hand, ifz 1 0 1 → 2 * 42 is equivalent to 0, showing that ⇒ and → * are not equivalent.
Recursive types introduce divergent terms. For example, given a type A, the Turing fixed point combinator on A can be encoded as follows: If, on the other hand, M is divergent in the sense that for any k there exists an N such that M → k * N , then M ⇒ n v is equivalent to ⊲ n 0.

Denotational Semantics
We now define the denotational semantics of FPC. First we recall the definition of the guarded recursive version of the lifting monad on types from [PMB15]. This is defined as the unique solution to the guarded recursive type equation which exists because the recursive variable is guarded by a ⊲. Recall (Section 2) that guarded recursive types are defined as fixed points of endomaps on the universe, so LA is only defined for small types A. We will only apply L to small types in this paper. The isomorphism induces a map θ LA : ⊲LA → LA and a map η : A → LA. An element of LA is either of the form η(a) or θ(r). We think of these cases as values "now" or Formallyf is defined as a fixed point of a term of type ⊲(LA → B) → LA → B. Recall that λr. next(f ) ⊛ r is the application of the functor ⊲ to the mapf , thusf is an algebra homomorphism.
Intuitively LA is the type of computations possibly returning an element of A, recording the number of steps used in the computation. We can define the divergent computation as ⊥ def == fix(θ) and a "delay" map δ LA of type LA → LA for any A as δ LA def == θ LA • next. The latter can be thought of as adding a step to a computation. The lifting L extends to a functor. For a map f : A → B the action on morphisms can be defined using the unique extension as

Interpretation of types
A type judgement Θ ⊢ τ is interpreted as a map of type U |Θ| → U, where |Θ| is the cardinality of the set of variables in Θ. This interpretation map is defined by a combination of induction and guarded recursion for the case of recursive types as in Figure 3.
More precisely, the case of recursive types is defined to be the fixed point of a map from ⊲(U |Θ| → U) to U |Θ| → U defined as follows: The first equation is the application of rule (2) for the guarded fix-point combinator, whereas the second equation is derived by distributivity over the later application operator described by rule (4). Finally, the last equation is derived by the fact that the elements of the code of the later operator is the later operator on types (rule (6)).
We prove now the substitution lemma for types which states that substitution behaves as expected, namely that substituting type variables in the syntax with syntactic types corresponds to applying a dependent type U → U to a type U. This can be proved using guarded recursion in the case of recursive types.
Lemma 4.1 (Substitution Lemma for Types). Let σ be a well-formed type with variables in Θ and let ρ be of type U |Θ| . If Θ, β ⊢ τ then Proof. The proof is by induction on Θ, β ⊢ τ . Most cases are straightforward, and we just show the case of Θ, β ⊢ µα.τ . The proof of this case is by guarded recursion, and thus we assume that Assuming (without loss of generality) that α is not β we get the following series of equalities The latter equals and so By direct use of the Substitution Lemma we can prove that the interpretation of the recursive type equals the interpretation of the unfolding of the recursive type itself, only one step later. Intuitively, this means that we need to consume one computational step to look at the data.
The interpretation of every closed type τ carries a ⊲-algebra structure, i.e., a map θ τ : ⊲ τ → τ , defined by guarded recursion and structural induction on τ as in Figure 4. The case of recursive types is welltyped by Lemma 4.2, and can be formally constructed as a fixed point of a term of type as follows. Suppose F : ⊲(Πσ : Type FPC .(⊲ σ → σ )), and define G(F ) essentially as in Figure 4 but with the clause G(F ) µα.τ for recursive types being defined as Here F σ is defined as F ⊛ next(σ) using a generalisation of ⊛ to dependent products to be defined in Section 5.1. Define θ as the fixed point of G. Then Using the θ we define the delay operation which, intuitively, takes a computation and adds one step. σ where x 1 : σ 1 , · · · , x n : σ n def == σ 1 × · · · × σ n . In the case of case, the function f is the extension of f to a homomorphism defined as in (21) above, using the fact that all types carry a ⊲-algebra structure. The interpretation of fold is welltyped because next( M (γ)) has type ⊲ τ [µα.τ /α] which by Lemma 4.2 is equal to µα.τ . In the case of unfold, since M (γ) has type µα.τ , which by Lemma 4.2 is equal to ⊲ τ [µα.τ /α] , the type of θ τ [µα.τ /α] ( M (γ)) is τ [µα.τ /α] .

Fig. 5. Interpretation of FPC terms
Proof. Straightforward by definition of the interpretation and by the type equality from Lemma 4.2.
Next lemma proves substitution is well-behaved for terms. The proof is standard textbook result from domain theory (e.g. [Win93;Str06]).
Lemma 4.4 (Substitution Lemma). Let Γ ≡ x 1 : σ 1 , · · · , x k : σ k be a context such that Γ ⊢ M : τ , and let ∆ ⊢ N i : σ i be a term for each i = 1, . . . k. If further γ ∈ ∆ , then which is now by definition what we wanted. The case for Γ ⊢ inr N : τ 1 + τ 2 is similar. Now the case for Γ ⊢ case L of x 1 .M ; x 2 .N : σ. By definition we know that which is by definition of the interpretation equal to where f is as in Figure 5. By induction hypothesis we know that this is equal to which is equal by definition to We now aim to show a soundness theorem for the interpretation of FPC. We do this by first showing soundness of the single step reduction as in the next lemma. As usual in denotational semantics, this proves that the model is agnostic to operational reductions. By induction hypothesis this is equal to θ(δ k µα.τ ( M 2 ( * ))) which by Lemma 4.7 is equal to δ k τ [µα.τ /α] (θ( M 2 ( * ))) thus concluding.
The two most complicated cases of the proof of Lemma 4.5, namely the unfold-fold reductions and case, are captured in the following two lemmas. In particular, the first of these states that the interpretation of case is a ⊲-algebra homomorphism. In other words, case analysing over a computation that perform n ticks and then produces a result v is equal to a computation that produces n ticks and then performs case analysis over a terminating computation producing a value v. Proof. For the proof of the first part, we use the notation f as in Figure 5. Since f is a homomorphism of ⊲-algebras we get For the second part, note that f is λx.case x of x 1 .M ; x 2 .N (γ), so We now prove the same for the interpretation of unfold. The key point here is to observe that the tick operation for a folded recursive type , namely θ µα.τ , is precisely the tick of the unfolded recursive type after one step of computation, namely ⊲(θ τ [µα.τ /α] ). Proof. The interpretation for λx : µα.τ.unfold x (θ µα.τ (r)) yields θ τ [µα.τ /α] (θ µα.τ (r)). This type checks as r has type ⊲ µα.τ , thus (θ µα.τ (r)) has type µα.τ which -by Lemma 4.2 -is equal to ⊲ τ [µα.τ /α] . Thus the term θ τ [µα.τ /α] (θ µα.τ (r)) has type τ [µα.τ /α] . Now by definition of θ µα.τ this is equal to For the second statement, we compute We can now prove Lemma 4.5. As stated above, this is soundness of the model w.r.t. the small-step operational semantics. For the proof, it is crucial that the interpretation of every term is an homomorphism of tickθ-algebras. This falls out in many cases. For the cases of the interpretation of unfold and the inductive case of case we use the lemmas we just proved above. Finally, the case for unfold M → k unfold M ′ . If k = 0 the case follows trivially from the induction hypothesis. If k = 1, the step from the induction hypothesis to the case is exactly the second statement of Lemma 4.7.
We now state and prove soundness of our model w.r.t. the operational semantics. We use the transitive closure over → k , namely ⇒ k , which is synchronised with the ⊲ operator in the type theory. Using ⇒ (rather than → * ) is not essential to prove soundness, but it is crucial to prove computational adequacy, which will be presented in the next section. On the other hand, the explicit step-indexing k in ⇒ k is necessary to relate the number of operational steps with the number of delays (or ticks) in the denotational semantics.  * )). By induction hypothesis we get ⊲( M ′′ ( * ) = δ n N ( * )) which implies next( M ′′ ( * )) = next(δ n N ( * ))) and since δ = θ • next, this implies δ( M ′′ ( * )) = δ k ( N ( * )). By putting together the equations we get finally M ( * ) = δ k N ( * ).

Computational Adequacy
Computational adequacy is the opposite implication of Proposition 4.8 in the case of terms of unit type. It is proved by constructing a (proof relevant) logical relation between syntax and semantics. The relation cannot be constructed just by induction on the structure of types, since in the case of recursive types, the unfolding can be bigger than the recursive type. Instead, the relation is constructed by guarded recursion: we assume the relation exists later, and from that assumption construct the relation now by structural induction on types. Thus the well-definedness of the logical relation is ensured by the type system of GDTT, more specifically by the rules for guarded recursion. This is in contrast to the classical proof in domain theory [Pit96], where existence requires a separate argument. The logical relation uses a lifting of relations on values available now, to relations on values available later. To define this lifting, we need delayed substitutions, an advanced feature of GDTT.

Delayed substitutions
In GDTT, if Γ, x : A ⊢ B type is a well formed type and t has type ⊲A in context Γ, one can form the type ⊲ [x t] .B. Intuitively, one time step from now, t delivers an element in A, and ⊲ [x t] .B is the type of elements that one time step from now delivers something in B with x substituted by the element delivered at that time by t. One motivation for this construction is to generalise ⊛ (described in Section 2) to a dependent version: if f : ⊲(Π(x : A).B), then f ⊛ t : ⊲ [x t] .B. The idea is that t will eventually reduce to a term of the form next u, and then ⊲ [x t] .B will be equal to ⊲B[u/x]. But if t is open, we may not be able to do this reduction yet.
More generally, we define the notion of delayed substitution as follows. Suppose Γ, Γ ′ ⊢ is a wellformed context, and suppose Γ ′ is on the form Γ ′ = x 1 : A 1 . . . x n : A n with all A i independent, i.e., no x j appears in an A i . A delayed substitution ξ : Γ Γ ′ is a vector of terms ξ = [x 1 t 1 , . . . , x n t n ] such that Γ ⊢ t i : A i for each i. [Biz+16] gives a more general definition of delayed substitution allowing dependencies between the A i 's, but for this paper we just need the definition above.
In Figure 6 we recall some rules from [Biz+16] needed below. Of these, (26) and (27) can be considered β and η laws, and (28) is a weakening principle. Rules (26), (28) and (29) also have obvious versions for types, e.g., Rather than be taken as primitive, later application ⊛ can be defined using delayed substitutions as Note that if g : ⊲(A → B) and y : ⊲A, the type of g ⊛ y is ⊲[f g, x y].B which reduces to ⊲B since f and x do not appear in B. With this definition, the rule next(f (t)) ≡ next f ⊛ next t from Section 2 generalises to which follows from (26). In fact, later application generalises to the setting of delayed substitutions: if g : ⊲ξ.Πx : A.B and y : ⊲ξ.A define Note that in the special case where y = next ξ.u we get

A logical relation between syntax and semantics
Our strategy to prove computational adequacy is by logical relation argument. We construct a logical relation R as in Figure 7 between syntax and semantics. This is done using first guarded recursion and then induction on the FPC types. Figure 7 uses an operation lifting relations R from A to B to relations ⊲R from ⊲A to ⊲B defined as As a consequence of (33) the following statement holds: The lifting on relations is used, e.g., in the second case of R 1 where x is assumed to have type ⊲L1. In that case θ 1 (x) is a semantic computation that takes a step, and so should only be related to M , if M can also reduce in one step to an M ′′ , that should be later related to x. Note that x is not necessarily of the form next(y) for some y, but we can still related x to next(M ′′ ) using delayed substitutions as in the definition of ⊲R 1 . Most of the definition of the logical relation is standard, e.g., in the case of function types, where related functions are required to map related input to related output. The case of recursive type deserves some attention. On the right hand side, we have x of type µα.τ , which means it is a piece of data which later will be unfolded and therefore available. More precisely, it has also type ⊲ τ [µα.τ /α] . This semantic program is related to a syntactic program M if and only if the unfolding of M reduces in one computational step to an M ′′ which is later related to x.
The logical relation is an example of a guarded recursive definition. To see this, note first that the lifting operation can be expressed on codes mapping R : A → B → U to λx : ⊲A, y : ⊲B. ⊲(next [x ′ x, y ′ y] .(x ′ R y ′ )) and this operation factors as F • next, for F : Using this, one can formally define the logical relation as a fixed point of a function of type similarly to the formal definition of θ in the equation (24).

Proof of computational adequacy
Before proving computational adequacy we need to show some key properties about the logical relation R. The first of these is that the relation respects the applicative structure of the ⊲ operator which is that we can apply an argument that will be available later to a function that will also be available later.
Lemma 5.1. If f ⊲R τ →σ next(M ) and r ⊲R τ next(L) then Proof. By definition f ⊲R τ →σ next(M ) is type equal to which by definition is By applying the latter to r and next L using the generalised later application of (36) we get an element of By further applying this to the hypothesis r ⊲R τ next( which is equivalent to (f ⊛ r) ⊲R σ next(M L), thus concluding the case.
Next we show that the relation is agnostic to 0-step reduction in the operational semantics.
Proof. We prove first the left to right implication by induction on σ, and show just a few cases.
In the case of coproducts, we proceed by case analysis on x. In the case of x = η(inl(y)), by the assumption we have that M → 0 * inl (N ′ ) and y R τ1 N ′ . If M = inl (N ′ ), then by N must be of the form inl (N ′′ ) for some N ′′ , such that N ′ → 0 N ′′ . In this case, by induction hypothesis y R τ1 N ′′ and so x R τ1+τ2 N . If the reduction M → 0 * inl (N ′ ) has positive length, by determinancy of the operational semantics (Lemma 3.1) we get N → 0 * inl N ′ , and thus x R τ1+τ2 N . The case where x = η(inl(y)) is similar. When x = θ τ1+τ2 (y), by the assumption x R τ1+τ2 M there exist M ′ and M ′′ such that M → 0 * M ′ and M ′ → 1 M ′′ and y ⊲R 1 next(M ′′ ). Again by determinancy of the operational semantics, N → 0 * M ′ and thus we conclude x R τ1+τ2 N . Now we consider the case for recursive types. By assumption we know there exists M ′ and M ′′ such that unfold M → 0 * M ′ and M ′ → 1 M ′′ and x ⊲R τ [µα.τ /α] next(M ′′ ). Since M → 0 N then also unfold M → 0 unfold N . Therefore, from the assumption and the fact that the operational semantics is deterministic (Lemma 3.1) we get unfold N → 0 * M ′ . By definition of the logical relation we get x R µα.τ N , which concludes the proof.
The proof of the right to left implication is also by induction on the structure of σ. Again we just show a few cases.
In the case of the unit type, we proceed by case analysis on x. When x = η( * ) we have that N → 0 * . Since M → 0 N we get M → 0 * as required. When x is θ 1 (x ′ ) by assumption x R 1 N implies that there exists N ′ and N ′′ such that N → 0 * N ′ and N ′ → 1 N ′′ and x ′ ⊲R 1 next(N ′′ ). Since also M → 0 * N ′ this implies x R 1 M . In the case of recursive types, by assumption we have that x R µα.τ N and M → 0 N . From the former we derive that there exists M ′ and M ′′ such that unfold N → 0 * M ′ ,M ′ → 1 M ′′ and x R τ [µα.τ /α] next(M ′′ ). Since M → 0 N then also unfold M → 0 unfold N . Therefore, we know that unfold M → 0 * M ′ , thus by definition of the logical relation we conclude. Now we show a key property of the logical relation. This states that for programs that are related later after a 1-step operational reduction are related now. Note that in the interpretation of the unit type we used the lifting monad. This was not strictly necessary to get a "tick" algebra structure, but it is crucial to make the following lemma to work.
Proof. The proof is by guarded recursion, so we assume that the lemma is "later true", i.e., that we have an inhabitant of the type obtained by applying ⊲ to the statement of the lemma. We proceed by induction on τ .
The cases for the unit type and for the coproduct are straightforward by definition. In the case for products, by assumption we have y ⊲R τ1×τ2 next(M ) .
Lemma 5.4 (Fundamental Lemma). Suppose Γ ⊢ M : τ , for Γ ≡ x 1 : τ 1 , · · · , x n : τ n and ⊢ N i : Proof. The proof is by guarded recursion, and so we assume ⊲ applied to the statement of the lemma. This implies that for all well-typed terms M with context Γ and type τ the following holds: and then applying this to L ( γ) R τ1+τ2 L[ M / x]. We prove (40) by guarded recursion thus assuming the statement is true later. Assume y of type τ 1 + τ 2 , L a term, and y R τ1+τ2 L. We proceed by case analysis on y which is of type τ 1 + τ 2 which by definition is L( τ 1 + τ 2 ). In the case y = η(inl(z)), where z is of type τ 1 we know by assumption that there exists L ′ s.t. L ⇒ 0 inl (L ′ ) and z R τ1 L ′ . Since which is true by induction hypothesis. The case y = η(inl(z)) where z is of type τ 2 is similar.
Now consider the case of y = θ τ1+τ2 (z), where z is of type ⊲ τ 1 + τ 2 . By induction hypothesis we know that θ τ1+τ2 (z) R τ1+τ2 L, thus there exist L ′ and L ′′ of type Term FPC such that L → 0 * L ′ , L ′ → 1 L ′′ and z ⊲R τ1+τ2 next(L ′′ ). Recall that we have assumed ⊲ of (40), i.e., Since L ′ → 1 L ′′ we can apply Lemma 5.3 and obtain And finally by simplifying the left-hand side using Lemma 4.6: as we wanted.
From the Fundamental lemma we can now prove computational adequacy.
Proof. The left to right implication is soundness (Proposition 4.8). For the right to left implication note first that the Fundamental Lemma (Lemma 5.4) implies δ k (η( * )) R 1 M . To complete the proof it suffices to show that δ k 1 (η( * )) R 1 M implies M ⇒ k . This is proved by guarded recursion and induction on k: the case of k = 0 is immediate by definition of R 1 . If k = k ′ + 1 first assume δ k 1 (η( * )) R 1 M . By definition of R there exist M ′ and M ′′ such that M → 0 * M ′ , M ′ → 1 M ′′ and next(δ k ′ 1 (η( * ))) ⊲R 1 next(M ′′ ) which is type equal to ⊲(δ k ′ 1 (η( * )) R 1 M ′′ ). By the guarded recursion assumption we get ⊲(M ′′ ⇒ k ′ ) which by definition implies M ⇒ k . From Theorem 5.5 one can deduce that whenever two terms have equal denotations they are contextually equivalent in a very intensional way, as we now describe. By a context, we mean a term C[−] with a hole, and we say that C[−] has type Γ, τ → (−, 1) if C[M ] is a closed term of type 1, whenever Γ ⊢ M : τ . As stated above, this is a very intensional result in the sense that whenever two FPCdenotable programs are equal we can derive that, under any context, they reduce to the same value with the same number of computational steps. This means that our model distinguishes programs whose input-output behaviour is the same, but the way in which the result is computed is computationally different. More specifically, two different algorithms implementing the same specification, but with a different computational complexity, will be considered different in the model. We explain how to recover this extensionality via a logical relation in the next section.

Extensional Computational Adequacy
Our model of FPC is intensional in the sense that it distinguishes between computations computing the same value in a different number of steps. In this section we define a logical relation which relates elements of the model if they differ only by a finite number of computation steps. In particular, this also means relating ⊥ to ⊥.
Such a relation must be defined on the types of the form ∀κ. σ rather than directly on the types σ . To see why, consider the case of σ = 1, in which case σ = L1. Recall from Section 2.1 that in the topos of trees model L1 is interpreted as the family of sets L1(n) = {⊥, 0, 1, . . . , n − 1} which describes computations terminating in at most n − 1 steps or using at least n steps (corresponding to ⊥). It cannot distinguish between termination in more than n − 1 steps and real divergence. Our relation should relate a terminating value x in L1(n) to any other terminating value, but not real divergence, which is impossible, if divergence cannot be distinguished from slow termination. Another, more semantic, way to phrase the problem is that termination as described by the subsets {0, 1, . . . , n − 1} of L1(n) for each n does not form a subobject of L1.
On the other hand, if L1 ∼ = 1 + ⊲ κ 1 then, as we saw in section the type is a coinductive solution to the type equation Semantically L gl 1 is modelled as the set N+{⊥}, and termination is the subset of this corresponding to the left inclusion of N. So on the global level we can, at least semantically, distinguish between termination and non-termination. This is reflected syntactically in Lemma 6.19.
We refer to ∀κ. 1 ≡ L gl 1 as the global interpretation of the type 1 because it captures the global behaviour (computable in any number of steps) of terms of type 1. We now extend this to the global interpretation of all types and terms and give the definition of the logical relation.

Global interpretation of types and terms
Recall that the developments above should be read as taking place in a context of an implicit clock κ. To be consistent with the notation of the previous sections, κ will remain implicit in the denotations of types and terms, although one might choose to write e.g. σ κ to make the clock explicit.
We define global interpretations of types and terms as follows: Note that σ gl is a wellformed type, because σ is a wellformed type in context σ : Type FPC and Type FPC is an inductive type formed without reference to clocks or guarded recursion, thus κ does not appear in Type FPC . By a similar argument M gl is welltyped.
Define for all σ the delay operator δ gl σ : σ gl → σ gl as follows Similarly for LA, δ gl ). With these definitions we can lift the adequacy theorem to the global points. To prove the denotational model is computationally adequate w.r.t. the standard big-step operational semantics ⇓ n we take the global view points of the the denotational semantics in order to be able to remove the occurrences of the ⊲ operator.
We have now a semantics that implies the standard operational semantics. However, we are still not able to prove that if two programs are equal they are going to be contextually equivalent w.r.t. the input-output behaviour. To achieve so, we need to lift the explicit step-indexing as well.

A weak bisimulation relation for the lifting monad
Before defining the logical relation on the interpretation of types, we define a relational version of the guarded recursive lifting monad L. If applied to the identity relation on a type A in which κ does not appear, we obtain a weak bisimulation relation similar to the one defined by Capretta [Cap05] for the coinductive partiality monad.
Intuitively, LR relates two elements if they either both diverge, or both both converge to elements related in R. For example, ⊥ as defined in Section 4 is always related to itself which can be shown by guarded recursion as follows. Suppose ⊲(⊥ LR ⊥). Since ⊥ = θ(next(⊥)), to prove ⊥ LR ⊥, we must prove next(⊥) ⊲LR next(⊥). But, this type is equal to the assumption ⊲(⊥ LR ⊥) by (39).
By the intuition given for LR below, it should be possible to add or remove ticks on either side without breaking relatedness in LR. The next lemma shows half of this. Lemma 6.3. If R : A × B → U, and x LR y then x LR δ LB (y) and δ LA (x) LR y.
Proof. Assume x LR y. We show x LR δ LB (y). The proof is by guarded recursion, hence we first assume: We proceed by case analysis on x and y. If x = η(x ′ ), then, since x LR y, there exist n and y ′ such that y = δ n LB (η(y ′ )) and x ′ R y ′ . So then δ LB (y) = δ n+1 LB (η(y ′ )), from which it follows that x LR δ LB (y).
For the case where x = θ LA (x ′ ) and y = η(v), it suffices to show that δ n LA (η(w)) LR η(v) implies δ n LA (η(w)) LR δ LB (η(v)). The case of n = 0 was proved above. For n = m + 1 we know that if δ n LA (η(w)) LR η(v) also δ m LA (η(w)) LR η(v) holds by definition, and this implies But this type can be rewritten as follows proving the case. Finally, the case when x = θ LA (x ′ ) and y = θ LB (y ′ ). The assumption in this case is x ′ ⊲LR y ′ , which means by (38), By the guarded recursion hypothesis (42) we get which can be rewritten to By (37) there is an inhabitant of the type and thus (43) implies ⊲ [x ′′ x ′ ] .x ′′ LR θ LB (y ′ ), which, by (39) and since y = θ LB (y ′ ) equals x ′ ⊲LR next(y). By definition, this is We can lift this result to L gl as follows. Suppose R : A × B → U and κ not in A or B. Define L gl R : L gl A × L gl B → U as Lemma 6.4. Let x : L gl A and y : L gl B. If x L gl R y then x L gl R δ gl (y) and δ gl (x) L gl R y.
Proof. Follows directly from Lemma 6.3.
One might expect that δ LA (x) LR δ LB (y) implies x LR y. This is not true, it only implies ⊲(x LR y). In the case of L gl , however, we can use force to remove the ⊲. Proof. Assume δ gl LA (x) L gl R δ gl LB (y). We can rewrite this type by unfolding definitions Using force this implies ∀κ.(x[κ] LR (y[κ])) which is equal to x L gl R y.
Lemma 6.6. For all x of type L gl A and y of type L gl B, if δ gl LA (x) L gl R y then x L gl R y.
Proof. Assume δ gl LA (x) L gl R y. Then by applying Lemma 6.4 we get δ gl LA (x) L gl R δ gl LB (y) and by applying Lemma 6.5 we get x L gl R y.
With this machinery in place we can now define a relation on the semantics that relates programs that produce the same value (or both diverge) and that discards the information about the number of delays used.

Relating terms up to extensional equivalence
The logical relation can be generalised to open terms and the global interpretation of terms as in the next two definitions.
Definition 6.8. For Γ ≡ x 1 : σ 1 , · · · , x n : σ n and for f , g of type Γ → τ define Perhaps surprisingly, this relation is not reflexive. For example the function f : L1 → L1 defined by f (η( * )) = η( * ) and f (θ L1 (x)) = ⊥ does not satisfy f ≈ 1→1 f . On the other hand, the denotation of any term is always related to itself, as the following proposition states.
The rest of this section is devoted to the proof of Proposition 6.9 which is important for the proof of the extensional computational adequacy theorem. To prove the proposition we first establish some basic properties of the logical relation. The first lemma states that delayed application ⊛ respects the logical relation.
Lemma 6.10. For all f, g of type ⊲ τ → σ and x, y of type ⊲ τ , if f ⊲ ≈ τ →σ g and Proof. Assume f ⊲ ≈ τ →σ g and x ⊲ ≈ τ y. By Definition 38 By applying this to x, y and x ⊲ ≈ τ y using the dependent version of ⊛ defined in (36) we get By (39) this is equal to which by rule (34) is equal to Next we show that θ respects the logical relation.
Lemma 6.11. Let x, y of type ⊲ σ , if (x ⊲ ≈ σ y) then θ σ (x) ≈ σ θ σ (y) Proof. We prove the statement by guarded recursion. Thus, we assume the statement holds "later" and we proceed by induction on σ. All the cases for the types that are interpreted using the lifting -namely the unit type and the sum type -in Definition 6.2 hold by definition of the lifting relation.
The case of the product is straightforward. For the case of recursive types, assume φ ⊲ ≈ µα.τ ψ. This is type equal to By definition this is equal to By the guarded recursion hypothesis we get By (39) this is equal to This equals By definition next(θ τ [µα.τ /α] ) ⊛ φ is equal to θ µα.τ (φ) thus we can derive which by definition of ≈ µα.τ is θ µα.τ (φ) ≈ µα.τ θ µα.τ (ψ) Next we generalise Lemma 6.3 to hold for ≈ σ for all σ.
Lemma 6.12. Let σ be a closed FPC type and let x and y of type σ , if x ≈ σ y then δ σ (x) ≈ σ y and x ≈ σ δ σ (y).
Proof. The proof is by guarded recursion and then by induction on the type σ. Thus, assume this lemma holds "later", and proceed by induction on σ. The cases of the unit type and coproduct follow from Lemma 6.3 and the case of products follows by induction from the fact that δ τi (π i (x)) = π i (δ τ1×τ2 (x)), for i = 1, 2. The case of function types follows from the fact that δ σ→τ (f )(x) = δ τ (f (x)).
For the case of recursive types assume x ≈ µα.τ y. Note that Lemma 6.13. Let σ be a closed FPC type and let x, y of type σ gl . If x ≈ gl σ y then x ≈ gl σ δ gl σ (y) and δ gl σ (x) ≈ gl σ y Proof. Direct from Lemma 6.12.
Proof of Proposition 6.9 The proof is by induction on M and we just show the interesting cases. In all cases we will assume Γ ≡ x 1 : σ 1 .., x n : σ n and that we are given x and y such that x ≈ σ y.
For case expressions, to prove that it suffices to prove that Thus that for all x, y s.t. x ≈ τ1+τ2 y λx.case x of x 1 .M ; holds. We prove (44) by guarded recursion. Thus, we assume the statement holds "later" and we proceed by case analysis on x and y. When x is η(x ′ ) and y is η(y ′ ) either x ′ and y ′ are both in the left component or they are both in the right component of the sum. The former case x ′ = inl(x ′′ ) and y ′ = inl(y ′′ ) reduces to which follows from the induction hypothesis, and the latter case is similar. Now consider the case of x = θ τ1+τ2 (x ′ ) and y = η(v). Since by assumption x ≈ τ1+τ2 y there exists n and w such that x = δ n τ1+τ2 (η(w)) and w ≈ τ1+τ2 v. As before, v and w must be in the same component of the coproduct, so assume w = inl(w ′ ) and v = inl(v ′ ) such that w ′ ≈ τ1 v ′ . By induction hypothesis we know that M ( x) ≈ τ1→τ M ( y) and thus that M ( x)(w ′ ) ≈ τ M ( y)(v ′ ). By Lemma 6.12 this implies δ n τ ( M ( x)(w ′ )) ≈ τ M ( y)(v ′ ). Since by Lemma 4.6 we get τ1+τ2 (η(w))) and thus we conclude The last case is when x is θ τ1+τ2 (x ′ ) and y is θ τ1+τ2 (y ′ ). By guarded recursion we know that Since the assumption θ τ1+τ2 (x ′ ) ≈ τ1+τ2 θ τ1+τ2 (y ′ ), means that x ′ ⊲ ≈ τ1+τ2 y ′ , by Lemma 6.10 this implies By Lemma 4.6 we conclude that λx.case x of x 1 .M ; x 2 .N ( x)(θ τ1+τ2 (x ′ )) ≈ τ λx.case x of x 1 .M ; x 2 .N )( y)(θ τ1+τ2 (y ′ )) proving the case.
Finally we prove the two cases for the recursive types. We first consider the case for unfold M of type τ [µα.τ /α]. We have to show that By induction hypothesis we know that M ( x) ≈ µα.τ M ( y) which by definition of ≈ µα.τ is M ( x) ⊲ ≈ τ [µα.τ /α] M ( y). By Lemma 6.11 we get and by definition of the interpretation function this is what we wanted. Now the case for fold M of type µα.τ . By induction hypothesis we know that By definition of ≈ µα.τ this is precisely next( M ( x)) ≈ µα.τ next( M ( y)) which by definition of the interpretation function is fold M ( x) ≈ µα.τ fold M ( y)

Extensional computational adequacy
Contextual equivalence of FPC is defined in the standard way by observing convergence at unit type. We first define the language of contexts. These are FPC programs with a hole [−] defined inductively as in the next definition.
Intuitively, a context is a term that takes a term and returns a new term. We define the "fill hole" function ·[·] : Ctx ×OTerm FPC → OTerm FPC by induction on the context in the standard way. Note that this may capture free variables in the term being substituted.
We say that a context C has type (Γ, σ) → (∆, τ ) if ∆ ⊢ C[M ] : τ whenever Γ ⊢ M : σ. This can be captured by a typing relation on contexts as defined in Figure 9. Next we define contextual equivalence using the big-step semantics ⇓. This states that two program are contextually equivalent if no context can distinguish them. Using ⇓ (instead of ⇓ k ) ensures that we capture the standard notion of contextual equivalence, thus that two programs producing the same value will be equivalent no matter how many steps they take to terminate.  To prove this theorem, we need the following lemma stating that contexts preserve the logical relation. Proof. The proof is by induction on C and most cases can be proved either very similarly to corresponding cases of Proposition 6.9, or by direct application of Proposition 6.9. We show how to do the latter in two cases. which is what we wanted. When the context binds a variable one has to be a bit more careful. For example, for a context of the form case L of x 1 .C; x 2 .N ′ of type (Γ, τ ) → (∆, σ) we have by induction that C has type (Γ, τ ) → ((∆, x 1 : τ 1 ), σ) and thus by induction hypothesis we know by applying the context parameters that C[M ] ( x) ≈ τ1,σ C[N ] ( y). From this we also know that By Proposition 6.9 we know that λx.case L of x 1 .x(x 1 ); x 2 .N ′ ( x) ≈ (τ1→σ)→σ λx.case L of x 1 .x(x 1 ); x 2 .N ′ ( y).
By applying this to (45) we conclude.
As a direct consequence we get the following lemma. The next lemma states that if two computations of unit type are related then the first converges iff the second converges. Note that this lemma needs to be stated using the fact that the two computations are globally related.

Executing the denotational semantics
In this final section we sketch an additional benefit of the denotational semantics described in this paper: The denotational semantics can be executed. More precisely, given a closed FPC term of base type and a number n, the denotational semantics can be executed up to n steps. This will terminate if and only if the big-step operational semantics terminates in n steps or less. The time-out n is necessary since FPC programs can diverge and programs in type theory must terminate. We emphasize that at the moment there is no full implementation of GDTT and so the practical implications of this section are speculative.
Using runstep we can define a function exec : N → (∀κ.L(L1 + L1)) → (1 + 1) + (∀κ.L(L1 + L1)) such that exec n iterates runstep until it gets a result, or for at most n+1 times. Precisely, we define exec 0 x = runstep x and exec (n + 1) x = runstep x if runstep x is in the left component and exec (n + 1) x = exec n y if runstep x = inr(y). We now show that executing the denotational semantics using exec n corresponds to executing the operational semantics for up to n steps.
Proposition 7.1. Let M be a closed term of FPC of type 1 + 1, and let n be a natural number. Then exec n M gl = inl(inl(⋆)) iff there exists an N such that M ⇓ k inl (N ) for some k ≤ n.
To prove Proposition 7.1 we need following two lemmas.

Conclusions and Future Work
We have shown that programming languages with recursive types can be given sound and computationally adequate denotational semantics in guarded dependent type theory. The semantics is intensional, in the sense that it can distinguish between computations computing the same result in different number of steps, but we have shown how to capture extensional equivalence in the model by constructing a logical relation on the interpretation of types. This work can be seen as a first step towards a formalisation of domain theory in type theory. Other, more direct formalisations have been carried out in Coq, e.g. [BKV09; Ben+10; Doc14] but we believe that the synthetic viewpoint offers a more abstract and simpler presentation of the theory. Moreover, we hope that the success of guarded recursion for operational reasoning, mentioned in the introduction, can be carried over to denotational models of more advanced programming language features as, for example, to general references, for which, at the present day, no denotational model exists.
Future work also includes implementation of GDTT in a proof assistant, allowing for the theory of this paper to be machine verified. Currently, initial experiments are being carried out in this direction [Bir+16].
Finally, we have not yet investigate the possible applications of the weak bisimulation introduced in Section 6.