CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES

T. SAKURAI Department of Mathematics and Informatics, Chiba University, 1-33 Yayoi, Inage, Chiba, 263-8522, JAPAN E-mail: sakurai@math.s.chiba-u.ac.jp

The observation that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction is clarified by the works of Hyland and Ong ^{5}, Altenkirch ^{1}, Stefanova and Geuvers ^{11}, and so on. The model of Hyland and Ong is based on PL-category^{10} and the models of Altenkirch and Stefanova and Geuvers are designed for this purpose. But no framework is known that includes all of them. In this paper, we will investigate such a categorical structure for the second order λ-calculus, that is, a structure that has as instances a PL-category type model and an intensional model. To demonstrate the significance of the intensional model, we will give a model in which we can carry out the proof of the uniqueness of the β-normal form. Our structure is a special case of the comprehension category ^{6,9} and the notion of semi-adjoint is used to interpret abstraction and application (uncurry).

1 Introduction

The observation that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction is clarified by several kinds of categorical or semantical frameworks. Here we will pick up only two of them. Hyland and Ong^{5} constructed a model that is an instance of the categorical model known as PL-category^{10} for the second order λ-calculus. Altenkirch^{1} and Stefanova and Geuvers^{11} constructed models motivated by this observation, but it is not known whether they are instances of some categories. However, Stefanova and Geuvers’s model cannot be an instance of the PL-category, because it is intensional whereas PL-category is extensional. The purpose of this paper is to present a structure for the second order λ-calculus which is a special case of the comprehension category^{6,9} and is an intensional version of PL-category restricted to the second order λ-calculus.

Roughly speaking, Hyland and Ong constructed a PL-category using SN terms, that is, types are interpreted as PERs (with additional information) of SN terms and terms are interpreted as equivalence classes of the PER where the strongly normalizability is preserved by the interpretation. The second object of this paper is to show that more theorems can be proved in a similar semantic setting. For example, we can show ‘well-typed β-equal terms have the common β-normal form’ roughly as follows: If two well-typed terms are β-equal, they have the same meaning. The meaning of a term is given by computing the β-normal form using the β-reduction of a specific strategy. Therefore, they have the common β-normal form. However, in the latter case, if we try to put the proof in the semantic setting like PL-category, we go into the difficulty: we cannot distinguish terms that are βη-equal but not β-equal, since βη-equal terms have the same meaning in the PL-category. In this paper, we will show we can escape from the difficulty by weakening the PL-category, that is, by using semi-adjoint^{4,7} instead of adjoint. Just to prove SN, only a weak structure which corresponds to the saturated set conditions is enough, but, since it has value of its own to embed the proof of SN into the well-known rich structure – PL-category, we will show that the PL-category is the special case of our structure and we can carry out the proof of SN.

Jacobs reformulated his notion of constant comprehension category^{6,9} for the case of simply-typed and untyped λ-calculus and defined λ1-category ^{8}. Our structure is essentially a λ1-category extended for second order λ-calculus and, in the instances of our structure in which we prove the syntactic properties of typed λ-terms, types are interpreted as PERs on terms and contexts are interpreted as sequences of PERs on terms.

The rest of this paper is organized as follows. In section 3 and 4, we consider the case of simply typed λ-calculus to explain the ideas of our structure. In section 3, we introduce a simplified version of our structure to interpret simply typed λ-calculus. In section 4, we give instances of the structure in which we can carry our the proofs of some theorems including SN. In section 5, we define our structure to interpret second order typed λ-calculus which is a special kind of the comprehension category and a generalization of the PLcategory. In section 6, we give instances of the structure in which types are interpreted as PERs of terms and β(η)-equal terms have the same meaning, and show we can carry out the prof of the theorem ‘well-typed β-equal terms have the common β-normal form’ and the proof of SN.

2 Second Order Typed λ-calculus

We define types σ and preterms M of second order typed λ-calculus λ2 by

σ ::= X | σ → σ | ∀X.σ
M ::= x^{σ} | app(σ → σ, M, M) | λx^{σ}.M | app(∀X.σ, M, σ) | ΛX.M

where X is a type variable and x^{σ} is a variable. We annotate the application by the type which is intended to be the type of the function part of the application. We will call the type-part of the variables and the type in the application the type annotations and omit them when they are irrelevant. For the judgement and the equality judgement, we use the following notations

X_{1}, …, X_{k} + x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} ⊢ M : σ
X_{1}, …, X_{k} + x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} ⊢ M = N : σ

and define inference rules of λ2 as usual. The system λ2 does not have η-rule and, when the η-rule is added, we denote the system by λη2.

In the following, we will write Λ for the set of preterms and T for the set of types.

3 Simple Semantic Structure

In this and next section, we explain the idea of our semantic structure by giving a simplified version of it in the case of simply-typed λ-calculus without equality judgement. The idea of our semantic structure comes from the environment model or the BMM model (Bruce, Meyer, and Mitchell’s model^{2,3}).

A structure ⟨{C_{B}^{A_{1},... ,A_{n}}}_{A_{i}∈T ,B∈T} , −^{∗}−, Ψ, Φ⟩ which satisfies the following conditions is called a λ-structure. In this and next section, T is the set of types of simply-typed λ-calculus constructed from some base types.

{C_{B}^{A_{1},... ,A_{n}}}_{A_{i}∈T ,B∈T} is a family of sets indexed by T^{n} and T (n ≥ 0). A context object is a sequence of types. (We denote the null sequence by ϵ.) We use the notation E, B for the concatenation of a context object E and a type B. An element f of C_{B}^{E} is called a base arrow and we will write f : E ⟶ B when f ∈ C_{B}^{E}. C_{A_{i}}^{A_{1},... ,A_{n}} contains a base arrow which we write (id^{A_{1},... ,A_{n}})_{i} and −^{∗}−, Ψ, Φ are operations on base arrows which satisfies the following conditions.

(R) if f : E, A ⟶ C and g : E ⟶ A, then g^{∗}f : E ⟶ C (A1) if f : E, A ⟶ C, then Ψf : E ⟶ (A → C) (A2) if g : E ⟶ (A → C), then Φg : E, A ⟶ C

The intention of these definitions is that (R) is reindexing, and (A1) and (A2) is a part of semi-adjointness. Ψ is an ‘abstraction’ and Φ is inverse of it (‘curried application’), but we do not assume either Φ ∘ Ψ = id or Ψ ∘ Φ = id in this structure. This λ-structure is just a redefinition of the λ-calculus, that is, a calculus obtained by changing atomic operations from abstraction and application to −^{∗}−, Ψ, and Φ. But this makes a categorical structure clearer as will be seen in section 5.

The extension of the above λ-structure is a tuple ⟨T, ⇝, {D_{a}}_{a∈T} , [−], [−−]⟩ where T is a non-empty set, ⇝ is a function T × T ⟶ T, {D_{a}}_{a∈T} is a family of sets indexed by T. We write D_{a_{1},... ,a_{n}} for the set {e_{1} … e_{n} | e_{i} ∈ D_{a_{i}}}. [−] is an operation that converts A ∈ T to an element of T which satisfies the following condition.

• [A → B] = [A] ⇝ [B]

[− −] is an operation that makes f ∈ C_{B}^{E} a set-theoretical function from D_{E} to D_{B}, that is, satisfies the following condition.

(F) for all \overline{e} ∈ D_{E}, [f \overline{e}] ∈ D_{B}

We define the interpretation of simply typed λ-calculus in a λ-structure and its extension. We define the interpretation of types and contexts by

• [[σ]] =^{def} σ

• [[x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}]] =^{def} [[σ_{1}]], …, [[σ_{n}]]

and define the interpretation of terms as follows.

• [[Γ ⊢ x^{σ}]] =^{def} (id^{[[Γ]]})_{i} : [[Γ]] ⟶ [[σ]] if x^{σ} is the i-th element of Γ

• [[Γ ⊢ λx^{σ}.M]] =^{def} Ψ[[Γ, x^{σ} ⊢ M]] if [[Γ, x^{σ} ⊢ M]] is defined

• [[Γ ⊢ app(σ → τ, M, N)]] =^{def} [[Γ ⊢ N]]^{∗}Φ[[Γ ⊢ M]]

