Lambda Definability with Sums via Grothendieck Logical Relations

Marcelo Fiore^{1} and Alex Simpson^{2}

1 COGS, University of Sussex

                        <marcelo@cogs.susx.ac.uk>

2 LFCS, Division of Informatics, University of Edinburgh

                       <Alex.Simpson@dcs.ed.ac.uk>

Abstract. We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary.

Introduction

The use of logical relations as a tool for characterising the λ-definable elements in a model of the simply-typed λ-calculus originated in the work of Plotkin [10], who obtained such a characterisation of the definable elements in the full type hierarchy using a notion of Kripke logical relation. Subsequently, the more general notion of a Kripke logical relation of varying arity was developed by Jung and Tiuryn, and shown to characterise the definable elements in any Henkin model [4]. Although not emphasised in [4], relations of varying arity are powerful enough to characterise relative definability with respect to any given set of elements considered as constants. The full generality of the approach is demonstrated in Alimohamed [1], where such relations are used to characterise relative definability in an arbitrary cartesian closed category.

In general, results about the pure simply-typed λ-calculus extend easily to analogous results for systems containing finite product types. This is not the case for finite coproduct (sum) types. Although the equational theory of bicartesian closed categories provides a basic formal system, the syntactic techniques used to study systems without coproducts fall over in their presence. Two fundamental properties of this equational theory, decidability (Ghani [3]) and its completeness relative to the equalities valid in the category, Set, of sets (Dougherty and Subrahmanyam [2]), were established only recently. It is apparently still an open question whether the finite model property holds for this theory (although it is inconceivable that it does not). Also, both the above results have been proved only for nonempty sums (i.e. with the empty type omitted).

In this paper, we extend the logical relations characterization of relative definability to the simply-typed λ-calculus with products and sums (including the empty type). As might be expected, this requires some development of the theory of logical relations. It turns out that what is needed is a natural generalization of Kripke logical relations of varying arity, in which the base poset (or, more generally, category) for the relation is endowed with a Grothendieck topology [6]. Using such Grothendieck logical relations, we characterise relative definability in any bicartesian closed category in which the finite coproducts are stable (as is the case in Set). We do not know if the characterisation extends also to the non stable case.

From the categorical point of view our results are best explained in terms of glueing [12, 1]. However, for this conference version of the paper, we keep our exposition elementary, in the hope that it will be accessible to most type theorists with some background in categorical semantics.

It should be said that the research in this paper originated as part of a strategy conceived by the authors for attacking the full abstraction problem for call-by-value FPC (which includes finite sums). Kripke logical relations of varying arity had already been used to obtain full abstraction for PCF by O’Hearn and Riecke [8]. The extension of these results to FPC seemed to us to require an additional analysis of both partiality and sums. This line of research was never fully pursued because similar full abstraction results for FPC were soon obtained by Riecke and Sandholm [11]. However, their treatment of coproducts is somewhat ad hoc (although one does get the feeling that a Grothendieck topology is at work behind the scenes). We believe that it would be very worthwhile to integrate our more conceptual approach to coproducts into the full abstraction picture.

It seems likely that the notion of Grothendieck logical relation will have other applications. For example, the lengthy and heavily syntactic proof of equational completeness relative to Set in [2], has hints of Grothendieck toplologies within it. It is plausible that Grothendieck logical relations will lead to simpler and more general such completeness proofs.

1 Simply typed lambda calculus with sums

The language we work with is a simply-typed λ-calculus with additional types for finite products and sums. In this section we describe the syntax of the language, and its interpretation in any bicartesian closed category.

Syntax. We use T, … to range over a set T of base types, and τ, … to range over types which are specified by the grammar below.

τ ::= T | τ_{1} [figure] τ_{2} | ×^{(n)}(τ_{1}, …, τ_{n}) | +^{(n)}(τ_{1}, …, τ_{n})  n ∈ ℕ

We write 1 and 0 for ×^{(0)}() and +^{(0)}() respectively. We use n-ary products and sums as primitive to emphasize that all our definitions for the zero-ary cases are just the natural instances of the general n-ary scheme. This is of particular interest in the case of the empty type 0, which is generally thought of as troublesome, and often omitted from consideration altogether [3, 2].

We use x, … to range over a countably infinite set of variables. A (type) environment is a finite sequence x_{1} : τ_{1}, …, x_{n} : τ_{n} where all the variables are distinct. We use Γ, … to range over environments. We write ⟨⟩ for the empty sequence in general, and the empty environment in particular.

Terms are specified according to a T -signature, Σ, which is a set of pairs of the form (c : τ) assigning types τ to constants c, such that each constant symbol in Σ is assigned only one type. The terms are generated by the rules in Fig. 1. For notational convenience, we will always omit the superscripts from the injections in_{i}^{τ_{1},...,τ_{n}}(t). As usual we consider terms as identified up to α-equivalence.

For the remainder of the paper we consider a fixed (though arbitrary) set of base types T and signature Σ.

Semantics. For the purpose of this paper, a bicartesian closed category is a category with finite coproducts, finite products and exponentials (we do not assume finite limits). Let S be bicartesian closed with chosen structure (0, +, 1, ×, [figure] ) (here we are distinguishing initial object, binary coproduct, terminal object, binary product and exponential). We define canonical finite coproducts by

∐^{(0)} =^{def} 0 and ∐^{(n+1)}(A_{1}, …, A_{n}, A_{n+1}) =^{def} ∐^{(n)}(A_{1}, …, A_{n}) + A_{n+1}. Canoni-

cal finite products ∏^{(n)}(A_{1}, …, A_{n}) are defined similarly. We use standard notation for injections, projections, the universal maps, and the “evaluation” map and “Currying” operation associated with the closed structure.

A T -interpretation in S is a function from T to objects of S. Under a T - interpretation I every type τ is interpreted as an object [[τ]]_{I} in the obvious way. The interpretation of types extends to environments by the usual definition:

[[x_{1} : τ_{1}, …, x_{n} : τ_{n}]]_{I} =^{def} ∏^{(n)}([[τ_{1}]]_{I}, …, [[τ_{n}]]_{I})

