Categorical Model Construction for Proving Syntactic Properties ^{∗}

Takafumi SAKURAI

          sakurai@math.s.chiba-u.ac.jp

Department of Mathematics and Informatics Chiba University

Abstract

It is observed that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction. The observation is clarified by the works of Hyland and Ong [8], Altenkirch [2], Stefanova and Geuvers [15], and so on. The model of Hyland and Ong is based on PL-category [14] and the model of Altenkirch or Stefanova and Geuvers is a non-categorical model that is specially designed for this purpose. In this paper, we will construct yet another categorical model for the second order λ-calculus — a non-extensional PL-category. To demonstrate the significance of the non-extensional model, we will give a model in which we can carry out the proof of the uniqueness of the βnormal form. The non-extensionality comes from the use of semi-adjoint for interpretation of abstraction and application (uncurry).

1 Introduction

It is observed that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction. The observation is clarified by several kinds of categorical or semantical frameworks. Here we will pick up two of them. Hyland and Ong [8] constructed a model that is an instance of the categorical model known as PL-category [14] for the second order λ-calculus. Altenkirch [2] and Stefanova and Geuvers [15] constructed models for CoC motivated by this observation, but it is not known whether they are instances of some categories. However, Stefanova and Geuvers’s model (restricted to the second order λ-calculus) cannot be an instance of the PLcategory, because it is non-extensional whereas PL-category is extensional. The purpose of this paper is to present a structure for the second order λ-calculus which is a non-extensional version of PL-category.

∗This is a corrected version of the paper:

T. Sakurai. Categorical Model Construction for Proving Syntactic Properties.

International Journal of Foundations of Computer Science, 20(12):213–244, 2001.

Roughly speaking, Hyland and Ong constructed a PL-category using SN terms, that is, types are interpreted as PERs (with additional information) on cpca which is the quotient set of SN terms and terms represent functions on equivalence classes of the PERs. To demonstrate the significance of the non-extensional model, we will 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 that we can escape from the difficulty by weakening the PL-category, that is, by using semi-adjoint [7, 9] 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. In this process, it is clarified what extra conditions other than saturated-set conditions are necessary to make the model categorical.

Besides the non-extensionality, our construction is different from the usual one in that we make the model using the theory of fibration over fibration [11, 12]. (But we do not assume knowledge about the theory of fibration except in the Appendix.) In [10], Jacobs introduced λ1-category to make a model of the simply typed and untyped λ-calculus and claimed that λ1-category describes the relation between contexts and functions (exponentials) more clearly than ccc. (A judgement is interpreted in the fibre on the interpretation of the context of the judgement.) Since we found that such a structure works fine for the term model construction, we define our structure by extending λ1-category for the second order λ-calculus. (In our structure, a context is interpreted in the fibre on the interpretation of the type variables that the context depends, and a judgement is interpreted as above. Therefore, fibration over fibration is necessary.) Then, we give term models as instances of our structure and prove the syntactic property of typed λ-terms by interpreting types as PERs on terms with the property and contexts as sequences of such PERs.

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 out the proofs of some theorems including SN. In section 5, we define our structure called λ2 semi-adjoint structure (which can be regarded as a nonextensional PL-category) to interpret the second order typed λ-calculus. 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 proof of the theorem ‘well-typed β-equal terms have the common β-normal form’ and the proof of SN. In the Appendix, we slightly generalize the notion of the λ2 semi-adjoint structure by using the theory of fibration and prove the soundness.

Notation: For sets X and Y, we write X → Y for the set of all (set-theoretical) functions from X to Y. For sets X_{1}, …, X_{k}, we write X_{1} × ⋯ × X_{k} for the cartesian product of these sets, write X^{k} when X = X_{1} = ⋯ = X_{k}, and write x_{1} ⋯ x_{k} or (x_{1}, …, x_{k}) for its element.

2 Second Order Typed λ-calculus

In this section, we define a second order λ-system λ2. We define types (σ, τ) of λ2 by

σ, τ ::= X | σ→τ | ∀X.σ

where X ranges over type variables. We assume that for each type σ, we have an infinite set of (typed) variables V_{σ} and V_{σ} and V_{τ} are disjoint if σ and τ are distinct. We will use x, y, z as meta-variables for variables and sometimes write x^{σ} if x ∈ V_{σ}. We will also use X, Y as meta-variables that ranges over type variables and use v as a meta-variable that ranges over type variables or variables. We define preterms (M, N) of λ2 by

M, N ::= x^{σ} | λx^{σ}.M | app(σ, M, N) | λX.M | app(σ, M, τ)

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 of the variables and the type in the application the type annotations and write MN, Mτ for app(σ, M, N), app(σ, M, τ) respectively, when σ is irrelevant. We define the set FV(M) of free variables of a preterm M, the set FTV(σ) of free type variables of a type σ, and the set FTV(M) of free type variables of a preterm M as usual. A typing judgement is an expression of the form Θ + Γ ⊢ M : σ where Θ is a sequence of type variables, Γ is a sequence of variables, and σ is a type. The inference rules to derive typing judgements of second order typed λ2 are given as follows and M is said to be a typed term if a typing judgement of the form Θ + Γ ⊢ M : σ is derivable for some Θ, Γ, and σ.

Θ + Γ ⊢ x^{σ} : σ (var) FTV(Γ) ⊆ Θ, x^{σ} ∈ Γ
{Θ + Γ, x^{σ} ⊢ M : τ \atop Θ + Γ ⊢ λx^{σ}.M : σ→τ} (→I)  Θ + Γ ⊢ M : σ→τ Θ + Γ ⊢ N : σ Θ + Γ ⊢ app(σ→τ, M, N) : τ (→E)
{Θ, X + Γ ⊢ M : τ \atop Θ + Γ ⊢ λX.M : ∀X.τ} (∀I) X ∉ FTV(Γ)
{Θ + Γ ⊢ M : ∀X.τ \atop Θ + Γ ⊢ app(∀X.τ, M, σ) : τ[X := σ]} (∀E) FTV(σ) ⊆ Θ

The equality judgement is of the form Θ + Γ ⊢ M = N : σ and the rules to derive equality judgements are the following β-rules

Θ + Γ ⊢ λx^{σ}.M : σ→τ Θ + Γ ⊢ N : σ
Θ + Γ ⊢ app(σ→τ, λx^{σ}.M, N) = M[x^{σ} := N] : τ

{Θ + Γ ⊢ M : ∀X.τ \atop Θ + Γ ⊢ app(∀X.τ, λX.M, σ) = M[X := σ] : τ[X := σ]} FTV(σ) ⊆ Θ

and obvious congruence rules for equality. The system λη2 is λ2 with the following η-rules added.

{Θ + Γ ⊢ M : σ→τ \atop Θ + Γ ⊢ λx^{σ}.app(σ→τ, M, x^{σ}) = M : σ→τ} x^{σ} ∉ FV(M)

{Θ + Γ ⊢ M : ∀X.τ \atop Θ + Γ ⊢ λX.app(∀X.τ, M, X) = M : ∀X.τ} X ∉ FTV(M)

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

We also introduce untyped λ-terms (M, N) by the following grammar

M, N ::= x | λx.M | MN

where x ranges over (untyped) variables. We will write Λ_{0} for the set of terms of untyped λ-terms and M̂ for the untyped λ-term obtained by stripping the type annotations of a term M of simply typed λ.

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 λ-system λ. So, T denotes the set of types of simply typed λ-calculus constructed from some base types in these sections. The idea of our semantic structure comes from the environment model or the BMM-model (Bruce, Meyer, and Mitchell’s model [3, 4]).

A structure ⟨{C_{B}^{A_{1},...,A_{n}}}_{A_{i}∈T ,B∈T} , −^{∗}−, Ψ, Φ⟩ which satisfies the following conditions is called a λ-structure. {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.

We define an interpretation of simply typed λ-calculus in a λ-structure as follows. 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]] : [[Γ]] ⟶ [[σ]].

4 Simple Term Model

Let P be a predicate on Λ_{0} that satisfies the following conditions.

(P0a) If P (M[x := z]) where z is a variable, then P (M).

(P0b) If P (M), then P (λx.M).

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

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

(TZ) α contains at least one variable.

We define a binary operation ⇝ on P -typesets as follows.

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

A type family is a non-empty family of P -typesets that is closed under ⇝ and contains a P -typeset of type K for each atomic type K. Given a type family, we can define a λ-structure as follows. We assume that, for each atomic type K, an element [K] of T is associated, and we define [A→B] =^{def} [A] ⇝ [B]. We

define D_{A} =^{def} [A] and D_{A_{1},...,A_{n}} =^{def} D_{A_{1}} × ⋯ × D_{A_{n}}. 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{γ}. For an arrow code \overline{γ}|M, we define a function [\overline{γ}|M] by [\overline{γ}|M](\overline{e}) =^{def} M[\overline{γ} := \overline{e}] for \overline{e} ∈ Λ_{0}^{n} (n is the length of \overline{γ}). Then, we define the λ-structure as follows.

• C_{B}^{A_{1},...,A_{n}} =^{def} \{\overline{γ}|M | [\overline{γ}|M] ∈ D_{A_{1},...,A_{n}} → D_{B}\}

• (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 ∉ FV(M))

It is easy to show from these definitions that [[Γ ⊢ M]] = Γ̂|M̂ holds. To show that the above definitions constitute a λ-structure, we have to check that (id_{A_{1},...,A_{n}})_{i} ∈ C_{A_{i}}^{A_{1},...,A_{n}} and (R), (A1), (A2) are satisfied. For example, 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}. We prove the following Propositions and Theorem 4.5 under the assumption that there is a type family of P -typesets.

Proposition 4.1 (id_{A_{1},...,A_{n}})_{i} ∈ C_{A_{i}}^{A_{1},...,A_{n}}. Proof. For e_{1} … e_{n} ∈ D_{A_{1},...,A_{n}}, we have [x_{1} ⋯ x_{n}|x_{i}](e_{1} … e_{n}) = e_{i} ∈ D_{A_{i}}. □

Proposition 4.2 (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.3 (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} contains a variable z by (TZ), M[\overline{γ} := \overline{e}][x := z] is a P -value. So, λx.M[\overline{γ} := \overline{e}] is a P -value by (P0a) and (P0b). 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}. □

Proposition 4.4 (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}. □

Theorem 4.5 If Γ ⊢ M : σ, then P (M̂).

Proof. By Theorem 3.1 and the definition of the above λ-structure, [[[Γ ⊢ M]]](\overline{e}) ∈ D_{[[σ]]} holds for any \overline{e} ∈ D_{[[Γ]]}. By (TZ), there exist variables x_{1}, …, x_{n} such that x_{1} … x_{n} ∈ D_{[[Γ]]}. So, we have [[[Γ ⊢ M]]](x_{1} … x_{n}) ∈ D_{[[σ]]}. Since [[[Γ ⊢ M]]](x_{1} … x_{n}) = M̂[Γ̂ := x_{1} ⋯ x_{n}], we have P (M̂). □

To construct a P -typeset that contains variables, we consider a P -typeset that contains a P -zeroset, which is defined as the following set.

{xN_{1} ⋯ N_{n} | N_{i} is a P -value (1 ≤ i ≤ n), n ≥ 0}.

For this method to work, we need the following condition

(Z) If N_{i} is a P -value (1 ≤ i ≤ n) where n ≥ 0, then xN_{1} ⋯ N_{n} is a P -value

and we put T_{z}^{P} =^{def} {α | α is a P -typeset that contains a P -zeroset}.

Proposition 4.6 If P satisfies the following condition

(P1) 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})

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