if [[Γ ⊢ M]] : [[Γ]] ⟶ [[σ → τ]] and [[Γ ⊢ N]] : [[Γ]] ⟶ [[σ]]

Theorem 3.1 (soundness) If Γ ⊢ M : σ, then [[Γ ⊢ M]] : [[Γ]] ⟶ [[σ]], therefore, for all \overline{e} ∈ D_{[[Γ]]}, [[[Γ ⊢ M]] \overline{e}] ∈ D_{[[[σ]]]}.

4 Simple Term Model

Let Λ_{0} be the set of all untyped λ-terms and M̂ be the untyped λ-term obtained by stripping the type annotations of M ∈ Λ. P is called a domain property if P is a predicate on Λ_{0} that satisfies the following condition.

(P1) if P (M[x := N]) and P (N), then P (λx.M)

An untyped λ-term M is called a P -value if P (M) holds. A P -typeset is a set a of P -values that satisfies the following condition.

(T1) if N_{i} is a P -value (n ≥ 1, 1 ≤ i ≤ n) and M_{0}[x := N_{1}]N_{2} ⋯ N_{n} ∈ a, then (λx.M_{0})N_{1}N_{2} ⋯ N_{n} ∈ a

We define the operation ⇝ on P -typesets as follows.

a ⇝ b =^{def} {M | M is a P -value, and for all N ∈ a, MN ∈ b}

Let P be a domain property and T be a non-empty family of P -typesets that is closed under ⇝. From T, we will define the λ-structure and its extension simultaneously. We assume an element of T is associated to each base type and define [A → B] =^{def} [A] ⇝ [B]. An expression of the form \overline{γ}|M is called an arrow code if \overline{γ} is a sequence of variables and M is an untyped term whose free variables are in \overline{γ}. We define the extension by

• D_{a} =^{def} a

• [\overline{γ}|M \overline{e}] =^{def} M[\overline{γ} := \overline{e}]

and λ-structure as follows.

• C_{B}^{A_{1},... ,A_{n}} =^{def} \{\overline{γ}|M | length of \overline{γ} is n and \overline{γ}|M satisfies (F)\}

• (id^{A_{1},... ,A_{n}})_{i} =^{def} x_{1} ⋯ x_{n}|x_{i}

• (\overline{γ}|N)^{∗}(\overline{γ}x|M) =^{def} \overline{γ}|M[x := N]

• Ψ(\overline{γ}x|M) =^{def} \overline{γ}|λx.M, Φ(\overline{γ}|M) =^{def} \overline{γ}x|Mx (x ∉ F V (M))

We will write D_{A} for D_{[A]} and D_{A⇝B} for D_{[A]⇝[B]}. It is easy to check [[Γ ⊢ M]] = Γ̂|M̂ from these definitions. Here, we have to check that (R), (A1), (A2) are satisfied, that is, in the case of (R), we have to check that if [f \overline{e}d] ∈ D_{C} for \overline{e}d ∈ D_{E,A} and [g \overline{e}] ∈ D_{A} for \overline{e} ∈ D_{E}, then [g^{∗}f \overline{e}] ∈ D_{C} for \overline{e} ∈ D_{E}. (R) and (A2) holds, but it depends on T and P whether (A1) satisfied or not. However, we have the following proposition.

Proposition 4.1 (R) is satisfied. proof Suppose \overline{γ}x|M ∈ C_{C}^{E,A} and \overline{γ}|N ∈ C_{A}^{E}, that is, M[\overline{γ}x := \overline{e}d] ∈ D_{C} for \overline{e}d ∈ D_{E,A} and N[\overline{γ} := \overline{e}] ∈ D_{A} for \overline{e} ∈ D_{E}. Because M[x := N][\overline{γ} := \overline{e}] ≡ M[\overline{γ}x := \overline{e}N[\overline{γ} := \overline{e}]] ∈ D_{C}, (\overline{γ}|N)^{∗}(\overline{γ}x|M)[\overline{γ} := \overline{e}] ∈ D_{C}, that is, (\overline{γ}|N)^{∗}(\overline{γ}x|M) ∈ C_{C}^{E} holds. □

Proposition 4.2 (A2) is satisfied. proof Suppose \overline{γ}|M ∈ C_{A→C}^{E}, that is, M[\overline{γ} := \overline{e}] ∈ D_{A⇝C} for \overline{e} ∈ D_{E}. By the definition of ⇝, we have M[\overline{γ} := \overline{e}]d ∈ D_{C} for d ∈ D_{A}. Therefore, Φ(\overline{γ}|M)[\overline{γ}x := \overline{e}d] ∈ D_{C}, that is, Φ(\overline{γ}|M) ∈ C_{C}^{E,A}. □

Proposition 4.3 If each typeset in T is non-empty, (A1) is satisfied. proof Suppose \overline{γ}x|M ∈ C_{C}^{E,A}, that is, M[\overline{γ}x := \overline{e}d] ∈ D_{C} for \overline{e} ∈ D_{E} and d ∈ D_{A}. Since D_{A} is non-empty and M[\overline{γ} := \overline{e}][x := d] is a P -value, λx.M[\overline{γ} := \overline{e}] is a P -value by (P1). On the other hand, we have (λx.M[\overline{γ} := \overline{e}])d ∈ D_{C} by (T1), therefore, λx.M[\overline{γ} := \overline{e}] ∈ D_{A⇝C}, that is, \overline{γ}|λx.M = Ψ(\overline{γ}x|M) ∈ C_{A→C}^{E}. □

A typeset that contains variables is not only non-empty but useful in proving the properties of the calculus. A family of such typesets can be obtained from P that satisfy the following zeroset condition.

(Z) if N_{i} is a P -value (n ≥ 0, 1 ≤ i ≤ n), then xN_{1} ⋯ N_{n} is a P -value We define the P -zeroset by {xN_{1} ⋯ N_{n} | n ≥ 0, N_{i} is a P -value (1 ≤ i ≤ n)} and put T_{z}^{P} =^{def} {a | a is a P -typeset, a ⊇ P -zeroset}.

Theorem 4.4 Suppose the structure defined above is a λ-structure and its extension, and T ⊆ T_{z}^{P}. If Γ ⊢ M : σ, then P (M̂). proof Let Γ ≡ x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}. Since x_{1} … x_{n} ∈ D_{[[Γ]]} by T ⊆ T_{z}^{P}, M̂ = [[[Γ ⊢ M]] x_{1} … x_{n}] ∈ D_{[[σ]]} by Theorem 3.1. Therefore, P (M̂). □

Proposition 4.5 If P satisfies the following condition

(P2) if N_{i} is a P -value (n ≥ 1, 1 ≤ i ≤ n) and P (M_{0}[x := N_{1}]N_{2} ⋯ N_{n}), then P ((λx.M_{0})N_{1} ⋯ N_{n})

then T_{z}^{P} is non-empty and closed under ⇝. proof (non-emptiness) We will show {M | M is a P -value} ∈ T_{z}^{P}. It is clear this set contains zeroset and by (P2) this set satisfies (T1). (closedness) Suppose a, b ∈ T_{z}. First, we will show a ⇝ b satisfies (T1). Suppose N_{i} is a P -value (n ≥ 1, 1 ≤ i ≤ n) and M_{0}[x := N_{1}]N_{2} ⋯ N_{n} ∈ a ⇝ b. By the definition of ⇝, M_{0}[x := N_{1}]N_{2} ⋯ N_{n}d ∈ b for d ∈ a and P (M_{0}[x := N_{1}]N_{2} ⋯ N_{n}). By (T1) for b, (λx.M_{0})N_{1} ⋯ N_{n}d ∈ b for d ∈ a, and by (P2), P ((λx.M_{0})N_{1} ⋯ N_{n}). Therefore, (λx.M_{0})N_{1} ⋯ N_{n} ∈ a ⇝ b. Next, we will show a ⇝ b ⊇ zeroset, that is, xN_{1} ⋯ N_{n} ∈ a ⇝ b if N_{i} is a P -value. Since b contains zeroset, xN_{1} ⋯ N_{n}d ∈ b for d ∈ a. By (Z), P (xN_{1} ⋯ N_{n}). Therefore, xN_{1} ⋯ N_{n} ∈ a ⇝ b. □