A (T , Σ)-interpretation I in S is a pair (I_{T} , I_{Σ}) where I_{T} is a T -interpretation, and I_{Σ} is a function mapping each constant (c : τ) ∈ Σ to a global element I_{Σ}(c) : 1 [figure] [[τ]] in S. Under a (T , Σ)-interpretation every term Γ ⊢ t : τ is interpreted as a generalised element [[Γ ⊢ t : τ]]_{I} : [[Γ]] [figure] [[τ]] in S by:

[[x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢ x_{i} : τ_{i}]] =^{def} π_{i}

[[Γ ⊢ c : τ]] =^{def} I_{Σ}(c) ∘ ⟨⟩

[[Γ ⊢ λx. : τ_{1}.t : τ_{1} [figure] τ_{2}]] =^{def} λ[[Γ, x : τ_{1} ⊢ t : τ_{2}]]

[[Γ ⊢ t(t_{1}) : τ_{2}]] =^{def} ev ∘ ⟨[[Γ ⊢ t : τ_{1} [figure] τ_{2}]], [[Γ ⊢ t_{1} : τ_{1}]]⟩

[[Γ ⊢ ⟨t_{1}, …, t_{n}⟩ : ×^{(n)}(τ_{1}, …, τ_{n})]] =^{def} ⟨[[Γ ⊢ t_{1} : τ_{1}]], …, [[Γ ⊢ t_{n} : τ_{n}]]⟩

[[Γ ⊢ proj_{i}(t) : τ_{i}]] =^{def} π_{i} ∘ [[Γ ⊢ t : ×^{(n)}(τ_{1}, …, τ_{n})]]

[[Γ ⊢ in_{i}(t) : +^{(n)}(τ_{1}, …, τ_{n})]] =^{def} ⨿_{i} ∘ [[Γ ⊢ t : τ_{i}]]

[[Γ ⊢ case t of [in_{1}(x_{1}).t_{1}, …, in_{n}(x_{n}).t_{n}] : τ]] =^{def}

[[[Γ, x_{1} : τ_{1} ⊢ t_{1} : τ]], …, [[Γ, x_{n} : τ_{n} ⊢ t_{n} : τ]]] ∘

δ^{(n)} ∘ ⟨id_{[[Γ]]}, [[Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n})]]⟩

where δ^{(n)} : C × (∐^{(n)}(A_{1}, …, A_{n})) [figure] ∐^{(n)}(C × A_{1}, …, C × A_{n})) is the distributivity isomorphism.

\overline{x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢ x_{i} : τ_{i}} 1 ≤ i ≤ n  \overline{Γ ⊢ c : τ} (c : τ) ∈ Σ

\frac{Γ, x : τ_{1} ⊢ t : τ_{2}}{Γ ⊢ λx : τ_{1}. t : τ_{1} [figure] τ_{2}}  \frac{Γ ⊢ t : τ_{1} [figure] τ_{2} Γ ⊢ t_{1} : τ_{1}}{Γ ⊢ t(t_{1}) : τ_{2}}

\frac{Γ ⊢ t_{1} : τ_{1} … Γ ⊢ t_{n} : τ_{n}}{Γ ⊢ ⟨t_{1}, …, t_{n}⟩ : ×^{(n)}(τ_{1}, …, τ_{n})} \frac{Γ ⊢ t : ×^{(n)}(τ_{1}, …, τ_{n})}{Γ ⊢ proj_{i}(t) : τ_{i}} 1 ≤ i ≤ n

\frac{Γ ⊢ t : τ_{i}}{Γ ⊢ in_{i}^{τ_{1},...,τ_{n}}(t) : +^{(n)}(τ_{1}, …, τ_{n})} 1 ≤ i ≤ n

\frac{Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n}) Γ, x_{i} : τ_{i} ⊢ t_{i} : τ 1 ≤ i ≤ n}{Γ ⊢ case t of [in_{1}(x_{1}).t_{1}, …, in_{n}(x_{n}).t_{n}] : τ}

Fig. 1. Term syntax

\overline{Γ | Ξ ⊢ t = t : τ}  \frac{Γ | Ξ ⊢ t = t′ : τ}{Γ | Ξ ⊢ t′ = t : τ}

\frac{Γ | Ξ ⊢ t_{1} = t_{2} : τ Γ | Ξ ⊢ t_{2} = t_{3} : τ}{Γ | Ξ ⊢ t_{1} = t_{3} : τ}

\overline{x_{1} : τ_{1}, …, x_{n} : τ_{n} | t_{1} =_{τ′_{1}} t′_{1}, …, t_{n} =_{τ′_{n}} t′_{n} ⊢ t_{i} = t′_{i} : τ′_{i}} 1 ≤ i ≤ n

\frac{Γ | Ξ ⊢ t_{1} = t′_{1} : τ_{1}}{Γ | Ξ ⊢ t(t_{1}) = t(t′_{1}) : τ_{2}}  \frac{Γ, x : τ_{1} | Ξ, x =_{τ_{1}} x ⊢ t = t′ : τ_{2}}{Γ | Ξ ⊢ λx : τ_{1}. t = λx : τ_{1}. t′ : τ_{1} [figure] τ_{2}}

\overline{Γ | Ξ ⊢ (λx : τ_{1}. t)(t′) = t[t′/x] : τ_{2}}  \overline{Γ | Ξ ⊢ t = λx : τ_{1}. t(x) : τ_{1} [figure] τ_{2}} x ∉ FV(t)

\overline{Γ | Ξ ⊢ proj_{i}⟨t_{1}, …, t_{n}⟩ = t_{i} : τ_{i}} 1 ≤ i ≤ n

Γ | Ξ ⊢ t = ⟨proj_{1}(t), …, proj_{n}(t)⟩ : ×^{(n)}(τ_{1}, …, τ_{n})

\overline{Γ | Ξ ⊢ casein_{i}(t) of [in_{1}(x_{1}).t_{1}, …, in_{n}(x_{n}).t_{n}] = t_{i}[t/x_{i}] : τ} 1 ≤ i ≤ n

