Fully Complete Models for ML Polymorphic Types

Samson Abramsky Marina Lenisa^{∗}

Laboratory for the Foundations of Computer Science University of Edinburgh, Scotland.

October 28, 1999

Abstract

We present an axiomatic characterization of models fully-complete for ML-polymor-phic types of system F. This axiomatization is given for hyperdoctrine models, which arise as adjoint models, i.e. co-Kleisli categories of suitable linear categories. Examples of adjoint models can be obtained from categories of Partial Equivalence Relations over Linear Combinatory Algebras. We show that a special linear combinatory algebra of partial involutions induces an hyperdoctrine which satisfies our axiomatization, and hence it provides a fully-complete model for ML-types.

Introduction

In this paper we address the problem of full completeness for system F. A categorical model of a type theory (or logic) is said to be fully-complete ([AJ94a]) if, for all types (formulae) A, B, all morphisms f : [[A]] → [[B]], from the interpretation of A into the interpretation of B, are denotations of a proof-term of the intailment A ⊢ B. The notion of full-completeness is the counterpart of the notion of full abstraction, in the sense that, if the term language is executable, then a fully-complete model is (up-to a possible quotient) fully-abstract. Besides full completeness, one can ask the question whether the theory induced by a model M coincides precisely with the syntactical theory or whether more equations are satisfied in M. A model M is called faithful if it realizes exactly the syntactical theory.

The importance of fully (and faithfully) complete, and fully-abstract denotational models is that they characterize the space of proofs/programs in a compositional, syntax-independent way. These models can give hindsigths in various directions. E.g., in the context of static analysis, Denotational Semantics has suggested interesting typing disciplines (see e.g. [CDHL82, Abr91]). Moreover, these models can also yield new mathematical principles for reasoning on syntactical theories (observational equivalences), like for example Scott’s Induction Principle.

Recently, Game Semantics has been used to define fully-complete models for various fragment of Linear Logic ([AJ94a, AM99]), and to give fully-abstract models for many programming languages, including PCF [AJM96, HO96, Nic94], richer functional languages [AM95, McC96, HY97], and languages with non-functional features such as reference types and non-local control constructs [AM97, AM97a, AM97b, Lai97].

∗Work supported by TMR Linear FMRX-CT98-0170.

Once many concrete fully-complete and fully-abstract models have been studied, the problem of abstracting and axiomatizing the key properties of these constructions arises naturally. This line of research has been started by [Abr97], where axioms on models of PCF are given in order to guarantee full abstraction, and axioms on models of the simply typed λ-calculus are given, in order to guarantee full completeness.

The axioms for PCF are abstracted from the key lemmas in the proof of full abstraction of the game model of [AJM96]. This proof makes essential use of the underlying linear structure of the game category. Correspondingly, the axiomatization in [Abr97] applies to models of PCF which arise as co-Kleisli categories of some linear category. These kind of models, where we have a linear category and a cartesian closed category, together with a monoidal adjunction between the two categories, are called adjoint models, following [Bie95, BW96].

The problem of full completeness for second order (polymorphic) λ-calculus, i.e. Girard’s system F ([Gir72]), is a very important problem, which has been extensively studied.

Here are some results in the literature.

In [HRR90], the category of Partial Equivalence Relations (PER) over the open term model of the untyped λ-calculus has been proved to be fully (and faithfully) complete for algebraic types. These are ML-types of rank less or equal than 2, like for instance the type ∀X.(X → X) → X → X of Church’s numerals. ML-types are universal closures of simple types, i.e. types of the form ∀X_{1}…. X_{n}.T, where T is ∀-free and F V (T) ⊆ {X_{1}, …, X_{n}}. The rank of an ML-type is the nesting level of negative occurrences of → in the simple type T. A fully-complete model for the whole system F has been provided in [BC88], but this model is built by means of a quotient on terms, and therefore it is not compositional and not sufficiently abstract. More recently, in [Hug97], a fully and faithfully complete game model for system F has been given. But, although this is a game model, it still has a syntactical flavour.

Summarizing the situation, the previous work on the full completeness problem for system F has produced semantically satisfactory models only for algebraic types. In this paper, we provide satisfactory denotational models fully-complete for the whole class of ML-types.

This paper consists of three parts.

In the first part, we provide an axiomatization of models fully-complete for ML-types. This axiomatization is given on the models of system F which are called hyperdoctrines ([Cro93]). As in [Abr97], our axiomatization also works in the context of adjoint models. It consists of two crucial steps. First, we axiomatize the fact that every morphism f : 1 → [[T]], where T is an ML-type generates, under decomposition, a possibly infinite typed Böhm tree. Then, we introduce an axiom which rules out infinite trees from the model.

In the second part of the paper, we present a linear realizability technique for building hyperdoctrine adjoint models. This technique allows us to construct a PER category over a Linear Combinatory Algebra, which turns out to be a linear category, and it forms an adjoint model with its co-Kleisli category. The notion of Linear Combinatory Algebra (LCA) introduced by Abramsky ([Abr96]) refines the standard notion of Combinatory Algebra, in the same way in which intuitionistic linear logic refines intutitionistic logic. The construction of PER models from LCA’s presented in this paper is quite simple and clear, and it yields models with extensionality properties, thus avoiding cumbersome quotienting operations which are often needed in defining game categories and models. Recently, there has been much interest in realizability techniques, and in particular in linear realizability, especially in connection with full completeness and full abstraction problems. Realizability can be regarded as a powerful tool for mediating between intensional and extensional aspects of computation, and it has been used for extensionalizing intensional constructions (e.g. in [AM99]), and as a technique for building directly interesting (possibly fully-complete/fully-abstract) models. Examples of this latter use of realizability are in this paper, and also in [AL99], where a fully-abstract PER model for PCF, alternative to the game model of [AJM96], is provided using the linear algebra of well-bracketed strategies.

In the third part of the paper, we build an example of a concrete fully-complete model for ML-types. This is built by linear realizability over a special linear combinatory algebra of partial involutions. This algebra arises in the context of Abramsky’s generalization of Girard’s Geometry of Interaction ([AJ94, Abr96, Abr96a, AHPS98]). The proof of full completeness consists in showing that this model satisfies the axioms in our axiomatization. In particular, proving that the model does not contain infinite typed Böhm trees is quite difficult, and it requires the study of an intermediate model. This is the model generated by the Sierpinski PER and it consists of all (possibly infinite) Böhm trees of the typed λ-calculus, with constants ⊥, ⊤. A crucial step in our proof consists in proving that, in the simply typed λ-calculus with typical ambiguity and ⊥-constants, “totality tests” are λ-definable by finite typed trees. These totality tests allow us to tell apart terms in which ⊥ appears from terms in which ⊥ does not appear. A further ingredient is an Approximation Lemma, in the line of [AJM96].

The authors are thankful to R.Jagadeesan, J.Laird, J.Longley, S.Martini for useful discussions on some of the issues of the paper.

Contents

1 Simply Typed λ-calculus, ML Polymorphism, System F 4 1.1 Statman’s Typical Ambiguity Theorem . . . . . . . . . . . . . . . . . . . . . . 6 1.2 λ-definability of Covergence Tests in the λ-calculus with Typical Ambiguity . 6

2 Models of System F 8 2.1 Adjoint Hyperdoctrines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3 Axiomatizing Models Fully Complete for ML Types 11 3.1 The Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.2 Axiomatic Full Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4 Models of PERs over a Linear Combinatory Algebra 16 4.1 Linear Realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.2 Partial Involutions Affine Combinatory Algebra . . . . . . . . . . . . . . . . . 18

5 A Fully Complete PER Model 28 5.1 Proof of the Axioms 2–4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 5.2 Proof of the Finiteness Axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

6 Final Remarks and Directions for Future Work 36

1 Simply Typed λ-calculus, ML Polymorphism, System F

First, we recall the syntax of the simply typed λ-calculus with type variables and constants, and of system F, and we introduce some notation. Then, we present two important results on the simply typed λ-calculus with a theory of Typical Ambiguity. Typical Ambiguity theories are obtained from theories of the simply typed λ-calculus by requiring that two terms are equated if and only if, for all possible substitutions of type variables, they are equated in the theory on simply typed λ-calculus. The first result that we present is Statman’s Typical Ambiguity Theorem, which ensures that there is exactly one consistent theory of Typical Ambiguity on the simply typed λ-calculus with infinite type variables, i.e. the βη-theory. An immediate consequence of this is that the only consistent theory on the fragment of system F consisting of ML-types is precisely the βη-theory. The second result concerns the definability of “convergence tests” in the simply typed λ-calculus with infinite type variables, ⊥-constants, and a theory of Typical Ambiguity. In particular, we prove that, for any given type, there are covergence test terms, which detect the presence of ⊥-constants in a term of that type. This implies immediately that, in a theory of Typical Ambiguity over the simply typed λ-calculus with infinite type variables and ⊥-constants, a term with ⊥ can never be equated to a term without ⊥.

Definition 1.1 (Simply Typed λ-calculus) The class SimType of simple types over a (possible infinite) set of type variables TVar is defined by:

(SimType ∋) T ::= X | T → T ,

where X ∈ TVar. Raw Terms are defined as follows:

M ::= c | x | λx : T.M | MM ,

where c ∈ C is a set of constants.

Well-typed terms. We introduce a proof system for deriving typing judgements of the form Δ ⊢ M : T, where Δ is a type assignment, i.e. a finite list x_{1} : T_{1}, …, x_{n} : T_{n}. The rules of the proof system are the following:

\overline{Δ ⊢ c : T_{c}}  \overline{Δ, x : T, Δ′ ⊢ x : T}
\frac{Δ, x : T, Δ′ ⊢ M : S}{Δ ⊢ λx : T.M : T → S}  \frac{Δ ⊢ M : T → S Δ ⊢ N : T}{Δ ⊢ MN : S}

βη-conversion. βη-conversion between well-typed terms is the least relation generated by the following rules and the rules for congruence closure (which we omit):

β) Δ ⊢ (λx : T.M)N = M[N/x] : S, where Δ, x : T ⊢ M : S, and Δ ⊢ N : T.

η) Δ ⊢ λx : T.Mx = M : T → S, where Δ ⊢ M : T → S, and x ∉ dom(Δ).

Notation. We call:

λ  : the simply typed λ-calculus with T V ar = {ι};
λ_{⊥}  : the simply typed λ-calculus with T V ar = {ι}

and a base constant ⊥∈ C of type ι;

λ_{⊥,⊤} : the simply typed λ-calculus with T V ar = {ι}

and two base constants ⊥, ⊤ of type ι;

λ^{∞} : the simply typed λ-calculus with infinite type variables in TVar

and C = ∅;

λ_{⊥}^{∞} : the simply typed λ-calculus with infinite type variables in TVar

and base constants ⊥ of type ι, for any ι ∈ T V ar;

λ_{⊥,⊤}^{∞} : the simply typed λ-calculus with infinite type variables in TVar

and base constants ⊥ of type ι, for any ι ∈ T V ar.

Definition 1.2 (System F) The class Type of system F types over an infinite set of type variables TVar is defined by:

(Type ∋) T ::= X | T → T | ∀X.T ,

where X ∈ TVar.

System F raw terms are defined as follows:

M ::= x | λx : T.M | MM | ΛX.M | MT ,

where x ∈ Var.

Well-typed terms. The proof system for deriving typing judgements is defined as follows. A typing judgement has the form Γ; Δ ⊢ M : T, where Γ is a context, i.e. a finite list of type variables, and Δ is a type assignment, i.e. a finite list x_{1} : T_{1}, …, x_{n} : T_{n}, such that each T_{i} is legal in Γ. The rules for deriving the judgement Γ ⊢ T, read as “T is legal in Γ”, are the following:

\overline{Γ, X, Γ′ ⊢ X}  \frac{Γ ⊢ T Γ ⊢ S}{Γ ⊢ T → S}  \frac{Γ, X ⊢ T}{Γ ⊢ ∀X.T}

The rules for deriving the typing judgement Γ; Δ ⊢ M : T are the following:

\overline{Γ; Δ, x : T, Δ′ ⊢ x : T}  \frac{Γ; Δ, x : T ⊢ M : S}{Γ; Δ ⊢ λx : T.M : T → S}