Now, as an example of the typeset method described above, we can prove the strong normalizability of typed terms of λ with respect to the following β rule.

(β) app(τ, λx^{σ}.M, N) →_{β} M[x^{σ} := N]

This rule is defined on preterms of λ, but we also need the following β rule on untyped λ-terms.

(β) (λx.M)N →_{β} M[x := N]

Let

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

then, it is clear that P_{sn} satisfies (P0a), (P0b), (Z). To show that T_{z} is a type family, we need the following well-known lemma which is used in all (as far as we know) proofs of strong normalizability.

Lemma 4.7 Let M_{0} and N_{i} (n ≥ 1, 1 ≤ i ≤ n) be untyped λ-terms. If N_{i} and M_{0}[x := N_{1}]N_{2} ⋯ N_{n} are strongly normalizable with respect to →_{β}, then (λx.M_{0})N_{1} ⋯ N_{n} is strongly normalizable with respect to →_{β} Proof. Let ν(M) for the length of the longest reduction sequence starting from M. We prove this Lemma by induction on ν(M_{0}[x := N_{1}]N_{2} ⋯ N_{n}) + ν(N_{1}). We put M =^{def} (λx.M_{0})N_{1} ⋯ N_{n} and suppose M →_{β} M′. We classify the redex as follows.

1. The redex is in M_{0}, N_{2}, …, or N_{n}: In this case, since M′ ≡ (λx.M′_{0})N_{1}N′_{2} ⋯ N′_{n}, we have ν(M′_{0}[x := N_{1}]N′_{2} ⋯ N′_{n}) < ν(M_{0}[x := N_{1}]N_{2} ⋯ N_{n}). Therefore, M′ is strongly normalizable by the induction hypothesis.

2. The redex is in N_{1}: In this case, M′ ≡ (λx.M_{0})N′_{1}N_{2} ⋯ N_{n} where N_{1} →_{β} N′_{1}. Then, we have ν(M_{0}[x := N′_{1}]N_{2} ⋯ N_{n}) ≤ ν(M_{0}[x := N_{1}]N_{2} ⋯ N_{n}) and ν(N′_{1}) < ν(N_{1}). Therefore, M′ is strongly normalizable by the induction hypothesis.

3. The redex is (λx.M_{0})N_{1}: M′ is strongly normalizable by the assumption.

Since M′ is strongly normalizable in all cases, M is strongly normalizable. □

Theorem 4.8 If Γ ⊢ M : σ, then M is strongly normalizable. Proof. By Lemma 4.7, P_{sn} satisfies (P1). Therefore, T_{z} is a type family by Proposition 4.6. By Theorem 4.5, we have P_{sn}(M̂). Since type annotations are not involved in reduction, M is strongly normalizable. □

Note that the conditions for typesets that a typeset contains zeroset and satisfies (T1) correspond to the conditions for the saturated set. To compare the proof of Theorem 4.8 with the proof of usual style, see e.g., [6]. It may be worth while mentioning that in the case of the normalizability (P1) 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’.

Remark: Suppose \overline{γ}x|M : E, A ⟶ C and \overline{γ}|N : E ⟶ (A→C), then we have the following equations.

Φ ∘ Ψ(\overline{γ}x|M) = Φ(\overline{γ}|λx.M) = \overline{γ}x|(λx.M)x
Ψ ∘ Φ(\overline{γ}|N) = Ψ(\overline{γ}x|Nx) = \overline{γ}|λx.Nx

With β-equality, we can identify M and (λx.M)x, and with η-equality, we can identify N and λx.Nx. As we have remarked in section 1, we want to identify only β-equal terms. Therefore, we need Φ ∘ Ψ = id but not Ψ ∘ Φ = id. To have such Ψ and Φ, we use the notion of semi-adjointness in the next section.

Remark: To interpret simply typed λ-calculus, it might be natural to introduce operations abs and app that interpret abstraction and application directly instead of −^{∗}−, Ψ, and Φ. We have chosen our structure to make the categorical structure clearer, but even if we use abs and app, we have the same result. Suppose we replace −^{∗}−, Ψ, and Φ of λ-structure by abs and app which satisfies the following conditions:

(Ab) if f : E, A ⟶ C, then absf : E ⟶ (A→C)

(Ap) if f : E ⟶ (A→C) and g : E ⟶ A, then appfg : E ⟶ C

and define these operations on the term model as follows.

• abs(\overline{γ}x|M) =^{def} \overline{γ}|λx.M, app(\overline{γ}|M)(\overline{γ}|N) =^{def} \overline{γ}|MN

Then (T1) and (TZ) work for the conditions of typeset. But if we change the definition of [\overline{γ}|M] by [\overline{γ}|M](\overline{e}) =^{def} (λ\overline{γ}.M)\overline{e}, we have to change (T1) as follows. (In the following, \overline{e} and \overline{K} are sequence of P -values and \overline{γ} is a sequence of variables of the same length as \overline{e}.)

(S1) if ((λ\overline{γ}.M)\overline{e})((λ\overline{γ}.N)\overline{e})\overline{K} ∈ α, then (λ\overline{γ}.MN)\overline{e}\overline{K} ∈ α

(S2) if e_{i}\overline{K} ∈ α, then (λ\overline{γ}.x_{i})\overline{e}\overline{K} ∈ α (e_{i} and x_{i} is the i-th element of \overline{e} and \overline{γ} respectively)

This means we have yet another kind of saturated set. Note that (S1) and (S2) looks like the expansion by the reduction rules of the calculus of explicit substitution or combinatory algebra. This suggests that in some situation it is better to use a calculus other than the λ-calculus to interpret the λ-calculus. But, in this paper, we will not investigate towards this direction. However, if we adapt this typeset method to the calculus of explicit substitutions, we will find similar conditions for typesets.

5 Categorical Model

In the BMM model [4], β-equal terms have the same meaning, but in our λstructure they do not because Φ ∘ Ψ = id does not necessarily hold. However, in this section, we will define −^{∗}−, Ψ, and Φ in the categorical setting and have the model in which β-equal terms have the same meaning.

To make a model that respects β(η)-equality, we have to identify some arrows which interpret terms. To do so, we have to identify some elements of sets which interpret types. Therefore, 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 [8]. However, as we have stated in the introduction, we want to [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]

Figure 1: Semi-adjoint diagram

make a model that respects only β-equality to prove the uniqueness of β-normal form (Theorem 6.6). For that purpose, the notion of semi-adjoint [7, 9] 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), and in section 5.3, we give an interpretation of λ2 in the structure. Since our goal is to make term models systematically in which we can prove various syntactic properties, our structure is syntax-oriented, that is, reflects the syntactical structure directly. In section 5.4, we will discuss about it and compare our model with other models. 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

We construct our structure based on the theory of fibration, but in this and next section we do not assume readers are familiar with it. We need only some preliminaries from the theory of semi-functor and semi-adjunction. A semifunctor 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 diagram in Figure 1 commute. We have the following lemma (Lemma 2.1.1 [9]).

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 = Φ(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) = Φ(Gid ∘ u ∘ v ∘ id) = id ∘ Φ(u ∘ v) ∘ F id = Φ(u ∘ v). □

5.2 λ2 Semi-adjoint Structure

In this section, we will define a structure called a λ2 semi-adjoint structure. Before going to the definitions, we will explain what syntactic objects these definitions are intended to interpret. A type with at most k type variables is interpreted by an element of _{k}T (Definition 5.2), a context is interpreted by a sequence of elements of _{k}T , that is, by an object of 𝔼_{k} (Definition 5.4), and a term of a judgement is interpreted by an arrow of 𝔼̃_{E} (Definition 5.4) where E is the interpretation of the context of the judgement.

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.

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.

Definition 5.4 Let 𝔹 be a type category and 𝔼 : 𝔹^{op} ⟶ Cat be a strict 𝔹indexed category, that is, 𝔼 maps k ∈ 𝔹 to a category 𝔼_{k} and F : l ⟶ k in 𝔹 to a functor F^{∗} : 𝔼_{k} ⟶ 𝔼_{l} that satisfies id_{k}^{∗} = id_{𝔼_{k}} and (F ∘ G)^{∗} = G^{∗} ∘ F^{∗}. 𝔼 is a term category on 𝔹, if

(1) Obj(𝔼_{k}) = _{k}T^{∗}

(2) If E ∈ _{k}T^{∗} and A ∈ _{k}T , then E, A (concatenation) is a product of E and A in 𝔼_{k} where we write π|_{1}^{E,A} for its first projection and π|_{2}^{E,A} for its second projection. _{k}ϵ is a terminal object of 𝔼_{k}.

(3) The object part of the functor F^{∗} is given by F^{∗}E =^{def} E ∘ F and F^{∗} preserves products strictly.

Therefore, if t : E ⟶ (B_{1}, …, B_{n}), we can regard t as a sequence (t_{1}, …, t_{n}) where t_{i} : E ⟶ B_{i}. By (3), we have F^{∗}(t_{1}, …, t_{n}) = (F^{∗}t_{1}, …, F^{∗}t_{n}).

Let E ∈ 𝔼_{k}. 𝔼̃_{E} is a category whose objects are pairs E; A where A ∈ _{k}T , and arrows are g : E; A ⟶ E; B where g : E × A ⟶ B. We define the composition of two arrows g : E; A ⟶ E; B and h : E; B ⟶ E; C by h∘^{E} g =^{def} h ∘ ⟨π|_{1}^{E,A}, g⟩ and identity on E; A by π|_{2}^{E,A}.

If F : l ⟶ k is an arrow in 𝔹, E ∈ 𝔼_{k}, E′ ∈ 𝔼_{l}, and t : E′ ⟶ F^{∗}E is an arrow in 𝔼_{l}, we write (F, t) : E′ ⟶ E. We define a reindexing functor (F, t)^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{E′} as follows. (g : E; A ⟶ E; B.)

(F, t)^{∗}(E; A) =^{def} E′; F^{∗}A
(F, t)^{∗}g =^{def} F^{∗}g ∘ (t × id_{F^{∗}A}) : E′; F^{∗}A ⟶ E′; F^{∗}B

(It is easy to check (F, t)^{∗} is a functor.) We will abbreviate (id_{k}, t)^{∗} as t^{∗}.

We introduce some notations. Let E ∈ _{k}T^{∗}, A ∈ _{k}T , E′ ∈ _{l}T^{∗}, and f ≡ (F, t) : E′ ⟶ E. We put

↓(E; A) =^{def} (id_{k}, π|_{1}^{E,A}) : E × A ⟶ E,

+E =^{def} (π|_{1}^{k+1})^{∗}E,

⇓(E) =^{def} (π|_{1}^{k+1}, id_{^{+}E}) : ^{+}E ⟶ E,

+f =^{def} (F × id_{1}, (π|_{1}^{l+1})^{∗}t).

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} for any E; A.

• There exists a right semi-adjoint functor Π_{⇓(E)} : 𝔼̃_{^{+}E} ⟶ 𝔼̃_{E} of a reindexing functor ⇓(E)^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{^{+}E} for any E.

• Let

f ≡ (F, t) : E′ ⟶ E, f̂ ≡ (F, t × id_{F^{∗}A}) : E′ × F^{∗}A ⟶ E × A, q ≡ ↓(E; A) : E × A ⟶ E, q′ ≡ ↓(E′; F^{∗}A) : E′ × F^{∗}A ⟶ E′,

Ê ≡ E × A

or

f ≡ (F, t) : E′ ⟶ E, f̂ ≡ ^{+}f : ^{+}E′ ⟶ ^{+}E,

q ≡ ⇓(E) : ^{+}E ⟶ E, q′ ≡ ⇓(E′) : ^{+}E′ ⟶ E′,