\frac{Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t ⊢ t_{i} = t′ : τ 1 ≤ i ≤ n}{Γ | Ξ ⊢ case t of [in_{1}(x_{1}).t_{1}, …, in_{n}(x_{n}).t_{n}] = t′ : τ}

Fig. 2. Equational rules

2 Stable coproducts

To obtain our characterisation of definability, we shall be interested in bicartesian closed categories which enjoy the additional property that coproducts are stable.

Definition 1 (Stable coproducts). In an arbitrary category, a coproduct {A_{i} [figure] A}_{i∈I} is said to be stable if, for every arrow X [figure] A and i ∈ I, there is a pullback square

\xymatrix{X_{i} \ar[r] \ar[d] & X \ar[d] \\ A_{i} \ar[r] & A}

and the family {X_{i} [figure] X}_{i∈I} is also a coproduct.

Note that, the stability of the empty coproduct amounts to the strictness of initial objects, which holds in any cartesian closed category [5, Proposition 8.3].

We call a bicartesian closed category stable if it has stable finite coproducts (for which it suffices that binary coproducts are stable). Any elementary topos provides an example of a stable bicartesian closed category, and so does any Heyting algebra (note that the latter example shows that stable coproducts need not be disjoint).

We next present a sound formal system for deriving equalities between terms, which is naturally interpreted in stable bicartesian closed categories. The formal system is essentially equivalent to the system WBCT of [2], which was introduced as a critical tool in their proof of the completeness of the equational theory of bicartesian closed categories relative to the valid equations in Set. The fact that this system has a natural interpretation in any stable bicartesian closed category has not been observed before.

The proof system is based on a notion of constrained (type) environment implementing equational assumptions about terms of sum type.

Definition 2 (Constrained environment). The constrained environments Γ | Ξ, consisting of an environment Γ subject to constraints Ξ, are defined inductively by the following rules.

\overline{⟨⟩ | ⟨⟩}  \frac{Γ | Ξ}{Γ, x : τ | Ξ, x =_{τ} x}  x ∉ Γ

\frac{Γ | Ξ Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n})}{Γ, x : τ_{i} | Ξ, in_{i}(x) =_{+^{(n)}(τ_{1},...,τ_{n})} t} x ∉ Γ, 1 ≤ i ≤ n

The equational rules manipulate judgements of the form Γ | Ξ ⊢ t = t′ : τ where both Γ ⊢ t : τ and Γ ⊢ t′ : τ are terms. The rules are given in Fig. 2. They are to be understood as applying only when all the premises and conclusions are genuine (well-typed) terms as specified above.

Henceforth in this section, let S be a stable bicartesian closed category with chosen structure. (In addition to the chosen bicartesian closed structure, described earlier, we assume a choice of pullbacks for coproduct morphisms. It is not necessary to assume any coherence conditions for these!) Let I be an interpretation in S. We interpret constrained environments Γ | Ξ as monos [[Γ | Ξ]] [figure] [[Γ]]. The definition is by structural induction as follows.

– ([[⟨⟩ | ⟨⟩]] [figure] [[⟨⟩]]) =^{def} id_{1}.

– ([[Γ, x : τ | Ξ, x =_{τ} x]] [figure] [[Γ]] × [[τ]]) =^{def} ([[Γ | Ξ]] [figure] [[Γ]]) × id_{[[τ]]}.

– [[Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) =_{+^{(n)}(τ_{1},...,τ_{n})} t]] [figure] [[Γ]]×[[τ_{i}]] is the pairing ⟨m∘p_{i}, q_{i}⟩ arising from the following pullback square.

[figure: [[Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t]]; p_{i}; q_{i}; [[Γ | Ξ]]; m; [[Γ]]; [[Γ ⊢t:+^{(n)}(τ_{1},...,τ_{n})]]; [[τ_{i}]]; ⨿_{i}; ∐^{(n)}([[τ_{1}]], …, [[τ_{n}]])] (1)

Note that, by stability, the family

{p_{i} : [[Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t]] [figure] [[Γ | Ξ]]}_{1≤i≤n}

from (1) is a coproduct. Observe also that, by definition, for a constrained environment Γ | Ξ of the form x_{1} : τ_{1}, …, x_{n} : τ_{n} | x_{1} =_{τ_{1}} x_{1}, …, x_{n} =_{τ_{n}} x_{n}, we have that ([[Γ | Ξ]] [figure] [[Γ]]) = id_{[[Γ]]}. Thus the interpretation of constrained environments extends that of environments. Furthermore, for any Γ | Ξ of the form (x_{1} : τ_{1}, …, x_{n} : τ_{n} | t_{1} =_{τ′_{1}} t′_{1}, …, t_{n} =_{τ′_{n}} t′_{n}), we have an equaliser diagram

[figure: [[Γ | Ξ]]; [[Γ]]; ⟨[[Γ ⊢t_{i}:τ′_{i}]]⟩_{i=1,n}; ⟨[[Γ ⊢t′_{i}:τ′_{i}]]⟩_{i=1,n}; – ∣∣ –; ∏^{(n)}([[τ′_{1}]], …, [[τ′_{n}]])]  (2)

Proposition 1 (Soundness). If Γ | Ξ ⊢ t = t′ : τ is derivable then

([[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t:τ]]] [[τ]]) = ([[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t′:τ]]] [[τ]]) .

The proof is the usual straightforward induction on the structure of derivations, using the facts observed above.

It would be interesting to obtain a completeness converse to Proposition 1. We do not know if such a result holds, although weaker versions can be obtained by not insisting that all exponentials exist in S. Also, following [2, Theorem 5.3], one can show that the proof system is sound and complete for deriving the equalities between terms in unconstrained environments that are valid in an arbitrary bicartesian closed category. These issues will be discussed further in the full version of this paper.

3 Grothendieck logical relations