\frac{Γ; Δ ⊢ M : T → S Γ; Δ ⊢ N : T}{Γ; Δ ⊢ MN : S}

\frac{Γ, X; Δ ⊢ M : T}{Γ; Δ ⊢ ΛX.M : ∀X.T} (∗) \frac{Γ; Δ ⊢ M : ∀X.T S is legal in Γ}{Γ; Δ ⊢ MS : T [S/X]}

(*) if X ∉ F V (ran(Δ)).

βη-conversion. The βη-conversion between well-typed terms is the least relation generated by the following rules and the rules for congruence closure (which we omit):

β) Γ; Δ ⊢ (λx : T.M)N = M[N/x] : S, where Γ; Δ, x : T ⊢ M : S, and Γ; Δ ⊢ N : T. η) Γ; Δ ⊢ λx : T.Mx = M : T → S, where Γ; Δ ⊢ M : T → S, and x ∉ dom(Δ).

β_{2}) Γ; Δ ⊢ (ΛX.M)T = M[T/X] : S, where Γ, X; Δ ⊢ M : S, and X ∉ F V (ran(Δ)).

η_{2}) Γ; Δ ⊢ ΛX.MX = M : ∀X.S, where Γ; Δ ⊢ M : ∀X.S, and X ∉ F V (ran(Δ)).

Now we introduce the class of ML-polymorphic types, which correspond to the limited kind of polymorphism allowed in the language ML.

Definition 1.3 (ML-types) The class ML-Type of ML-types is defined by:

ML-Type = {∀X⃗.T | T ∈ SimType ∧ F V (T) ⊆ X⃗} .

Terms of ML-types have essentially the same “combinatorics” as terms of the simply typed λ-calculus. More precisely, ML-terms can be regarded as the terms of the λ^{∞}-calculus with a Typical Ambiguity theory.

1.1 Statman’s Typical Ambiguity Theorem

The following is a result about simply typed λ^{∞} first proved in [Sta88]. An immediate consequence of this theorem is that the theory at ML-types of any non-trivial model of system F is exactly the βη-theory.

Theorem 1.1 (Statman’s Typical Ambiguity) Let T be a type of λ^{∞} such that F V (T) ⊆ {X_{1}, …, X_{n}}. If ⊬ M =_{βη} N : T, then, there exist types S_{1}, …, S_{n}, and Y ∈ T V ar, and a term L such that ⊢ L[S⃗/X⃗] : T → Bool_{Y}, where Bool_{Y} = Y → Y → Y, such that

⊢ LMS⃗ =_{βη} true : Bool_{Y} ∧ ⊢ LNS⃗ =_{βη} false : Bool_{Y} ,

where true = λx : Y.y : Y.x and false = λx : Y.y : Y.y, and MS⃗ denotes the term M in which the type variables X⃗ have been substituted by S⃗.

Corollary 1.1 The maximal consistent theory of Typical Ambiguity on λ^{∞} is the βη-theory.

Corollary 1.2 The maximal consistent theory on the fragment of system F consisting of ML-types is the βη-theory.

1.2 λ-definability of Covergence Tests in the λ-calculus with Typical Ambiguity

We show that “convergence tests” are λ-definable in λ_{⊥}^{∞} with a theory of Typical Ambiguity. This result will be used in Section 5, where we prove that the model of PERs over the linear combinatory algebra of partial involutions is fully-complete at ML-types.

Definition 1.4 (Typed Convergence Tests) Let T = T_{1} → … → T_{n} → X_{k} ∈SimType, let ι be a distinguished type variable, and let α_{T} = T [ι → ι/X⃗]. We define, by induction on T, the convergence test term ⊢ S_{α_{T}} : α_{T} as follows:

• if T = X, then

S_{ι→ι} = I_{ι→ι} ,

• otherwise, let T = T_{1} → … → T_{n} → X_{k}, where T_{i} = U_{i1} → … → U_{iq_{i}} → X_{i}, then

S_{α_{T}} = λx_{1} : α_{T_{1}} … x_{n} : α_{T_{n}}.λz : ι.(x_{1}S_{α_{U_{11}}} … S_{α_{U_{1q_{1}}}} )(… (x_{n}S_{α_{U_{n1}}} … S_{α_{Unq_{n}}} z)) .

Now we show how the “convergence test” terms defined above give us a procedure for deciding whether a term of λ_{⊥}^{∞} contains a divergent subterm. Let M be a term of λ_{⊥}^{∞} of type T_{1} → … → T_{n} → X_{k}. We first instantiate all the free variables in M by ι → ι, then we apply M to the sequence of convergence tests S_{α_{T_{1}}} , …, S_{α_{Tn}}. The effect of this is that, in the head reduction of MS_{α_{T_{1}}} , …, S_{α_{Tn}}, each subterm of M definitely appears in head position, and it reduces to the identity, until a ⊥ is detected.

For a term y⃗ : U⃗ ⊢ M : T, we denote by y⃗ : α⃗_{U} ⊢ M_{α_{T}} : α_{T} (or simply by M_{α_{T}}) the term of type α_{T} obtained from y⃗ : U⃗ ⊢ M : T by instantiating all the type variables free in T by ι → ι.

Theorem 1.2 (Typed Separability) Let T = T_{1} → … → T_{n} → X_{k} ∈SimType, and let ⊢ M : T be a term of λ_{⊥}^{∞}. Then

M_{α_{T}} S_{α_{T_{1}}} … S_{α_{Tn}} = \{ \begin{matrix}I_{ι→ι} & if M is ⊥-free \\ λx : ι. ⊥ & otherwise . \end{matrix}

Proof. Let y⃗ : U⃗ ⊢ M : T be a (possibly open) term of λ_{⊥}^{∞}, and let M̃_{α_{T}} = M_{α_{T}} [S⃗_{α_{U}} /y⃗] be the closed term obtained by saturating all the free variables in M_{α_{T}} by convergence tests of the appropriate types. We prove, by induction on the structure of M, that

M̃_{α_{T}} S_{α_{T_{1}}} … S_{α_{Tn}} = \{ \begin{matrix}I_{ι→ι} & if M is ⊥-free \\ λx : ι. ⊥ & otherwise . \end{matrix}

Base case: y⃗ : U⃗ ⊢ x : T. We have to prove that S_{α_{T}} S_{α_{T_{1}}} … S_{α_{Tn}} = I_{ι→ι}. But this latter fact can be immediately shown by induction on T. Induction Step: y⃗ : U⃗ ⊢ λz⃗.x_{i}M_{1} … M_{q_{i}}. Let M̃_{α_{T}} = λz⃗.x_{i}(M̃_{1})_{α_{U_{i1}}} … (M̃_{q_{i}})_{α_{U_{iq_{i}}}}. Then

M̃_{α_{T}} S_{α_{T_{1}}} … S_{α_{Tn}} = S_{α_{T_{i}}} (M̃_{1})_{α_{U_{i1}}} … (M̃_{q_{i}})_{α_{U_{iq_{i}}}} = λz : ι.((M̃_{1})_{α_{U_{i1}}} S⃗)(… (M̃_{q_{i}})_{α_{U_{iq_{i}}}} S⃗)z).

The thesis follows applying the induction hypothesis to each (M̃_{j})_{α_{U_{ij}}}, for all j = 1, …, q_{i}. □

Theorem 1.2 above can be regarded as a typed version of Böhm Separability Theorem, in the sense that, if we think of ⊥ as a generic unsolvable term, then Theorem 1.2 allows us to tell apart normal forms from unsolvable terms.

Corollary 1.3 In any theory of Typical Ambiguity on λ_{⊥}^{∞}, a term in which the ⊥-constant appears cannot be equated to a term without ⊥-constants.

The typed separability result above can be read by saying that all non-divergent computations can be reduced in some way to the identity computation. This is consistent with the view taken in the Geometry of Interaction/Game Semantics paradigm, whereby computations in the simply typed λ-calculus can be handled just by operations/strategies which do nothing more than copying information, without producing any new result.

2 Models of System F

We focus on hyperdoctrine models of system F. First, we recall the notion of 2λ×-hyperdoctrine (see [Cro93]). This essentially corresponds to the notion of external model (see [AL91]). Then, we give the formal definition of full (and faithful) complete hyperdoctrine model. Finally, we carry out a linear analysis of the notion of 2λ×-hyperdoctrine. This will allow us to express conditions which guarantee full completeness of the model w.r.t. ML-types. In particular, we introduce a categorical notion of adjoint hyperdoctrine. Adjoint hyperdoctrines arise as co-Kleisli indexed categories of linear indexed categories.

In what follows, we assume that all indexed categories which we consider are strict (see e.g. [AL91, Cro93] for more details on indexed categories).

Definition 2.1 (2λ×-hyperdoctrine) A 2λ×-hyperdoctrine is a triple (C, G, ∀), where:

• C is the base category, it has with finite products, and it consists of a distinguished object U which generates all other objects using the product operation ×. We will denote by U^{m}, for m ≥ 0, the objects of C.

• G : C^{op} → CCCat is a C-indexed cartesian closed category, where CCCat is the category of cartesian closed categories and strict cartesian closed functors, such that: for all U^{m}, the underlying collection of objects of the cartesian closed fibre category G(U^{m}) is indexed by the collection of morphisms from U^{m} to U in C, i.e. the objects of G(U^{m}) are the morphisms in Hom_{C}(U^{m}, U), and, for any morphism f : U^{m} → U^{n} in C^{op}, the cartesian closed functor G(f) : G(U^{n}) → G(U^{m}), called reindexing functor and denoted by f^{∗}, is such that, for any object h : U^{n} → U, f^{∗}(h) = f; h;

• For each object U^{m} of C, we are given a functor ∀_{m} : G(U^{m} × U) → G(U^{m}) such that

– ∀_{m} is right adjoint to the functor π_{m}^{∗} : G(U^{m}) → G(U^{m} × U), where π_{m} : U^{m} × U → U^{m} is the projection in C;

– ∀_{m} satisfies the Beck-Chevalley condition, i.e.:

∗ for any morphism f : U^{m} → U^{n} in C, the following diagram of functors commutes

[figure: G(U^{n} × U); ∀_{U^{n}}; (f×id_{U})^{∗}; G(U^{n}); f^{∗}; G(U^{m} × U); ∀_{U^{m}}; G(U^{m})]

∗ for any f : U^{m} → U^{n}, the canonical natural transformation f^{∗} ∘ ∀_{U^{n}} → ∀_{U^{m}} ∘ (f × id_{U})^{∗} is an identity.

Any 2λ×-hyperdoctrine can be endowed with a notion of interpretation [[ ]] for the language of system F.

Types with free variables in X_{1}, …, X_{m} are interpreted by morphisms from U^{m} to U in the category C, i.e. by objects of G(U^{m}):

[[X_{1}, …, X_{m} ⊢ T]] : U^{m} → U .

Well-typed terms, i.e. X_{1}, …, X_{m}; x_{1} : T_{1}, …, x_{n} : T_{n} ⊢ M : T, are interpreted by morphisms in the category G(U^{m}):

[[X_{1}, …, X_{m}; x_{1} : T_{1}, …, x_{n} : T_{n} ⊢ M : T]] : [[X⃗ ⊢ T_{1}]] × … × [[X⃗ ⊢ T_{n}]] → [[X⃗ ⊢ T]] .

More precisely:

Definition 2.2 We can endow any 2λ×-hyperdoctrine (C, G, ∀) with an interpretation function [[ ]] for the language of system F as follows.

[[ ]] is defined on types by induction on derivations of the judgement Γ ⊢ T:

• [[Γ, X, Γ′ ⊢ X]] = π_{i} : [[Γ]] × U × [[Γ′]] → U

• [[Γ ⊢ T → S]] = [[[Γ ⊢ T]] → [[Γ ⊢ S]]];

• [[Γ ⊢ ∀X.T]] = ∀([[Γ, X ⊢ T]]) .

[[ ]] is defined on terms by induction on derivations of the typing judgement Γ; Δ ⊢ M : T:

• [[Γ; x_{1} : T_{1}, …, x_{i} : T_{i}, …, x_{n} : T_{n} ⊢ x_{i} : T_{i}]] = π_{i} : [[Γ ⊢ T_{1}]] × … × [[Γ ⊢ T_{i}]] × … × [[Γ ⊢ T_{n}]] → [[Γ ⊢ T_{i}]]

• [[Γ; Δ ⊢ λx.M : T → S]] = Λ([[Γ; Δ, x : T ⊢ M : S]])

• [[Γ; Δ ⊢ MN : S]] = ⟨[[Γ; Δ ⊢ M : T → S]], [[Γ; Δ ⊢ N : T]]⟩; Ap

• [[Γ; Δ ⊢ ΛX.M : ∀X.T]] = \overline{[[Γ, X; Δ ⊢ M : T]]} , where ^{−} is the bijection given by the adjiunction between ∀ and π^{∗} in Definition 2.1;

• [[Γ; Δ ⊢ MS : T [S/X]]] = [[Γ; Δ ⊢ M : ∀X.T]]; ⟨id[[Γ]], [[Γ ⊢ S]]⟩^{∗}(îd_{∀([[Γ, Y ⊢ T [Y/X]]])}), where is the inverse of ^{−}.

Proposition 2.1 ([Cro93]) Any 2λ×-hyperdoctrine with the interpretation function [[ ]] of Definition 2.2 is a model of system F.

Definition 2.3 (Full (and Faithful) Completeness) Let M = (C, G, ∀, [[ ]]) be a 2λ×- hyperdoctrine.

i) M is fully complete w.r.t. the class of closed types T if, for all T ∈ T ,