Ê ≡ ^{+}E

In both cases, the following conditions hold (X ∈ 𝔼̃_{E}, Y ∈ 𝔼̃Ê).

– f̂^{∗}q^{∗} = q′^{∗}f^{∗} ; – Π_{q′} f̂^{∗} = f^{∗}Π_{q} ; – f^{∗}Ψ_{X,Y} = Ψ_{f^{∗}X,f̂^{∗}Y} f̂^{∗} ; – f̂^{∗}Φ_{X,Y} = Φ_{f^{∗}X,f̂^{∗}Y} f^{∗}  [figure: ·; f̂; Ê; E′; q′; f; E; q]

(Note that the first condition always holds.)

We define A ⇒ B and ∇B by _{k}ϵ; A ⇒ B =^{def} Π_{↓(_{k}ϵ;A)}(A; B) and _{k}ϵ; ∇B =^{def}

Π_{⇓(_{k}ϵ)}(_{k+1}ϵ; B).

The following Proposition is from Lemma 3.3 of Jacobs [10].

Proposition 5.6 1) Π_{↓(E;A)}(E, A; B) = E; A ⇒ B. 2) Π_{⇓(E)}(^{+}E; B) = E; ∇B. Proof. 1)

Π_{↓(E;A)}(E, A; B) = Π_{↓(E;A)}(id_{E,A}, π|_{2}^{E,A})^{∗}(A; B)
= (id_{E},!_{E})^{∗}Π_{↓(_{k}ϵ;A)}(A; B)
= E; A ⇒ B

2) Similar. □ By this proposition, the object-part of Π can be specified by

giving A ⇒ B or ∇B.

Definition 5.7 A structure ⟨T, 𝔹, 𝔼⟩ 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 𝔹 that has semi-products. A λ2 semi-adjoint structure is non-trivial if there exists an object • ∈ _{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.

Remark: Here, we will see the relation between λ2 semi-adjoint structure and λ-structure. Let X ≡ E; B and Y ≡ E, A; C, then Ψ of Π_{↓(E;A)} is a mapping with the following domain and codomain.

Ψ_{X,Y} ∈ 𝔼̃_{E,A}(↓(E; A)^{∗}X, Y) → 𝔼̃_{E}(X, Π_{↓(E;A)}Y)
= 𝔼̃_{E,A}(E, A; B, E, A; C) → 𝔼̃_{E}(E; B, E; A ⇒ C)

Suppose we construct a λ-structure from _{k}T instead of T (we use ⇒ instead of →), and compare the Ψ of the λ-structure with the above Ψ_{X,Y}. The domain of an arrow is slightly different (there is extra B), but it can be virtually removed by considering the base arrow that is defined at the beginning of 5.3. (Similar for ↓(E; A)^{∗} and Φ_{X,Y}.) Therefore, 𝔼_{k} can be regarded as a λ-structure.

5.3 Interpretation

We give an interpretation of λ2 in a non-trivial λ2 semi-adjoint structure.

For E ∈ 𝔼_{k}, we define E::• =^{def} E;_{k}• where _{k}• =^{def} !_{k}^{∗}• and !_{k} : k ⟶ 0 in 𝔹. (Note that 𝔼_{k}(_{k}ϵ,_{k}•) ≠ ∅.) An arrow g ∈ 𝔼̃_{E} is called a base arrow if dom(g) = E::• and g = g_{0} ∘ π|_{1}^{E,_{k}•} for some g_{0}, Since g_{0} is uniquely determined (g ∘ ⟨id_{E}, e∘!⟩ = g_{0} ∘ π|_{1}^{E,_{k}•} ∘ ⟨id_{E}, e∘!_{E}⟩ = g_{0} for e ∈ 𝔼_{k}(_{k}ϵ,_{k}•) where !_{E} : E ⟶ kϵ), we write b(g) for ⟨id_{E}, g_{0}⟩. (Therefore, a base arrow plays the role of a global element.)

Proposition 5.8 Reindexing functors and Ψ and Φ of above semi-adjunctions map base arrows to base arrows. Proof. (Case reindexing functor) Let (F, t) : E′ ⟶ E and g be a base arrow in 𝔼̃_{E}, that is, there is an arrow g_{0} such that dom(g) = E::• and g = g_{0} ∘ π|_{1}^{E,_{k}•} : E,_{k}• ⟶ A.

(F, t)^{∗}g =^{def} F^{∗}g ∘ (t × id_{F^{∗}A})

=^{def} F^{∗}g_{0} ∘ F^{∗}π|_{1}^{E,_{k}•} ∘ (t × id_{F^{∗}A})

=^{def} F^{∗}g_{0} ∘ t ∘ π|_{1}^{E′,F^{∗}_{k}•}

=^{def} F^{∗}g_{0} ∘ t ∘ π|_{1}^{E′,_{l}•}

(Case Ψ) Fix e ∈ 𝔼_{k}(_{k}ϵ,_{k}•) and define †_{E} =^{def} e∘!_{E}. Then, g : E::• ⟶ E; A is a base arrow iff g = g ∘ ⟨id_{E}, †_{E}⟩. Let f : E, A::• ⟶ E, A; C be a base arrow.

Ψf =^{def} Ψ(f ∘^{E,A} (†_{E,A} ∘ π|_{1}^{E,A,_{k}•}))

=^{def} Ψ(f ∘^{E,A} ((π|_{1}^{E,A})^{∗}†_{E} ∘ π|_{1}^{E,_{k}•}))

=^{def} Ψf ∘^{E} (†_{E} ∘ π|_{1}^{E,_{k}•}) by Lemma 5.1 2)

Therefore, Ψf is a base arrow. □

Let Θ+Γ be a context, σ be a type, and M be a term. By our interpretation, they are interpreted by the following object or arrow.

[[Θ]]  an object of 𝔹
[[Θ + Γ]]  an object of 𝔼_{[[Θ]]}
[[Θ + Γ ; σ]] an object of 𝔼̃_{[[Θ+Γ]]}
[[Θ + Γ | M]] a base arrow of 𝔼̃_{[[Θ+Γ]]}

By the definition of 𝔼̃_{[[Θ+Γ]]}, [[Θ + Γ ; σ]] is of the form [[Θ + Γ]]; A where A ∈ _{k}T , so we write [[σ / Θ + Γ]] for the A.

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}^{i} ∘ π|_{1}^{i+1} ∘ ⋯ ∘ π|_{1}^{k} ∈ _{k}T

where X is the i-th type variable in Θ

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

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

• [[Θ + Γ | x^{σ}]] =^{def} π|_{2}^{E_{i}} ∘ π|_{1}^{E_{i+1}} ∘ ⋯ ∘ π|_{1}^{E_{n}} ∘ π|_{1}^{E_{n+1}}

: [[Θ + Γ]]::• ⟶ [[Θ + Γ ; σ]]

where x^{σ} is the i-th variable in Γ ≡ x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}

and E_{j} ≡ [[Θ + x_{1}^{σ_{1}}, …, x_{j}^{σ_{j}}]] (i ≤ j ≤ n), E_{n+1} ≡ [[Θ + Γ]] ×_{k}•

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

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

where g ≡ b([[Θ + Γ | N]]),

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

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

[figure: [[]]::•; f; [[;σ→τ]]; [[x^{σ}]]::•; Φf; [[x^{σ} ; τ]]; [[]]::•; [[;τ]]; [[]]; [[x^{σ}]]; g; [[]]]

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

• [[Θ + Γ | λX.M]] =^{def} Ψ_{[[Θ+Γ]]::•,cod([[Θ,X+Γ|M]])}[[Θ, X + Γ | M]]

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

where S ≡ ⟨id_{k}, [[σ / Θ + Γ]]⟩ : k ⟶ k + 1 in 𝔹 and g ≡ (S, id_{[[Θ,X+Γ]]}), if [[Θ + Γ | M]] has the following form

[[Θ + Γ | M]] : [[Θ + Γ]]::•  [[Θ + Γ ; ∀X.τ]]

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

2) If Θ + Γ ⊢ M = N : σ in λ2 (λη2), then [[Θ + Γ | M]] = [[Θ + Γ | N]] in every non-trivial λ2 (resp. λη2) semi-adjoint structure. Proof. We prove this theorem in the Appendix in a more general setting. □

5.4 Comparison with Other Models

A λ2 semi-adjoint structure is a fibred CT-structure (See Definition A.1) such that fibres (𝔼_{k}’s) are explicitly constructed from _{k}T . We need to define a semiexponential A ⇒ B only for A, B ∈ _{k}T (Proposition 5.6), but, as discussed in [10] for the case of λ1-category, we can define a semi-exponential E ⇒ E′ for any E, E′ ∈ 𝔼_{k}, that is, we can define semi-ccc structure on 𝔼_{k}. This approach has the advantage that it coincides with the well-known PL-category in the case of λη2 adjoint structure, but if we extend λ2 by adding pair terms without surjectivity, we should distinguish cartesian products for such terms and those for contexts. We will discuss about this point at the end of section 6. Here, we recall some notions related to the environment model [3, 4] to see the relation with the λ2 semi-adjoint structure.

Definition 5.10 A type domain is a tuple ⟨T, ⇝, △⟩, where T is a non-empty set, ⇝ is a binary operation on T, and △ ∈ [T → T] → T where [T → T] ⊆ T → T. Let η be a type environment, that is, a partial map from type variables to T. We define M[[σ]]η as follows.

• M[[X]]η =^{def} η(X)

• M[[σ→τ]]η =^{def} M[[σ]]η ⇝ M[[τ]]η

• M[[∀X.τ]]η =^{def} △g where g : a ↦ M[[τ]]η[X ↦ a] for a ∈ T

If M[[σ]]η is defined for every type σ in λ2 and type environment η such that FTV(σ) ⊆ dom(η), we say ⟨T, ⇝, △⟩ is a type model.

A second order functional domain [9, 3, 4] is a tuple

⟨⟨T, ⇝, △⟩, {D_{a}}_{a∈T} , {Φ^{a,b}, Ψ^{a,b}}_{a,b∈T} , {Φ^{f}, Ψ^{f}}_{f∈[T →T]}⟩

where ⟨T, ⇝, △⟩ is a type domain, {D_{a}}_{a∈T} is a family of sets indexed by T, Φ and Ψ’s are functions such that

Φ^{a,b} ∈ D_{a⇝b} → (D_{a} → D_{b}), Ψ^{a,b} ∈ [D_{a} → D_{b}] → D_{a⇝b}

where [D_{a} → D_{b}] is the image of Φ^{a,b} and Φ^{a,b} ∘ Ψ^{a,b} = id_{[D_{a}→D_{b}]}, and

Φ^{f} ∈ D_{△f} → Π_{a∈T} D_{fa}, Ψ^{f} ∈ [Π_{a∈T} D_{fa}] → D_{△f}

where [Π_{a∈T} D_{fa}] is the image of Φ^{f} and Φ^{f} ∘Ψ^{f} = id_{[Π_{a∈T} D_{fa}]}. We say a second order functional domain is a BMM-model if every typed term has a meaning in every environment. (We omit the definition of the meaning.) A second order applicative structure, which is more common among literatures (e.g. [13]), is a structure obtained by dropping Ψ^{a,b} and Ψ^{f} from the second order functional structure. (Usually, symbols App^{a,b} and App^{f} are used instead of Φ^{a,b} and Φ^{f}.) Therefore, a second order functional domain is a second order applicative structure with the choice of inverse functions of App^{a,b} and App^{f}. (If the second order functional domain is extensional, that is, Φ^{a,b} and Φ^{f} are one-to-one, Ψ^{a,b} and Ψ^{f} are uniquely determined. In that case, it is an extensional second order applicative structure.)