For each object A of the semantic category S we define the notion of a (categorical) Kripke relation of varying arity over A. The idea is that the arity of the relation varies over a category 𝕎 (of worlds), as specified by a functor a : 𝕎 [figure] S (that associates arities to worlds). For each object w of 𝕎, the object a(w) is considered as an arity in the natural internal sense that a(w)-tuples of A are given by morphisms x : a(w) [figure] A in S. The action of the arity functor a on morphisms allows such a tuple x of arity a(w) to be reinterpreted along any change of world ψ : v [figure] w in 𝕎 to obtain the a(v)-tuple x ∘ a(ψ). For notational convenience, we write x · ψ for x ∘ a(ψ) when a is clear from the context.

Definition 3 (Kripke relation). Given a small category 𝕎 and a functor a : 𝕎 [figure] S, a 𝕎-Kripke relation R of arity a over an object A of S is a family {R(w) ⊆ S(a(w), A)}_{w∈|𝕎|} satisfying

(Monotonicity) For every ψ : w [figure] v in 𝕎 and every x : a(v) [figure] A in S, if x ∈ R(v) then x · ψ ∈ R(w).

The notion of Kripke relation has a natural formulation in the language of presheaves. Writing 𝕎̂ for the category of presheaves [𝕎^{op}, Set], any arity functor a : 𝕎 [figure] S induces a hom functor a ∗ : S [figure] 𝕎̂ given by (a ∗ A)( ) =^{def} S(a , A) : 𝕎^{op} [figure] Set. A Kripke relation of arity a over A ∈ S is just a subpresheaf R ⊆ a ∗ A in 𝕎̂. So, a Kripke relation of arity a is a unary relation on a ∗ A in the internal logic of the presheaf topos 𝕎̂.

Our generalisation of Kripke relation allows us to impose additional structure on the category of worlds in the form of a Grothendieck topology. A Grothendieck topology is a collection of covers, which are families of morphisms with the same codomain, subject to axioms on the collection. A cover {φ_{i} : w_{i} [figure] w}_{i∈I} of w specifies that information about w can be recovered “locally” by piecing together relevant information about each of the w_{i} along φ_{i}. The formal definition of a Grothendieck topology specifies the properties that the collection of covers must satisfy in order for such local determination to behave properly.

Definition 4 (Basis for a topology). A (basis for a Grothendieck) topology K on a category 𝕎 consists of a family of (basic) covers K(w) ⊆ ⋃_{v∈𝕎} 𝕎(v, w) for each object w in 𝕎, satisfying:

(Identity) The singleton family {id_{w}} ∈ K(w). (Stability) For every family {φ_{i}}_{i∈I} ∈ K(w) and morphism ψ : v [figure] w there

exists a family {γ_{j}}_{j∈J} ∈ K(v) such that, for each γ_{j} ∈ K(v), there exists φ_{i} ∈ K(w) such that ψ ∘ γ_{j} factors through φ_{i}.

(Transitivity) If {φ_{i} : w_{i} [figure] w}_{i∈I} ∈ K(w) and {γ_{ij}}_{j∈J_{i}} ∈ K(w_{i}) for every i ∈ I then the family {φ_{i} ∘ γ_{ij}}_{i∈I, j∈J_{i}} ∈ K(w).

A small category together with a Grothendieck topology is called a site.

Example 1. In any category the trivial topology, I, consists only of the singleton families {id}.

Example 2. In a category with stable finite coproducts, the finite coproduct topology is given by

{{φ_{i} : w_{i} [figure] w}_{1≤i≤n} | n ≥ 0 and {φ_{i} : w_{i} [figure] w}_{1≤i≤n} is a coproduct}.

The stability of coproducts ensures that the stability axiom for a Grothendieck topology is satisfied. Note that the empty family covers an object if and only if the object is (necessarily strict) initial.

In order to generalise the notion of Kripke relation to take into account a Grothendieck topology, we add an extra condition establishing that the relation is determined locally in the sense discussed above.

Definition 5 (Grothendieck relation). Given a site (𝕎, K) and a functor a : 𝕎 [figure] S, a (𝕎, K)-Grothendieck relation of arity a over A ∈ S is a 𝕎-Kripke relation {R(w) ⊆ S(a(w), A)}_{w∈|𝕎|} that further satisfies:

(Local character) For every cover {φ_{i} : w_{i} [figure] w}_{i∈I} ∈ K(w) and for all maps x : a(w) [figure] A in S, if x · φ_{i} ∈ R(w_{i}) for all i ∈ I then x ∈ R(w).

In the case of the trivial topology, the local character property is vacuous and so any Kripke relation is a Grothendieck relation.

It is instructive to reformulate the notion of a Grothendieck relation in terms of standard concepts from sheaf theory. For notational convenience, given a presheaf P in 𝕎̂, for any ψ : v [figure] w in 𝕎 and x ∈ P (w) we write x · ψ for the element P (ψ)(x) ∈ P (v). (This generalises our previous notation for presheaves a ∗ A to arbitrary presheaves.)

Definition 6 (Closed subpresheaf). Given a site (𝕎, K) and a presheaf P in 𝕎̂, a subpresheaf R ⊆ P is said to be K-closed if, for every cover {φ_{i} : w_{i} [figure] w}_{i∈I} ∈ K(w) and for all x ∈ P (w) if x · φ_{i} ∈ R(w_{i}) for all i ∈ I then x ∈ R(w).

Hence, a Grothendieck relation R of arity a over A is precisely a K-closed subpresheaf R ⊆ a ∗ A.

There is another, less elementary, characterisation of Grothendieck relations. Writing \underline{Sh}(𝕎, K) for the full subcategory of 𝕎̂ whose objects are sheaves (for K) [6], it is well-known (see [6, III.5 and V.3] for example) that the embedding \underline{Sh}(𝕎, K) [figure] 𝕎̂ has a (left-exact) left adjoint, the associated sheaf functor a : 𝕎̂ [figure] \underline{Sh}(𝕎, K). For every presheaf P, the closed subpresheaves of P are in natural bijective correspondence with the subsheaves of a(P) [6]. Thus, a Grothendieck relation of arity a over A is just a subsheaf of a(a ∗ A) in \underline{Sh}(𝕎, K). In particular, when the presheaf a ∗ A is already a sheaf for K, a Grothendieck relation over A is just a subsheaf of a ∗ A. However, we shall not assume in general that a ∗ A is a sheaf.