Now, we are prepared to give an example by which we can prove the strong normalizability of well-typed terms. Let

P_{sn}(M) =^{def} ‘M is strongly normalizable’, T_{z} =^{def} T_{z}^{P_{sn}}

then, it is clear that P_{sn} is a domain property and satisfies (Z). To show the non-emptiness and the closedness of T_{z}, we need the following well-known lemma which is used in all (as far as we know) proofs of strong normalizability and from Proposition 4.7 and Theorem 4.4, we have Theorem 4.8.

Lemma 4.6 If N_{i} (n ≥ 1, 1 ≤ i ≤ n) and M_{0}[x := N_{1}]N_{2} ⋯ N_{n} are strongly normalizable, then (λx.M_{0})N_{1} ⋯ N_{n} is strongly normalizable.

Proposition 4.7 T_{z} is non-empty and closed under ⇝. proof By Lemma 4.6, P_{sn} satisfies (P2). □

Theorem 4.8 If Γ ⊢ M : σ, then M is strongly normalizable.

Note that the conditions for typesets that a typeset contains zeroset and satisfies (T1) corresponds to the conditions for the saturated set. It may be worth while mentioning that in the case of the normalizability (P2) is trivial and other conditions can be checked similarly to the case of strong normalizability. We give another example: let

R_{ol} =^{def} ‘the outermost leftmost reduction’, P_{ol}(M) =^{def} R_{ol}(M)↓

then, P_{ol} and T_{z}^{P_{ol}} forms a λ-structure for the theorem ‘well-typed terms have outermost leftmost normal form’.

In the BMM-model^{3}, β-equal terms have the same meaning, but in our λ-structure it does not hold because Φ ∘ Ψ = id does not necessarily hold. But we will show in the next section that λ-structure is a substructure of our structure in which β-equal terms have the same meaning.

5 Categorical Model

To make a model that respects β(η)-equality, PER is a convenient tool. We will make a model in which closed types are interpreted as PERs. Of course, such kinds of models of λ2 are well-known and it is shown that proof of strong normalizability can be carried out in that kind of model^{5}. However, as we have stated in the introduction, we want to make a model that respects β-equality strictly. For that purpose, the notion of semi-adjoint ^{4,7} provides the right setting. In section 5.2, we will define a structure which incorporates the idea of using semi-adjoint to define exponentials (function space). The structure is a λ2-version of λ1-category^{8}, and can also be regarded as a multicategory-version (but arrows and codomains are sequences) of PL-category (but semi-adjoints are used instead of adjoints). In section 6, we will make examples of the structure using PERs on terms, in which we can prove strong normalizability and uniqueness of normal form.

5.1 preliminaries

Our model is based on the comprehension category^{6,9}, but to avoid requiring preliminaries from the theory of comprehension category, we only give the specialized case of general definitions related to the comprehension category.

Let 𝔼 and 𝔹 be categories, p : 𝔼 ⟶ 𝔹 be a functor, and T be a subset of Obj(𝔼) such that E ∈ Obj(𝔼) and X ∈ T has a product if pE = pX. 𝔼//T is a category whose objects are pairs E; X where E ∈ Obj(𝔼) and X ∈ T with pE = pX, and arrows are [f, g] : E; X ⟶ E′; X′ where f : E ⟶ E′ and g : E × X ⟶ X′ with pf = pg. We define the composition of two arrows

[f, g] : E; X ⟶ E′; X′ and [h, k] : E′; X′ ⟶ E′′; X′′ by [h, k] ∘ [f, g] =^{def}

[h ∘ f, k ∘ ⟨f ∘ π_{1}, g⟩] and identity on E; X by [id_{E}, π_{2}]. We call 𝔼//T a context category over p. (𝔼//T)_{E} is a category whose objects are E; X and arrows are [id_{E}, g].

We need some more preliminaries from the theory of semi-functor and semi-adjunction. A semi-functor F : ℂ ⟶ 𝔻 is a pair of a function from Obj(ℂ) to Obj(𝔻) and a function from ℂ(X, Y) to 𝔻(F X, F Y) that preserve compositions: F (f ∘ g) = F (f) ∘ F (g) (that is, a semi-functor is a functor that does not necessarily preserve identities). A semi-functor G : 𝔻 ⟶ ℂ is a right semi-adjoint of a semi-functor F : ℂ ⟶ 𝔻, if there are collections of functions {Ψ_{X,Y} , Φ_{X,Y} }_{X∈ℂ,Y ∈𝔻} such that the four squares in the following diagram commute.

[figure: Y; 𝔻(F X, Y); Ψ_{X,Y}; \underline{Φ_{X,Y}}; ℂ(X, GY); X; Y′; f; 𝔻(F X′, Y′); f ∘ − ∘ F g; Ψ_{X′,Y′}; \underline{Φ_{X′,Y′}}; ℂ(X′, GY′); Gf ∘ − ∘ g; X′; g]

We have the following lemma^{7}.

Lemma 5.1 If F is a functor and G is its right semi-adjoint, then (1) Φ ∘ Ψ = id, (2) Ψ(u ∘ F v) = Ψ(u) ∘ v, (3) Φ(u) ∘ F v = Φ(Gid ∘ u ∘ v). proof (1) (Φ∘Ψ)(u) = id∘Φ(Ψ(u))∘F id = Φ(Gid∘Ψ(u)∘id) = id∘u∘F id = u.

(3) Φ(u) ∘ F v = id ∘ Φ(u) ∘ F v = Φ(Gid ∘ u ∘ v). □

5.2 λ2 semi-adjoint structure

In this section, we will define a structure called a λ2 semi-adjoint structure and its set-theoretical interpretation called an extension.

Definition 5.2 A type object family is a family {_{k}T }_{k=0,1,...} where _{k}T is a non-empty set. A type object of arity k is an element of _{k}T and a context object of arity k is a sequence of type objects of arity k. We denote the set of context objects of length l by _{k}T^{l} and the set of context objects by _{k}T^{∗}. (We use the notation (A_{1}, …, A_{l}) for a context object.) For each k, _{k}T^{∗} contains a null sequence _{k}ϵ which is a context object of arity k whose length 0. We will sometimes identify a type object and a context object of length 1 and put T =^{def} {A | A is a type object}.

Definition 5.3 Let T ≡ {_{k}T } be a type object family. 𝔹 is a type category on T if it is a category whose objects are natural numbers k (k = 0, 1, …), arrows 𝔹(l, k) = _{l}T^{k}, k + 1 is a product of k and 1 where we write π|_{1}^{k,1} for its first projection and π|_{2}^{k,1} for its second projection, and 0 is the terminal object. We will sometimes write F^{∗}E for E ∘ F.

Let 𝔼 be a category whose objects are context objects. 𝔼 is a term category on 𝔹 via p, if

(1) p : 𝔼 ⟶ 𝔹 is a functor which maps a context object of arity k to k,

(2) 𝔼 satisfies 𝔼(E, (B_{1}, …, B_{n})) = {(f_{1}, …, f_{n}) | f_{i} ∈ 𝔼(E, B_{i}), pf_{i} = pf_{j}} for B_{i} ∈ _{k}T and 𝔼(E,_{k}ϵ) = ϵ (null sequence),

(3) if E ∈ _{k}T^{∗} and A ∈ _{k}T , then E, A (concatenation) is a product of E and A where we write π|_{1}^{E,A} for its first projection and π|_{2}^{E,A} for its second projection,

(4) for F : l ⟶ k and E ∈ _{k}T^{∗}, there is an arrow \overline{F} E : F^{∗}E ⟶ E which is p-cartesian, that is, for every f : D ⟶ E with pf = F ∘ G, there is a unique g : D ⟶ F^{∗}E such that pg = G and \overline{F} E ∘ g = f

In the following, we will abbreviate 𝔼//T as 𝔼̃. For f : E′ ⟶ E, f^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{E′} is a reindexing functor defined by f^{∗}(E; X) =^{def} E; (pf)^{∗}X and