∀f ∈ Hom_{G(1)}(I, [[⊢ T]]). ∃M. ⊢ M : T ∧ f = [[⊢ M : T]] .

ii) M is fully and faithfully complete w.r.t. the class of closed types T if, for all T ∈ T ,

∀f ∈ Hom_{G(1)}(I, [[⊢ T]]). ∃!βη-normal form M. ⊢ M : T ∧ f = [[⊢ M : T]] .

2.1 Adjoint Hyperdoctrines

We start by recalling some definitions:

Definition 2.4 (Linear Category, [Bie95, BW96]) A linear category is a symmetric monoidal closed category (L, I, ⊗, −∘) with

• a symmetric monoidal comonad (!, der, δ, ϕ, ϕ′) on L;

• monoidal natural transformations with components weak_{A} :!A → I and con_{A} :!A → !A⊗!A such that

– each (!A, weak_{A}, con_{A}) is a commutative comonoid,

– weak_{A} and con_{A} are !-coalgebra maps from (!A, δ_{A}) to (I, ϕ′_{I}), and from (!A, δ_{A}) to (!A⊗!A, δ_{A} ⊗ δ_{A}; ϕ_{!A,!A}), respectively.

– all coalgebra maps between free !-coalgebras preserve the canonical structure.

Definition 2.5 (Adjoint Model, [BW96]) An adjoint model is specified by

1. a symmetric monoidal closed category (L, I, ⊗, −∘);

2. a cartesian closed category (C, 1, ×, →);

3. a symmetric monoidal adjunction from C to L.

Now we give the indexed version of the notion of adjoint model:

Definition 2.6 (Indexed Adjoint Model) An indexed adjoint model is specified by

1. a symmetric monoidal closed indexed category L : C^{op} → SMCCat, where SMCCat is the category of symmetric monoidal closed categories and strict monoidal closed functors;

2. a cartesian closed indexed category G : C^{op} → CCCat, where CCCat is the category of cartesian closed categories and strict cartesian closed functors;

3. a symmetric monoidal indexed adjunction from G to L.

In the following definition, we capture those 2λ×-hyperdoctrines which arise from a co-Kleisli construction over an indexed linear category.

Definition 2.7 (Adjoint Hyperdoctrine) An adjoint hyperdoctrine is a quadruple (C, L, G, ∀), where:

• C is the base category, it has finite products, which consists of a distinguished object U which generates all other objects using the product operation ×. We will denote by U^{m}, for m ≥ 0, the objects of C.

• L : C^{op} → LCat is a C-indexed linear category, where LCat is the category of linear categories and strict monoidal closed functors, such that: for all U^{m}, the underlying collection of objects of the linear fibre category L(U^{m}) is indexed by the collection of morphisms from U^{m} to U in C.

• G : C^{op} → CCCat is the C-indexed co-Kleisli category of L, which we assume to be cartesian closed.

• For each object U^{m} of C, we are given a functor ∀_{m} : G(U^{m} × U) → G(U^{m}) such that

– ∀_{m} : G(U^{m} × U) → G(U^{m}) is right adjoint to the functor G(π_{m}) : G(U^{m}) → G(U^{m} × U), where π_{m} : U^{m} × U → U^{m} is the projection in C;

– ∀_{m} : G(U^{m} × U) → G(U^{m}) satisfies the Beck-Chevalley condition.

An adjoint hyperdoctrine is, in particular, an indexed adjoint model, and it gives rise to a 2λ×-hyperdoctrine:

Theorem 2.1 Let (C, L, G, ∀) be an adjoint hyperdoctrine. Then

i) the categories L and G form an indexed adjoint model; ii) (C, G, ∀) is an hyperdoctrine.

Remark. Notice that, in the definition of adjoint hyperdoctrine, we require the indexed categories L and G to form an adjoint model, but we assume the existence of a family of functors ∀_{m} only on the fibre categories of G. Therefore, we have a model of linear first order types, but not of linear higher order types, and our definition does not capture models of L/NL system F. Hence our notion of model is more general, but it is sufficient for dealing with ML-types, and for expressing axioms for full completeness at ML-types (see Section 3).

3 Axiomatizing Models Fully Complete for ML Types

We isolate sufficient conditions on adjoint hyperdoctrine models for system F, in order to guarantee full completeness at ML-polymorphic types. These conditions amount to the six axioms of Subsection 3.1. Our axiomatization of full completeness for ML polymorphism is in the line of the work in [Abr97], where an axiomatic approach to full abstraction/full completeness for PCF/simply typed λ-calculus is presented. These axiomatizations are inspired by the proof of full abstraction of the Game Semantics model for PCF of [AJM96]. Our axiomatization of full completeness for ML-types consists of two parts:

1. Axioms for ensuring the Decomposition Theorem. This theorem allows to recover the top-level structure of the (possibly infinite) Böhm tree denoted by morphisms from the terminal object into the interpretation of an ML-type in the fibre category G(1). The axioms for the Decomposition Theorem (Axioms 1–5 of Section 3.1) make essential use of the linear category underlying an adjoint hyperdoctrine. These axioms (apart from the axioms 1 and 3), are expressed by requiring some canonical maps between suitable spaces of morphisms in the fibre categories L(U⃗) to be isomorphisms.

2. A Finiteness Axiom, which allows to rule out infinite Böhm trees from the model.

Notice that, by definition of interpretation function on a hyperdoctrine (Definition 2.2), morphisms f in G(1) from the terminal object of G(1) into [[⊢ T]], where ∀X⃗.T_{1} → … → T_{n} → X_{k} is an ML-type, are λ-definable if and only if morphisms of G(U⃗) from ×_{i=1}^{n}[[X⃗ ⊢ T_{i}]] into [[X⃗ ⊢ X_{k}]] are λ-definable. Namely, f = [[⊢ ΛX⃗.x⃗ : T⃗.x_{i}M_{1} … M_{q_{i}} : ∀X⃗.T⃗ → X_{k}]] if and

only if Λ⃗^{−1}(f̂) = [[X⃗; x⃗ : T⃗ ⊢ x_{i}M_{1} … M_{q_{i}} : X_{k}]]. Therefore, from now on we focus on the

space of morphisms of G(U⃗) from ×_{i=1}^{n}[[X⃗ ⊢ T_{i}]] into [[X⃗ ⊢ X_{k}]], where T_{1}, …, T_{n} are simple types.

We start by presenting the main result of this section, i.e. the Decomposition Theorem. The proof of this theorem follows from the Strong Decomposition Theorem 3.2, which is proved in Section 3.2.

If a morphism f of G(U⃗) from ×_{i=1}^{n}[[X⃗ ⊢ T_{i}]] into into [[X⃗ ⊢ X_{k}]] is λ-definable, then f =

[[X⃗; x⃗ : T⃗ ⊢ x_{i}M_{1} … M_{q_{i}} : X_{k}]], for some X⃗; x⃗ : T⃗ ⊢ M_{1} : U_{i1}, …, X⃗; x⃗ : T⃗ ⊢ M_{q_{i}} : U_{iq_{i}}. I.e., making evident the top-level structure of the Böhm tree:

f = [[X⃗; x⃗ : T⃗ ⊢ x_{i} : T_{i}]] • [[X⃗; x⃗ : T⃗ ⊢ M_{1} : U_{i1}]] • … • [[X⃗; x⃗ : T⃗ ⊢ M_{q_{i}} : U_{iq_{i}}]] .

The Decomposition Theorem allows to recover the top-level structure of the Böhm tree corresponding to f in the following sense:

Theorem 3.1 (Decomposition) Let (C, L, G, ∀) be an adjoint hyperdoctrine satisfying Axioms 1–5 of Section 3.1. Let T = T_{1} → … → T_{n} → X_{k} be a simple type with F V (T) ⊆ {X_{1}, …, X_{n}}, where, for all i = 1, …, n, T_{i} = U_{i1} → … → U_{iq_{i}} → X_{i}.

Then, for all f ∈ Hom_{G(U⃗)}( ×_{i=1}^{n}[[X⃗ ⊢ T_{i}]], [[X⃗ ⊢ X_{k}]]), there exist i ∈ {1, …, n} and g_{j} ∈

Hom_{G(U⃗)}( ×_{i=1}^{n}[[X⃗ ⊢ T_{i}]], [[X⃗ ⊢ U_{ij}]]), for all j = 1, …, q_{i}, such that

f = [[X⃗; x⃗ : T⃗ ⊢ x_{i} : T_{i}]] • g_{1} … • g_{q_{i}} .

Since the g’s appearing in the Decomposition Thereom still live (up-to-uncurrying) in a space of morphisms denoting a simple type, we could keep on iterating the decomposition, expanding in turn these g’s, thus getting a possible infinite tree from f:

[figure: f = [[X⃗; x⃗ : T⃗ ⊢ x_{i} : T_{i}]]; g_{1}; …; g_{q_{i}}]

If the Decomposition Theorem holds, in order to get the full completeness result, we are only left to rule out morphisms generating trees whose height is infinite, which would correspond to infinite typed Böhm trees. This is expressed in the Finiteness Axiom 6 below.

3.1 The Axioms

The first axiom is a base axiom, which expresses the fact that the type ∀X⃗.X_{k} is empty, i.e. there are no closed terms typable with ∀X⃗.X_{k}.

Axiom 1 (Base)

Hom_{L(U⃗)}(1, π_{k}) = ∅ ,

where 1 is the terminal object in G(U⃗), and π_{k} : U⃗ → U⃗ denotes the k-th projection in G(U⃗), i.e. π_{k} = weak_{1} ⊗ … ⊗ weak_{k−1} ⊗ der_{k} ⊗ weak_{k+1} ⊗ … ⊗ weak_{n}.

The following axiom allows to extract one copy of the type of the head variable, corresponding to the first use of this variable. Notice that the property expressed by this axiom is truly linear. In fact, in order to state it, we are implicitly using the isomorphism A⊗!A ≃!A.

Axiom 2 (Linearization of Head Occurrence)

case_{i}{σ_{i}}_{i=1,... ,n} : n ; ∐_{i=1}Hom_{L(U⃗)}^{t}(h_{i}, (h⃗−∘π_{k})) ≃ Hom_{L(U⃗)}(h⃗, π_{k}) ,

where

• ∐ denotes coproduct in Set;

• h⃗ = ⊗_{i=1}^{n}!h_{i} and ∀i ∈ {1, …, n}. h_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}−∘π_{p_{i}};

• Hom_{L(U⃗)}^{t}(h_{i}, (h⃗−∘π_{k})) is a suitable subset of Hom_{L(U⃗)}(h_{i}, (h⃗−∘π_{k})), intended to contain only total elements (i.e. strict and not divergent);