We define a category of Grothendieck relations over S whose morphisms are given by those morphisms of S that preserve the relations.

Definition 7. Given a site (𝕎, K) and an arity functor a : 𝕎 [figure] S:

1. \underline{G}(𝕎, K, a) is the category with \underline{objects}: given by pairs (A, R) consisting of an object A ∈ S and a (𝕎, K)- Grothendieck relation R of arity a over A, \underline{arrows} (A, R) [figure] (B, S): given by arrows f : A [figure] B in S such that,

for all x : a(w) [figure] A, x ∈ R(w) implies f ∘ x ∈ S(w) ,  (3)

\underline{identity} and \underline{composition}: as in S.

2. We write U : \underline{G}(𝕎, K, a) [figure] S for the forgetful functor mapping (A, R) to A.

Proposition 2. For S bicartesian closed, the category \underline{G}(𝕎, K, a) is bicartesian closed and the forgetful functor U : \underline{G}(𝕎, K, a) [figure] S is faithful, and preserves and creates the bicartesian closed structure.

Proof. \underline{Finite coproducts}: ∐_{n}(A_{n}, R_{n}) = (∐_{n} A_{n}, ⋁_{n} R_{n}) where (a(w) [figure: x] ∐_{n} A_{n}) ∈ (⋁_{n} R_{n})(w) iff_{def} there exists a cover {φ_{i} : w_{i} [figure] w}_{i∈I} ∈ K(w) such that for all

i ∈ I, there exist n_{i} with 1 ≤ n_{i} ≤ n and (a(w_{i}) [figure: x_{i}] A_{n_{i}}) ∈ R_{n_{i}}(w_{i}) such that x · φ_{i} = ⨿_{n_{i}} ∘ x_{i} : a(w_{i}) [figure] ∐_{n} A_{n}.

\underline{Finite products}: ∏_{n}(A_{n}, R_{n}) = (∏_{n} A_{n}, ⋀_{n} R_{n}) where (a(w) [figure: x] ∏_{n} A_{n}) ∈

(∏_{n} R_{n})(w) iff_{def} for all n, (a(w) [figure: x] ∏_{n} A_{n} [figure: π_{n}] A_{n}) ∈ R_{n}(w).

\underline{Exponentials}: (A, R) [figure] (B, S) = (A [figure] B, S^{R}) where (a(w) [figure: f] (A [figure] B)) ∈

S^{R}(w) iff_{def} for all ψ : v [figure] w and all (a(v) [figure: x] A) ∈ R(v), we have

(a(v) [figure: ⟨f·ψ, x⟩] (A [figure] B) × A [figure: ev] B) ∈ S(v).
⊓ ⊔

Although straightforward, the proposition above is the categorical analogue of the fundamental lemma of logical relations [7], which states that any syntactically definable morphism in S automatically preserves relations. To formulate this result explicitly, we require further definitions.

Definition 8. Given a site (𝕎, K), an arity functor a : 𝕎 [figure] S and a Grothendieck relation R of arity a over A ∈ S, we say that a global element x : 1 [figure] A in S satisfies R if, for all w ∈ | 𝕎 |, it holds that (a(w) [figure] 1 [figure: x] A) ∈ R(w).

Definition 9 (Grothendieck logical relation). Let I be a (T , Σ)-interpretation in a bicartesian closed category S. A Grothendieck logical relation for Σ under I is given by: a site (𝕎, K); an arity functor a : 𝕎 [figure] S; and, a family {R_{T}}_{T∈T} such that:

1. each R_{T} is a Grothendieck relation of arity a over I_{T} (T), and

2. for all (c : τ) ∈ Σ, it holds that I_{Σ}(c) satisfies R_{τ}, where we write R_{τ} (R_{Γ}) for the Grothendieck relation on [[τ]] ([[Γ]]) determined by the bicartesian closed structure on \underline{G}(𝕎, K, a) according to the structure of τ (Γ).

Lemma 1 (Fundamental Lemma of GLRs). Let S be a bicartesian closed category and let I be a (T , Σ)-interpretation in S. For any Grothendieck logical relation ((𝕎, K), a, {R_{T}}_{T∈T} ) for Σ under I, the following two equivalent statements hold.

1. For every term Γ ⊢ t : τ, the interpretation [[Γ ⊢ t : τ]] is an arrow ([[Γ]], R_{Γ}) [figure] ([[τ]], R_{τ}) in \underline{G}(𝕎, K, a).

2. For every term ⊢ t : τ, the global element [[⊢ t : τ]] : 1 [figure] [[τ]] satisfies R_{τ}.

Our motivation for generalising Kripke relations to Grothendieck relation is to obtain the converse: any global element of S that satisfies all Grothendieck logical relations is syntactically definable. At present we have such a result only in the special case that S is stable. This is the content of the theorem below, which is the principal result of the paper.

Theorem 1 (Definability). Suppose S is a stable bicartesian closed category and I is a (T , Σ)-interpretation in S. Then there exists a Grothendieck logical relation ((𝕎, K), a, {R_{T}}_{T∈T} ) for Σ under I, such that every global element of [[τ]] that satisfies R_{τ} is definable by a closed term of type τ.

4 Proof of Definability

In this section we prove Theorem 1. Accordingly, suppose S is a stable bicartesian closed category (with chosen structure) and I is a (T , Σ)-interpretation in S. We construct a Grothendieck logical relation, satisfying the property of Theorem 1, based on a syntactic site (W, K) defined below. The construction has similarities with the syntactic sites used in recent approaches to obtaining intuitionistic completeness results for intuitionistic logic, see e.g. [9].

Definition 10 (Syntactic site).

1. The category W has \underline{objects}: given by constrained environments as in Definition 2,

\underline{arrows} Γ′ | Ξ′ [figure]Γ | Ξ: given by renamings ( =^{def} monotone injections) ρ : dom(Γ) [figure] dom(Γ′), where dom(x_{1} : τ_{1}, …, x_{n} : τ_{n}) =^{def} (x_{1} ≤ ⋯ ≤ x_{n}), that preserve typing:

\xymatrix{x : τ ∈ Γ \ar@{=>}[r] & ρ(x) : τ ∈ Γ′ ,}

and preserve constraints:

\xymatrix{t =_{τ} t′ ∈ Ξ \ar@{=>}[r] & t[ρ] =_{τ} t′[ρ] ∈ Ξ′ ,}

\underline{identities} and \underline{composition}: as for functions.

2. The covers in K are defined inductively by the following rules:

{id_{dom(Γ)}} ∈ K(Γ | Ξ)

\frac{\{ρ_{j}\} ∪ \{ρ : Γ′ | Ξ′ [figure] Γ | Ξ\} ∈ K(Γ | Ξ) Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n})}{\{ρ_{j}\} ∪ \{ρ ∘ ι_{k} : Γ′_{k} | Ξ′_{k} [figure] Γ | Ξ\}_{1≤k≤n} ∈ K(Γ | Ξ)}

where Γ′_{k} | Ξ′_{k} = (Γ′, x′_{k} : τ_{k} | Ξ′, in_{k}(x′_{k}) = t) for any choice of fresh variables x′_{1}, …, x′_{n} and the renamings ι_{k} : dom(Γ′) [figure] dom(Γ′, x′_{k} : τ_{k}) are the inclusion functions.

It follows that any cover {ρ_{j}} consists entirely of inclusion functions (which is why Γ′_{k} | Ξ′_{k} can be defined using t rather than t[ρ]). Observe also that a constrained environment Γ | Ξ is covered by the empty family if and only if there exists a term Γ ⊢ t : 0.

The above definition provides, for every Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n}), sub-basic covers of the form

{ (Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t) − [figure] (Γ | Ξ) }_{1≤i≤n}

keeping the morphisms as simple a possible whilst allowing the axioms of a Grothendieck topology to hold. For instance, the stability axiom holds because for any inclusion

ι_{i} : (Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t) − [figure] Γ | Ξ

(as present in the non-trivial covers) and any renaming ρ : Γ′ | Ξ′ [figure] Γ | Ξ, we have a commuting diagram:

(Γ′, x′ : τ_{i} | Ξ′, in_{i}(x′) = t[ρ])_{ι′_{i}} [figure]  ^{ρ[x_{i} [figure] x′]} [figure] (Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t)_{ι_{i}} [figure] (Γ′ | Ξ′)  _{ρ}  [figure] (Γ | Ξ)

for any x′ not in Γ′. Observe that the possibility of morphisms renaming variables is crucial here, as the variable x_{i} may already appear in the environment Γ′. Thus the stability of covers would not hold if we only allowed inclusions as morphisms in W. Indeed, the category W is not a preorder.

Definition 11 (Standard arity functor). The standard arity functor s : W [figure] S sends any constrained environment Γ | Ξ to its interpretation [[Γ | Ξ]], and any renaming ρ : Γ′ | Ξ′ [figure] Γ | Ξ to the unique map s(ρ), given by the universal property of the equaliser [[Γ | Ξ]] [figure] [[Γ]] of (2) in Section 2, such that the square below commutes.

[figure: [[Γ′ | Ξ′]]; s(ρ); [[Γ′]]; ⟨π_{ρx} ⟩_{x∈Γ}; [[Γ | Ξ]]; [[Γ]]]  (4)

For a cover {ι_{i} : (Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t) [figure] Γ | Ξ}_{1≤i≤n} in K it follows, from (1) and the stability of coproducts, that the family {s(ι_{i})}_{1≤i≤n} is a coproduct in S. By induction, this property extends to arbitrary covers in K and hence we have the following consequence.

Proposition 3. For every cover { ρ_{i} : Γ_{i} | Ξ_{i} [figure] Γ | Ξ }, the family { s(ρ_{i}) : [[Γ_{i} | Ξ_{i}]] [figure] [[Γ | Ξ]] } is a coproduct.

Corollary 1. For all A ∈ | S |, the presheaf s ∗ A in Ŵ is a sheaf for K.

The key lemma for establishing the definability result follows.

Lemma 2. For every cover { ρ_{i} : Γ_{i} | Ξ_{i} [figure] Γ | Ξ } and every family of terms { Γ_{i} ⊢ t_{i} : τ } there exists a term Γ ⊢ t : τ such that

1. Γ_{i} | Ξ_{i} ⊢ t_{i} = t : τ.

2. If Γ ⊢ t′ : τ is such that Γ_{i} | Ξ_{i} ⊢ t_{i} = t′ : τ for all i, then Γ | Ξ ⊢ t′ = t : τ.

3. The diagram below commutes for all i

[figure: [[Γ_{i} | Ξ_{i}]]; s(ρ_{i}); [[Γ | Ξ]]; x; [[Γ_{i}]]; [[Γ_{i}⊢t_{i}:τ]]; [[τ]]]

iff x = ([[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t:τ]]] [[τ]]).

Proof. (1)–(2) To a derivation D of a cover { ρ_{i} : Γ_{i} | Ξ_{i} [figure] Γ | Ξ } and terms { Γ_{i} ⊢ t_{i} : τ } we associate a term Γ ⊢ T (D, {Γ_{i} ⊢ t_{i} : τ}) : τ by induction on the structure of the derivation as follows.

– T ({id_{dom(Γ)}}, {Γ ⊢ t : τ}) =^{def} t.

– For r the rule

\frac{\{ρ_{j}\}_{j∈J} ∪ \{ρ\}}{\{ρ_{j}\}_{j∈J} ∪ \{ρ ∘ ι_{k}\}_{1≤k≤n}}

where ι_{k} : (Γ, x_{k} : τ_{k} | Ξ, in_{k}(x_{k}) = t) [figure] Γ | Ξ, we set

T (D.r, {Γ_{j} ⊢ t_{j} : τ}_{j∈J} ∪ {Γ, x_{k} : τ_{k} ⊢ t_{k} : τ}_{1≤k≤n})

=^{def} T (D, {Γ_{j} ⊢ t_{j} : τ}_{j∈J} ∪ {Γ ⊢ case t of [in_{1}(x_{1}).t_{1}, …, in_{n}(x_{n}).t_{n}] : τ}) .