f^{∗}[id_{E}, g] =^{def} [id_{E′}, g ∘ (f × \overline{pf}X)]. For F : l ⟶ k and f : E′ ⟶ E,

there is an arrow f ∘ \overline{F} E′ : F^{∗}E′ ⟶ E. By (4), there is a unique arrow g : F^{∗}E′ ⟶ F^{∗}E. We write F^{∗}f for the arrow g.

An arrow [id_{E}, g] ∈ 𝔼̃_{E} (arity of E is k) is called a base arrow if dom(g) = E × A, g = g_{0} ∘ π|_{1}^{E,A} for some g_{0}, and 𝔼(_{k}ϵ, A) ≠ ∅. Since g_{0} is uniquely determined (calculate g ∘ ⟨id_{E}, e∘!⟩ for e ∈ 𝔼(_{k}ϵ, A)), we write base(g) for the g_{0}. (Therefore, a base arrow plays the role of a global element.)

We introduce some notations. Let E ∈ _{k}T^{∗}, A ∈ _{k}T , and E′ ∈ _{l}T^{∗}. We

define ↓(E; A) =^{def} π|_{1}^{E,A} : E × A ⟶ E, ^{+}E =^{def} (π|_{1}^{k,1})^{∗}E, ⇓(E) =^{def} \overline{π|_{1}^{k,1}}E :

+E ⟶ E, and for f : E′ ⟶ E in 𝔼, ^{+}f =^{def} (π|_{1}^{k,1})^{∗}f.

Definition 5.4 Suppose 𝔼 is a term category on a type category 𝔹, the following diagram is a pullback in 𝔼, and the reindexing functors q^{∗} and q′^{∗} have right semi-adjoint functors Π_{q} and Π_{q′} respectively. We say (f, f̂, q, q′) satisfies the semi-Beck-Chevalley condition if the following conditions are satisfied.

[figure: Ê′; f̂; Ê; E′; q′; f; E; q]  • f̂^{∗}q^{∗} = q′^{∗}f^{∗} ; • Π_{q′} f̂^{∗} = f^{∗}Π_{q} ; • f^{∗}Ψ_{X,Y} = Ψ_{f^{∗}X,f̂^{∗}Y} f̂^{∗} (X ∈ 𝔼̃_{E}, Y ∈ 𝔼̃Ê) ; • f̂^{∗}Φ_{X,Y} = Φ_{f^{∗}X,f̂^{∗}Y} f^{∗} (X ∈ 𝔼̃_{E}, Y ∈ 𝔼̃Ê)

Definition 5.5 Let 𝔼 be a term category on a type category 𝔹. 𝔼 has semiproducts if

• there exists a right semi-adjoint functor Π_{E;A} : 𝔼̃_{E,A} ⟶ 𝔼̃_{E} of a reindexing functor ↓(E; A)^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{E,A}, and for any f : E′ ⟶ E and A (pE = pA), (f, f × \overline{pf}A, ↓(E; A), ↓(E′; (pf)^{∗}A)) satisfies the semi-Beck-Chevalley condition.

• there exists a right semi-adjoint functor Π_{^{+}E} : 𝔼̃_{^{+}E} ⟶ 𝔼̃_{E} of a reindexing functor ⇓(E)^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{^{+}E}, and for any f : E′ ⟶ E, (f,^{+}f, ⇓(E), ⇓(E′)) satisfies the semi-Beck-Chevalley condition.

Proposition 5.6 Reindexing functors and Ψ and Φ of above semi-adjunctions map base arrows to base arrows. proof For reindexing functor, use the definition. For Ψ and Φ, use Lemma 5.1 (2) (3).

Proposition 5.7 1) If Π_{E;A}(E, A; B) = E; C and Π_{E′;A}(E′, A; B) = E′; C′, then C = C′.

2) If Π_{^{+}E}(^{+}E; B) = E; C and Π_{^{+}E′}(^{+}E′; B) = E′; C′, then C = C′. proof See Jacobs^{8}.

We write A ⇒ B for the C of 1) and ∇B for the C of 2). By the above Prop, the object-part of Π can be specified by giving A ⇒ B or ∇B.

Definition 5.8 A structure ⟨T, 𝔹, 𝔼, p⟩ is called a λ2 semi-adjoint structure if T is a type object family, 𝔹 is a type category on T, and 𝔼 is a term category on 𝔹 via p that has semi-products. A λ2 semi-adjoint structure is non-trivial if there exists an object _{0}⋆ ∈ _{0}T such that 𝔼(_{0}ϵ,_{0}⋆) ≠ ∅. A λ2 semi-adjoint structure is called a λη2 adjoint structure if its Π_{E;A} and Π_{^{+}E} are functors.

Our λ2 semi-adjoint structure is a natural generalization of PL-category.

Theorem 5.9 A λη2 adjoint structure can be regarded as a PL-category and from a PL-category a λη2 adjoint structure can be constructed. proof A λη2 adjoint structure ⟨T, 𝔹, 𝔼, p⟩ can be regarded as a PL-category as follows. Let 𝔼_{k} be a category whose objects are {E | pE = k} and arrows are {f | pf = id_{k}} and H : 𝔹^{op} ⟶ Cat be a functor which maps k ∈ Obj(𝔹) to 𝔼_{k} and E : l ⟶ k to a functor F^{∗} : 𝔼_{k} ⟶ 𝔼_{l}. Then, (𝔹, H) is a PL-category.

A λη2 adjoint structure ⟨T, 𝔹, 𝔼, p⟩ can be constructed from a PL-category (𝔹, H) (we can assume Obj(𝔹) is the set of natural numbers), by taking _{k}T =^{def} Hk.

Definition 5.10 A type domain is a tuple ⟨T, ⇝, △⟩, where T is a non-empty set, ⇝ is a function T × T ⟶ T, and △ is a function [T ⟶ T] ⟶ T where [T ⟶ T] ⊆ {set-theoretical functions from T to T }. The extension of a λ2 semi-adjoint structure is ⟨⟨T, ⇝, △⟩, {D_{a}}_{a∈T} , [−], [− −]⟩, where {D_{a}}_{a∈T} is a family of sets indexed by T and the following conditions are satisfied. [−] is an operation that converts A ∈ _{k}T to a set-theoretical function [A] : T^{k} ⟶ T which satisfies the following conditions.

• [(id_{k})_{i}](a_{1}, …, a_{k}) = a_{i}

• [A ⇒ B](\overline{a}) = [A](\overline{a}) ⇝ [B](\overline{a})

• [∇C](\overline{a}) = △g where g : b ↦ [C](\overline{a}b) and g ∈ [T ⟶ T]

[− −] is an operation that converts f ∈ 𝔼(E, B) (E ∈ _{k}T^{∗}, B ∈ _{k}T ) to a set-theoretical function [f −] : D_{[E](\overline{a})} ⟶ D_{[B](\overline{a})} which satisfies the fol-

lowing conditions ([(A_{1}, …, A_{n})](\overline{a}) =^{def} [A_{1}](\overline{a}), …, [A_{n}](\overline{a}) and D_{a_{1},... ,a_{n}} =^{def}

{e_{1} … e_{n} | e_{i} ∈ D_{a_{i}}}).

(F1) for all \overline{a} ∈ T^{k} and e_{1} … e_{n} ∈ D_{[E](\overline{a})}, [(id_{E})_{i} e_{1} … e_{n}] = e_{i} (F2) for all \overline{a} ∈ T^{k} and \overline{e} ∈ D_{[E](\overline{a})}, [f \overline{e}] ∈ D_{[B](\overline{a})}

5.3 interpretation

We give an interpretation of λ2 in a non-trivial λ2 semi-adjoint structure. (We put _{k+1}⋆ =^{def} (π|_{1}^{k,1})^{∗}_{k}⋆. Note that 𝔼(_{k}ϵ,_{k}⋆) ≠ ∅.) Let Θ + Γ be a context, σ be a type, and M be a term. By our interpretation, they are interpreted by the following object or arrow in a suitable category.