To make the correspondence between a λ2 semi-adjoint structure and a BMM-model clearer, we will first construct a term category 𝔼 from the second order functional domain.

(1) Definition of a type object family T ≡ {_{k}T }: _{k}T =^{def} T^{k} → T.

(2) Definition of a type category 𝔹 on T: For F ≡ (F_{1}, …, F_{l}) : k ⟶ l and G ≡ (G_{1}, …, G_{m}) : l ⟶ m, we define the composition by (G ∘ F)_{j}(\overline{a}) =^{def} G_{j}(F_{1}(\overline{a}), …, F_{l}(\overline{a})) (\overline{a} ∈ T^{k}) and the identity on k by the identity function on T^{k}.

(3) Definition of a term category 𝔼 on 𝔹: We define an arrow f : E ⟶ A (E ∈ kT^{n}, A ∈ _{k}T ) as a family of functions \{f\overline{a}\}_{\overline{a}∈T^{k}} such that f\overline{a} ∈ D_{E(\overline{a})} → D_{A(\overline{a})}, and the composition of arrows by the composition of functions on D_{a}’s. We define the functor F^{∗} : 𝔼_{k} ⟶ 𝔼_{l} by F^{∗}(\{f\overline{a}\}_{\overline{a}∈T^{k}}) =^{def} \{f_{F (\overline{a})}\}_{\overline{a}∈T^{l}}.

It is easy to check that 𝔼 is a term category on 𝔹. Next, we will try to define semi-products in 𝔼. (We omit the case Π_{⇓(E)}.)

(4) Let f ≡ \{f\overline{a}\}_{\overline{a}∈T^{k}} : E, A; B ⟶ E, A; C, that is, f\overline{a}(\overline{e}ab) ∈ D_{C(\overline{a})} for

\overline{e} ∈ D_{E(\overline{a})}, a ∈ D_{A(\overline{a})}, b ∈ D_{B(\overline{a})}. We define Π_{↓(E;A)} by Π_{↓(E;A)}f =^{def}

\{g\overline{a}\} such that g\overline{a}(\overline{e}h) = Ψ^{A(\overline{a}),C(\overline{a})}f′ for h ∈ D_{A(\overline{a})⇒B(\overline{a})} where f′(a) = f\overline{a}(\overline{e}a(Φ^{A(\overline{a}),B(\overline{a})}h)(a)) for a ∈ D_{A(\overline{a})}.

(5) Let f ≡ \{f\overline{a}\}_{\overline{a}∈T^{k}} : E, A; B ⟶ E, A; C. We define Ψ by Ψf =^{def} \{g\overline{a}\} such

that g\overline{a}(\overline{e}b) = Ψ^{A(\overline{a}),C(\overline{a})}f′ where f′(a) = f\overline{a}(\overline{e}ab) for a ∈ D_{A(\overline{a})}.

(6) Let f ≡ \{f\overline{a}\}_{\overline{a}∈T^{k}} : E; B ⟶ E; A ⇒ C. We define Φ by Φf =^{def} \{g\overline{a}\} such

that g\overline{a}(\overline{e}ab) = (Φ^{A(\overline{a}),C(\overline{a})}f\overline{a}(\overline{e}b))(a) for a ∈ D_{A(\overline{a})}.

However, this is not necessarily a λ2 semi-adjoint structure or, worse, Π or Ψ may not be defined on some arrows. Requiring this to be a λ2 semi-adjoint structure implies that the second order functional domain is a BMM-model, and we can show by routine calculation that the interpretation in the λ2 semiadjoint structure coincides with the meaning in the BMM-model. However, the conditions of semi-products (Definition 5.5) force some kind of uniformity in arrows, Ψ, Φ. Therefore, we have to find a suitable subcategory, but it is difficult to do so without assuming some kind of structure on T and D_{a}. In [9], objects and arrows of 𝔼 are restricted to those that can represented by types or terms. In the framework of the BMM-model, it is proved in [4] that a certain kind of second order combinatorial structure on D_{a} implies the model condition. In the next section, we focus on the term models and investigate the conditions that T and D_{a} should satisfy to make a λ2 semi-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. One of the changes is the use of Λ instead of Λ_{0}. It make the description a bit messy, but it is necessary to prove the uniqueness of normal form because we have to keep type annotations of terms when we interpret terms. We put AFV(M) =^{def} FV(M) ∪ FTV(M) in the following.

For a PER α, we use the following notations: [N]_{α} =^{def} {M | N α M},

dom(α) =^{def} {N | N α N}, classes(α) =^{def} {[N]_{α} | N ∈ dom(α)}. We write α|X

for the PER α ∩ (X × X). Let α and β be PERs and f be a function from dom(α) to dom(β). We say f represents a function from α to β (or classes(α) to classes(β)) if, for all N_{1} α N_{2}, f(N_{1}) β f(N_{2}) holds.

Let P be a predicate on Λ that satisfies the following condition.

(P0a) If P (M[v := N]) where N is a variable or a type, then P (M).

(P0b) If P (M), then P (λv.M).

A P -PER-typeset is a PER α on P -values that satisfies the following conditions. (C[ ] is a context, that is, a term with a hole.)

(T1) if N_{i} is a P -value or a type (n ≥ 1, 1 ≤ i ≤ n), M_{0}[v := N_{1}]N_{2} ⋯ N_{n} ∈ dom(α), and σ is a type, then M_{0}[v := N_{1}]N_{2} ⋯ N_{n} α app(σ, λv.M_{0}, N_{1})N_{2} ⋯ N_{n}

(T2) if C[M] ∈ dom(α), no variables in AFV(M) − {v} become bound in C[M], v becomes bound in C[app(σ, λv.M, v)], and σ is a type, then C[M] α C[app(σ, λv.M, v)]

(TZ) dom(α) contains at least one variable.

Clearly, the condition (T1) corresponds to one of the saturated set conditions (closure property under head β-expansion), but what does (T2) mean? (T2) is used in Proposition 6.1 to prove that Π is a right semi-adjoint functor. This may seem to be just an ad-hoc condition, but with (T1) we can show the following: If C[M[x := N]] ∈ dom(α) and no variables in FV(N) ∪ (FV(M) − {x}) become bound,

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

(u is a fresh variable) holds by (T1) and (T2), and furthermore, if the condition

(⋆) if app(σ, λx.M_{0}, N_{1})N_{2} ⋯ N_{n} ∈ dom(α), then app(σ, λx.M_{0}, N_{1})N_{2} ⋯ N_{n} α M_{0}[x := N_{1}]N_{2} ⋯ N_{n}

holds, we have (λu.C[(λx.M)u])N α C[(λx.M)N]. Therefore, with (⋆), if C[M[x := N]] ∈ dom(α) and no variables in FV((λx.M)N) become bound, we have the following closure property under expansion.

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

In the case P is the strong normalizability, this corresponds to the Crucial Lemma in [8]. Now, consider the following condition which corresponds to the non-interference condition in [8].

(⋆⋆) if C[M[x := N]] ∈ dom(α), no variables in AFV(app(σ, λx.M, N)) become bound in C[app(σ, λx.M, N)], and σ is a type, then C[M[x := N]] α C[app(σ, λx.M, N)]

In [8], the smallest equivalence relation ≈ on Λ_{∗} (the set of λ-terms with a distinguished constant ∗) that satisfies untyped version of (⋆⋆) is considered and PERs on cpca SN_{∗}^{0}/≈ (where SN_{∗}^{0} is the set of closed SN terms of Λ_{∗}) are used to interpret types. In our construction, we will use PERs on terms that satisfy (T1) and (T2) to interpret types. This means we need more coarse PERs, because we use PERs on terms not on the equivalence classes of terms, and indeed (⋆⋆) implies (T1) but not (T2).

We want to define a family T of P -PER-typesets and operations ⇝ and △ so that ⟨T, ⇝, △⟩ becomes a type domain. But instead of explicitly defining ⇝ and △, we list conditions they should satisfy.

(T3) if α ⇝ β, α ∈ T, M_{1} (α ⇝ β) M_{2}, N_{1} α N_{2}, and σ is a type, then app(σ, M_{1}, N_{1}) β app(σ, M_{2}, N_{2})

(T4) if α, β ∈ T, M_{1}[x := N_{1}] β M_{2}[x := N_{2}] for all N_{1} α N_{2}, and λx.M_{i} are P -values, then λx.M_{1} (α ⇝ β) λx.M_{2}

(T5) if g ∈ [T → T], M_{1} (△g) M_{2}, α ∈ T, and σ and τ are types, then app(σ, M_{1}, τ) (gα) app(σ, M_{2}, τ)

(T6) if g ∈ [T → T], M_{1}[X := τ] gα M_{2}[X := τ] for all α ∈ T and all types τ, and λX.M_{i} are P -values, then λX.M_{1} (△g) λX.M_{2}

Note that conditions (T4) and (T6) can be regarded as typed version of weak extensionality conditions and we do not assume any extensionality condition such as “if α, β ∈ T and M_{1}N_{1} β M_{2}N_{2} for all N_{1} α N_{2}, then M_{1} (α ⇝ β) M_{2}”.

Given a type model ⟨T, ⇝, △⟩ where T is a non-empty family of P -PER-typesets, we can define a term category PT (⟨T, ⇝, △⟩) ≡ ⟨T, 𝔹, 𝔼⟩, which will turn out to be a λ2 semi-adjoint structure under some conditions. We make PT (⟨T, ⇝, △⟩) following the line described in section 5.4, but this time we restrict objects and arrows to representable ones, that is, objects of 𝔼 that can be represented by types and arrows of 𝔼 by terms. We define composition, reindexing functor, and so on as operations on the representatives. It is easy to check that 𝔼 is a term category, but conditions (T1) – (T6), (TZ) are necessary to have semi-functors.

(1) Definition of a type object family T ≡ \{_{k}T \}: An expression of the form \overline{θ}|σ is called a type code if \overline{θ} ≡ X_{1} ⋯ X_{k} and σ is a type such that FTV(σ) ⊆ \overline{θ}.

We define [\overline{θ}|σ] ∈ T^{k} → T by [\overline{θ}|σ](\overline{a}) =^{def} M[[σ]]η where \overline{a} ≡ a_{1} ⋯ a_{k} and

η is a type environment that maps X_{i} to a_{i}, and define _{k}T =^{def} \{[\overline{θ}|σ] | \overline{θ}|σ is a type code\}.

(2) Definition of a type category 𝔹 on T: For F ≡ (F_{1}, …, F_{l}) : k ⟶ l and G ≡ (G_{1}, …, G_{m}) : l ⟶ m where F_{i} ≡ [X_{1} ⋯ X_{k}|σ_{i}] and G_{j} ≡ [Y_{1} ⋯ Y_{l}|τ_{j}], we define the composition ∘ and the identity id_{k} on 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 𝔼 on 𝔹: An expression of the form \overline{θ}\overline{γ}|M is called a arrow 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{γ}. We define D_{a} =^{def} classes(a) for a ∈ T and D_{a_{1},...,a_{n}} =^{def}

D_{a_{1}} × ⋯ × D_{a_{n}}. Let (A_{1}, …, A_{n}) ∈ _{k}T^{n}, B ∈ _{k}T , the length of \overline{θ} be k, \overline{γ} ≡ x_{1}^{σ_{1}} ⋯ x_{n}^{σ_{n}}, A_{i} ≡ \overline{θ}|σ_{i}, and \overline{θ}\overline{γ}|M be an arrow code. We define an arrow [\overline{θ}\overline{γ}|M] : (A_{1}, …, A_{n}) ⟶ B as follows. Let \overline{a} ∈ T^{k} and f\overline{a} be a function defined by