• σ_{i} : Hom_{L(U⃗)}(h_{i}, (h⃗−∘π_{k})) → Hom_{L(U⃗)}(h⃗, π_{k}) is the following canonical morphism:

[figure: Hom_{L(U⃗)}(h_{i}, (h⃗−∘π_{k})); Λ^{−1}; Hom_{L(U⃗)}(h_{i} ⊗ h⃗, π_{k}); Hom_{L(U⃗)}(π_{i};τ,id_{π_{k}}); Hom_{L(U⃗)}(h⃗ ⊗ h⃗, −∘π_{k}); Hom_{L(U⃗)}(conh⃗,id_{π_{k}}); Hom_{L(U⃗)}(h⃗, π_{k})]

where τ : I ⊗ … ⊗ I ⊗ h_{i} ⊗ I … ⊗ I ≃ h_{i}.

The following axiom reflects a form of coherence of the type of the head variable w.r.t. the global type of the term. I.e., if T⃗ → X_{k} is the type of a term, then the type of the head variable must be of the shape U⃗ → X_{i}, with k = i.

Axiom 3 (Type Coherence)

Hom_{L(U⃗)}^{t}(l−∘π_{i}, h−∘π_{k}) = ∅ ,

if i ≠ k.

The following axiom expresses the fact that the only thing that we can do with a linear functional parameter is applying it to an argument. Axiom 4 (Linear Function Extensionality)

Hom_{L(U⃗)}((·), id_{π_{k}}) : Hom_{L(U⃗)}(h, l) ≃ Hom_{L(U⃗)}^{t}(l−∘π_{k}, h−∘π_{k}) .

The following axiom expresses the fact that morphisms from !f to !g in the fibre category L(U⃗) have uniform behaviour in all threads. Axiom 5 (Uniformity of Threads)

Hom_{L(U⃗)}(id_{!h}, der_{l}) : Hom_{L(U⃗)}(!h,!l) ≃ Hom_{L(U⃗)}(!h, l) : λf ∈ Hom(!h, l).(f)^{†} . Axioms 1–5 guarantee the validity of a strong Decomposition Theorem (see Section 3.2

below), which allows to decompose in a unique way all morphisms in Hom_{L(U⃗)}( ⊗_{i=1}^{n}!h_{i}, π_{k}), where h_{i} = ⊗_{j=1}^{q_{i}}!l_{j}−∘π_{p_{1}}, for any l_{1}, …, l_{q_{i}}, even if Hom_{L(U⃗)}( ⊗_{i=1}^{n}!h_{i}, π_{k}) is not the space of morphisms from ⊗_{i=1}^{n}![[X⃗ ⊢ T_{i}]] into [[X⃗ ⊢ X_{k}]], for some simple types T_{1}, …, T_{n}.

The final axiom in our axiomatization guarantees that the tree generated via repeated applications of the Decomposition Theorem 3.2 to morphisms in Hom_{L(U⃗)}( ⊗_{i=1}^{n}!h_{i}, π_{k}), where

h_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}−∘π_{p_{1}}, for j = 1, …, q_{i}, is finite.

Axiom 6 (Finiteness) There exists a size function

H : ⋃{Hom_{L(U⃗)}( ⊗_{i=1}^{n}!h_{i}, π_{k}) | k ∈ N, h_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}−∘π_{p_{i}}} ⟶ N ,

such that

∀j ∈ {1, …, q_{i}}. H(g_{j}) < H(f) ,

where the g_{j}’s are defined in the Decomposition Theorem 3.2.

3.2 Axiomatic Full Completeness

By Axioms 1–5, all morphisms in Hom_{L(U⃗)}(h⃗, π_{k}), where h⃗ = ⊗_{i=1}^{n}!h_{i} and, for all i = 1, …, n, h_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}−∘π_{p_{i}}, have a unique decomposition:

Theorem 3.2 (Strong Decomposition) Let (C, G, L, ∀) be an adjoint hyperdoctrine satisfying Axioms 1–5 of Section 3.1. Let f ∈ Hom_{L(U⃗)}(h⃗, π_{k}), where h⃗ = ⊗_{i=1}^{n}!h_{i} and, for all

i = 1, …, n, h_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}−∘π_{p_{i}}. Then there exist a unique i and unique g_{1}, …, g_{q_{i}} such

that, for all j = 1, …, q_{i}, g_{j} ∈ Hom_{L(U⃗)}(h⃗, l_{ij}), and

f = conh⃗; (π_{k} ⊗ ⟨g_{1}, …, g_{q_{i}}⟩^{†}); Ap .

Proof. By Axiom 2, there exists a unique i ∈ {1, …, n} and a unique f′ ∈ Hom_{L(U⃗)}^{t}(h_{i}, h⃗−∘π_{k}) such that f = conh⃗; π_{i} ⊗ idh⃗; Λ^{−1}(f′). By Axiom 3, π_{i} = π_{k}. By Axiom 4, there exists a

unique g ∈ Hom(h⃗, l⃗_{i}), where l⃗_{i} = ⊗_{j=1}^{q_{i}}!l_{ij}, such that f′ = g−∘π_{k} = Λ((id ⊗ g); Ap). Then

f = conh⃗; π_{k} ⊗ g; Ap. Finally, by Axiom 5, and by the universal property of the product, we obtain g = ⟨g_{1}, …, g_{q_{i}}⟩^{†}. □

Summarizing the results of this section, we have:

Theorem 3.3 (Axiomatic Full Completeness) Let M be an adjoint hyperdoctrine. If M satisfies Axioms 1–6, then M is fully and faithfully complete at ML-types.

Proof. Let ∀X⃗.T = T_{1} → … → T_{n} → X_{k} be an ML-type, and let f ∈ Hom_{L(1)}(!I, [[⊢ ∀X⃗.T]]).

One can easily prove, by induction on H(\overline{Λ⃗(f)}) that there exists X⃗; x⃗ : T⃗ ⊢ x_{i}M_{1} … M_{q_{i}} : X_{k} such that \overline{Λ⃗(f)} = [[X⃗; x⃗ : T⃗ ⊢ x_{i}M_{1} … M_{q_{i}} : X_{k}]]. Then f = [[⊢ ΛX⃗.λx⃗ : T⃗.x_{i}M_{1} … M_{q_{i}} : ∀X⃗.T⃗ → X_{k}]]. □

The Strong Decomposition Theorem is stronger than the Decomposition Theorem 3.1 in two respects. First of all, it guarantees the unicity of the decomposition. The unicity condition implies immediately that the model is faithful. We could give alternative forms of the axioms by substituting the isomorphisms requirements by weaker conditions, in order to ensure just the existence of a decomposition. This would be sufficient, since faithfulness of the model follows from Statman’s Theorem 1.1. More precisely, in order to guarantee the existence of a decomposition, it is sufficient to ask that the canonical morphisms in Axioms 2 and 4 and the morphism λf ∈ Hom(!h, l).(f)^{†} in Axiom 5 are surjective maps.

The axioms could be weakened also by considering only morphisms f whose domains and codomains are denotations of types, instead of generic objects.

The strong form of the axioms, that we have given, has the advantage of being more readable and concise. Moreover, as we will see in Section 5, the strong axioms for the Decomposition Theorem that we have given hold in our concrete example of fully-complete model, except for the Linearization of Head Occurrence, for which we only prove a weak form. But we conjecture that also this axiom holds in its strong form. In Section 5, also the Finiteness Axiom is proved in a weak form. More precisely, we show that there exists a size function for morphisms whose domains and codomains are denotations of appropriate types.

4 Models of PERs over a Linear Combinatory Algebra

Canonical examples of 2λ×-hyperdoctrines arise by considering the Partial Equivalence Relation (PER) category over a combinatory algebra (see [Cro93], Chapter 5, Section 5.5 for more details). In this section, we show how to build a PER category from a linear combinatory algebra (LCA). Furthermore, we prove that this category forms an adjoint model with its co-kleisli category, and we show how adjoint hyperdoctrines arise from PER categories over a linear combinatory algebra. Finally, we present the special LCA of partial involutions which we will show to provide a fully-complete model at ML-types (see Section 5).

We start by recalling the definition of linear combinatory algebra ([Abr96, AHPS98]):

Definition 4.1 (Linear Combinatory Algebra) A linear combinatory algebra A = (A, •,!) is an applicative structure (A, •) with a unary (injective) operation !, and distinguished elements (combinators) B, C, I, K, W, D, δ, F satisfying the following equations:

Equation  Principal type  Logical rule
Ix = x  α−∘α  Identity
Bxyz = x(yz)  (α−∘β)−∘(γ−∘α)−∘γ−∘β  Cut
Cxyz = (xz)y  (α−∘β−∘γ)−∘β−∘α−∘γ  Exchange
Kx!y = x  α−∘!β−∘α  Weakening
Wx!y = x!y!y  (!α−∘!α−∘β)−∘!α−∘β  Contraction
D!x = x  !α−∘α  Dereliction
δ!x =!!x  !α−∘!!α  Comultiplication
F!x!y =!(xy)  !(α−∘β)−∘!α−∘!β  Closed Functoriality .

LCA’s correspond to Hilbert style axiomatization of −∘,! fragment of Linear Logic. Given an LCA A = (A, •,!), we can form a standard CA A_{s} = (A, •_{s}) by the “combinatory version” of Girard’s translation of Intuitionistic Logic into Linear Logic. We define: α •_{s} β = α•!β (standard combinators can be defined in terms of the linear ones, see [AHPS98] for details).

4.1 Linear Realizability

We start by considering a BCI-algebra, i.e. an applicative structure (A, •) with B, C, I combinators. We define a PER category over a BCI-algebra, and we show that this category is symmetric monoidal closed.

Definition 4.2 Let A = (A, •) be a BCI-algebra. We define the category PER_{A} as follows. Objects: partial equivalence relations R⊆ A × A, i.e. symmetric and transitive relations. Morphisms: a morphism f from R to S is an equivalence class of the PER R −∘ S, where the PER R −∘ S is defined by

α(R −∘ S)β iff ∀γ R γ′. α • γ S β • γ′ .

On BCI-algebras which satisfy extensionality of pairs, standard pairing gives rise to a tensor product:

Lemma 4.1 Let A = (A, •) be a BCI-algebra. Let P be the pairing combinator, i.e. (using λ-notation) P = λzxy.zxy. If A satisfies extensionality of pairs, i.e.

P αβ = P α′β′ ⟹ α = α′ ∧ β = β′ ,

then, for all PERs R, S, the following PER is well defined

P αβ(R ⊗ S)P α′β′ iff α R α′ ∧ β S β′ .

Notice in particular that, if the BCI-algebra is affine, i.e. it is a BCK-algebra, then extensionality of pairs holds.

Proposition 4.1 Let A = (A, •) be a BCI-algebra satisfying extensionality of pairs. Then PER_{A} is a symmetric monoidal closed category.

Proof. Let ⊗ : PER_{A} × PER_{A} → PER_{A} be defined on objects as in Lemma 4.1. For any arrows f :R→S, f′ :R′→S′, we define f ⊗ f′ :R ⊗ R′→S ⊗ S′ by [λz.UzA], where U = λxy.xy and A = λxy.P (fx)(f′y). The PER I = {(I, I)} plays the role of tensor identity. The following are natural isomorphisms: ρ_{R} :R ⊗I →R, ρ_{R} = [λz.z(λxy.yx)], α_{R_{1},R_{2},R_{3}} : (R_{1} ⊗ R_{2}) ⊗ R_{3} → R_{1} ⊗ (R_{2} ⊗ R_{3}), α_{R_{1},R_{2},R_{3}} = [λz.UzA], where A = λx.UxZ, and Z = λxyz.P x(P yz); σ_{R_{1},R_{2}} :R_{1} ⊗ R_{2}→R_{2} ⊗ R_{1}, σ_{R_{1},R_{2}} = [λz.Uz(λzz′.P z′z)]; Λ : (R_{1} ⊗ R_{2} −∘ R_{3}) → (R_{1} −∘ R_{2} −∘ R_{3}), Λ = [λfxy.f(P xy)]. □

Now we show how an LCA gives rise to a linear category.