[[Θ]]  an object of 𝔹
[[Θ + Γ]]  an object of 𝔼
[[Θ + Γ ; σ]] an object of (𝔼//T )_{[[Θ+Γ]]}
[[Θ + Γ | M]] a base arrow of (𝔼//T )_{[[Θ+Γ]]} whose dom is [[Θ + Γ]];_{k}⋆

By the definition of (𝔼//T )_{[[Θ+Γ]]}, [[Θ + Γ ; σ]] is of the form [[Θ + Γ]]; [[σ / Θ + Γ]] where [[σ / Θ + Γ]] ∈ T .

We define [[Θ + Γ]], [[Θ + Γ ; σ]], [[Θ + Γ | M]] inductively by the following clauses. (In the following definition, the length of Θ is k.)

• [[Θ]] =^{def} k

• [[Θ + <>]] =^{def} _{k}ϵ

• [[Θ + Γ, x^{σ}]] =^{def} [[Θ + Γ]], [[σ / Θ + Γ]]

• [[X / Θ + Γ]] =^{def} π|_{2} ∘ π|_{1} ∘ ⋯ ∘ π|_{1} ∈ _{k}T

where X is the i-th type variable in Θ and π|_{1} is composed n − i times

• [[σ → τ / Θ + Γ]] =^{def} [[σ / Θ + Γ]] ⇒ [[τ / Θ + Γ]]

• [[∀X.τ / Θ + Γ]] =^{def} ∇[[τ / Θ, X + Γ]]

• [[Θ + Γ | x^{σ}]] =^{def} [id_{[[Θ+Γ]]}, π|_{2} ∘ π|_{1} ∘ ⋯ ∘ π|_{1}] : [[Θ + Γ]];_{k}⋆ ⟶ [[Θ + Γ ; σ]]

where x^{σ} is the i-th variable in Γ and π|_{1} is composed n − i + 1 times

• [[Θ + Γ | λx^{σ}.M]] =^{def} Ψ_{[[Θ+Γ]];_{k}⋆,cod([[Θ+Γ,x^{σ}|M]])}([[Θ + Γ, x^{σ} | M]])

• [[Θ + Γ | app(σ → τ, M, N)]] =^{def} g^{∗}(Φ_{[[Θ+Γ]];_{k}⋆,[[Θ+Γ,x^{σ};τ]]}[[Θ + Γ | M]])

if [[Θ + Γ | M]] and [[Θ + Γ | N]] have the following form,

where g ≡ base([[Θ + Γ | N]]).

[[Θ + Γ | M]] : [[Θ + Γ]];_{k}⋆ ^{f} [[Θ + Γ ; σ → τ]]
[[Θ + Γ | N]] : [[Θ + Γ]];_{k}⋆  [[Θ + Γ ; σ]]

[figure: [[]];_{k}⋆; f; [[;σ → τ]]; [[x^{σ}]];_{k}⋆; Φf; [[x^{σ} ; τ]]; [[]];_{k}⋆; [[;τ]]; [[]]; [[x^{σ}]]; g; [[]]]

(Θ + Γ is omitted in the above diagram.)

• [[Θ + Γ | ΛX.τ]] =^{def} Ψ_{[[Θ+Γ]];_{k}⋆,cod([[Θ,X+Γ|M]])}([[Θ, X + Γ | M]])

• [[Θ + Γ | app(∀X.τ, M, σ)]] =^{def} g^{∗}(Φ_{[[Θ+Γ]];_{k}⋆,[[Θ,X+Γ;τ]]}[[Θ + Γ | M]])

if [[Θ + Γ | M]] has the following form,

where g ≡ \overline{S}[[Θ, X + Γ]] and S ≡ id_{k}, [[σ / Θ + Γ]] : k ⟶ k + 1 in 𝔹.

[[Θ + Γ | M]] : [[Θ + Γ]];_{k}⋆ ^{f} [[Θ + Γ ; ∀X.τ]]

Remark: Usually, the meaning of application is defined

[[Θ + Γ | app(σ → τ, M, N)]] =^{def} ev ∘ ⟨[[Θ + Γ | M]], [[Θ + Γ | N]]⟩

like this using the cartesian closedness. In our framework, this corresponds to

id_{[[Θ+Γ]]}, [[app(σ → τ, M, N) ← Θ + Γ]] =^{def}

ev ∘ [id_{[[Θ+Γ,x^{σ}]]}, [[M ← Θ + Γ, x^{σ}]]] ∘ [id_{[[Θ+Γ]]}, [[N ← Θ + Γ]]]

where ev ≡ Φ(id). We can show this is equivalent to our definition in the case of λη2 but not necessarily so in the case of λ2.

Theorem 5.11 (soundness) 1) If Θ + Γ ⊢ M : σ, then [[Θ + Γ]], [[Θ + Γ ; σ]], and [[Θ + Γ | M]] are defined and cod([[Θ + Γ | M]]) = [[Θ + Γ ; σ]] in the λ2 semi-adjoint structure.

2) If Θ + Γ ⊢ M = N : σ in λ2, then [[Θ + Γ | M]] = [[Θ + Γ | N]] in the λ2 semi-adjoint structure.

3) If Θ + Γ ⊢ M = N : σ in λη2, then [[Θ + Γ | M]] = [[Θ + Γ | N]] in the λη2 adjoint structure.

6 PER Model

We will give examples of the λ2 semi-adjoint structure which is the term model in which types are interpreted as PERs on terms. We will revise some definitions and conditions in section 4. In the following, πx stands for λx if x is a variable and Λx if x is a type variable. For a PER a, we use the

following notations: [N]_{a} =^{def} {M | N a M}, dom(a) =^{def} {N | N a N},

classes(a) =^{def} {[N]_{a} | N ∈ dom(a)}.

P is called a domain property if P is a predicate on Λ that satisfies the following condition.

(P1) if P (M[x := N]) for some P -value or type N, then P (πx.M)

Let P be a domain property. A P -PER-typeset is a PER a on P -values that satisfies the following conditions.

(T0) if M ∈ dom(a) and M′ is a preterm that differs from M only in type

annotations, then M′ ∈ dom(a) (T1) if N_{i} is a P -value or a type (n ≥ 1, 1 ≤ i ≤ n) and M_{0}[x := N_{1}]N_{2} ⋯ N_{n} ∈

dom(a), then M_{0}[x := N_{1}]N_{2} ⋯ N_{n} a (πx.M_{0})N_{1}N_{2} ⋯ N_{n} (T2) if C_{1}[πx.C_{2}[M]] ∈ dom(a), then C_{1}[πx.C_{2}[M]] a C_{1}[πx.C_{2}[(πx.M)x]] where

C_{i}[] is a context (term with a hole)

Remark: Here, P is a predicate on preterms Λ, but (T0) is added to make it essentially untyped. This change is necessary to prove the uniqueness of normal form. Remark: Note that

C[(λx.M)N] a λu.(C[(λx.M)u])N a λu.C[M[x := u]]N a C[M[x := N]]

holds from (T1) and (T2), if F V (N) = ϕ and the above terms are P -values. Note that it includes the relation that is generated from the closed β-reduction^{5} C[(λx.M)N] → C[M[x := N]] where F V ((λx.M)N) = ϕ. Remark: Let ≈ be the smallest equivalence relation on Λ_{0} that satisfies (untyped version of) (T1) and (T2). Then, Λ_{0}/≈ turns out to be a cpca ^{5} as follows. Let N_{1} ≈ N_{2} where N_{1} ≡ K_{0}[x := L_{1}]L_{2} ⋯ L_{n} and N_{2} ≡ (λx.K_{0})L_{1}L_{2} ⋯ L_{n}. Then, MN_{1} ≈ (λx.MK_{0}L_{2} ⋯ L_{n})L_{1} ≈ (λx.M(λx.K_{0})x L_{2} ⋯ L_{n})L_{1} ≈ M((λx.K_{0})L_{1}L_{2} ⋯ L_{n}) ≡ MN_{2}. Other case are trivial, and k and s are given by k = λxy.x and s = λxyz.xz(yz). Therefore, making a family of P -PER-typesets that satisfies (T3) to (T6) (and (T0)) corresponds to making a family of PERs on that cpca and (T3) corresponds to the weak extensionality of the cpca.