f\overline{a}(N_{1}, …, N_{n}) =^{def} M[\overline{γ} := N_{1} ⋯ N_{n}] (N_{i} ∈ dom([A_{i}](\overline{a}))).

If f\overline{a} satisfies f\overline{a}(N_{1}, …, N_{n}) ∈ dom([B](\overline{a})) and represents a function from D_{[A_{1}](\overline{a}),...,[A_{n}](\overline{a})} to D_{[B](\overline{a})}, then we denote the family of functions \{f\overline{a}\}_{\overline{a}∈T^{k}} by [\overline{θ}\overline{γ}|M].

Let E ∈ _{k}T^{n}, E′ ∈ _{k}T^{m}, E′′ ∈ _{k}T^{l}. Given s ≡ (s_{1}, …, s_{m}) : E ⟶ E′ (where s_{i} ≡ [\overline{θ}x_{1} ⋯ x_{n}|M_{i}]), t ≡ (t_{1}, …, t_{l}) : E′ ⟶ E′′ (where t_{j} ≡ [\overline{θ}y_{1} ⋯ y_{m}|N_{j}]), F ≡ (F_{1}, …, F_{k}) : h ⟶ k (where F_{i} ≡ \overline{θ′}|σ_{i}), [\overline{θ}\overline{γ}|M] : E ⟶ A, we define the composition ∘ and ^{∗} as follows.

(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{σ}]]

The identity id_{E} on E ∈ _{k}T^{n} 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}).

(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 arrow codes, but we will show in Proposition 6.1 that they are well-defined under some conditions.

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

(z^{σ→τ} ∉ FV(M), [\overline{θ}\overline{γ}x^{σ}y^{τ} |M] : E, \overline{θ}|σ; \overline{θ}|τ ⟶ E, \overline{θ}|σ; C)

– Ψ(\overline{θ}\overline{γ}x^{σ}y|M) =^{def} \overline{θ}\overline{γ}y|λx^{σ}.M ([\overline{θ}\overline{γ}x^{σ}y|M] : E, \overline{θ}|σ; B ⟶ E, \overline{θ}|σ; C)

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

(x^{σ} ∉ FV(M), [\overline{θ}\overline{γ}y|M] : E; B ⟶ E; \overline{θ}|σ→τ)

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

(z^{∀X.τ} ∉ FV(M), [\overline{θ}X\overline{γ}y^{τ} |M] : ^{+}E; \overline{θ}X|τ ⟶ ^{+}E; C)

– Ψ(\overline{θ}X\overline{γ}y|M) =^{def} \overline{θ}\overline{γ}y|λX.M ([\overline{θ}X\overline{γ}y|M] : ^{+}E; B ⟶ ^{+}E; C)

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

(X ∉ FTV(M), [\overline{θ}\overline{γ}y|M] : E; B ⟶ E; \overline{θ}|∀X.τ)

(5) Definition of •: Any type object [|σ] (that is, σ is closed) such that D_{[|σ]()} ≠ ∅ can play the role of •.

Proposition 6.1 Let ⟨T, ⇝, △⟩ be a type model. If T is a non-empty family of P -PER-typesets that satisfies the conditions (T1) – (T6), (TZ), then PT (⟨T, ⇝ , △⟩) is a λ2 semi-adjoint structure. Proof. We have to check that Π, Ψ, Φ defined in (4) constitutes the semi-adjoint and satisfies 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} ∈ dom([E](\overline{a})), d ∈ dom([A](\overline{a})), and d′ ∈ dom([B](\overline{a})), and take g ∈ dom([A ⇒ B](\overline{a})). Then gd ∈ dom([B](\overline{a})) by (T3). Since dom([A](\overline{a})) contains a variable z, M_{i}[y := gx][\overline{γ} := \overline{e}][x := z] are P -values. Therefore, by (P0a), (P0b) 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.)

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