Proposition 4.2 Let A = (A, •,!) be an LCA satisfying extensionality of pairs. Let ! : PER_{A} → PER_{A} be the functor defined by:

• ∀ R, ! R= {(!α,!β) | α R β}

• ∀f :R_{1}→R_{2}, !f = [F!f].

Then (!, D, δ, ϕ, ϕ′) is a symmetric monoidal comonad, where

• ϕ_{R_{1},R_{2}} : ! R_{1} ⊗! R_{2}→ !(R_{1} ⊗ R_{2}) is defined by ϕ_{R_{1},R_{2}} = [λz.UzA], where A = λxy.F (F!T x)y;

• ϕ′ : I ≃ !I is [δ]_{I→!I}.

Notice that the following isomorphisms hold immediately in PER categories over LCA’s:

Lemma 4.2 Let A = (A, •,!) be an LCA satisfying extensionality of pairs. Then, for all PERs R, S,

1. (Idempotency of !) [D] : !! R≃ ! R : [δ];

2. (Uniformity of Threads) ψ : ! R −∘! S≃ ! R −∘ S : (·)^{†} , where ψ = [λx.x; D]; Equivalently: ∀α ∈ ! R −∘! S, (α; [D])^{†} = α; 3. (Commutativity of ⋂ w.r.t. !) ⋂_{X}! R≃!(⋂_{X} R).

The second isomorphism in Lemma 4.2 above is relevant for full completeness. In fact, as we will see in Section 4, this isomorphism amounts exactly to the Uniformity of Threads Axiom in our axiomatization of full completeness. The isomorphisms of Lemma 4.2 above highlight some degeneracies of the present construction of PER models.

Theorem 4.1 Let A = (A, •,!) be an LCA satisfying extensionality of pairs. Then

• The category PER_{A} is linear.

• The co-Kleisli category (PER_{A})_{!}, induced by the comonad ! on the category PER_{A}, is cartesian closed.

• The categories PER_{A} and (PER_{A})_{!} form an adjoint model.

• The category (PER_{A})_{!} is isomorphic to the category PER_{A_{s}}, where PER_{A_{s}} is the category obtained by standard realizability from the standard combinatory algebra A_{s}.

Finally, we show how to build an adjoint hyperdoctrine from an LCA:

Theorem 4.2 (PER Adjoint Hyperdoctrine) Let A = (A, •,!) be an LCA satisfying extensionality of pairs. Then A gives rise to an adjoint hyperdoctrine (C, L, G, ∀), by defining:

C : Let U be the set {R | R is a PER on A}. The objects of C, U^{n}, for n ≥ 0, are the finite products in Set of n copies of the set U, in particular U^{0} is the terminal object in Set. A morphism in C, f : U^{n} → U^{m}, is a set-theoretic function from U^{m} to U^{n}.

L : The morphisms in the fibre category L(U^{m}) from h_{1} : U^{m} → U to h_{2} : U^{m} → U are the equivalence classes of the PER ⋂_{X⃗∈U^{m}}(h_{1}X⃗−∘h_{2}X⃗). For any object f : U^{m} → U in L(U^{m}), we define !f to be λX⃗.!(fX⃗). For any morphism f : U^{m} → U^{n} in C, we define the behaviour of the functor L(f) : L(U^{n}) → L(U^{m}) on morphisms by: for any morphism H : h_{1} → h_{2} in L(U^{n}), H = ΛX⃗.H′ ∈ ⋂X⃗(h_{1}X⃗−∘h_{2}X⃗), let L(f)(H) : L(f)(h_{1}) → L(f)(h_{2}) be ΛX⃗.H′ ∘ f(X⃗) ∈ ⋂X⃗(L(f)(h_{1})X⃗−∘L(f)(h_{2})X⃗).

∀ : The functor ∀_{m} : L(U^{m} × U) → L(U^{m}) is defined as follows. For any h : U^{m} × U → U, ∀_{m}(h) = λX⃗.⋂_{X⃗}h(X⃗). For any morphism H : h_{1} → h_{2} in L(U^{m} × U), ∀_{m}(H) = H.

4.2 Partial Involutions Affine Combinatory Algebra

Many examples of LCAs arise from Abramsky’s categorical version of Girard’s Geometry of Interaction (GoI) construction, based on traced symmetric monoidal categories ([Abr96, Abr96a, AHPS98]). A basic example of GoI LCA, introduced in [Abr96], can be defined on the space [N ⇀ N] of partial functions from natural numbers into natural numbers, applying the GoI construction to the the traced category Pfn of sets and partial functions. Here we briefly recall the definition of this LCA, without discussing the categorical framework (see [Abr96, Abr96a, AHPS98] for more details). The LCA of partial involutions, which will be shown to provide a fully-complete model for ML-types (see Section 5), arises as subalgebra of this.

Let us consider the space [N ⇀ N] of partial functions from natural numbers to natural numbers. For any α ∈ [N ⇀ N] injective, we denote by α^{−1} the inverse of α. Now we show how we can endow the space [N ⇀ N] with a structure of LCA. Actually, the algebra which we will obtain is affine, i.e. it has a full K-combinator. We start by fixing the following two injective coding functions t and p:

t : N + N ▷ N : t^{−1} p : N × N ▷ N : p^{−1} .

The first is used in order to define application, it allows to transform an one-input/one-output function into a two-input/two-output function, . The latter is used for creating infinitely many copies of an one-input/one-output function α, i.e. for defining !α.

We now explain how application is computed geometrically, using the language of “boxes and wires” which arises in the general setting of traced symmetric monoidal categories (see [JSV96] for the general categorical treatment).

Let us represent an one-input/one-output function α ∈ [N ⇀ N] by the following oneinput-port/one-output-port box:

[figure: α]

In order to define the application α • β, for α, β ∈ [N ⇀ N], we regard α as a twoinput/two-output function via the coding t, i.e.:

[figure: t; α; t^{−1}]

In particular, t; α; t^{−1} : N+N ⇀ N+N can be described as a matrix of 4 one-input/one-output functions:

( \begin{matrix}α_{11} & α_{12} \\ α_{21} & α_{22} \end{matrix} )

where α_{ij} = in_{i}; t; α; t^{−1}; in_{j}^{−1} : N ⇀ N account for the contribution from the i-th input wire into the j-th output wire. I.e., graphically:

[figure: α_{11}; α_{12}; α_{22}; α_{21}]

The result of the application α • β is an one-input/one-output function which can be computed as follows. For any given input (token) n, this becomes input for t; α; t^{−1} along its lefthand input wire (see Fig. 1). The function t; α; t^{−1} sends it either to the lefthand or to the righthand output wire. In the first case, this is the result, in the latter case the resulting token becomes input for β and then it keeps traveling along the lefthand wires of t; α; t^{−1} and the input wire of β, until t; α; t^{−1} (possibly) sends it to its righthand output wire. Formally:

α • β = α_{22} ∪ α_{21}; (β; α_{11})^{⋆}; β; α_{12} ,  (1)

where ∪ denotes union of graph relations, and ^{⋆} denotes ⋃_{n≥0}(β; α_{11})^{n}.

The formula 1 for computing the application is essentially the Execution Formula from Girard’s Geometry of Interaction ([Gir89]).

The definition of the !-operation on our applicative structure is quite simple. The operation ! is intended to produce, from a single copy of α, infinitely many copies of α. These are obtained by simply tagging each of these copies with a natural number, i.e. we define:

!α = p^{−1}; (id_{N} × α); p .

Finally, we are left to show that (affine) combinators can be defined on the structure ([N ⇀ N], •,!). The formal (algebraic) definition of the combinators is the following:

[figure: n; t; α; t^{∗}; α • β(n); β]

Figure 1: Linear application.

Definition 4.3 (Combinators) I :

I = s_{I}^{−1}; f_{I}; s_{I} ,

where • s_{I} = t

• f_{I} : N + N ⇀ N + N is defined by:

– ∀n. f_{I}(r, n) = (l, n)

– ∀n. f_{I}(l, n) = (r, n).

B :

B = s_{B}^{−1}; f_{B}; s_{B} ,

where

• s_{B} : (((N + N) + (N + N)) + N) + N ⇀ N is defined by s_{B} = ((t + t) + id_{N}) + id_{N}; (t + id_{N}) + id_{N}; t + id_{N}; t

• f_{B} : (((N + N) + (N + N)) + N) + N ⇀ (((N + N) + (N + N)) + N) + N is the function defined by the following equations together with their symmetric closure:

– ∀n. f_{B}(r, n) = (l, (l, (l, (r, n))))

– ∀n. f_{B}(l, (l, (l, (l, n)))) = (l, (l, (r, (r, n))))

– ∀n. f_{B}(l, (l, (r, (l, n)))) = (l, (r, n)).

C :

C = s_{C}^{−1}; f_{C}; s_{C} ,

where • s_{C} : ((N + N) + ((N + N) + N)) + N ⇀ N is defined by

s_{C} = (t + (t + id_{N})) + id_{N}; (t + t) + id_{N}; t + id_{N}; t

• f_{C} : ((N + N) + ((N + N) + N)) + N ⇀ ((N + N) + ((N + N) + N)) + N is the function defined by the following equations together with their symmetric closure:

– ∀n. f_{C}(r, n) = (l, (r, (r, n)))

– ∀n. f_{C}(l, (r, (l, (r, n)))) = (l, (l, (r, n)))

– ∀n. f_{C}(l, (r, (l, (l, n)))) = (l, (l, (l, n))).

K :

K = s_{K}^{−1}; f_{K}; s_{K} ,

where

• s_{K} : (N + N) + N ⇀ N is defined by

s_{K} = t + id_{N}; t

• f_{K} : (N + N) + N ⇀ (N + N) + N is the function defined by the following equations:

– ∀n. f_{K}(r, n) = (l, (r, n))

– ∀n. f_{C}(l, (r, n)) = (r, n).

W : In order to define W, we need first to fix i, j ∈ N such that i ≠ j. Then

W = s_{W}^{−1}; f_{W}; s_{W} ,

where

• s_{W} : ((N × N) + ((N + N) + N)) + N ⇀ N is defined by

s_{W} = (p + (t + id_{N})) + id_{N}; (id_{N} + t) + id_{N}; t + id_{N}; t

• f_{W} : ((N × N) + ((N + N) + N)) + N ⇀ ((N × N) + ((N + N) + N)) + N is the function defined by the following equations together with their symmetric closure:

– ∀n. f_{W}(r, n) = (l, (r, (r, n)))

– ∀n. f_{W}(l, (r, (l, (r, n)))) = (l, (l, (i, n)))

– ∀n. f_{W}(l, (r, (l, (l, n)))) = (l, (l, (j, n))).

D : In order to define D, we need to fix i ∈ N. Then

D = s_{D}^{−1}; f_{D}; s_{D} ,

where • s_{D} : (N × N) + N ⇀ N is defined by

s_{D} = p + id_{N}; t

• f_{D} : (N × N) + N ⇀ (N × N) + N is the function defined by the following equations:

– ∀n. f_{D}(r, n) = (l, (i, n))

– ∀n. f_{D}(l, (i, n)) = (r, n).

δ : In order to define δ, we need to fix i, j ∈ N. Then

δ = s_{δ}^{−1}; f_{δ}; s_{δ} ,

where

• s_{δ} : (N × (N × N)) + N ⇀ N is defined by

s_{δ} = (id_{N} × p) + id_{N}; p + id_{N}; t

• f_{δ} : (N × (N × N)) + N ⇀ (N × (N × N)) + N is the function defined by the following equations:

– ∀n. f_{δ}(r, n) = (l, (i, (j, n)))

– ∀n. f_{δ}(l, (i, (j, n))) = (r, n).

F : In order to define F, we need to fix i, j ∈ N. Then

F = s_{F}^{−1}; f_{F}; s_{F} ,

where

• s_{F} : ((N × N) + N × (N + N)) + N ⇀ N is defined by

s_{F} = (p + (id_{N} × t)) + id_{N}; (id_{N} + p) + id_{N}; t

• f_{F} : ((N × N) + N × (N + N)) + N ⇀ ((N × N) + N × (N + N)) + N is the function defined by the following equations together with their symmetric closure:

– ∀n. f_{F}(r, n) = (l, (r, (i, (r, n))))