Let ⟨T, ⇝, △⟩ be a type domain where T is a non-empty family of P -PER-typesets that satisfies the following conditions. (Instead of defining ⇝ and △, we list conditions they should satisfy.)

(T3) if a ⇝ b, a ∈ T, M_{1} (a ⇝ b) M_{2}, and N_{1} a N_{2}, then there exists σ → τ

s.t. app(σ → τ, M_{1}, N_{1}) b app(σ → τ, M_{2}, N_{2}) (T4) if a, b ∈ T, M_{1}[x := N_{1}] b M_{2}[x := N_{2}] for all N_{1} a N_{2}, and λx.M_{i} are

P -values, then λx.M_{1} (a ⇝ b) λx.M_{2} (T5) if g ∈ [T ⟶ T], M_{1} (△g) M_{2}, a ∈ T, and τ is a type, then there exists

∀X.σ s.t. app(∀X.σ, M_{1}, τ) (ga) app(∀X.σ, M_{2}, τ) (T6) if g ∈ [T ⟶ T], M_{1}[X := τ] ga M_{2}[X := τ] for all a ∈ T and all types

τ, and ΛX.M_{i} are P -values, then ΛX.M_{1} (△g) ΛX.M_{2}

From the type domain, we will define a λ2 semi-adjoint structure and its extension simultaneously. First, we define D_{a} =^{def} classes(a) for a ∈ T.

(1) Definition of a type object family: A type object of arity k is an expression of the form \overline{θ}|σ where \overline{θ} is a k-sequence of type variables and σ is a type whose free type variables are in \overline{θ}. We define [−] by

• [\overline{θ}|X](a_{1}, …, a_{k}) =^{def} a_{i} where X is the i-th element of \overline{θ}

• [\overline{θ}|σ → τ](\overline{a}) =^{def} [\overline{θ}|σ](\overline{a}) ⇝ [\overline{θ}|τ](\overline{a})

• [\overline{θ}|∀X.τ](\overline{a}) =^{def} △g where g : b ↦ [\overline{θ}X|τ](\overline{a}b) and g ∈ [T ⟶ T]

but it depends on the type domain if g ∈ [T ⟶ T] holds in the last definition.

(2) Definition of a type category 𝔹: For F ≡ (F_{1}, …, F_{l}) : k ⟶ l (= _{k}T^{l}) and G ≡ (G_{1}, …, G_{m}) : l ⟶ m (= _{l}T^{m}) where F_{i} ≡ X_{1} ⋯ X_{k}|σ_{i} and G_{j} ≡ Y_{1} ⋯ Y_{l}|τ_{j}, we define the their composition and identity on k id_{k} as follows.

(G ∘ F)_{j} =^{def} X_{1} ⋯ X_{k}|τ_{j}[Y_{1} ⋯ Y_{l} := σ_{1} ⋯ σ_{l}]
(id_{k})_{i} =^{def} X_{1} … X_{k}|X_{i}

(3) Definition of a term category 𝔼 and p: An expression of the form \overline{θ}\overline{γ}|M is called a tracking code if \overline{θ} is a sequence of type variables, \overline{γ} is a sequence of variables, and M is a term whose free type variables are in \overline{θ} and free variables are in \overline{γ}. For (A_{1}, …, A_{n}) ∈ _{k}T^{n} and B ∈ _{k}T , we define a set Č_{B}^{(A_{1},... ,A_{n})} of tracking codes as follows. Let \overline{a} ∈ T^{k}, N_{i} ∈ dom([A_{i}](\overline{a})), the length of \overline{θ} be k, and the length of \overline{γ} be n. If the function \{\overline{θ}\overline{γ}|M\} defined by

\{\overline{θ}\overline{γ}|M\}(N_{1} … N_{n}) =^{def} M[\overline{γ} := N_{1} … N_{n}]

is well-defined as a function from D_{[A_{1}](\overline{a}),... ,[A_{n}](\overline{a})} to D_{[B](\overline{a})}, that is, N_{i}[A_{i}](\overline{a}) N′_{i} (1 ≤ i ≤ n) imply \{\overline{θ}\overline{γ}|M\}(\overline{N})[B](\overline{a})\{\overline{θ}\overline{γ}|M\}(\overline{N′}), then \overline{θ}\overline{γ}|M ∈ Č_{B}^{(A_{1},... ,A_{n})}. In this case, we use the notation \{\overline{θ}\overline{γ}|M_{1}\}(\overline{e}) or M[\overline{γ} := \overline{e}] to denote the resulting equivalence class. We define an equivalence relation ∼ on Č_{B}^{(A_{1},... ,A_{n})} by