Above two arrows are equal, because for \overline{a} ∈ T^{k}, \overline{e} ∈ dom([E](\overline{a})), c ∈ dom([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] where α ≡ [A ⇒ D](\overline{a}), 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{γ}x|x_{1}, …, \overline{γ}x|x_{n}) where \overline{γ} ≡ x_{1} ⋯ x_{n}
↓(E; A)^{∗}(\overline{γ}y|N) = \overline{γ}xy|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, A; C′); f ∘^{E,A} − ∘^{E,A} ↓(E; A)^{∗}g; Ψ; \underline{Φ}; 𝔼̃_{E}(E; B′, E; A ⇒ C′); Π_{↓(E;A)}f ∘^{E} − ∘^{E} 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 ∘^{E} Ψh ∘^{E} g) = Φ((\overline{γ}z|λx.M[y := zx]) ∘^{E} (\overline{γ}y|λx.H) ∘^{E} (\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 ∘^{E,A} h ∘^{E,A} ↓(E; A)^{∗}g = (\overline{γ}xy|M) ∘^{E,A} (\overline{γ}xy|H) ∘^{E,A} (\overline{γ}xu|N)
= \overline{γ}xu|M[y := H][y := N]

These two arrows are equal, because for \overline{a} ∈ T^{k}, \overline{e} ∈ dom([E](\overline{a})), c ∈ dom([A](\overline{a})), d ∈ dom([B′](\overline{a}))

((λx.M[y := (λx.H)x][y := N])x)[\overline{γ}xu := \overline{e}cd] α M[y := H][y := N][\overline{γ}xu := \overline{e}cd]

where α ≡ [C′](\overline{a}), holds by (T1) and (T2).

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

Proposition 6.2 Suppose PT (⟨T, ⇝, △⟩) is a λ2 semi-adjoint structure. Then,

[[Θ + Γ ⊢ M]] = [ΘΓ|M].

We 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 re-define the associated condition as follows.

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

Then, we put T_{z}^{P} =^{def} {a | a is a P -PER-typeset, dom(a) ⊇ P -zeroset}.

Theorem 6.3 Suppose PT (⟨T, ⇝, △⟩) is a λ2 semi-adjoint structure and T ⊆ T_{z}^{P}. If Θ + Γ ⊢ M = N : σ in λ2, then, for any \overline{a} ∈ T^{k} (k is the length of Θ), M [[[σ / Θ + Γ]]](\overline{a}) N (therefore P (M) and P (N)). Proof. Similarly to the proof of Theorem 4.5, we have M [[[σ / Θ + Γ]]](\overline{a}) N by Theorem 5.9. □

Example: uniqueness of normal form

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} {α | α ∈

T_{z}^{P_{ol}}, α = R_{ol}|dom(α)}. We say a term M is a function code from PER α to PER β, if for all c ∈ classes(α) and types σ, there exists d ∈ classes(β) such that app(σ, M, N) ∈ d for all N ∈ c. Let α, β be PERs, T be a family of PERs, and f be a function from T to the set of PERs.

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

△_{iβ}f =^{def} R_{ol}| \{M | \begin{matrix}M is a P -value, \\ and for all types τ and σ \\ app(σ, M, τ) ∈ dom(∩f) \end{matrix} \}

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

Lemma 6.5 PT (⟨T_{iβ}, ⇝_{iβ}, △_{iβ}⟩) is a λ2 semi-adjoint structure.

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 Theorem 6.3, M α N holds for some α ∈ T_{iβ}. Therefore, M R_{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 in the case of simply typed λ-calculus. (See also the subset interpretation in [13] 9.3.) 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. (This model is essentially the one given in [1].)

M_{1}(α ⇝_{e} β)M_{2} =^{def} \{ \begin{matrix}M_{i} is a P -value (i = 1, 2), \\ and for all N_{1} α N_{2} and types σ \\ app(σ, M_{1}, N_{1}) β 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 τ and σ \\ app(σ, M_{1}, τ) (∩f) app(σ, M_{2}, τ) \end{matrix}

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

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

Proof. (non-emptiness) The PER ⊤ defined by N_{1}⊤N_{2} =^{def} N_{i} is a P_{sn}-value (i = 1, 2) is in T_{sn}. Closedness under ⇝_{e} and △_{e} can be easily proved. □

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

Theorem 6.9 If Θ + Γ ⊢ M : σ in λ2, then M is strongly normalizable. Proof. By Theorem 6.3, M β M holds for some β ∈ T_{iβ}. Therefore, M satisfies P_{sn}(M). □

Extension

In the λ2 semi-adjoint structure, we have used concatenation as cartesian products to construct the interpretation of contexts from types. However, if we introduce pair terms without surjectivity of pairing, the cartesian product necessary to interpret such pair terms cannot be overloaded with the cartesian product used to interpret contexts. Suppose we extend types and terms of λ2 by

σ, τ ::= ⋯ | σ × τ, M, N ::= ⋯ | ⟨M, N⟩ | π_{1}M | π_{2}M

with appropriate type inference rules, and add the following rule to β-rules.

{Θ + Γ ⊢ ⟨M_{1}, M_{2}⟩ : σ_{1} × σ_{2} \atop Θ + Γ ⊢ π_{i}⟨M_{1}, M_{2}⟩ = M_{i} : σ_{i}}

To interpret this system, pair terms should be interpreted by using left semiadjoint functors of reindexing functors. Otherwise, we cannot prove Theorem 6.6. In the term model extended for this system, the left semi-adjoint Σ_{↓(E;A)} of the reindexing functor ↓(E; A)^{∗} is defined like this:

• Σ_{↓(E;\overline{θ}|σ)}(\overline{θ}\overline{γ}x^{σ}y^{τ} |M) =^{def} \overline{θ}\overline{γ}z^{σ×τ} |⟨π_{1}z^{σ×τ} , M[x^{σ}y^{τ} := (π_{1}z^{σ×τ})(π_{2}z^{σ×τ})]⟩

(z^{σ×τ} ∉ FV(M), [\overline{θ}\overline{γ}x^{σ}y^{τ} |M] : E, \overline{θ}|σ; \overline{θ}|τ ⟶ E, \overline{θ}|σ; C)

• Ψ(\overline{θ}\overline{γ}z^{σ×τ} |M) =^{def} \overline{θ}\overline{γ}x^{σ}y^{τ} |M[z^{σ×τ} := ⟨x^{σ}, y^{τ} ⟩]

(x^{σ}, y^{τ} ∉ FV(M), [\overline{θ}\overline{γ}z^{σ×τ} |M] : E; \overline{θ}|σ×τ ⟶ E; C)

• Φ(\overline{θ}\overline{γ}x^{σ}y^{τ} |M) =^{def} \overline{θ}\overline{γ}z^{σ×τ} |M[x^{σ}y^{τ} := (π_{1}z^{σ×τ})(π_{2}z^{σ×τ})]

(z^{σ×τ} ∉ FV(M), [\overline{θ}\overline{γ}x^{σ}y^{τ} |M] : E, \overline{θ}|σ; \overline{θ}|τ ⟶ E, \overline{θ}|σ; C)

Note that Ψ ∘ Φ = id but Φ ∘ Ψ ≠ id. Ψ ∘ Φ = id should hold because the dual of Lemma 5.1 holds, and Φ ∘ Ψ ≠ id reflects the fact that surjectivity of pairing is not required.

7 Conclusions and Future Works

We have defined a non-extensional category called a λ2 semi-adjoint structure using semi-adjointness and have shown that we can carry out the proof of several theorems such as strong normalizability or uniqueness of normal form in the term models constructed as instances of the category. We have also spelled out the extra conditions other than saturated-set conditions to make the term model categorical.

One of the first motivations of this work is to find the categorical structure for the model of CoC given by Stefanova and Geuvers [15]. But the goal is not achieved in this thesis, because in [15] types are interpreted by the saturated sets whereas we had to interpret types by PERs to make Π a right semi-adjoint functor. As remarked at the end of [15], the model construction in [15] can be done using PERs instead of saturated sets. We could find a similar structure as λ2 semi-adjoint structure in it, but, as a future work, we will investigate the categorical structure in the case of the saturated sets. It seems that more subtle structure such as P-category [5] or bicategory is necessary.

Acknowledgments

I would like to thank Masahito Hasegawa for helpful comments and Masahiko Sato for support and encouragements. I also thank anonymous referees for their valuable comments.

References

[1] Y. Akama. A Lambda-to-CL Translation for Strong Normalization. In Proc. of Typed Lambda Calculi and Applications, LNCS 1210, pages 1–10, 1997.

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

[3] 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.

[4] K. B. Bruce, A. R. Meyer, and J. C. Mitchell. The Semantics of Second-Order Lambda Calculus. Information and Computation, 85:76–134, 1990.

[5] D. Čubrić, P. Dybjer, and P. Scott. Normalization and the Yoneda Embedding. Mathematical Structures in Computer Science, 8:153–192, 1998.

[6] J. Gallier. On Girard’s “candidats de reductibilité”. In P. Odifreddi, editor, Logic and Computer Science, pages 123–203. Academic Press, 1990.

[7] S. Hayashi. Adjunction of Semifunctors: Categorical Structures in Nonextensional Lambda Calculus. Theoretical Computer Science, 41:95–104, 1985.

[8] 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.

[9] B. Jacobs. Semantics of Second-Order Lambda Calculus. Mathematical Structures in Computer Science, 1:327–360, 1991.

[10] 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.

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

[12] B. Jacobs. Categorical Logic and Type Theory. North-Holland, 1999.

[13] J. C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.

[14] R. A. G. Seely. Categorical Semantics of Higher-Order Polymorphic Lambda Calculus. J. Symb. Log., 52:969–989, 1987.

[15] 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.

A Fibration Model

In this section, we assume readers are familiar with the definition of the fibration and some related definitions (see, for example, [11, 12]). We give a more general categorical definition of λ2 semi-adjoint structure (Theorem A.4) using the theory of fibration over fibration [11, 12] and prove the soundness (Theorem A.8, A.17).

A.1 Preliminaries

Let p : 𝔼 ⟶ 𝔹 be a fibration. For an arrow u : A ⟶ B in 𝔹 and E over B, there is a cartesian lifting of u with the codomain u. We write \overline{u}E : u^{∗}E ⟶ E to denote the choice of the cartesian lifting (cleavage). In the following, we consider only cloven fibrations, that is, fibrations equipped with cleavages. The fibration p is called split if the cleavage satisfies \overline{v ∘ u}E = \overline{v}E ∘ \overline{u}v^{∗}E and \overline{id}E = id_{E}. For f : E′ ⟶ E ∈ 𝔼, there is a unique arrow f′ such that f = \overline{pf}E ∘ f′ and pf′ = id, because \overline{pf}E is cartesian. We will write v(f) for the arrow f′.

Definition A.1 (see [12]) Let p : 𝔼 ⟶ 𝔹 be a fibration and T be a subset of Obj(𝔼). When T satisfies the two conditions:

E ∈ Obj(𝔼) and X ∈ T with pE = pX has a product E × X, and
if E ∈ T and f : E′ ⟶ E is cartesian, then E′ ∈ T,

we define a fibration p^{T} : s_{p}(T) ⟶ 𝔼 as follows and call it a fibred CT-structure. s_{p}(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}]. The arrow ⟨f ∘ π_{1}, g⟩ in the definition of composition is in fact the following arrow (u = pf = pg).

E × X ^{v(f∘π_{1})×v(g)} u^{∗}E′ × u^{∗}X′ ^{≅} u^{∗}(E′ × X′) ^{\overline{u}(E′×X′)} E′ × X′

We define a fibration p^{T} by p^{T} (E; X) =^{def} E and p^{T} ([f, g]) =^{def} f, and its cleavage by \overline{f}(E; X) = [f, \overline{pf}X ∘ π_{2}] (f : E′ ⟶ E).

Note that the fibre s_{p}(T)_{E} is a category whose objects are E; X and arrows are [id_{E}, g], and the reindexing functor f^{∗} : s_{p}(T)_{E} ⟶ s_{p}(T)_{E′} (f : E′ ⟶ E) is induced as follows. ([id_{E}, g] : E; X ⟶ E; Y.)

f^{∗}(E; X) =^{def} E′; (pf)^{∗}X
f^{∗}[id_{E}, g] =^{def} [id_{E′}, (pf)^{∗}g ∘ (v(f) × id_{(pf)^{∗}X})]

Note also that if p is split, p^{T} is split.

Definition A.2 Let p : 𝔼 ⟶ 𝔹 be a fibration and D be a subset of Arr(𝔹) which is closed under pullback, that is, for every d : A ⟶ B ∈ D and h : B′ ⟶ B in 𝔹, there is a pullback

[figure: A′; h′; A; B′; d′; h; B; d]

such that d′ ∈ D. To denote the choice of the pullback, we write h^{∗}(d) for d′ and \overline{h}(d) for h′. We say p has D-semi-products if • for every d : A ⟶ B ∈ D, the reindexing functor d^{∗} : 𝔼_{B} ⟶ 𝔼_{A} has a

right semi-adjoint Π_{d},

• the semi-Beck-Chevalley condition holds, that is, for d, h, d′, h′ as above, the following conditions hold.

– h′^{∗}d^{∗} = d′^{∗}h^{∗}

– Π_{d′}h′^{∗} = h^{∗}Π_{d}

– h^{∗}Ψ_{X,Y} = Ψ_{h^{∗}X,h′^{∗}Y} h′^{∗} (X ∈ 𝔼_{A}, Y ∈ 𝔼_{B})

– h′^{∗}Φ_{X,Y} = Φ_{h′^{∗}X,h^{∗}Y} h^{∗} (X ∈ 𝔼_{A}, Y ∈ 𝔼_{B})

A.2 Semi-adjoint Model

Definition A.3 Let p : 𝔼 ⟶ 𝔹 be a fibration, T be a subset of Obj(𝔼), and Ω be an object of 𝔹. We put

D_{∗} =^{def} {π_{1} : E × X ⟶ E | E ∈ 𝔼, X ∈ T }
D_{□} =^{def} \{\overline{π_{1}}E : π_{1}^{∗}E ⟶ E | π_{1} : pE × Ω ⟶ pE in 𝔹\}

and give the choice of pullback as follows. For π_{1} : E × X ⟶ E ∈ D_{∗} and f : E′ ⟶ E,

f^{∗}(π_{1}) =^{def} π_{1} : E′ × (pf)^{∗}X ⟶ E′
\overline{f}(π_{1}) =^{def} f × \overline{pf}X

and for \overline{q}E : q^{∗}E ⟶ E ∈ D_{□} (q ≡ π_{1} : pE × Ω ⟶ pE) and f : E′ ⟶ E,

f^{∗}(\overline{q}E) =^{def} \overline{q′}E′ : q′^{∗}E′ ⟶ E′
\overline{f}(\overline{q}E) =^{def} \overline{pf}q^{∗}E ∘ q′^{∗}v(f)

where and q′ ≡ π_{1} : pE′ × Ω ⟶ pE′.

[figure: E′ × (pf)^{∗}X; f × \overline{pf}X; E × X; E′; π_{1}; f; E; π_{1}]

[figure: q′^{∗}E′; q′^{∗}v(f); ·; \overline{pf}q^{∗}E; q^{∗}E; E′; \overline{q′}E′; v(f); (pf)^{∗}E; \overline{q′}(pf)^{∗}E; \overline{pf}E; E; \overline{q}E]

This setting is called a λ2-category, if the following conditions hold.

• p is split, the reindexing functors preserve products × strictly, and there is a terminal object functor 1_{p} : 𝔹 ⟶ 𝔼.

• 𝔹 is a category with finite products (including terminal object 1_{𝔹}).

• p^{T} is a fibred CT-structure.

• p^{T} has D_{∗}-semi-products and D_{□} -semi-products.

• p has a split generic object G ∈ 𝔼 above Ω.

A λ2-category is non-trivial if there is an object • ∈ T such that p• = 1_{𝔹} and 𝔼_{1_{𝔹}}(1_{p}1_{𝔹}, •) ≠ ∅. A λ2-category is called a λη2-category if semi-adjoint functors Π in the definition of semi-products are functors.

We introduce some notations. We put ↓(E; X) =^{def} π_{1} : E × X ⟶ E for

E; X ∈ s_{p}(T), and ⇓(E) =^{def} \overline{π_{1}}E : π_{1}^{∗}E ⟶ E where π_{1} : pE × Ω ⟶ pE in 𝔹

for E ∈ 𝔼.

By the definition of the split generic object, for each E ∈ 𝔼, there is a unique arrow u ∈ 𝔹(pE, Ω) such that u^{∗}G = E. We will write ⌈E⌉ for the arrow u. Note that ⌈·⌉ is one-to-one.

Theorem A.4 1) A λ2 semi-adjoint structure gives rise to a λ2-category.

2) A λη2 adjoint structure gives rise to a λη2-category and a PL-category. Proof. 1) Let ⟨T, 𝔹, ℂ⟩ be a λ2 semi-adjoint structure. We will construct the each component of Definition A.3, but omit the proof that they satisfies the properties of λ2-category. 𝔼 is a category whose objects are ⋃_{k} Obj(ℂ_{k}) and arrows are (F, t) : E′ ⟶ E (E′ ∈ ℂ_{l}, E ∈ ℂ_{k}) where F : l ⟶ k is an arrow in 𝔹 and t : E′ ⟶ F^{∗}E is an arrow in ℂ_{l}. 𝔹 is 𝔹 of the λ2 semi-adjoint structure. (Note that 1_{𝔹} is 0.) p is a functor that maps E ∈ ℂ_{k} to k and (F, t) to F. 1_{p} is a functor that maps k ∈ 𝔹 to _{k}ϵ and F : k ⟶ l to (F, id_{_{k}ϵ}). T is ⋃_{k} _{k}T , Ω is 1, and G is id_{1} in 𝔹.

2) By the construction of 1), p^{T} is a λη2-category. By the discussion in [10], we can define an exponential E ⇒ E′ for any E, E′ ∈ 𝔼_{k} and show that p is a PL-category. □

We assume × is left associative, that is,

A_{0} × A_{1} ⋯ × A_{n−1} × A_{n} =^{def} (⋯ (A_{0} × A_{1}) × ⋯ × A_{n−1}) × A_{n}

⟨f_{0}, f_{1}, ⋯, f_{n−1}, f_{n}⟩ =^{def} ⟨⟨⋯ ⟨f_{0}, f_{1}⟩, ⋯, f_{n−1}⟩, f_{n}⟩

We define π_{≤i}^{n} : A_{0} × ⋯ × A_{n} ⟶ A_{0} × ⋯ × A_{i} as follows

π_{≤n}^{n} =^{def} id, π_{≤i−1}^{n} =^{def} π_{1} ∘ π_{≤i}^{n}

and define π_{i}^{n} : A_{0} × ⋯ × A_{n} ⟶ A_{i} by π_{i}^{n} =^{def} π_{2} ∘ π_{≤i}^{n}.

A.3 Interpretation