– ∀n. f_{F}(l, (r, (i, (l, n)))) = (l, (l, (j, n))).

There is a simple, intutitive, geometrical explanation of these combinators, which makes use of the language of boxes and wires (see Fig. 2 and 3).

For example, let us consider the identity combinator I. Since I has to satisfy the equation Ix = x, in order to define I, it is convenient to regard I as a two-input/two-output function, up-to-coding (see Fig. 2). The Identity combinator just copies informations from the lefthand input-wire to the righthand output-wire, and vice versa from the righthand input-wire to the lefthand output-wire.

[figure: I; x]

[figure: B; z; ^{y}; ^{x}]

[figure: C; z; ^{y}; ^{x}]

[figure: K; y; x]

Figure 2: IBCK-combinators.

[figure: W; ^{!y}; ^{x}; (i, n); (j, n); n; n; …; …; …; …]

[figure: D; (i, n); n; …; …; …; …; ^{!x}]

[figure: δ; (p(i, j), n); (i, (j, n)); …; …; …; …; ^{!x}]

[figure: F; ^{!y}; ^{!x}; ^{(i,x)}; (j, n); (i, (l, n)); (i, (r, n)); …; …; …; …; …; …; …; …]

Figure 3: WDδF-combinators.

The fact that I satsfies the identity equation has a simple geometrical explanation. Let us apply I to a partial function x:

[figure: x]

Now yank the string connecting the input and the output wires of the result of the application, forgetting about the box corresponding to I. This gives us immediately the expected result:

[figure: x]

Our argument is based on the Yanking Property of the trace on the symmetric monoidal category Pfn underlying our combinatory algebra. In particular, Yanking is one of the axioms characterizing the trace operation in the general setting of traced symmetric monoidal categories. We do not elaborate more on this here.

Let us now consider the combinator B which satisfies the equation Bxyz = x(yz). In order to define the box for B (and that of any other purely linear combinator), we only need to determine how many input wires (and correspondingly output wires) this box should have, and how these wires have to be connected inside the box. The number of input/output wires depends on the number of arguments which the combinator takes, and on the role played by these arguments, i.e. whether they just appear as arguments in the righthand side of the equation satisfied by the combinator or they are used as functions of one or more arguments. Concretely, the box for B (see Fig. 2) has two input (and two output) wires for x and two input (and two output) wires for y, since both x and y are applied to an argument, one input (and one output) wire for z, which appears only as argument, plus one extra input (and one output) wire, along which the input-token (output-token) is intended to enter (exit). The connections of the wires inside the box for B are determined by the control flow between x, y, z in the righthand part of the equation. First of all, the control flow passes from the input port of B to the input port of x. The second port of x is then connected to the input port of y, while the second port of y is connected to the unique port of z. The remaining connections are then obtained by symmetry. Now let us compute the result of the application of B to x, y, z:

[figure: z; y; x]

Pulling the global input/output string, and forgetting about the box corresponding to B, we get the expected result, i.e.:

[figure: z; y; x]

Now we briefly review through the remaining combinators. The combinator C (see Fig.

2) can be explained in a similar way as B. The affine combinator K simply forgets about its second argument y. In order to define W (see Fig. 3), we need to fix two different indeces i, j ∈ N, tagging the copies of y which are used as arguments by x. The remaining copies of y are ignored. The behaviour of D, δ, F can be explained similarly.

Essentially, all the combinators of Fig. 2 and 3 are functions that mediate the required interactions between the arguments simply by copying informations between the various ports.

There are many possible conditions that can be imposed on partial functions in order to cut down the space [N ⇀ N], still maintaining closure under application, !, and all the affine combinators. The subalgebra which gives rise to the fully-complete model of Section 5 is obtained by considering partial involutions:

Definition 4.4 Let f : N ⇀ N. f is a partial involution if and only if its graph is a symmetric relation. Let us denote by [N ⇀_{Inv} N] the space of partial involutions from N to N.

One can check that partial involutions are closed under the application, the !-operation, and all the combinators of Definition 4.3, i.e.:

Proposition 4.3 A_{P Inv} = ([N ⇀_{Inv} N], •,!) is an affine combinatory algebra.

A_{P Inv} is a highly constrained algebra, in which all computations are reversible. Partial involutions are reminescent of copy-cat strategies of game categories, in that the only computational effect that they have is that of copying informations from input to output wires.

A similar idea to the one used to define A_{P Inv} is used in [AL99], in order to provide a fully-abstract model for PCF. Here constraints of a different nature are put on the space [N ⇀ N], so as to capture only functions representing strategies in the [AJM96] style.

5 A Fully Complete PER Model

In this section, we prove that the PER category over the LCA A_{P Inv} of Section 4.2 satisfies the Axioms of Section 3 (some of them in a weak form), and hence it gives rise to a fully and faithfully complete PER model for ML-types.

By definition of PER adjoint models (see Theorem 4.2 of Section 4.1), and by the fact that PER categories are well-pointed, for any morphisms h, l in the fibre category L(U⃗),

Hom_{L(U⃗)} = F (⋂_{X⃗}h(X⃗)−∘l(X⃗)) ,

where F : P ER_{A} → Set is the forgetful functor. Therefore, in order to verify the main axioms for the Decomposition Theorem, we are left to establish some isomorphisms between the images in Set of suitable closed polymorphic PERs. First of all, notice that Axiom 1 and the Uniformity of Threads Axiom hold immediately on PER models. In fact, for the first axiom to hold, we need only to verify that the PER ⋂_{X⃗}X_{k} is the empty PER. This

follows immediately, by instantiating X_{k} with the empty per. Uniformity of Threads Axiom follows from the isomorphism ⋂_{X⃗}! R −∘!S ≃ ⋂_{X⃗}! R −∘S, which is an immediate consequence

of Lemma 4.2 of Section 4.1.

The rest of this section is devoted to the proof of the validity of the Axioms 2–4, 6. The proof of the validity of Axioms 2–4 is based essentially on the nature of partial

involutions, and it requires a careful analysis of their applicative behaviour. The most difficult part of the proof of full completeness for the model PER_{A_{PInv}} consists in proving the Finiteness Axiom, i.e. in ruling out infinite typed trees. The proof of this Axiom makes use of the Typed Separability result presented in Section 1.2, and it requires an Approximation Lemma, along the lines of [AJM96].

5.1 Proof of the Axioms 2–4

With the following three technical lemmata, we carry out the analysis of the structure of the partial involutions which inhabit the PERs involved in Axioms 2–4. In particular, in Lemma 5.1, we show that the partial involutions in dom(⋂_{X⃗} ⊗_{i=1}^{n}! R_{i} −∘X_{k}), where ∀i. R_{i}=S_{i} −∘X_{i},

are “total”, in the sense that, for any possible sequence of arguments in input, they always “look” at them, before producing an output, and they are different from the empty partial involution. In Lemma 5.2, we show that any of this partial involutions always “ask” first for the same argument, say the i-th argument, for any possible sequence of arguments. This allows us to isolate the first use of a copy in ! R_{i}. Finally, Lemma 5.3 will be used in order to define the space of total morphisms appearing in Axioms 2–4. This space amounts to a PER of total partial involutions (see Definition 5.2 below).

Lemma 5.1 Let ⋂_{X⃗}R⃗−∘X_{k} be a closed PER, where R⃗ = ⊗_{i=1}^{n}!R_{i}, and, for all i = 1, …, n,

R_{i}= S_{i}−∘X_{i}. Let f ∈ dom(⋂_{X⃗}R⃗−∘X_{k}). Then f is total, i.e.

∀m∃m′. f^{∗}(r, m) = (l, m′) ,

where f^{∗} = t; f; t^{−1} : N + N ⇀ N + N.

Proof. By contradiction. Assume that ∃m. f^{∗}(r, m)↑. Then we reach a contradiction by instantiating X⃗ as follows: X_{k} = {h : N ⇀_{Inv} N | h(m)↓}, and X_{j} = 1, for all j ≠ k. In fact: ∀g⃗ ∈ dom(R⃗). fg⃗(m)↑, i.e. fg⃗ ∉ X_{k}. Hence f ∉ dom(⋂_{X⃗}R⃗−∘X_{k}). In order to conclude,

we are left only to check that ∃g⃗ ∈ dom(R⃗). I.e., we have to check that ∀i.∃g_{i} ∈ dom(R_{i}). Such g_{i}’s exist, since each g_{i} can be taken to be the function constantly equal to an element in X_{i}, i.e., let h ∈ X_{i}, we define, for all n,m, t; g; t^{−1}(r, n) = (r, m) if and only if h(n) = m. Similarly, we can rule out the case ∃m, m′. f^{∗}(r, m) = (r, m′). □

The following technical definition will be useful in the sequel.

Definition 5.1 Let f : N ⇀_{Inv} N. Let f_{n}^{∗} : D_{n} ⇀_{Inv} D_{n}, where

D_{n} = \underbrace{(N × (N + N) + … + N × (N + N)}_{n} +N,

be defined as follows:

[figure: \underbrace{N × (N + N) + … + N × (N + N)}_{n} +N; _{\underbrace{id_{N} × t + … + id_{N} × t}_{n} +id_{N}}; \underbrace{N × N + … + N × N}_{n} +N; _{\underbrace{p + … + p}_{n} +id_{N}}; \underbrace{N + … + N}_{n} +N; t_{n−1}; N; t_{n−1}^{−1}; \underbrace{N + … + N}_{n} +N; _{\underbrace{p^{−1} + … + p^{−1}}_{n} +id_{N}}; \underbrace{N × N + … + N × N}_{n} +N; _{\underbrace{id_{N} × t^{−1} + … + id_{N} × t^{−1}}_{n} +id_{N}}; N]

where t_{n} is defined by induction on n as follows: t_{0} = t : N + N ⇀ N

t_{n+1} = [t_{n}, id_{N}] : \underbrace{(N + N) + … + N}_{n+3} ⇀ N.

Lemma 5.2 Let ⋂_{X⃗}R⃗−∘X_{k} be a closed PER, where R⃗ = ⊗_{i=1}^{n}!R_{i}, and, for all i = 1, …, n,

R_{i}= S_{i}−∘X_{i}. Let f ∈ dom(⋂_{X⃗}R⃗−∘X_{k}). Then there exists a unique i, 1 ≤ i ≤ n, such that:

• X_{i} = X_{k},

• ∀m. f_{n}^{∗}(r, m) = (l, (i,!(r, m))) , where f_{n}^{∗} is defined as in Definition 5.1, and !(r, m) denotes any element of N×(N+N), whose second projection is (r, m).

Proof. By Lemma 5.1, if f ∈ dom(⋂_{X⃗}R⃗−∘X_{k}), then ∀m. ∃a. f_{n}^{∗}(r, m) = (l, a). We prove

first, by contradiction, that ∀m.∃i. f_{n}^{∗}(r, m) = (l, (i,!(r, m))). Assume that ∃i.∃a′. f_{n}^{∗}(r, m) = (l, (i,!(l, a′))). We instantiate each X_{j} by {f : N ⇀_{Inv} N | f(m) = m}. Then the partial involution g_{j} such that g_{j}^{∗}(r, m) = (r, m), where g_{j}^{∗} = t; g_{j}; t^{−1}, is in R_{j}. In particular, we take g_{i} such that g_{i}^{∗}(l, a′)↑. Then f • g⃗ ∉ X_{k}. Hence we reach a contradiction. Using a similar argument, we rule out the case f_{n}^{∗}(r, m) = (l, (i,!(r, m′))), for m ≠ m′. Moreover, if f_{n}^{∗}(r, m) = (l, (i,!(r, m))), then X_{i} = X_{k}. Because, if X_{i} ≠ X_{k}, then we can instantiate X_{k′} by 1, for k′ ≠ k, and X_{k} by {h : N ⇀_{Inv} N | h(m)↓}. But, for g_{i} = ∅, this yields f • g⃗(m)↑, i.e. f • g⃗ ∉ X_{k}. Therefore, we are left to show that ∃!i.∀m. f^{∗}(r, m) = (l, (i, (r, m))). We prove it by contradiction. Assume that ∃m, m′, ∃i, j such that f_{n}^{∗}(r, m) = (l, (i,!(r, m))) and f_{n}^{∗}(r, m′) = (l, (j,!(r, m′))). First of all notice that, by the argument above, X_{i} = X_{j} = X_{k}. Then let X_{k} = {f : N ⇀_{Inv} N | f(m)↕f(m′)}^{1}, and X_{k′} = 1, for k′ ≠ k. Let g_{i} be such that g_{i}^{∗}(r, m) = (r, m), g_{i}^{∗}(r, m′) = (r, m′), then g_{i} ∈ T_{i}, and let g_{j} = ∅ ∈ T_{j}. Then, for any g_{l} ∈ T_{l}, for l ≠ i, j, fg⃗(m) = m, while fg⃗(m′)↑. □

Lemma 5.3 Let ⋂_{X⃗}R⃗−∘X_{k} be a PER, where R⃗ = ⊗_{i=1}^{n}!R_{i}, and, for all i = 1, …, n, R_{i}=

S_{i}−∘X_{i}. Let f, f′ ∈ dom(⋂_{X⃗}R⃗−∘X_{k}). If f(⋂_{X⃗}R⃗−∘X_{k})f′, then

∀m. f_{n}^{∗}(r, m) = f′_{n}^{∗}(r, m) ,

where f_{n}^{∗}, f′_{n}^{∗} are defined as in Definition 5.1.

Proof. By contradiction. Assume that ∀m. f_{n}^{∗}(r, m) = (l, (i,!(r, m))) and ∀m. f′_{n}^{∗}(r, m) = !(l, (j,!(r, m))), for i ≠ j. Then taking X_{k} to be the PER with the two equivalence classes {h : N ⇀_{Inv} N | h(m)↑} and {h : N ⇀_{Inv} N | h(m)↓}, and taking g_{i} = ∅, and g_{j} such that g_{j}^{∗}(r, m) = (r, m), where g_{j}^{∗} = t; g_{j}; t^{−1}, we get (fg⃗, f′g⃗) ∉ X_{k}. Contradiction. □

Now we introduce the total space of morphisms appearing in Axioms 2–4. This is induced by a suitable subPER of the PER ⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k}), which is meant to contain only