That the term T (D, {Γ_{i} ⊢ t_{i} : τ}) has the desired properties can be shown by induction using the equational rules.

(3) By Proposition 3, because

([[Γ_{i} | Ξ_{i}]] [figure] [[Γ_{i}]] [figure: [[Γ_{i}⊢t_{i}:τ]]] [[τ]])

= ([[Γ_{i} | Ξ_{i}]] [figure] [[Γ_{i}]] [figure: [[Γ_{i}⊢t:τ]]] [[τ]])  , by Proposition 1
= ([[Γ_{i} | Ξ_{i}]] [figure] [[Γ_{i}]] [figure: ⟨π_{ρ_{i}(x)}⟩_{x∈Γ}] [[Γ]] [figure: [[Γ ⊢t:τ]]] [[τ]])
= ([[Γ_{i} | Ξ_{i}]] [figure: s(ρ_{i})] [[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t:τ]]] [[τ]]) , by (4)

Proposition 4. Let S be a stable bicartesian closed category (with chosen structure) and let I be a (T , Σ)-interpretation in S. Then

1. for

R_{T}(Γ | Ξ) =^{def} { [[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t:T]]] [[T]] } ,  (5)

((W, K), s, {R_{T}}_{T∈T} ) is a Grothendieck logical relation for Σ under I;

2. for every type τ,

R_{τ} (Γ | Ξ) = { [[Γ | Ξ]] [figure] [[Γ]] [figure: [[Γ ⊢t:τ]]] [[τ]] } .

Proof. (1) Follows from (2) below.

(2) By induction on the structure of τ.

\underline{τ = T}: By (5). \underline{τ = τ_{1} [figure] τ_{2}}:

(⊇) Let m = ([[Γ | Ξ]] [figure] [[Γ]]) and m′ = ([[Γ′ | Ξ′]] [figure] [[Γ′]]). For ρ : Γ′ | Ξ′ [figure] Γ | Ξ and x ∈ R_{τ} (Γ′ | Ξ′) we have, by induction, that x = [[Γ′ ⊢ t′ : τ_{1}]]∘m′ for some t′. Thus, to establish that [[Γ ⊢ t : τ_{1} [figure] τ_{2}]]∘m is in R_{τ_{1} [figure] τ_{2}}(Γ | Ξ) we need show that ev∘⟨[[Γ ⊢ t : τ_{1} [figure] τ_{2}]]∘m∘s(ρ), [[Γ′ ⊢ t′ : τ_{1}]] ∘ m′⟩ is in R_{τ_{2}}(Γ′ | Ξ′). Using that m ∘ s(ρ) = ⟨π_{ρx}⟩_{x∈Γ} ∘ m′ and that [[Γ ⊢ t : τ_{1} [figure] τ_{2}]] ∘ ⟨π_{ρx}⟩_{x∈Γ} = [[Γ′ ⊢ t[ρ] : τ_{1} [figure] τ_{2}]] one sees that ev ∘ ⟨[[Γ ⊢ t : τ_{1} [figure] τ_{2}]] ∘ m ∘ s(ρ), [[Γ′ ⊢ t′ : τ_{1}]] ∘ m′⟩ = [[Γ′ ⊢ t[ρ](t′) : τ_{2}]] ∘ m′ and, by induction, we are done. (⊆) Let

f ∈ R_{τ_{1} [figure] τ_{2}}(Γ | Ξ) .  (6)

Recall that ([[Γ, x : τ_{1} | Ξ, x =_{τ_{1}} x]] [figure][[Γ]] × [[τ_{1}]]) = m × id_{[[τ]]} where m = ([[Γ | Ξ]] [figure] [[Γ]]). Thus, for ι : (Γ, x : τ_{1} | Ξ, x =_{τ_{1}} x) [figure] Γ | Ξ the inclusion, we have that s(ι) = π_{1} : [[Γ | Ξ]] × [[τ_{1}]] [figure] [[Γ | Ξ]]. Since, by induction, π_{2} = [[Γ, x : τ_{1} ⊢ x : τ_{1}]] ∘ (m × id_{[[τ_{1}]]}) : [[Γ | Ξ]] × [[τ_{1}]] [figure] [[τ_{1}]] is in R_{τ_{1}}(Γ, x : τ_{1} | Ξ, x =_{τ_{1}} x) it follows from (6) that ev ∘ ⟨f ∘ π_{1}, π_{2}⟩ is in R_{τ_{2}}(Γ, x : τ_{1} | Ξ, x =_{τ_{1}} x). So, again by induction, ev∘⟨f ∘π_{1}, π_{2}⟩ = [[Γ, x : τ_{1} ⊢ t : τ_{2}]]∘(m×id_{[[τ_{1}]]}) for some t, and hence f = [[Γ ⊢ λx : τ_{1}.t : τ_{1} [figure] τ_{2}]]∘m.

\underline{τ = ×^{(n)}(τ_{1}, …, τ_{n})}: (⊇) Let m = ([[Γ | Ξ]] [figure] [[Γ]]). By induction, for 1 ≤ i ≤ n, π_{i} ∘ [[Γ ⊢ t : ×^{(n)}(τ_{1}, …, τ_{n})]] ∘ m = [[Γ ⊢ proj_{i}(t) : τ_{i}]] ∘ m is in R_{τ_{i}}(Γ | Ξ). Thus, [[Γ ⊢ t : ×^{(n)}(τ_{1}, …, τ_{n})]] ∘ m is in R_{×^{(n)}(τ_{1},...,τ_{n})}(Γ | Ξ). (⊆) Let x ∈ R_{×^{(n)}(τ_{1},...,τ_{n})}(Γ | Ξ). Then, for 1 ≤ i ≤ n, we have that π_{i} ∘ x ∈ R_{τ_{i}}(Γ | Ξ). By induction, π_{i} ∘ x = [[Γ ⊢ t_{i} : τ_{i}]] ∘ m, where m = ([[Γ | Ξ]] [figure] [[Γ]]), for some t_{i} (1 ≤ i ≤ n). Thus, x = [[Γ ⊢ ⟨t_{1}, …, t_{n}⟩ : ×^{(n)}(τ_{1}, …, τ_{n})]] ∘ m.