We give an interpretation of λ2 in the non-trivial λ2-category. For E ∈ 𝔼_{B}, we define E::• =^{def} E; •_{B} where •_{B} =^{def} !_{B}^{∗}• and !_{B} : B ⟶ 1_{𝔹} in 𝔹. (Note that 𝔼_{B}(1_{p}1_{𝔹}, •_{B}) ≠ ∅.) An arrow f ≡ [id_{E}, g] ∈ s_{p}(T)_{E} is called a base arrow if dom(g) = E::• and g = g_{0} ∘ π_{1} (π_{1} : E × •_{B} ⟶ E) for some g_{0}, Since g_{0} is uniquely determined (g ∘ ⟨id_{E}, e∘!⟩ = g_{0} ∘ π_{1} ∘ ⟨id_{E}, e∘!_{E}⟩ = g_{0} for e ∈ 𝔼_{B}(1_{p}1_{𝔹}, •_{B}) where !_{E} : E ⟶ 1_{p}1_{𝔹}), we write b(f) for ⟨id_{E}, g_{0}⟩.

Let Θ + Γ be a context, σ be a type, and M be a term. [[Θ + Γ]], [[Θ + Γ ; σ]], [[Θ + Γ | M]], if defined, are given by the following objects or arrows.

[[Θ]]  an object of 𝔹
[[Θ + Γ]]  an object of 𝔼_{[[Θ]]}
[[Θ + Γ ; σ]] an object of s_{p}(T)_{[[Θ+Γ]]}
[[Θ + Γ | M]] a base arrow of s_{p}(T)_{[[Θ+Γ]]}

We define [[Θ + Γ]], [[Θ + Γ ; σ]], [[Θ + Γ | M]] inductively by the following clauses. (We put [[σ / Θ + Γ]] =^{def} π_{2}(dom(↓[[Θ + Γ ; σ]])).)

• [[Θ]] =^{def} 1_{𝔹} × Ω × ⋯ × Ω (k times Ω)

where the length of Θ is k

• [[Θ + ⟨⟩]] =^{def} 1_{p}[[Θ]]

• [[Θ + Γ, x^{σ}]] =^{def} dom(↓[[Θ + Γ ; σ]])

• [[Θ + Γ ; X]] =^{def} [[Θ + Γ]]; π_{i}^{k}^{∗}G

where the length of Θ is k and X is the i-th type variable in Θ

• [[Θ + Γ ; σ→τ]] =^{def} Π_{↓[[Θ+Γ;σ]]}[[Θ + Γ, x^{σ} ; τ]]

• [[Θ + Γ ; ∀X.τ]] =^{def} Π_{⇓[[Θ+Γ]]}[[Θ, X + Γ ; τ]]

• [[Θ + Γ | x^{σ}]] =^{def} [id_{[[Θ+Γ]]}, π_{i}^{n}] : [[Θ + Γ]]::• ⟶ [[Θ + Γ ; σ]] where the length of Γ is n and x^{σ} is the i-th variable in Γ

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

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

where g ≡ b([[Θ + Γ | N]]),

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

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

[figure: [[]]::•; f; [[;σ→τ]]; [[x^{σ}]]::•; Φf; [[x^{σ} ; τ]]; [[]]::•; [[;τ]]; [[]]; [[x^{σ}]]; g; [[]]]

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

• [[Θ + Γ | λX.M]] =^{def} Ψ_{[[Θ+Γ]]::•,cod([[Θ,X+Γ|M]])}[[Θ, X + Γ | M]]

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

where g ≡ \overline{⟨id_{[[Θ]]}, ⌈[[σ / Θ + Γ]]⌉⟩}[[Θ, X + Γ]], if [[Θ + Γ | M]] has the following form

[[Θ + Γ | M]] : [[Θ + Γ]]::•  [[Θ + Γ ; ∀X.τ]]

In the following lemmas and propositions, we work in a non-trivial λ2category unless stated explicitly.

Lemma A.5 If FTV(σ) ∪ FTV(Γ) ⊆ Θ, then [[σ / Θ + Γ]] = [[σ / Θ + ⟨⟩]]. Proof. By Proposition 5.6, which holds in λ2-category too. □

Lemma A.6 Let k_{i} be the length of Θ_{i}, k = k_{1} + k_{2}, and q ≡ \overline{π_{≤k_{1}}^{k}}[[Θ_{1} + Γ]] where π_{≤k_{1}}^{k} : [[Θ_{1}, Θ_{2}]] ⟶ [[Θ_{1}]], then

q^{∗}[[Θ_{1} + Γ ; τ]] = [[Θ_{1}, Θ_{2} + Γ ; τ]].

Proof. By the induction given in Lemma A.7. □

Let k_{i} be the length of Θ_{i}, k = k_{1} + k_{2}, and FTV(σ) ⊆ Θ_{1}. We put

⌊_{Θ_{1}}σ_{Θ_{2}}⌋ =^{def} ⟨π_{≤k_{1}}^{k}, ⌈[[σ / Θ_{1}, Θ_{2} + ⟨⟩]]⌉, π_{k_{1}+1}^{k}, …, π_{k}^{k}⟩ : [[Θ_{1}, Θ_{2}]] ⟶ [[Θ_{1}, X, Θ_{2}]]

where π_{≤k_{1}}^{k} : [[Θ_{1}, Θ_{2}]] ⟶ [[Θ_{1}]], π_{j}^{k} : [[Θ_{1}, Θ_{2}]] ⟶ Ω. Note that ⌊_{Θ}σ_{⟨⟩}⌋ = ⟨id_{[[Θ]]}, ⌈[[σ / Θ + Γ]]⌉⟩.

Lemma A.7 Suppose FTV(σ) ⊆ Θ_{1}. Let g ≡ \overline{⌊_{Θ_{1}}σ_{Θ_{2}}⌋}[[Θ_{1}, X, Θ_{2} + Γ]], then

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ ; τ]] = [[Θ_{1}, Θ_{2} + Γ[X := σ] ; τ[X := σ]]].  (⋆)

Proof. Let |τ| be the size of τ (number of symbols in τ) and |x^{τ_{1}}, …, x^{τ_{n}}| = |τ_{1}| + ⋯ + |τ_{n}|. We prove by induction on |τ| + |Γ|. First, note that

\overline{⌊_{Θ_{1}}σ_{Θ_{2}}⌋}[[Θ_{1}, X, Θ_{2} + ⟨⟩]] = 1_{p}⌊_{Θ_{1}}σ_{Θ_{2}}⌋, dom(1_{p}⌊_{Θ_{1}}σ_{Θ_{2}}⌋) = [[Θ_{1}, Θ_{2} + ⟨⟩]]

and that (⋆) implies

dom(g′) = [[Θ_{1}, Θ_{2} + (Γ, y^{τ})[X := σ]]] where g′ ≡ \overline{⌊_{Θ_{1}}σ_{Θ_{2}}⌋}[[Θ_{1}, X, Θ_{2} + Γ, y^{τ}]].

• τ ≡ X: Let k be the length of Θ_{1}, Θ_{2} and X be the i-th variable of Θ_{1}, X, Θ_{2}.

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ ; X]] = g^{∗}([[Θ_{1}, X, Θ_{2} + Γ]]; π_{i}^{k+1}^{∗}G)
= [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; (pg)^{∗}π_{i}^{k+1}^{∗}G by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; ⌈[[σ / Θ_{1}, Θ_{2} + ⟨⟩]]⌉^{∗}G
= [[Θ_{1}, Θ_{2} + Γ[X := σ] ; σ]]

• τ ≡ Y ≢ X: Let k be the length of Θ_{1}, Θ_{2} and Y be the i-th variable of Θ_{1}, X, Θ_{2} and the j-th variable of Θ_{1}, Θ_{2}.

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ ; Y]] = g^{∗}([[Θ_{1}, X, Θ_{2} + Γ]]; π_{i}^{k+1}^{∗}G)
= [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; (pg)^{∗}π_{i}^{k+1}^{∗}G by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; π_{j}^{k}^{∗}G
= [[Θ_{1}, Θ_{2} + Γ[X := σ] ; Y]]

• τ ≡ τ_{1}→τ_{2}: There exist arrows g and g′ in the following diagram by I.H. and the following diagram is a pullback.

[[Θ_{1}, Θ_{2} + (Γ, x^{τ_{1}})[X := σ]]] \overline{\begin{matrix}g′ \\  \end{matrix}}[[Θ_{1}, X, Θ_{2} + Γ, x^{τ_{1}}]]

[figure: [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; π_{1}; g; [[Θ_{1}, X, Θ_{2} + Γ]]; π_{1}]

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ ; τ_{1}→τ_{2}]]
= g^{∗}Π_{↓[[Θ_{1},X,Θ_{2}+Γ;τ_{1}]]}[[Θ_{1}, X, Θ_{2} + Γ, x^{τ_{1}} ; τ_{2}]]
= Π_{↓[[Θ_{1},Θ_{2}+Γ[X:=σ];τ_{1}[X:=σ]]]}g′^{∗}[[Θ_{1}, X, Θ_{2} + Γ, x^{τ_{1}} ; τ_{2}]]
= Π[[Θ_{1}, Θ_{2} + (Γ, x^{τ_{1}})[X := σ] ; τ_{2}[X := σ]]] by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ] ; (τ_{1}→τ_{2})[X := σ]]]

• τ ≡ ∀Y.τ_{1}: There exist arrows g and g′ in the following diagram by I.H. and the following diagram is a pullback by Lemma A.6.

[[Θ_{1}, Θ_{2}, Y + Γ[X := σ]]] \overline{\begin{matrix}g′ \\  \end{matrix}}[[Θ_{1}, X, Θ_{2}, Y + Γ]]

[figure: [[Θ_{1}, Θ_{2} + Γ[X := σ]]]; \overline{π_{1}}[[Θ_{1}, Θ_{2} + Γ[X := σ]]]; g; [[Θ_{1}, X, Θ_{2} + Γ]]; \overline{π_{1}}[[Θ_{1}, X, Θ_{2} + Γ]]]

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ ; ∀Y.τ_{1}]]
= g^{∗}Π_{⇓[[Θ_{1},X,Θ_{2}+Γ]]}[[Θ_{1}, X, Θ_{2}, Y + Γ ; τ_{1}]]
= Π_{⇓[[Θ_{1},Θ_{2}+Γ[X:=σ]]]}g′^{∗}[[Θ_{1}, X, Θ_{2}, Y + Γ ; τ_{1}]]
= Π[[Θ_{1}, Θ_{2}, Y + Γ[X := σ] ; τ_{1}[X := σ]]] by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ] ; (∀Y.τ_{1})[X := σ]]]
□

Theorem A.8 (soundness) If Θ + Γ ⊢ M : σ, then [[Θ + Γ]], [[Θ + Γ ; σ]], and [[Θ + Γ | M]] are defined and cod([[Θ + Γ | M]]) = [[Θ + Γ ; σ]] in every non-trivial λ2-category. Proof. By induction on the derivation of Θ + Γ ⊢ M : σ. □

Lemma A.9

⌊_{Θ_{1},X,Θ_{2}}τ_{⟨⟩}⌋ ∘ ⌊_{Θ_{1}}σ_{Θ_{2}}⌋ = ⌊_{Θ_{1}}σ_{Θ_{2},Y} ⌋ ∘ ⌊_{Θ_{1},Θ_{2}}τ[X := σ]_{⟨⟩}⌋  (⋆)

Proof. By the definition of ⌊⌋ and Lemma A.6, the left-hand side and the right-hand side of (⋆) are (where k_{i} is the length of Θ_{i} and k = k_{1} + k_{2})