the equivalences classes of total maps. By subPER we intend a PER whose equivalence classes form a subset of the set of equivalence classes of the original per. Notice that, in general, in PER categories, there is no natural notion of strict/total map, since there are no natural ⊥-elements in any PER. But, in the special case of our combinatory algebra, there is a natural candidate for ⊥, i.e. the equivalence class of the empty partial involution. Of course, this makes sense only if we restrict ourselves to PERs to which ∅ belongs. Then strict maps turn out to be those maps which indeed “look” at their arguments, and total maps can be defined, as usual, as strict maps different from ⊥. Bearing on this intuition, we can define the space of total polymorphic maps used in Axiom 2 as follows (by Lemma 5.3 we are guaranteed that the following definition yields a subPER, i.e. it identifies a subset of the set of the equivalence classes of the original PER):

Definition 5.2 Let ⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k}) be a closed PER.

1f(m)↕f(m′) is the equiconvergence predicate, to be read as: f(m) ↓⇔ f(m′) ↓.

• We define the total PER (⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k}))_{t} to be the subPER of ⋂_{X⃗}(S −∘X_{i})−∘

(R −∘X_{k}), which contains only total partial involutions, i.e.:

f ∈ dom((⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k}))_{t}) iff

f ∈ dom(⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k})) ∧ ∀m. f^{∗}(r, (r, m)) = (l, (r, m)) ,

where f^{∗} = t + t; t; f; t^{−1}; t^{−1} + t^{−1}.

• We define the space of total morphisms Hom_{L(U⃗)}^{t}(ΛX⃗. S −∘π_{i}, R −∘π_{k}) to be the set

F (⋂_{X⃗}(S −∘X_{i})−∘(R −∘X_{k})_{t}) .

We start by proving the validity of Axioms 3 and 4, leaving Axiom 2, which is the most problematic, at the end.

Theorem 5.1 (Type Coherence) Let ⋂_{X⃗}(S−∘X_{i})−∘(R−∘X_{k}) be a closed PER such that

X_{i} ≠ X_{k}. Then

(⋂_{X⃗}(S−∘X_{i})−∘(R−∘X_{k}))_{t} = ∅ .

Proof. Assume by contradiction f ∈ dom(⋂_{X⃗}(S−∘X_{i})−∘(R−∘X_{k}))_{t}. Then, since f is total,

∀m.∃a. f^{∗}(r, (r, m)) = (l, a), where f^{∗} : (N + N) + (N + N) → (N + N) + (N + N) is t + t; t; t^{−1}; t^{−1} + t^{−1}. First of all, by suitably instantiating the X_{j}’s (by mimicking part of the proof of Lemma 5.2), one one can check that f^{∗}(r, (r, m)) = (l, (r, m)). But then, instantiating X_{k} by {h : N ⇀_{Inv} N | h(m)↓}, and X_{j} = 1, for all j ≠ k, we get: ∅ ∈ S⃗−∘X_{i}, but f • ∅ = ∅ ∉ X_{k}. □

Theorem 5.2 (Linear Function Extensionality) Let ⋂_{X⃗}(S−∘X_{k})−∘(R−∘X_{k}) be a closed

PER. Then

ΛX⃗.(·)X⃗−∘id_{X_{k}} : ⋂_{X⃗}R−∘S ≃ (⋂_{X⃗}(S−∘X_{k})−∘(R−∘X_{k}))_{t} .

Proof. We define the inverse τ of ΛX⃗.(·)X⃗−∘id_{X_{k}} to be the equivalence class of \overline{τ}, where \overline{τ} = t^{−1}; t^{−1} + t^{−1}; (t^{−1} + t^{−1}) + id_{N+N}; \overline{τ}^{∗}; (t + t) + t; t + id_{N}; t, and \overline{τ}^{∗} : ((N + N) + (N + N)) + (N + N) ⇀ ((N + N) + (N + N)) + (N + N) is the partial involution such that ∀n.\overline{τ}^{∗}(l, (l, (l, n))) = (r, (r, n)) and ∀n.\overline{τ}^{∗}(l, (r, (l, n))) = (r, (l, n)). Then one can easily check that τ is the inverse of ΛX⃗.(·)X⃗−∘id_{X_{k}}. □

We are left to show Axiom 2, i.e.:

case_{i}{F (σ_{i})}_{i=1,... ,n} : n ; ∐_{i=1}F ((⋂_{X⃗} R_{i} −∘(R⃗−∘X_{k}))_{t}) ≃ F (⋂_{X⃗}R⃗−∘X_{k}) ,

where σ_{i} is the appropriate canonical morphism.

The function case_{i}{F (σ_{i})}_{i=1,... ,n} is easily shown to be surjective. Proving injectivity is problematic. In fact, this amounts to showing that, if it is not the case that f(⋂_{X⃗} R_{i}

−∘(R⃗−∘X_{k}))_{t}f′, then it is not the case that σ_{i}(f)(⋂_{X⃗}R⃗−∘X_{k})σ_{i}(f′). As already remarked

at the end of Section 3.1, the sole surjectivity of the function case_{i}{F (σ_{i})}_{i=1,... ,n} is at any rate sufficient to guarantee that the relevant morphisms have a decomposition, and therefore, if also finiteness condition holds, we have full completeness. The question remains whether the strong version of the Linearization of Head Occurrence Axiom holds. What we can say is that we can prove a posteriori that the isomorphism holds in the case in which we restrict ourselves to universal PERs denoting ML-types. Namely, using the fact that the weak Decomposition Theorem and the Finiteness Axiom hold in our model (the latter is proved in Section 5.2), we can infer that our model is fully-complete, i.e. all morphisms from type interpretations to type interpretations are λ-definable. But then, by Stataman Theorem, since the model is non-trivial, any relevant morphism denotes exactly one βη-normal form, and therefore the following isomorphism holds:

Theorem 5.3 (Weak Linearization of Head Occurrence) Let ⋂_{X⃗}R⃗−∘X_{k} denote an ML-

type. Then

case_{i}{F (σ_{i})}_{i=1,... ,n} : n ; ∐_{i=1}F ((⋂_{X⃗} R_{i} −∘(R⃗−∘X_{k}))_{t}) ≃ F (⋂_{X⃗}R⃗−∘X_{k}) ,

where σ_{i} = ΛX.Λ^{−1}; ΛX.π_{i}; τ−∘id_{X_{k}}; ΛX.conR⃗−∘id_{X_{k}}.

Proof. The proof follows using Theorems 1.1 and 5.4. □

5.2 Proof of the Finiteness Axiom

We only prove a weak form of the Finiteness Axiom, i.e. we consider only universal PERs which are denotations of ML-types. In particular, we prove that the trees generated by elements of these PERs, via repeated applications of the Decomposition Theorem, have finite height. Therefore, the size function in the Finiteness Axiom can be taken directly to be the height of the tree generated via the Decompostion Theorem.

In order to prove the finiteness result, we need to study an intermediate model, which contains also approximant terms of possibly infinite trees live. To this aim, we introduce the Sierpinski PER, and the corresponding hierarchy of simple PERs over it. This hierarchy gives rise to a model for the simply typed calculus λ_{⊥,⊤} of Section 1.

Definition 5.3 (Sierpinski PER) • Let n ∈ N. The Sierpinski PERO_{n} is the twoequivalence classes PER defined as follows:

– ⊥_{O_{n}}= {f : N ⇀_{Inv} N | f(n)↑}

– ⊤_{O_{n}} = {f : N ⇀_{Inv} N | f(n)↓}.

• We define the hierarchy of simple PERs over the Sierpinski PER O_{n} as follows:

(SimPer_{O_{n}} ∋) R ::= O_{n} | R→R .

In what follows, we will omit the index n in denoting the Sierpinski PER O_{n}, since, for all n, all these PERs are isomorphic.

The simple PERs over O yield a model of λ_{⊥,⊤}. More precisely, this model is the CCC freely generated by the Sierpinski PER. We denote by [[ ]]^{O} the interpretation function. Notice that this model is trivially not faithful, i.e. its theory contains properly the βηtheory. In fact, since O has only a finite number of equivalence classes, then also (O → O) → (O → O) has a finite number of equivalence classes, and therefore, some Church’s numerals are identified in the model. More precisely, the model generated by O induces the minimal theory =_{m} on simply typed λ-calculus defined by induction on types as follows: ⊥=_{m}⊥ : ι ∧ ⊤ =_{m} ⊤ : ι M =_{m} N : T → U iff ∀P =_{m} Q. : T .MP =_{m} NQ : U. The model generated by the Sierpinski PER has a remarkable property, i.e. all partial involutions which inhabit a simple PER over O decompose as in Lemma 5.4 below. The proof of this lemma proceeds along the line of the proof of the Decomposition Theorem 3.2, except for the fact that here we deal directly with partial involutions, and not with equivalence classes. The proof of Lemma 5.4 is omitted.

Lemma 5.4 Let f ∈ dom(R_{1}→ … R_{n}→ O), where R_{1}→ … →R_{n}→ O ∈SimPer_{O}, and, for all i = 1, …, n, R_{i}=S_{i1}→ … →S_{iq_{i}}→ O. Then

• either f ∈ [[λx⃗. ⊥]]^{O}

• or f ∈ [[λx⃗.⊤]]^{O}

• or ∃!i ∈ {1, …, n}, ∃h ∈ [[λz⃗λx⃗.x_{i}(z_{1}x⃗) … (z_{q_{i}} x⃗)]], and ∃g_{1}, …, g_{q_{i}}, where ∀j ∈ {1, … q_{i}}. g_{j} ∈ dom(R⃗ → S_{ij}), such that

f = h • g_{1} • … • g_{q_{i}} .

Now we define approximants for partial involutions in the simple PERs over O. These approximants are defined using the Decomposition Theorem. By repeatedly applying the Decomposition Theorem to a partial involution f, we obtain a (possibly) infinite typed Böhm tree. The k-th approximant of f is obtained by truncating at level k this tree, and by substituting the empty partial involution for the possibly erased subtrees. Formally:

Definition 5.4 (Approximants) Let f ∈ dom(R) ∈ SimPer_{O}.