\underline{τ = +^{(n)}(τ_{1}, …, τ_{n})}:

(⊇) Let m = ([[Γ | Ξ]] [figure] [[Γ]]) and, for x_{i} ∉ Γ (1 ≤ i ≤ n), let m_{i} = ([[Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) =_{+^{(τ_{1},...,τn)}} t]] [figure] [[Γ]] × [[τ_{1}]]). By induction, we have that π_{2} ∘m_{i} = [[Γ, x_{i} : τ_{i} ⊢ x_{i} : τ_{i}]]∘m_{i} is in R_{τ_{i}}(Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) =_{+^{(n)}(τ_{1},...,τ_{n})} t) for all i. Consider the cover

{ (Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) =_{+^{(n)}(τ_{1},...,τ_{n})} t) [figure: ι_{i}]Γ | Ξ }_{1≤i≤n} .

Then since, for 1 ≤ i ≤ n, the diagram below commutes,

[figure: [[Γ, x_{i} : τ_{i} | Ξ, in_{i}(x_{i}) = t]]; p_{i}=s(ι_{i}); q_{i}; ⟨m∘p_{i},q_{i}⟩; [[Γ | Ξ]]; m; [[Γ]] × [[τ_{i}]]; π_{1}; π_{2}; −∣∣−; [[Γ]]; [[Γ ⊢t:+^{(n)}(τ_{1},...,τ_{n})]]; [[τ_{i}]]; ⨿_{i}; ∐^{(n)}(τ_{1}, …, τ_{n})]

it follows that [[Γ ⊢ t : +^{(n)}(τ_{1}, …, τ_{n})]] ∘ m is in R_{+^{(n)}(τ_{1},...,τ_{n})}(Γ | Ξ). (⊆) If x ∈ R_{+^{(n)}(τ_{1},...,τ_{n})}(Γ | Ξ) then there exists a cover { ρ_{i} : Γ_{i} | Ξ_{i} [figure] Γ | Ξ } such that for all i, using the induction hypothesis, there exist Γ_{i} ⊢ t_{i} : τ_{n_{i}} with 1 ≤ n_{i} ≤ n such that for all i

[figure: [[Γ_{i} | Ξ_{i}]]; s(ρ_{i}); [[Γ | Ξ]]; x; [[Γ_{i}]]; [[Γ_{i}⊢in_{n_{i}} (t_{i}):+^{(n)}(τ_{1},...,τ_{n})]]; [[+^{(n)}(τ_{1}, …, τ_{n})]]]

Hence, by Lemma 2, we are done.

⊓ ⊔

Corollary 2. For the Grothendieck logical relation ((W, K), s, {R_{T}}_{T∈T} ), a global element of [[τ]] in S satisfies R_{τ} if and only if it is definable by a closed term of type τ.

5 Further results

In the full version of this paper, we shall show that Theorem 1 can be strengthened by requiring that a “universal” site (𝕎, K) can be found in which 𝕎 is a partial order. This strengthening could be proved directly by making clumsy modifications to the construction of the syntactic site (W, K) given in Section 4. It is preferable, however, to derive the result by means of an elegant general construction. As in the well-known construction of the Diaconescu cover of a Grothendieck topos [6, IX.9], any site (𝕎, K) determines a related site \underline{D}(𝕎, K) over a poset \underline{D}(𝕎) together with a surjective functor d_{𝕎} : \underline{D}(𝕎) [figure] (𝕎). We have proved that, for any arity functor a : 𝕎 [figure] S (for S bicartesian closed), there is an associated full and faithful bicartesian closed functor \underline{G}(𝕎, K, a) [figure] \underline{G}(\underline{D}(𝕎), \underline{D}(K), a d_{𝕎}). This means that our definability result for the syntactic site (W, K) yields the desired poset-based definability result for \underline{D}(W, K).

Other aspects of the paper also benefit from a more abstract categorical treatment. For example, the construction of the category \underline{G}(𝕎, K, a) is an example of the subscone variant of glueing [1], in which the objects are restricted to K-closed monos (in 𝕎̂). Essentially this amounts to glueing relative to a factorization system. The analysis of the structure on \underline{G}(𝕎, K, a) can be performed entirely at this more general level.

Finally, it is also possible to give syntax-free account of definability. For any bicartesian closed functor F : 𝔹 [figure] S where 𝔹 is small and S is stable, there exists a site (𝕎, K) (with 𝕎 a poset) and an arity functor a : 𝕎 [figure] S such that F factors as UG where G : 𝔹 [figure] \underline{G}(𝕎, K, a) is a full bicartesian closed functor.

References

1. M. Alimohamed. A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science, 146:5–23, 1995.

2. D. Dougherty and R. Subrahmanyam. Equality between functionals in the presence of coproducts. Submitted to Information and Computation. An earlier version appeared in Proceedings of 10th LICS, pages 282–291, 1995.

3. N. Ghani. βη-equality for coproducts. In Typed Lambda Calculi and Applications, Proceedings of TLCA ’95, pages 171–185. Springer LNCS 902, 1995.

4. A. Jung and J. Tiuryn. A new characterisation of lambda definability. In Typed Lambda Calculi and Applications, Proceedings of TLCA ’93, pages 230–244. Springer LNCS 664, 1993.

5. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

6. S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

7. J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume II, pages 365 – 458. Elsevier Science Publishers, 1990.

8. P.W. O’Hearn and J.G. Riecke. Kripke logical relations and PCF. Information and Computation, 120:107–116, 1995.

9. E. Palmgren. Constructive sheaf semantics. Mathematical Logic Quarterly, 43:321 – 325, 1997.

10. G.D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980.

11. J.G. Riecke and A.B. Sandholm. A relational account of call-by-value sequentiality. In Proceedings of 12th Annual Symposium on Logic in Computer Science, pages 258–267, 1997.

12. G. Wraith. Artin glueing. Journal of Pure and Applied Algebra, 4:345–348, 1974.