⟨π_{≤k_{1}}^{k}, ⌈[[σ / Θ_{1}, Θ_{2} + ⟨⟩]]⌉, π_{k_{1}+1}^{k}, …, π_{k}^{k}, ⌊_{Θ_{1},X,Θ_{2}}τ_{⟨⟩}⌋ ∘ ⌊_{Θ_{1}}σ_{Θ_{2}}⌋⟩ and
⟨π_{≤k_{1}}^{k}, ⌈[[σ / Θ_{1}, Θ_{2} + ⟨⟩]]⌉, π_{k_{1}+1}^{k}, …, π_{k}^{k}, ⌈[[τ[X := σ] / Θ_{1}, Θ_{2} + ⟨⟩]]⌉⟩

respectively. By Lemma A.7 and the definition of the generic object,

⌊_{Θ_{1}}σ_{Θ_{2}}⌋^{∗}[[Θ_{1}, X, Θ_{2} + ⟨⟩; τ]] = [[Θ_{1}, Θ_{2} + ⟨⟩; τ[X := σ]]]
⌊_{Θ_{1}}σ_{Θ_{2}}⌋^{∗}⌈[[τ / Θ_{1}, X, Θ_{2} + ⟨⟩]]⌉^{∗}G = ⌈[[τ[X := σ] / Θ_{1}, Θ_{2} + ⟨⟩]]⌉^{∗}G.

Since the generic object G is the split generic object,

⌈[[τ / Θ_{1}, X, Θ_{2} + ⟨⟩]]⌉ ∘ ⌊_{Θ_{1}}σ_{Θ_{2}}⌋ = ⌈[[τ[X := σ] / Θ_{1}, Θ_{2} + ⟨⟩]]⌉

holds. □

Lemma A.10 Suppose FTV(σ) ⊆ Θ_{1} and Θ_{1}, X, Θ_{2} + Γ ⊢ M : τ. Let g ≡ \overline{⌊_{Θ_{1}}σ_{Θ_{2}}⌋}[[Θ_{1}, X, Θ_{2} + Γ]], then

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ | M]] = [[Θ_{1}, Θ_{2} + Γ[X := σ] | M[X := σ]]].

Proof. By induction on the derivation of Θ_{1}, X, Θ_{2} + Γ ⊢ M : τ.

• (var): Let n be the length of Γ and x^{τ} be the i-th variable in Γ.

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ | x^{τ}]] = g^{∗}[id_{[[Θ_{1},X,Θ_{2}+Γ]]}, π_{i}^{n}]
= [id_{[[Θ_{1},Θ_{2}+Γ[X:=σ]]]}, (pg)^{∗}π_{i}^{n}]
= [id_{[[Θ_{1},Θ_{2}+Γ[X:=σ]]]}, π_{i}^{n}]
= [[Θ_{1}, Θ_{2} + Γ[X := σ] | x^{τ[X:=σ]}]]

• (→I): Let g′ be the arrow given in the case τ ≡ τ_{1}→τ_{2} of Lemma A.7.

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ | λx^{τ_{1}}.M]]
= g^{∗}Ψ[[Θ_{1}, X, Θ_{2} + Γ, x^{τ_{1}} | M]]
= Ψg′^{∗}[[Θ_{1}, X, Θ_{2} + Γ, x^{τ_{1}} | M]]
= Ψ[[Θ_{1}, Θ_{2} + (Γ, x^{τ_{1}})[X := σ] | M[X := σ]]] by I.H.
= Ψ[[Θ_{1}, Θ_{2} + Γ[X := σ] | (λx^{τ_{1}}.M)[X := σ]]]

• (→E): Let

h ≡ [[Θ_{1}, X, Θ_{2} + Γ | N]]
h′ ≡ [[Θ_{1}, Θ_{2} + Γ[X := σ] | N[X := σ]]]

and g′ be the arrow same as the above case. Since g^{∗}h = h′ by I.H., we have b(h) ∘ g = g′ ∘ b(h′).

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ | app(τ_{1}→τ_{2}, M, N)]]
= g^{∗}(b(h))^{∗}Φ[[Θ_{1}, X, Θ_{2} + Γ | M]]
= (b(h′))^{∗}g′^{∗}Φ[[Θ_{1}, X, Θ_{2} + Γ | M]]
= (b(h′))^{∗}Φg^{∗}[[Θ_{1}, X, Θ_{2} + Γ | M]]
= (b(h′))^{∗}Φ[[Θ_{1}, Θ_{2} + Γ[X := σ] | M[X := σ]]] by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ] | app(τ_{1}→τ_{2}, M, N)[X := σ]]]

• (∀I): Similar to the case (→I).

• (∀E): Suppose the following is the last rule.

Θ_{1}, X, Θ_{2} + Γ ⊢ M : ∀Y.τ_{1}

Θ_{1}, X, Θ_{2} + Γ ⊢ app(∀Y.τ_{1}, M, τ′) : τ_{1}[Y := τ′] FTV(τ′) ⊆ Θ_{1}, X, Θ_{2}

Let

h ≡ \overline{⌊_{Θ_{1},X,Θ_{2}}τ′_{⟨⟩}⌋}[[Θ_{1}, X, Θ_{2}, Y + Γ]]
h′ ≡ \overline{⌊_{Θ_{1},Θ_{2}}τ′[X := σ]_{⟨⟩}⌋}[[Θ_{1}, Θ_{2}, Y + Γ[X := σ]]]

and g′ be the arrow given in the case τ ≡ ∀Y.τ_{1} of Lemma A.7. By Lemma A.9, we have ⌊_{Θ_{1},X,Θ_{2}}τ′_{⟨⟩}⌋ ∘ ⌊_{Θ_{1}}σ_{Θ_{2}}⌋ = ⌊_{Θ_{1}}σ_{Θ_{2},Y} ⌋ ∘ ⌊_{Θ_{1},Θ_{2}}τ′[X := σ]_{⟨⟩}⌋. By taking the cartesian lifting of these arrows, we have h ∘ g = g′ ∘ h′.

g^{∗}[[Θ_{1}, X, Θ_{2} + Γ | app(∀Y.τ_{1}, M, τ′)]]
= g^{∗}h^{∗}Φ[[Θ_{1}, X, Θ_{2} + Γ | M]]
= h′^{∗}g′^{∗}Φ[[Θ_{1}, X, Θ_{2} + Γ | M]]
= h′^{∗}Φg^{∗}[[Θ_{1}, X, Θ_{2} + Γ | M]]
= h′^{∗}Φ[[Θ_{1}, Θ_{2} + Γ[X := σ] | M[X := σ]]] by I.H.
= [[Θ_{1}, Θ_{2} + Γ[X := σ] | app(∀Y.τ_{1}, M, τ′)[X := σ]]]
□

Proposition A.11 Suppose Θ + Γ ⊢ app(∀X.τ, λX.M, σ) : τ[X := σ]. Then

[[Θ + Γ | app(∀X.τ, λX.M, σ)]] = [[Θ + Γ | M[X := σ]]].

Proof. Let g ≡ \overline{⌊_{Θ}σ_{⟨⟩}⌋}[[Θ, X + Γ]].

[[Θ + Γ | app(∀X.τ, λX.M, σ)]] = g^{∗}Φ[[Θ + Γ | λX.M]]

= g^{∗}ΦΨ[[Θ, X + Γ | M]]

= g^{∗}[[Θ, X + Γ | M]] by ΦΨ = id

= [[Θ + Γ | M[X := σ]]] by Lemma A.10

□

Lemma A.12 Suppose Θ+Γ_{1}, x^{σ}, Γ_{2} ⊢ M : τ and x^{σ} ∉ FV(M). Let n_{i} be the length of Γ_{i}, n = n_{1}+n_{2}, and p ≡ ⟨π_{≤n_{1}}^{n+1}, π_{n_{1}+2}^{n+1}, …, π_{n+1}^{n+1}⟩ : [[Θ + Γ_{1}, x^{σ}, Γ_{2}]] ⟶ [[Θ + Γ_{1}, Γ_{2}]]. Then,

p^{∗}[[Θ + Γ_{1}, Γ_{2} | M]] = [[Θ + Γ_{1}, x^{σ}, Γ_{2} | M]].

Lemma A.13 Suppose Θ + Γ_{1} ⊢ N : σ and Θ + Γ_{1}, x^{σ}, Γ_{2} ⊢ M : τ. Let n_{i} be the length of Γ_{i}, n = n_{1} + n_{2}, and g ≡ ⟨b([[Θ + Γ_{1} | N]]) ∘ π_{≤n_{1}}^{n}, π_{n_{1}+1}^{n}, …, π_{n}^{n}⟩ : [[Θ + Γ_{1}, Γ_{2}]] ⟶ [[Θ + Γ_{1}, x^{σ}, Γ_{2}]]. Then,

g^{∗}[[Θ + Γ_{1}, x^{σ}, Γ_{2} | M]] = [[Θ + Γ_{1}, Γ_{2} | M[x^{σ} := N]]].

Proof. By induction on the derivation of Θ + Γ_{1}, x^{σ}, Γ_{2} ⊢ M : τ. □

Proposition A.14 Suppose Θ + Γ ⊢ app(σ→τ, λx^{σ}.M, N) : τ. Then

[[Θ + Γ | app(σ→τ, λx^{σ}.M, N)]] = [[Θ + Γ | M[x^{σ} := N]]].

Proof. Let g ≡ b([[Θ + Γ | N]]).

[[Θ + Γ | app(σ→τ, λx^{σ}.M, N)]] = g^{∗}Φ[[Θ + Γ | λx^{σ}.M]]
= g^{∗}ΦΨ[[Θ + Γ, x^{σ} | M]]
= g^{∗}[[Θ + Γ, x^{σ} | M]] by ΦΨ = id

= [[Θ + Γ | M[x^{σ} := N]]] by Lemma A.13

□

Proposition A.15 Suppose Θ+Γ ⊢ λX.app(∀X.τ, M, X) : ∀X.τ in λη2. Then

[[Θ + Γ | λX.app(∀X.τ, M, X)]] = [[Θ + Γ | M]]

in every non-trivial λη2-category. Proof. Similar to Proposition A.16. □

Proposition A.16 Suppose Θ + Γ ⊢ λx^{σ}.app(σ→τ, M, x^{σ}) : σ→τ in λη2. Then

[[Θ + Γ | λx^{σ}.app(σ→τ, M, x^{σ})]] = [[Θ + Γ | M]]

in every non-trivial λη2-category.

Proof. Since we have the following diagram

[figure: [[Θ + Γ, x^{σ}]]; g; [[Θ + Γ, x^{σ}, y^{σ}]]; q′; [[Θ + Γ, y^{σ}]]]

[figure: [[Θ + Γ, x^{σ}]]; π_{1}; q; [[Θ + Γ]]; π_{1}]

(g ≡ b([[Θ + Γ, x^{σ} | x^{σ}]]), q ≡ π_{1} : [[Θ + Γ, x^{σ}]] ⟶ [[Θ + Γ]]), we can prove the proposition as follows.

[[Θ + Γ | λx^{σ}.app(σ→τ, M, x^{σ})]] = Ψ[[Θ + Γ, x^{σ} | app(σ→τ, M, x^{σ})]]
= Ψg^{∗}Φ[[Θ + Γ, x^{σ} | M]]
= Ψg^{∗}Φq^{∗}[[Θ + Γ | M]] by Lemma A.12
= Ψg^{∗}q′^{∗}Φ[[Θ + Γ | M]]
= ΨΦ[[Θ + Γ | M]]
= [[Θ + Γ | M]] by ΨΦ = id
□

Theorem A.17 (soundness) If Θ + Γ ⊢ M = N : σ in λ2 (λη2), then [[Θ + Γ | M]] = [[Θ + Γ | N]] in every non-trivial λ2-category (resp. λη2-category). Proof. By Proposition A.11, A.14, A.15, A.16. □