• We define the k-th tree, t_{k}(f), of height at most k + 1, generated from f after k applications of the Decomposition Theorem by induction on k as follows:

– t_{0}(f) is the tree of height 1 with root f;

– given the tree t_{k}(f) of height at most k + 1, the tree t_{k+1}(f) is obtained from the tree t_{k}(f) by expanding the possible leaves at level k + 1 via the Decomposition Theorem.

• We define the k-th approximant partial involution of f, p_{k}(f) ∈ dom(R) ∈ SimPer_{O}, as the partial involution obtained from the tree t_{k}(f) by substituting, if necessary, any partial involution at level k + 1 by the empty partial involution.

The supremum of the heights of the trees t_{k}(f) yields a measure on partial involutions:

Definition 5.5 (Size Function) Let f ∈ dom(R), where R∈ SimPer_{O}. We define

H(f) = sup_{k} H(t_{k}(f)) ,

where H(t_{k}(f)) is the height of the tree t_{k}(f).

Lemma 5.5 (Approximation) Let f ∈ dom(⋂_{X⃗}R⃗ → X_{k}), where (R⃗ → X_{k})[O⃗/X⃗] is a

simple PER over O. Then i)

f(⋂_{X⃗}R⃗ → X_{k}) ⋃_{k∈ω}p_{k}(f) .

ii) For all X⃗, for all g⃗ ∈ dom(R⃗),

( ⋃_{k∈ω}p_{k}(f)) • g⃗ = ⋃_{k∈ω}(p_{k}(f) • g⃗) .

Proof.(Sketch) The proof of ii) follows from the definition of application between partial involutions. The proof of i) follows from the fact that, for all X⃗, for all g⃗ ∈ dom(R⃗), for all n, m,

(f • g⃗)(n) = m ⟺ (( ⋃_{k∈ω}p_{k}(f)) • g⃗)(n) = m .

The implication (⇐) is immediate by definition of approximants. In order to prove the converse, one can check, by induction on k, that, if f • g⃗(n) = m with a “thread” of length at most 2k, then p_{k}(f) • g⃗(n) = m. □

Lemma 5.6 Let f ∈ dom(R), where R∈ SimPer_{O}. Then

p_{k}(f) ∈ [[M_{k}]] ,

where M_{k} is the term of λ_{⊥,⊤} whose (typed) Böhm tree is obtained from the tree p_{k}(f) by relabeling the nodes, in such a way that the nodes appearing in the k + 1-th level of p_{k}(f) are relabeled by the constant ⊥ (of the appropriate type), and the remaining nodes are labeled by the corresponding projections.

Proof. By induction on k. □

Theorem 5.4 (Finiteness) Let f ∈ dom(⋂_{X⃗}R⃗ → X_{k}), where ⋂_{X⃗}(R⃗ → X_{k}) is a closed PER

denoting the ML-type ∀X⃗.T⃗ → X_{k}. Then H(f) < ∞.

Proof. By contradiction. Assume H(f) = ∞. Then, ∀Y.f ∈ dom(R [Y → Y/X⃗] →

(Y → Y)). Let g_{1} ∈ [[ΛY.S_{α_{T_{1}}} ]], …, g_{n} ∈ [[ΛY.S_{α_{Tn}}]]. Then fg_{1} … g_{n} ∈ dom(⋂_{Y}Y →

Y). By Lemma 5.5i), also ( ⋃_{k∈ω}p_{k}(f))g_{1} … g_{n} ∈ dom(⋂_{Y}Y → Y). By Lemma 5.5ii),

( ⋃_{k∈ω}p_{k}(f))g_{1} … g_{n} = ⋃_{k∈ω}(p_{k}(f)g_{1} … g_{n}). Then, by Lemma 5.6,

(p_{k}(f)g_{1} … g_{n}) ∈ [[M_{k}]]^{O}[[S_{α_{T_{1}}} ]]^{O} … [[S_{α_{Tn}}]]^{O} = by the Typed Separability Theorem 1.2, [[λx : ι. ⊥: ι → ι]]^{O} = {h : N ⇀ N | t; h; t^{−1}(r, n)↑}.

Therefore, (( ⋃_{k∈ω}p_{k}(f))g_{1} … g_{n})(n)↑, and hence ( ⋃_{k∈ω}p_{k}(f))g_{1} … g_{n} ∉ ⋂_{Y}Y → Y ⊆ {h : N ⇀

N | t; h; t^{−1}(r, n)↓}. Contradiction. □

6 Final Remarks and Directions for Future Work

Here we give a list of remarks and interesting issues which still remain to be addressed (some of them are currently under investigation).

• In this paper, we have presented a fully-complete model for ML-types. A natural question arises: what happens beyond ML-types. Here is a partial answer. Already at the type Nat → Nat, where Nat is the type of Church’s numerals, i.e. ∀X.(X → X) → X → X, the PER model of partial involutions is not fully-complete. In fact, all recursive functions, even all functions from natural numbers to natural numbers, can be encoded in the type Nat → Nat. A similar problem arises even if we consider the term combinatory algebra. PER models as they are defined in this paper, do not seem to give full-completeness beyond ML-types. An innovative construction is called for here.

• Another question which arises naturally is whether the PER model over the linear term combinatory algebra is fully-complete at ML-types. We conjecture that this is the case, but a proof of this fact seems difficult. A logical relation technique relating the term algebra and the term subalgebra of partial involutions could be useful here. The interest of linear term algebras lies in the fact that the PER model generated by these is essentially the PER model shown to be fully-complete at algebraic types in [HRR90].

• We have presented a linear realizability technique for building PER categories over an LCA. These PER categories turn out to be linear categories. It would be interesting to carry on the investigation of the general properties of these categories, e.g. define coproducts, products, etc..

• Besides full completeness, parametricity is another “quality filter” for models of polymorphic functions. In particular, in [Plo93], a logic for linear parametric models has been suggested, in the line of [PA93]. It would be interesting to develop further this approach, and see whether this logic holds on our linear PER models. Longo’s genericity ([LMS92]) can be viewed as a form of parametricity, in that it amounts to a uniformity property of polymorphic functions w.r.t. their input types. This issue and that of parametricity à la Reynolds will be investigated in [AL99a].

• Models of partial involutions are worthwhile investigating also for typed/untyped λcalculi different from system F. E.g. strategies in the [AJM96] style, which are represented by partial involutions from Opponent moves to Player moves, should provide fully-complete models for simply typed λ-calculus with ⊥, ⊤-base constants. In the untyped setting, partial involutions strategies could possibly provide fully-abstract models , alternative to those in [DFH99, KNO99].

• In the category PER_{PInv}, models of typed Böhm trees naturally arise (e.g. the model induced by the Sierpinski PER in Section 5.2). These are in particular models of the simply typed λ-calculus together with a fixed point combinator, as suggested by Alex Simpson. All these “infinite” calculi seem interesting by themselves, but have not yet been propertly investigated.

References

[Abr91] S.Abramsky. Domain Theory in logical form, Annals of Pure and Applied Logic 51, 1991, 1–77.

[Abr96] S.Abramsky. Interaction, Combinators, and Complexity, Notes, Siena (Italy), 1996.

[Abr96a] S.Abramsky. Retracing some paths in Process Algebra, Concur’96 Conf. Proc., 1996.

[Abr97] S.Abramsky. Axioms for Full Abstraction and Full Completeness, 1997, to appear.

[AHPS98] S.Abramsky, E.Haghverdi, P.Panangaden, P.Scott. Geometry of Interaction and Models of Combinatory Logic, 1998, to appear.

[AJ94] S.Abramsky, R.Jagadeesan. New foundations for the Geometry of Interaction, Inf. and Comp. 111(1), 1994, 53–119.

[AJ94a] S.Abramsky, R.Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic, J. of Symbolic Logic 59(2), 1994, 543–574.

[AJM96] S.Abramsky, R.Jagadeesan, P.Malacaria. Full Abstraction for PCF, 1996, to appear.

[AL99] S.Abramsky, J.Longley. Realizability models based on hystory-free strategies, Draft paper, 1999.

[AL99a] S.Abramsky, M.Lenisa. On Full Completeness, Genericity, Parametric Polymorphism, in preparation.

[AM95] S.Abramsky, G.McCusker. Games and full abstraction for the lazy lambdacalculus, LICS Conf. Proc., 234–243, 1995.

[AM97] S.Abramsky, G.McCusker. Full abstraction for idealized Algol with passive expressions, 1997, to appear.

[AM97a] S.Abramsky, G.McCusker. Call-by-value games, CSL’97 Conf. Proc., LNCS, 1997.

[AM97b] S.Abramsky, G.McCusker. Linearity, sharing and state, in P.O’Hearn and R.Tennent eds., Algol-like Languages, Birkhauser, 1997, 297–329.

[AM99] S.Abramsky, P.Mellies. Concurrent Games and Full Completeness, LICS’99 Conf. Proc., 1999.

[AL91] A.Asperti, G.Longo. Categories, Types ad Structures: An introduction to category theory for the working computer scientist, Foundations of Computing Series, The MIT Press, 1991.

[BC88] V.Breazu-Tannen, T.Coquand. Extensional models for polymorphism, TCS 59, 1988, 85–114.

[BW96] N.Benton, P.Wadler. Linear Logic, Monads and the Lambda Calculus, LICS’96 Conf. Proc., 1996.

[Bie95] G.Bierman. What is a categorical Model of Intuitionistic Linear Logic?, TL-CA’95 Conf. Proc., LNCS, 1995.

[CDHL82] M.Coppo, M.Dezani, F.Honsell, G.Longo. Extended Type Structures and Filter Lambda Models, Logic Colloquium’82 Conf. Proc., G.Longo et al. eds., North Holland, 1983.

[Cro93] R.Crole, Categories for Types, Cambridge University Press, 1993.

[DFH99] P.Di Gianantonio, G.Franco, F.Honsell. Game Semantics for Untyped λ-calculus, TLCA’99 Conf. Proc., LNCS, 1999.

[Gir72] J.Y.Girard. Interprétation functionelle et élimunation des coupures de l’arithmètique d’ordre supérieur, Thèse d’Etat, Université Paris VII, 1972.

[Gir89] J.Y.Girard. Towards a Geometry of Interaction.Contemporary Mathematics 92, 1989, 69–108.

[Hug97] D.Hughes. Games and Definability for system F, LICS’97 Conf. Proc., 1997.

[HRR90] J.Hyland, E.Robinson, G.Rosolini. Algebraic types in PER models, MFPS Conf. Proc., M.Main et al. eds, LNCS 442, 1990, 333–350.

[HO96] M.Hyland, L.Ong. On full abstraction for PCF, Information and Computation, 1996, to appear.

[HY97] K.Honda, N.Yoshida. Game-theoretic analysis of call-by-value computation, IC-AlP’97 Conf. Proc., LNCS, 1997, 225–236.

[KNO99] A.Ker, H.Nickau, L.Ong. More Universal Game Models of Untyped λ-Calculus: The Böhm Tree Strikes Back, CSL’99 Conf. Proc., LNCS, 1999.

[JSV96] A.Joyal, R.Street, D.Verity. Traced monoidal categories, Math. Proc. Comb. Phil. Soc. 119, 1996, 447–468.

[Lai97] J.Laird. Full abstraction for functional languages with control, LICS Conf. Proc., 58–64, 1997.

[LMS92] G.Longo, K.Milsted, S.Soloviev. The Genericity Theorem and the Notion of Parametricity in the Polymorphic λ-calculus, LICS’92 Conf. Proc., 1992.

[McC96] G.McCusker. Games and full abstraction for FPC, LICS’96 Conf. Proc., 1996.

[Nic94] H.Nickau. Hereditarily sequential functionals, Proc. of the Symposium Logical Foundations for Computer Science, LNCS 813, 1994.

[Plo93] G.Plotkin. Linear Parametricy, Notes, 1993.

[PA93] G.Plotkin, M.Abadi. A Logic for Parametric Polymorphism, TLCA’93 Conf. Proc., LNCS, 1993.

[Sta88] Statman. λ-definable functionals and βη-conversion, Arch. Math. Logik 23, 1983, 21–26.