\overline{θ}\overline{γ}|M_{1} ∼ \overline{θ}\overline{γ}|M_{2} =^{def} \{ \begin{matrix}\{\overline{θ}\overline{γ}|M_{1}\}(\overline{e}) = \{\overline{θ}\overline{γ}|M_{2}\}(\overline{e}) \\ for all \overline{a} ∈ T^{k} and \overline{e} ∈ D_{[A_{1}](\overline{a}),... ,[A_{n}](\overline{a})} \end{matrix}

and put C_{B}^{(A_{1},... ,A_{n})} =^{def} Č_{B}^{(A_{1},... ,A_{n})}/∼ and C_{(B_{1},... ,B_{n})}^{E} =^{def} {(s_{1}, …, s_{n}) | s_{i} ∈

C_{B_{i}}^{E}}.

For E ∈ _{k}T^{n}, E′ ∈ _{k}T^{m}, E′′ ∈ _{k}T^{l}, [\overline{θ}\overline{γ}|M]_{∼} ∈ C_{A}^{E}, s ≡ (s_{1}, …, s_{m}) ∈ C_{E′}^{E}, t ≡ (t_{1}, …, t_{l}) ∈ C_{E′′}^{E′}, s_{i} ≡ [\overline{θ}x_{1} ⋯ x_{n}|M_{i}]_{∼}, t_{j} ≡ [\overline{θ}y_{1} ⋯ y_{m}|N_{j}]_{∼}, F ≡ (F_{1}, …, F_{k}) : h ⟶ k, F_{i} ≡ \overline{θ′}|σ_{i}, we define following operations.

(t ∘ s)_{j} =^{def} [\overline{θ}x_{1} ⋯ x_{n}|N_{j}[y_{1} ⋯ y_{m} := M_{1} ⋯ M_{m}]]_{∼}
F^{∗}([\overline{θ}\overline{γ}|M]_{∼}) =^{def} [\overline{θ′}\overline{γ}[\overline{θ} := \overline{σ}]|M[\overline{θ} := \overline{σ}]]_{∼}  F^{∗}s =^{def} (F^{∗}s_{1}, …, F^{∗}s_{m})

Note that the definitions of ∘ and ^{∗} do not depend on the choice of the representative of the equivalence class of ∼, but for the definition of composition in 𝔼 work, the following condition should be satisfied.

(C) t ∘ s ∈ C_{E′′}^{E} and F^{∗}([\overline{θ}\overline{γ}|M]_{∼}) ∈ C_{F^{∗}A}^{F^{∗}E}

An arrow in 𝔼 from E ∈ _{k}T^{∗} to E′ ∈ _{l}T^{∗} is a pair (F, s) where F : l ⟶ k in 𝔹 and s ∈ C_{F^{∗}E}^{E′}. For arrows f ≡ (F, s) : E′′ ⟶ E′ and g ≡ (G, t) : E′ ⟶ E, we define their composition by g ∘ f =^{def} (G ∘ F, (F^{∗}t) ∘ s). Then,

identity on E id_{E} ≡ (id_{k}, id^{E}) is given by (id^{E})_{i} =^{def} [X_{1} ⋯ X_{k}x_{1}^{σ_{1}} ⋯ x_{n}^{σ_{n}}|x_{i}^{σ_{i}}]_{∼}

(E ≡ (A_{1}, …, A_{n}) and A_{i} ≡ X_{1} ⋯ X_{k}|σ_{i}) and the function p that maps a context object of arity k to k and a arrow (F, s) to its first component F is a functor p : 𝔼 ⟶ 𝔹. We define \overline{F} E by \overline{F} E =^{def} (F, id^{F^{∗}E}) : F^{∗}E ⟶ E. Then,

for f ≡ (F, s) : E′ ⟶ E where F : l ⟶ k, ^{+}f =^{def} (F × id_{1}, (π|_{1}^{l,1})^{∗}s) holds.

For (F, s) ∈ 𝔼(E, B) (E ∈ _{k}T^{∗}, B ∈ _{k}T ), we define [− −] by [(F, s) \overline{e}] =^{def}

\{\overline{θ′}\overline{γ′}|M′\}(\overline{e}) where \{\overline{θ′}\overline{γ′}|M′\}(\overline{e}) ≡ F^{∗}s.

(4) Definition of semi-adjointness: The object-parts of Π are defined by the following.

• (\overline{θ}|σ) ⇒ (\overline{θ}|τ) =^{def} \overline{θ}|σ → τ

• ∇(\overline{θ}X|τ) =^{def} \overline{θ}|∀X.τ

The following Π, Ψ, and Φ which determine the mappings of arrows are defined on tracking codes, but we will show in Prop. 6.1 that they are well-defined.

• Π_{E;A}(\overline{θ}\overline{γ}x^{σ}y^{τ} |M) =^{def} \overline{θ}\overline{γ}z^{σ→τ} |λx^{σ}.M[y^{τ} := app(σ → τ, z^{σ→τ} , x^{σ})]

(z^{σ→τ} ∉ F V (M), \overline{θ}\overline{γ}x^{σ}y^{τ} |M ∈ C_{C}^{E,\overline{θ}|σ,\overline{θ}|τ})

• Ψ(\overline{θ}\overline{γ}x^{σ}y|M) =^{def} \overline{θ}\overline{γ}y|λx^{σ}.M (\overline{θ}\overline{γ}x^{σ}y|M ∈ C_{C}^{E,\overline{θ}|σ,B})

• Φ(\overline{θ}\overline{γ}y|M) =^{def} \overline{θ}\overline{γ}x^{σ}y|app(σ → τ, M, x^{σ})

(x^{σ} ∉ F V (M), \overline{θ}\overline{γ}y|M ∈ C_{\overline{θ}|σ→τ}^{E,B})

• Π_{^{+}E}(\overline{θ}X\overline{γ}y^{τ} |M) =^{def} \overline{θ}\overline{γ}z^{∀X.τ} |ΛX.M[y^{τ} := app(∀X.τ, z^{∀X.τ} , X)]

(z^{∀X.τ} ∉ F V (M), \overline{θ}X\overline{γ}y^{τ} |M ∈ C_{C}^{^{+}E,\overline{θ}X|τ})

• Ψ(\overline{θ}X\overline{γ}y|M) =^{def} \overline{θ}\overline{γ}y|ΛX.M (\overline{θ}X\overline{γ}y|M ∈ C_{C}^{^{+}E,B})

• Φ(\overline{θ}\overline{γ}y|M) =^{def} \overline{θ}X\overline{γ}y|app(∀X.τ, M, X)

(X ∉ T F V (M), \overline{θ}\overline{γ}y|M ∈ C_{\overline{θ}|∀X.τ}^{E,B})

The structures defined above will constitute a λ2 semi-adjoint structure and its extension if some conditions stated below are satisfied. We will denote them by PT (⟨T, ⇝, △⟩) and PT(⟨T, ⇝, △⟩).

Proposition 6.1 PT (⟨T, ⇝, △⟩) and PT(⟨T, ⇝, △⟩) is a λ2 semi-adjoint structure and its extension, if each P -PER-typeset in T is non-empty, [−] is welldefined, and the condition (C) is satisfied. proof We have to check that Π, Ψ, Φ defined in (4) satisfies the semi-adjoint conditions and the semi-Beck-Chevalley conditions. We will prove only the case of Π_{E;A}, but the case of Π_{^{+}E} can be proved similarly.

First, we will show Π_{E;A} is defined without depending on the choice of the representative, that is, if [\overline{θ}\overline{γ}xy|M_{1}]_{∼} : E, A; B ⟶ E, A; C and \overline{θ}\overline{γ}xy|M_{1} ∼ \overline{θ}\overline{γ}xy|M_{2}, then [\overline{θ}\overline{γ}z|λx.M_{1}[y := zx]]_{∼} : E; A ⇒ B ⟶ E; A ⇒ C and \overline{θ}\overline{γ}z|λx.M_{1}[y := zx] ∼ \overline{θ}\overline{γ}z|λx.M_{2}[y := zx]. Suppose M_{1}[\overline{γ}xy := \overline{e}dd′] [C](\overline{a}) M_{2}[\overline{γ}xy := \overline{e}dd′] for \overline{a} ∈ T^{k}, \overline{e} ∈ D_{[E](\overline{a})}, d ∈ D_{[A](\overline{a})}, and d′ ∈ D_{[B](\overline{a})}, and take g ∈ D_{[A⇒B](\overline{a})}. Then gd ∈ D_{[B](\overline{a})} by (T3) and M_{i}[y := gx][\overline{γ} := \overline{e}][x := d] are P -values. Therefore, by (P1) and (T4), λx.M_{1}[y := gx][\overline{γ} := \overline{e}] [A ⇒ C](\overline{a}) λx.M_{2}[y := gx][\overline{γ} := \overline{e}].

For Ψ and Φ, we can prove non-dependency similarly. Therefore, we will omit [ ]_{∼} in the following.

Next, we will show Π_{E;A} is a semi-functor. Let f ≡ \overline{θ}\overline{γ}xy|M : E, A; B ⟶ E, A; C and g ≡ \overline{θ}\overline{γ}xu|N : E, A; C ⟶ E, A; D. (\overline{θ} and some type annotations are omitted below.)

Π(f ∘ g) = Π(\overline{γ}xy|N[u := M]) = \overline{γ}z|λx.N[u := M][y := zx]
= \overline{γ}z|λx.N[u := M[y := zx]]
Π(f) ∘ Π(g) = (\overline{γ}z|λx.M[y := zx]) ∘ (\overline{γ}w|λx.N[y := wx])
= \overline{γ}z|λx.N[u := (λx.M[y := zx])x]

Above two arrows are equal, because for \overline{a} ∈ T^{k}, \overline{e} ∈ D_{[E](\overline{a})}, c ∈ D_{[A→B](\overline{a})}

(λx.N[u := M[y := zx]])[\overline{γ}z := \overline{e}c] = (λx.N[u := (λx.M[y := zx])x])[\overline{γ}z := \overline{e}c]

holds by (T2).

Third, we will show Π_{E;A} is a right semi-adjoint functor of a reindexing functor ↓(E; A)^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{E,A}. Note that

↓(E; A) = (\overline{θ}\overline{γ}x|γ_{1}, …, \overline{θ}\overline{γ}x|γ_{n}) where \overline{γ} ≡ (γ_{1}, …, γ_{n})
↓(E; A)^{∗}(\overline{θ}\overline{γ}y|N) = \overline{θ}\overline{γ}xy|N ↓(E; A)^{∗}(\overline{θ}\overline{γ}|N) = \overline{θ}\overline{γ}x|N

holds. In the diagram in section 5.1, put ℂ ≡ 𝔼̃_{E}, 𝔻 ≡ 𝔼̃_{E,A}, X ≡ E; B, X′ ≡ E; B′, Y ≡ E, A; C, Y′ ≡ E, A; C′, F ≡ ↓(E; A)^{∗}, G ≡ Π_{E;A}.

[figure: E, A; C; 𝔼̃_{E,A}(E, A; B, E, A; C); Ψ; \underline{Φ}; 𝔼̃_{E}(E; B, E; A → C); E; B; E, A; C′; f; 𝔼̃_{E,A}(E, A; B′, E; C′); f ∘ − ∘ ↓(E; A)^{∗}g; Ψ; \underline{Φ}; 𝔼̃_{E}(E; B′, E; A → C′); Π_{E;A}f ∘ − ∘ g; E; B′; g]

We show the commutativity of only one square, but other cases are similar. Let f ≡ \overline{θ}\overline{γ}xy|M, g ≡ \overline{θ}\overline{γ}u|N, h ≡ \overline{θ}\overline{γ}y|H where h ∈ 𝔼̃_{E,A}(E, A; B, E, A; C).

Φ(Πf ∘ Ψh ∘ g) = Φ((\overline{γ}z|λx.M[y := zx]) ∘ (\overline{γ}y|λx.H) ∘ (\overline{γ}u|N))
= Φ(\overline{γ}u|(λx.M[y := zx])[z := λx.H][y := N])
= Φ(\overline{γ}u|λx.M[y := (λx.H)x][y := N])
= \overline{γ}xu|(λx.M[y := (λx.H)x][y := N])x
f ∘ h ∘ ↓(E; A)^{∗}g = (\overline{γ}xy|M) ∘ (\overline{γ}xy|H) ∘ (\overline{γ}xu|N) = \overline{γ}xu|M[y := H][y := N]

These two arrows are equal by (T1) and (T2).

The semi-Beck-Chevalley conditions can be proved similarly. □

Proposition 6.2 Suppose PT (⟨T, ⇝, △⟩) and PT(⟨T, ⇝, △⟩) is a λ2 semiadjoint structure and its extension. Then [[Θ + Γ ⊢ M]] = [ΘΓ|M]_{∼}.

We re-define the zeroset condition as follows

(Z) if N_{i} is a P -value or a type, then xN_{1} ⋯ N_{n} is a P -value

and re-define the P -zeroset by {xN_{1} ⋯ N_{n} | n ≥ 0, N_{i} is a P -value or a type (1 ≤ i ≤ n)} and put T_{z}^{P} =^{def} {a | a is a P -PER-typeset, dom(a) ⊇ P -zeroset}.

Theorem 6.3 Suppose PT (⟨T, ⇝, △⟩) and PT(⟨T, ⇝, △⟩) is a λ2 semi-adjoint structure and its extension, and T ⊆ T_{z}^{P}. If Θ + Γ ⊢ M = N : σ in λ2, then M b N (therefore P (M) and P (N)), where b ≡ [[[σ / Θ + Γ]]](a_{1}, …, a_{k}) and a_{i} are arbitrary elements of T. proof Similarly to the proof of Theorem 4.4, we have M bN by Theorem 5.11. □

Example: uniqueness of normal form

We say a term M is a function code from PER a to PER b, if for all c ∈ classes(a) there exists d ∈ classes(b) such that for all N ∈ c there exists σ → τ s.t. app(σ → τ, M, N) ∈ d. Let a, b be PERs, T a family of PERs, and f be a function from T to the set of PERs.

a ⇝_{i} b =^{def} {M | M is a P -value, M is a function code from a to b}
∩f =^{def} ⋂_{a∈T} fa (intersection of PERs fa)

△_{i}f =^{def} \{M | \begin{matrix}M is a P -value, \\ and for all types τ there exists ∀X.σ \\ s.t. app(∀X.σ, M, τ) ∈ dom(∩f) \end{matrix} \}

When a partial function R : Λ ⇀ Λ is given, we will write M R N for the PER defined by R(M) = R(N). Let R_{ol} be a function that does outermost

leftmost reduction and put P (M) ≡ P_{ol}(M) =^{def} R_{ol}(M)↓, T ≡ T_{iβ} =^{def} {a | a ∈

T_{z}^{P_{ol}}, a = dom(a)/R_{ol}}, a ⇝_{iβ} b =^{def} (a ⇝_{i} b)/R_{ol}, △_{iβ}f =^{def} △_{i}f/R_{ol}.

Proposition 6.4 ⟨T_{iβ}, ⇝_{iβ}, △_{iβ}⟩ is a type domain. proof First, note that (T1) and (T2) are easily proved for the relation R_{ol}. (non-emptiness) Clearly, {M | M is a P_{ol}-value}/R_{ol} ∈ T_{iβ}. (closedness under ⇝_{iβ}) Suppose a, b ∈ T_{iβ}. a ⇝_{iβ} b = dom(a ⇝_{iβ} b)/R_{ol} holds by the definition of ⇝_{iβ}. We can show dom(a ⇝_{iβ} b) ⊇ zeroset similarly to the proof of proposition 4.5. (closedness under △_{iβ}) Similar to the case of ⇝_{iβ}. □

Proposition 6.5 PT (⟨T_{iβ}, ⇝_{iβ}, △_{iβ}⟩) and PT(⟨T_{iβ}, ⇝_{iβ}, △_{iβ}⟩) is a λ2 semiadjoint structure and its extension.

Theorem 6.6 If Θ + Γ ⊢ M = N : σ in λ2, then M and N have the common β-normal form. Therefore, β-equal terms have the unique β-normal form. proof By Th. 6.3, M b N holds for some b ∈ T_{iβ}. Therefore, MR_{ol} N, that is, R_{ol}(M) = R_{ol}(N) holds. □

Example: strong normalizability

To prove SN, a weaker structure than λ2 semi-adjoint structure is enough as we have shown in section 4. But it is also interesting to investigate how rich structure we can make from SN terms. We will make a λη2 adjoint structure in which we can carry out the proof of SN.

M_{1}(a ⇝_{e} b)M_{2} =^{def} \{ \begin{matrix}M_{i} is a P -value (i = 1, 2), \\ and for all N_{1} a N_{2} there exists σ → τ \\ s.t. app(σ → τ, M_{1}, N_{1}) b app(σ → τ, M_{2}, N_{2}) \end{matrix}

M_{1}(△_{e}f)M_{2} =^{def} \{ \begin{matrix}M_{i} is a P -value (i = 1, 2), \\ and for all types τ there exists ∀X.σ \\ s.t. app(∀X.σ, M_{1}, τ) (∩f) app(∀X.σ, M_{2}, τ) \end{matrix}

Put P (M) ≡ P_{sn}(M) =^{def} ‘M is strongly normalizing’, T ≡ T_{sn} =^{def} {a | a ∈ T_{z}^{P_{sn}}, and if N, N′ ∈ P_{sn}-zeroset then N a N′}.

Proposition 6.7 ⟨T_{sn}, ⇝_{e}, △_{e}⟩ is a type domain.

Proposition 6.8 PT (⟨T_{sn}, ⇝_{e}, △_{e}⟩) and PT(⟨T_{sn}, ⇝_{e}, △_{e}⟩) is a λη2 adjoint structure and its extension.

Acknowledgments

I would like to thank Masahito Hasegawa and one of the referees for helpful comments.

References

1. T. Altenkirch, Proving Strong Normalization of CC by Modifying Realizability Semantics, In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, LNCS 806, pages 3 – 18, 1994.

2. K. B. Bruce and A. R. Meyer, The Semantics of second-order Polymorphic Lambda Calculus, In Proc. Conf. on Semantics of Data Types, LNCS 173, 1984.

3. K. B. Bruce, A. R. Meyer, and J. C. Mitchell, The Semantics of secondorder Lambda Calculus, Information and Computation, 85:76–134, 1990.

4. S. Hayashi, Adjunction of Semifunctors: Categorical structures in nonextensional lambda calculus, Theoretical Computer Science, 41:95–104, 1985.

5. J. M. E. Hyland and C.-H. L. Ong, Modified Realizability Toposes and Strong Normalization Proofs (extended abstract), In Proc. of Typed Lambda Calculi and Applications, LNCS 664, 1993.

6. B. Jacobs, Categorical Type Theory, PhD thesis, Univ. Nijmegen, 1991.

7. B. Jacobs, Semantics of second-order Lambda Calculus, Mathematical Structures in Computer Science, 1:327–360, 1991.

8. B. Jacobs, Simply typed and untyped Lambda Calculus revisited, In Applications of Categories in Computer Science, LMS Lecture Note Series 177, pages 119–142, 1992.

9. B. Jacobs, Comprehension Categories and the Semantics of Type Dependency, Theoretical Computer Science, 107:169–207, 1993.

10. R. A. G. Seely, Categorical Semantics of higher-order Polymorphic Lambda Calculus, J. Symb. Log., 52:969–989, 1987.

11. M. Stefanova and H. Geuvers, A Simple Model Construction for the Calculus of Constructions, In Proc. Int. Workshop TYPES ’95, LNCS 1158, pages 249–264, 1996.