Typed Applicative Structures and Normalization by Evaluation for System F^{ω}

Andreas Abel

Department of Computer Science Ludwig-Maximilians-University Munich

Abstract. We present a normalization-by-evaluation (NbE) algorithm for System F^{ω} with βη-equality, the simplest impredicative type theory with computation on the type level. Values are kept abstract and requirements on values are kept to a minimum, allowing many different implementations of the algorithm. The algorithm is verified through a general model construction using typed applicative structures, called type and object structures. Both soundness and completeness of NbE are conceived as an instance of a single fundamental theorem.

1 Introduction and Related Work

The Curry-Howard isomorphism, which identifies proofs with programs and propositions with types, is the basis of several type-theoretic theorem provers, such as Coq [INR07], Agda [Nor07], Epigram [CAM07] and LEGO [Pol94a]. In these systems, checking the validity of proofs or typings relies on deciding equality of types. Types are recognized as equal if they have the same normal form, this is why normalization plays a key role in the study of the theories underlying these theorem provers, such as the Calculus of Constructions (CC) which underlies Coq and LEGO, and Martin-Löf Type Theory which is the basis of Agda and Epigram. The hardwired type equality of these systems, often referred to as definitional equality, is necessarily intensional, since fully extensional equality is undecidable. The minimal equality is induced by just the computational laws (β-laws), yet, the stronger the hardwired equality, the less manual equality proofs, and the more succinct proofs can get. Thus, it is desirable to add bits of extensionality as long as decidability is preserved. For the CC, different directions have been explored, such as rewriting [Bla05,CWC07] and decision procedures [BJS07]. Our goal is to integrate η-laws. which provide some extensionality for functions, into definitional equality of CC.

Normalization by evaluation (NbE) [BS91,Dan99] is a systematic method to perform βη-normalization. In a first step, the object t of type T is evaluated. The resulting value d is then reified to an η-long β-normal form v. The reification process is directed by the shape of type T. NbE has proven a valid tool to structure extensional normalization, especially in the notoriously difficult case of sum types [ADHS01,BCF04,Bar08]. We are convinced it is the perfect tool to account for the meta-theory of η, thus, we are researching the type systems of the lambda cube with βη-equality given by judgements.

The lambda cube organizes type systems in three dimensions: dependency, impredicativity, and higher-order. In previous work [ACD07], we have adapted NbE to a dependent type theory with one predicative universe and judgmental βη-equality. What is the challenge when stepping up to impredicativity? Predicative type theories allow to define the semantics of types from below via induction-recursion [Dyb00], and the reification function can be defined by induction on types. This fails in the presence of impredicativity, where one first has to lay out a lattice of semantic type candidates and then define impredicative quantification using an intersection over all candidates [GLT89]. Hence, the semantic type structure is not inductive, and reification cannot be defined by induction on types.^{1} There are at least two ways out of this dilemma: Altenkirch, Hofmann, and Streicher [AHS96] construct a total normalization function type-wise while building a model for System F. In previous work [Abe08], I have conceived reification as a deterministic relation between value d and normal form v and their type T, and showed through a model construction that it corresponds to a total function.

In this work, we are moving one step closer to NbE for the CC: we are considering the simplest type system which features impredicativity and computation on the type level: the higher-order polymorphic lambda-calculus F^{ω}. It adds to the problem of impredicativity the difficulty that types are no longer fixed syntactic expressions as in System F, but they need to be normalized as well. One solution would be to keep types always in long normal form, e. g., by the use of hereditary substitutions [WCPW03,AR08]. This is possible since the types are simply-kinded, so normalization can be defined by induction on kinds. However, this approach would not scale, e.g., to CC, where “serious” computation is happening on the type level. Furthermore, we would like to use the same normalization procedure both on object and type level.

In our solution, reification of objects is directed by type values A. Syntactic types T are interpreted by a pair (A, A) of a type value A and a semantic type A which is a set of objects that are reifiable at type A. Furthermore, type value A reifies to a normal form V which is βη-equal to T. These considerations lead us to the concept of a type structure which captures the similarities between syntactic types, type values, and semantic types. Consequently, syntactic objects and their values both form an object structure over a type structure, the syntactical type structure in case of syntactic objects and the structure of type values in case of (object) values.

We reorganize a typical normalization proof for System F^{ω} by model construction [Gir72] into our framework of type and object structures. Central to such a normalization proof is the fundamental theorem of typing which states that ⦇t⦈ ∈ [[T]] for any object t of type T. Herein, ⦇t⦈ interprets object t in some applicative structure, for instance in the structure of syntactical objects. The semantic type [[T]] is a collection of values, typically a set of normalizing objects, where the function type [[T_{1} → T_{2}]] is defined à la Tait [Tai67], i. e., as all values f such that f applied to d inhabits [[T_{2}]] for all d in [[T_{1}]]. The essence of the fundamental theorem is that the (hereditarily) normalizing terms model the typing rules where these terms are a (non-proper) subset of the typable

1 The reflection function ↑, which is defined mutually inductive with reification, yields at universal quantification (↑^{∀XA}t)(B) = ↑^{A[B/X]}(t B). Clearly A[B/X] can be bigger as ∀XA. For similar reasons, the set of η-long normal forms cannot be defined by induction on the type in System F; it lacks the subformula property for normal forms.

terms.^{2} In our abstract setting, the fundamental theorem proves that a part of an object structure with the above function type definition is an object substructure, casting the fundamental theorem into an algebraic setting.

Or notions of type and object structures are very general, in essence typed versions of Barendregt’s syntactical applicative structures [Bar84, Def. 5.3.1]. The fundamental theorems we prove are also very general since we do not fix an interpretation of types; we only require that semantic types inhabit a candidate space. By choosing different candidate spaces we can harvest different results from the same fundamental theorem, e. g., soundness of NbE, completeness of NbE, or weak normalization of β- or βηreduction [Abe08].

syntax  value  semantics  structures
kind  κ ∈ Ki  Kripke family K_{Ξ} ⊆ T_{Ξ}^{κ} of sets of types  Ki, T̂
type T ∈ Ty_{Ξ}^{⋆} A ∈ T_{Ξ}^{⋆}  Kripke family A_{Δ} ⊆ D_{Δ}^{Ξ ⊢A} of sets of objects Ty, T , D̂
T ∈ Ty_{Ξ}^{κ→κ′} F ∈ T_{Ξ}^{κ→κ′} operator F ∈ D̂^{Ξ ⊢F:κ→κ′}
object t ∈ Obj_{Γ}^{Ξ ⊢T} d ∈ D_{Δ}^{Ξ ⊢A} —  Obj, D

Table 1. Systematics of kind, type, and object structures.

1.1 Overview

Table 1 systematizes the main structures introduced in this article. Kind structures are inhabited by kinds, the types of types of System F^{ω}. The free kind structure Ki is inhabited by the syntactic kinds κ which coincide with their values, since no computation takes place on the kind level. A kind κ can be interpreted as a family K of types which are drawn from a type structure T ; with Tait’s interpretation of the function arrow between kinds, the set T̂ of subsets of T forms another kind structure. Instances of type structures are Ty, which contains the syntactical types T, or T , which contains type values A of some sort, or D̂ which contains semantics types A, sets of objects, hence, subsets of an object structure D. At higher kinds κ → κ′, Ty is inhabited by proper type constructors, T by their values F, and D̂ by operators F on sets of objects. On the level of objects, we have syntactical objects t in structure Obj and values d in structure D.

All structures are sorted, so types always have a kind, and objects always have a type, syntactical objects a syntactical type, and values a type value. The reason is that we prove the fundamental theorems just once, and instantiate them, amongst other uses, to show soundness of NbE, which is formulated in terms of sorted, i. e., judgmental, equality.

1.2 Preliminaries

Contexts Ξ, Θ, Γ, Δ, Φ, Ψ are functions from variables to some codomain. We write ⋄ for the totally undefined function and Φ, x:a for the function Φ′ with domain dom(Φ)⊎

2 As a consequence, the hereditarily normalizing typable terms coincide with the typable terms.

{x} such that Φ′(x) = a and Φ′(y) = Φ(y) for y ≠ x. We say Ψ′ extends Ψ, written Ψ′ ≤ Ψ, if Ψ′(x) = Ψ(x) for all x ∈ dom(Ψ).

Families T_{Ξ} indexed by a context Ξ are always understood to be Kripke, i. e., Ξ′ ≤ Ξ implies T_{Ξ} ⊆ T_{Ξ′}. The notion Kripke family is also used for maps M_{Ξ}. There it implies that M does not depend on the context parameter, i. e., M_{Ξ}(a) = M_{Ξ′}(a) for a ∈ dom(M_{Ξ}) and Ξ′ ≤ Ξ. (Note that dom(M_{Ξ}) ⊆ dom(M_{Ξ′}) since M is Kripke.)

We identify a pair of functions (f, g) with the function h(x) = (f(x), g(x)), especially in the case of contexts (Δ, Γ) or environments (σ, ρ). We will sometimes drop the parentheses and write just the comma. We write (a ∈ A) → B(a) for the dependent function space {f ∈ A → ⋃_{a∈A} B(a) | f(a) ∈ B(a) for all a ∈ A}.

2 Syntax

In this section, we present the syntax and inference rules for System F^{ω}. The system consists of three levels: On the lowest level there live the objects, meaning polymorphic, purely functional programs. On the middle level live the types of objects, and the type constructors, which are classified by kinds that themselves inhabit the highest level.

Kinds κ ∈ Ki are given by the grammar κ ::= ⋆ | κ → κ′. Kind ⋆ classifies type constructors which are actually types, and kind κ → κ′ classifies the type constructors which map type constructors of kind κ to type constructors of kind κ′. In the following, we will refer to all type constructors as types.

Assume a countably infinite set of type variables TyVar whose members are denoted by X, Y, Z. Kinding contexts Ξ, Θ ∈ KiCxt are partial maps from the type variables into Ki. The set TyCst = {→, ∀^{κ} | κ ∈ Ki} contains the type constants C. Their kinds are given by the signature Σ ∈ TyCst → Ki defined by

Σ(→) = ⋆ → ⋆ → ⋆
Σ(∀^{κ}) = (κ → ⋆) → ⋆  for all κ ∈ Ki.

Types are given by the grammar T, U, V ::= C | X | λX: κ. T | T U, where X ∈ TyVar, and form a “simply-kinded” lambda calculus. As usual, we write T → U for → T U. Objects are given by the grammar t, u, v ::= x | λx: T. t | t u | ΛX: κ. t | t U and form a polymorphic lambda-calculus with type abstraction and type application. Herein, object variables x are drawn from a countably infinite set ObjVar which is disjoint from TyVar. We write b[a/x] for capture-avoiding substitution of a for variable x in syntactic expression b, and FV for the function returning the set of all free type and object variables of a syntactic expression.

Kinding, typing, and equality for System F^{ω} is given by five judgements whose inference rules are displayed in Figure 1.

Ξ ⊢ T : κ
Ξ ⊢ T = T′ : κ
Ξ; Γ ⊢ t : T
Ξ; Γ ⊢ t = t′ : T

Herein, the auxiliary judgement Ξ ⊢ Γ, read “Γ is a well-formed typing context in Ξ”, is defined as Ξ ⊢ Γ (x) : ⋆ for all x ∈ dom(Γ).

Kinding Ξ ⊢ T : κ. “In context Ξ, type T has kind κ.”

\overline{Ξ ⊢ C : Σ(C)}  \overline{Ξ ⊢ X : Ξ(X)}

\frac{Ξ, X:κ ⊢ T : κ′}{Ξ ⊢ λX:κ. T : κ → κ′}  \frac{Ξ ⊢ T : κ → κ′  Ξ ⊢ U : κ}{Ξ ⊢ T U : κ′}

Type equality Ξ ⊢ T = T′ : κ. “In context Ξ, types T and T′ are βη-equal of kind κ.”

\frac{Ξ, X:κ ⊢ T : κ′  Ξ ⊢ U : κ}{Ξ ⊢ (λX:κ. T) U = T [U/X] : κ′}  \frac{Ξ ⊢ T : κ → κ′}{Ξ ⊢ λX:κ. T X = T : κ → κ′} X ∉ dom(Ξ)
symmetry transitivity  \overline{Ξ ⊢ C = C : Σ(C)}  \overline{Ξ ⊢ X = X : Ξ(X)}

\frac{Ξ, X:κ ⊢ T = T′ : κ′}{Ξ ⊢ λX:κ. T = λX:κ. T′ : κ → κ′}  \frac{Ξ ⊢ T = T′ : κ → κ′  Ξ ⊢ U = U′ : κ}{Ξ ⊢ T U = T′ U′ : κ′}

Typing Ξ; Γ ⊢ t : T. “In contexts Ξ, Γ, object t has type T.”

\frac{Ξ ⊢ Γ}{Ξ; Γ ⊢ x : Γ (x)}  \frac{Ξ; Γ, x:U ⊢ t : T}{Ξ; Γ ⊢ λx:U. t : U → T}  \frac{Ξ; Γ ⊢ t : U → T  Ξ; Γ ⊢ u : U}{Ξ; Γ ⊢ t u : T}

\frac{Ξ ⊢ T : κ → ⋆  Ξ, X:κ; Γ ⊢ t : T X}{Ξ; Γ ⊢ ΛX:κ. t : ∀^{κ}T} X ∉ dom(Ξ)  \frac{Ξ; Γ ⊢ t : ∀^{κ}T  Ξ ⊢ U : κ}{Ξ; Γ ⊢ t U : T U}

\frac{Ξ; Γ ⊢ t : T Ξ ⊢ T = T′ : ⋆}{Ξ; Γ ⊢ t : T′}

Object equality Ξ; Γ ⊢ t = t′ : T. “In contexts Ξ, Γ, objects t and t′ are βη-equal of type T.”

\frac{Ξ; Γ, x:U ⊢ t : T  Ξ; Γ ⊢ u : U}{Ξ; Γ ⊢ (λx:U. t) u = t[u/x] : T}  \frac{Ξ; Γ ⊢ t : U → T}{Ξ; Γ ⊢ λx:U. t x = t : U → T} x ∉ dom(Γ)

\frac{Ξ, X:κ; Γ ⊢ t : T  Ξ ⊢ U : κ}{Ξ; Γ ⊢ (ΛX:κ. t) U = t[U/X] : T [U/X]}  \frac{Ξ; Γ ⊢ t : ∀^{κ}T}{Ξ; Γ ⊢ ΛX:κ. t X = t : ∀^{κ}T} X ∉ dom(Ξ)
symmetry transitivity
\frac{Ξ ⊢ Γ}{Ξ; Γ ⊢ x = x : Γ (x)}  \frac{Ξ ⊢ U = U′ : ⋆  Ξ; Γ, x:U ⊢ t = t′ : T}{Ξ; Γ ⊢ λx:U. t = λx:U′. t′ : U → T}

\frac{Ξ; Γ ⊢ t = t′ : U → T Ξ; Γ ⊢ u = u′ : U}{Ξ; Γ ⊢ t u = t′ u′ : T}

\frac{Ξ ⊢ T : κ → ⋆  Ξ, X:κ; Γ ⊢ t = t′ : T X}{Ξ; Γ ⊢ ΛX:κ. t = ΛX:κ. t′ : ∀^{κ}T} X ∉ dom(Ξ)  \frac{Ξ; Γ ⊢ t = t′ : ∀^{κ}T  Ξ ⊢ U = U′ : κ}{Ξ; Γ ⊢ t U = t′ U′ : T U}

\frac{Ξ; Γ ⊢ t = t′ : T Ξ ⊢ T = T′ : ⋆}{Ξ; Γ ⊢ t = t′ : T′}

Fig. 1. F^{ω}: kinding, type equality, typing, object equality.

3 Abstract Normalization by Evaluation

In the following, we present normalization by evaluation (NbE) for System F^{ω} for an abstract domain D of values and type values. This leaves the freedom to implement values in different ways, e. g., β-normal forms, weak head normal forms (as in Pollack’s constructive engine [Pol94b]), closures (as in Coquand’s type checker [Coq96]), tagged functions (Epigram 2 [CAM07]) or virtual machine instructions (compiled reduction in Coq [GL02]). All implementations of values that satisfy the interface given in the following can be used with our NbE algorithm, and in this article we provide a framework to prove all these implementations correct.

In this section, we will understand functions in terms of a programming language, i. e., partial and possibly non-terminating. We unify the syntax of kinds, types, and objects into a grammar of expressions Exp. Let Var = TyVar ∪ ObjVar.

Expressions Exp ∋ M, N ::= ⋆ | C | X | x | λx:M. N | ΛX:M. N | M N
Values  D ∋ d, e, f, A, B, F, G (abstract)

Environments Env are finite maps from variables to values. Look-up of variable x in environment ρ is written ρ(x), update of environment ρ with new value v for variable x is written ρ[x ↦ v], and the empty environment is written ⋄. The call fresh(ρ) returns a variable x which is not in dom(ρ).

Application and evaluation (see Fig. 2) make values into a syntactical applicative structure [Bar84, 5.3.1], provided the equations below are satisfied. Such structures will appear later, in a sorted setting, as type and object structures (defs. 3 and 19). Note that establishing the laws of evaluation can be arbitrarily hard, e. g., if ⦇ ⦈ involves an optimizing compiler.

Values are converted back to expressions through reification. However, this process can only be implemented for term-like value domains, in particular, we require an embedding of variables into D, and an analysis neView of values that arise as iterated application of a variable (a so-called neutral value) or as iterated application of a constant (a constructed value). Some constructed values are types or kinds, they are analyzed by tyView, which can actually be defined from neView.

Values d of type V in context Δ, which assigns type values to variables, are reified by a call to ↘^{⇑}(Δ, d, V). It is mutually defined with ↘^{⇑}(Δ, n) which returns the normal form M and type V of neutral value n. Later in this article, reification will be presented as two relations Δ ⊢ d ↘ M ⇓⇑ V such that Δ ⊢ d ↘ M ⇑ V iff ↘^{⇑}(Δ, d, V) = M and Δ ⊢ d ↘ M ⇓ V iff ↘^{⇓}(Δ, d) = (M, V).

NbE is now obtained as reification after evaluation. For closed expressions M of type or kind N we define

nbe(M, N) = ↘^{⇑}(⋄, ⦇M⦈_{⋄}, tyView⦇N⦈_{⋄}).

A concrete instance of NbE is obtained by defining a recursive data type D with the constructors:

Constr : TyCst → D^{∗} → D
Ne : Var → D^{∗} → D
Abs : (D → D) → D

Applicative structure D of values.

Application ·  : D → D → D
Evaluation ⦇ ⦈  : Exp → Env → D
⦇x⦈_{ρ}  = ρ(x)
⦇λx:M. N⦈_{ρ} · d = ⦇N⦈_{ρ[x↦d]}
⦇X⦈_{ρ}  = ρ(X)
⦇ΛX:M. N⦈_{ρ} · G = ⦇N⦈_{ρ[X↦G]}
⦇M N⦈_{ρ}  = ⦇M⦈_{ρ} · ⦇N⦈_{ρ}

D is term-like.

Embedding var : Var → D
View as neutral NeView ∋ n  ::= C | X | x | e d
neView  : D → NeView
neView⦇C⦈_{ρ}  = C
neView(var X)  = X
neView(var x)  = x
neView(e · d)  = e d if neView e is defined
View as type TyView ∋ V ::= ⋆ | A → B | ∀^{κ}F
tyView  : D → TyView
tyView ⦇⋆⦈_{ρ}  = ⋆
tyView ⦇M → N⦈_{ρ} = tyView ⦇M⦈_{ρ} → tyView ⦇N⦈_{ρ}
tyView ⦇∀^{κ}M⦈_{ρ}  = ∀^{κ} tyView ⦇M⦈_{ρ}

Reification.

↘^{⇑}  : Env → D → TyView → Exp
↘^{⇑}(Δ, f, A → B) = let x  = fresh(Δ) (U, ) = ↘^{⇓}(Δ, neView A)

in λx:U. ↘^{⇑}(Δ[x ↦ A], f · var x, tyView B)

↘^{⇑}(Δ, d, ∀^{κ}F) = let X = fresh(Δ) in ΛX:κ. ↘^{⇑}(Δ[X ↦ κ], d · var X, tyView(F · var X))
↘^{⇑}(Δ, e, ⋆)  = let (M, ) = ↘^{⇓}(Δ, neView e) in M
↘^{⇓}  : Env → NeView → Exp × TyView
↘^{⇓}(Δ, C)  = (C, Σ(C))
↘^{⇓}(Δ, X)  = (X, tyView(Δ(X)))
↘^{⇓}(Δ, x)  = (x, tyView(Δ(x)))
↘^{⇓}(Δ, e d)  = let (M, V) = ↘^{⇓}(Δ, e) in case V of
A → B ↦ (M (↘^{⇑}(Δ, d, tyView A)), tyView B)
∀^{κ}F ↦ (M (↘^{⇑}(Δ, d, κ)), tyView(F · d))

Normalization by evaluation. nbe(M, N) = ↘^{⇑}(⋄, ⦇M⦈_{⋄}, tyView⦇N⦈_{⋄})

Fig. 2. Specification of an NbE algorithm.

Application, evaluation, and variable embedding are given by the following equations.

(Constr C Gs) · G = Constr C (Gs, G)
(Ne x ds)  · d = Ne x (ds, d)
(Abs f)  · d = f d
⦇λx:M. N⦈_{ρ}  = Abs f  where f d = ⦇N⦈_{ρ[x↦d]}
⦇ΛX:M. N⦈_{ρ}  = Abs f  where f G = ⦇N⦈_{ρ[X↦G]}
⦇C⦈_{ρ}  = Constr C ()
var X  = Ne X ()
var x  = Ne x ()

This instance of NbE is now easily completed using the equations of the specification, and can be implemented directly in Haskell.

In this article we show that any instance of the NbE-specification terminates with the correct result for well-formed expressions of F^{ω}, i. e., we show the following two properties:

1. Soundness: if ⊢ M : N, then ⊢ nbe(M, N) = M : N.

2. Completeness: if ⊢ M : N and ⊢ M′ : N, then nbe(M, N) = nbe(M′, N) (same expression up to α).

In contrast to the untyped presentation in this section, which saves us from some repetition, we will distinguish the three levels of F^{ω} consequently in the remainder of the article.

4 Kind Structures

Definition 1 (Kind structure). A kind structure is a set 𝕂 with a distinguished element ⋆ ∈ 𝕂 and a binary operation → ∈ 𝕂 → 𝕂 → 𝕂.

The free kind structure is Ki. A kind structure can also consist of semantic kinds which are sets of types drawn from a type structure T . In the following, we present this abstractly.

Definition 2 (Kind candidate space). Let (𝕂^{κ}, ⊑^{κ}) be a Ki-indexed family of posets with a (polymorphic) binary operation → ∈ 𝕂^{κ} → 𝕂^{κ′} → 𝕂^{κ→κ′}. A kind candidate space ℂ consists of two families \underline{ℂ}^{κ}, \overline{ℂ}^{κ} ∈ 𝕂^{κ} indexed by κ ∈ Ki, written \underline{κ}, \overline{κ} if no ambiguity arises, such that

k-base \underline{⋆}  ⊑ \overline{⋆},
k-fun-i \underline{κ} → \overline{κ′} ⊑ \overline{κ → κ′},
k-fun-e \underline{κ → κ′} ⊑ \overline{κ} → \underline{κ′}.

For K ∈ 𝕂^{κ} we write κ ⊩_{ℂ} K and say κ realizes K w. r. t. ℂ iff \underline{κ} ⊑ K ⊑ \overline{κ}. For a family K^{κ} ∈ 𝕂^{κ} we write ⊩_{ℂ} K if κ ⊩_{ℂ} K^{κ} for all κ.

Lemma 1 (Realizability kind structure). In the context of the above definition: If → is antitone in its first argument and monotone in its second argument, then ℂ := {(κ, K) | κ ⊩_{ℂ} K\} constitutes a kind structure with distinguished element (⋆, \underline{⋆}) and operation (κ, K) → (κ′, K′) = (κ → κ′, K → K′).

Proof. We have ⋆ ⊩ \underline{⋆}, and κ ⊩ K and κ′ ⊩ K′ imply κ → κ′ ⊩ K → K′. ⊓ ⊔

5 Type Structures

In this section, we define type structures as an abstraction over syntactic types, type values, and semantic types. Type structures form a category which has finite products. Let Ty_{Ξ}^{κ} = {T | Ξ ⊢ T : κ}.

Definition 3 (Type structure). An (F^{ω}) type structure is a tuple (T , Cst, App, [[ ]] ) where T is a Kripke family T_{Ξ}^{κ} of sets with the following Kripke families of maps:

Cst_{Ξ}  ∈ (C ∈ TyCst) → T_{Ξ}^{Σ(C)}
App_{Ξ}^{κ→κ′} ∈ T_{Ξ}^{κ→κ′} → T_{Ξ}^{κ} → T_{Ξ}^{κ′}

Usually, we will just write F · G for App_{Ξ}^{κ→κ′}(F, G). Let ρ ∈ T_{Θ}^{Ξ} iff ρ(X) ∈ T_{Θ}^{Ξ(X)} for all X ∈ dom(Ξ). The interpretation function has the following properties:

\begin{aligned}[[ ]] & ∈ & Ty_{Ξ}^{κ} → T_{Θ}^{Ξ} → T_{Θ}^{κ} \\ [[C]]_{ρ} & = & Cst_{Θ}(C) \\ [[X]]_{ρ} & = & ρ(X) \\ [[λX:κ. T]]_{ρ} · G & = & [[T]]_{ρ[X↦G]} \\ [[T U]]_{ρ} & = & [[T]]_{ρ} · [[U]]_{ρ} \\ [[T [U/X]]]_{ρ} & = & [[T]]_{ρ[X↦[[U]]_{ρ}]} (∗) \end{aligned}

If the condition (∗) is fulfilled, we speak of a combinatory type structure, since (∗) is a characterizing property of combinatory algebras. The condition (∗) is only necessary since we chose to use eager substitution in the inference rules of F^{ω}, it can be dropped when switching to explicit substitutions [ACD08].

We use “interpretation” and “evaluation” synonymously. Note that while the equations determine the interpretation of constants, variables, and application, there is some freedom in the interpretation of functions [[λX: κ. T]]_{ρ}. It could be lambda-terms (taking T = Ty), set-theoretical functions (see Def. 28), functional values in an interpreter, machine code etc.

Since Cst_{Ξ} is independent of Ξ, we have Cst_{Ξ} = Cxt_{⋄}, we usually suppress the index Ξ in Cst_{Ξ}. We may even drop Cst altogether, i. e., we just write → ∈ T_{Ξ}^{⋆→⋆→⋆} instead of Cst(→) ∈ T_{Ξ}^{⋆→⋆→⋆}.

To avoid ambiguities when different type structures are in scope, we may write →_{T}, ∀_{T}^{κ}, ·_{T} and T [[ ]] to emphasize that we mean the type structure operations of T .

Simple examples of type structures are Ty and Ty modulo β, βη, or judgmental equality. In these instances, the interpretation function is parallel substitution.

Our notion of type structure essentially coincides with Barendregt’s syntactical applicative structure [Bar84, 5.3.1], except that we are working in a kinded setting and Barendregt in untyped lambda-calculus.

Definition 4 (Type structure morphism). Given two type structures S and T , a type structure morphism M : S → T is a Kripke family of maps M_{Ξ}^{κ} ∈ S_{Ξ}^{κ} → T_{Ξ}^{κ} that commute with the operations of S, i. e.,

\begin{aligned}M_{Ξ}^{κ}(C_{S}) & = & C_{T} & (C:κ) ∈ Σ \\ M_{Ξ}^{κ′}(F ·_{S} G) & = & M_{Ξ}^{κ→κ′}(F) ·_{T} M_{Ξ}^{κ}(G) & F ∈ S_{Ξ}^{κ→κ′}, G ∈ S_{Ξ}^{κ} \\ M_{Θ}^{κ}(S[[T]]_{ρ}) & = & T [[T]]_{M_{Θ}^{Ξ}∘ρ} & T ∈ Ty_{Ξ}^{κ}, ρ ∈ S_{Θ}^{Ξ} \end{aligned}

where (M_{Θ}^{Ξ} ∘ ρ)(X) := M_{Θ}^{Ξ(X)}(ρ(X)).

Definition 5 (Environment pairing). Given two type structures S, T and environments ρ ∈ S_{Θ}^{Ξ} and ρ′ ∈ T_{Θ}^{Ξ}, we define

(ρ, ρ′) ∈ (X ∈ dom(Ξ)) → S_{Θ}^{Ξ(X)} × T_{Θ}^{Ξ(X)}

pointwise by (ρ, ρ′)(X) = (ρ(X), ρ′(X)).

For the environment update operation then holds (ρ, ρ′)[X ↦ (G, G′)] = (ρ[X ↦ G], ρ′[X ↦ G′]).

Def. and Lem. 1 (Product type structure) Given two type structures S, T , the pointwise product

(S × T )_{Ξ}^{κ} = S_{Ξ}^{κ} × T_{Ξ}^{κ}

forms a new type structure with

C_{S×T}  := (C_{S}, C_{T})  for all C ∈ TyCst
(F, F′) · (G, G′) := (F · G, F′ · G′)
[[F]]_{ρ,ρ′}  := ([[F]]_{ρ}, [[F]]_{ρ′}).

Proof. One easily validates the laws

\begin{aligned}[[X]]_{ρ,ρ′} & = & (ρ, ρ′)(X) \\ [[λX:κ. T]]_{ρ,ρ′} · (G, G′) & = & [[T]]_{(ρ,ρ′)[X↦(G,G′)]} \\ [[T U]]_{ρ,ρ′} & = & [[T]]_{ρ,ρ′} · [[U]]_{ρ,ρ′} \end{aligned}

using the definition of application and evaluation. ⊓ ⊔

The two projections π_{1} : S × T → S and π_{2} : S × T → T are trivially type structure morphisms, and × is a product in the category of type structures and their morphisms.

5.1 Type Substructures and the Fundamental Theorem for Kinding

Definition 6 (Type substructure). Given a type structure T , the Kripke family S_{Ξ}^{κ} ⊆ T_{Ξ}^{κ} is a type substructure of T if

C_{T} ∈ S_{Ξ}^{κ}  for all (C:κ) ∈ Σ
·_{T} ∈ S_{Ξ}^{κ→κ′} → S_{Ξ}^{κ} → S_{Ξ}^{κ′}
T [[ ]] ∈ Ty_{Ξ}^{κ} → S_{Θ}^{Ξ} → S_{Θ}^{κ}

Basically, a type substructure is a subfamily which is still a type structure with the original operations. One could also say that S is a type substructure of T iff the identity on S is a type structure morphism from S to T . However, then the notion of type structure morphism must be set up more liberally, not requiring S to be a type structure a priori. In the following we simply write S ⊆ T to mean S_{Ξ}^{κ} ⊆ T_{Ξ}^{κ} for all κ, Ξ.

Lemma 2 (Projection type substructure). If S ⊆ T_{1} × T_{2} is a type substructure, so are π_{1}(S) ⊆ T_{1} and π_{2}(S) ⊆ T_{2}.

Definition 7 (Function space). We write K ∈ T̂^{κ} if K is a Kripke family of subsets K_{Ξ} ⊆ T_{Ξ}^{κ}. Given K ∈ T̂^{κ} and K′ ∈ T̂^{κ′} we define the Kripke function space

(K →T̂ K′)_{Ξ} = {F ∈ T_{Ξ}^{κ→κ′} | F · G ∈ K′_{Ξ′} for all Ξ′ ≤ Ξ and G ∈ K_{Ξ′}}

The set {(κ, K) | K ⊆ T^{κ} Kripke} forms the powerset kind structure with operation (κ, K) → (κ′, K′) = (κ → κ′, K →T̂ K′) and an arbitrarily chosen distinguished element (⋆, K_{0}) with K_{0} ⊆ T^{⋆}.

If no ambiguities arise, we write → for →T̂.

Definition 8 (Induced type structure). Let T be a type structure and S ⊆ T be Kripke. If

\begin{aligned}C_{T} & ∈ & S_{Ξ}^{κ} & for all (C:κ) ∈ Σ \\ S_{Ξ}^{κ→κ′} & = & (S^{κ} →T̂ S^{κ′})_{Ξ} \end{aligned}

then S is called induced or an induced type substructure of T (see Thm. 2).

Such an S is called induced since it is already determined by the choice of the denotation of the base kind S^{⋆}.

Theorem 2 (Fundamental theorem of kinding). Let T be a type structure. If S ⊆ T is induced, then S is a type substructure of T .

Proof. We mainly need to show that evaluation is well-defined. This is shown by induction on the kinding derivation, as usual.

Let ρ ∈ S_{Θ}^{Ξ}. We show ⦇T ⦈_{ρ} ∈ S_{Θ}^{κ} by induction on Ξ ⊢ T : κ. The cases for variables and constants are trivial.

Case

\frac{Ξ, X:κ ⊢ T : κ′}{Ξ ⊢ λX:κ. T : κ → κ′}

Since S is induced, it is sufficient to show ⦇λX : κ. T ⦈_{ρ} · G ∈ S_{Θ′}^{κ′} for arbitrary Θ′ ≤ Θ and G ∈ S_{Θ′}^{κ}. This follows from the induction hypothesis ⦇T ⦈_{ρ′} ∈ S_{Θ′}^{κ′} with ρ′ = ρ[X ↦ G] ∈ S_{Θ′}^{Ξ,X:κ}. Case

\frac{Ξ ⊢ T : κ → κ′ Ξ ⊢ U : κ}{Ξ ⊢ T U : κ′}

Since S^{κ→κ′} ⊆ S^{κ} →T̂ S^{κ′}, the goal follows by the induction hypotheses and ⦇T U⦈_{ρ} = ⦇T ⦈_{ρ} · ⦇U⦈_{ρ}.

⊓ ⊔

5.2 NbE for Types and Its Soundness

We are ready to define the reification relation for type values and show that NbE, i. e., the composition of evaluation of a syntactic type T and reification to a normal form V, is sound, i. e., T and V are judgmentally equal. As a byproduct, we show totality of NbE on well-kinded types. The structure T of type values is left abstract, a concrete definition will be given in Sect. ??. However, not every T permits reification of its inhabitants. It needs to include the variables which need to be distinguishable from each other and other type values. Neutral types, i. e., of the shape X · G, need to be analyzable into head X and spine G. We call a suitable T term-like; on such a T we can define contextual reification [ACD08,Abe08].

Definition 9 (Type structure with variables). A type structure T has variables if there exists a Kripke family of maps Var_{Ξ} ∈ (X ∈ dom(Ξ)) → T_{Ξ}^{Ξ(X)} such that Var_{Ξ}(X) ∈ T_{Ξ′}^{κ′} iff Ξ′(X) = κ′. Usually, we simply write X for Var_{Ξ}(X).

1. Types X · G are called neutral.

2. Types C · G are called constructed.

If clear from the context of discourse, we drop the index Ξ to Var. To disambiguate, we sometimes write Var_{T} to refer to the variable embedding of type structure T . Usually, we write T [[T]] instead of T [[T]]_{Var_{T}} for the interpretation in the identity environment.

Definition 10 (Term-like type structure). A type structure T is term-like if it has variables and there exists a Kripke family of partial maps

View_{Ξ}^{κ} ∈ T_{Ξ}^{κ} ⇀ {(C, G) ∈ TyCst × T_{Ξ}^{κ} | Σ(C) = κ → κ}
+ {(X, G) ∈ TyVar × T_{Ξ}^{κ} | Ξ(X) = κ → κ}

such that:

– View(F) = (C, G) iff F = Cst(C) · G.

– View(F) = (X, G) iff F = Var(X) · G.

Lemma 3 (Injectivity in term-like type structures). In a term-like type structure T , Cst and Var are families of injective maps and neutral and constructed application is injective, i. e., H · G = H′ · G′ implies H = H′ and G = G′ for neutral or constructed H, H′.

Proof. Assume, for instance H = X · G, H′ = X′ · G′ neutral. We have (X; G, G) = View(H · G) = View(H′ · G′) = (X′; G′, G′), thus X = X′, G = G′, and G = G′. Immediately, H = H′ follows. ⊓ ⊔

Trivially, Ty is a term-like type structure with Var_{Ty}(X) = X. The product of termlike type structures S and T is again term-like with Var_{S×T} = (Var_{S}, Var_{T}). Ty/=_{β} is term-like due to confluence of β-reduction. Ty modulo judgmental equality is not trivially term-like, since first injectivity of the type constructors needs to be proven.

Definition 11 (Reifiable type structure). A type structure T with variables is reifiable, if there are relations

Ξ ⊢ F ↘ V ⇑ κ  in Ξ, F reifies to V at kind κ,
Ξ ⊢ H ↘ U ⇓ κ  in Ξ, H reifies to U, inferring kind κ,

(where F, H ∈ T_{Ξ}^{κ} with H neutral or constructed, and V, U ∈ Ty_{Ξ}^{κ}) which obey the following rules:

\overline{Ξ ⊢ C ↘ C ⇓ Σ(C)}  \overline{Ξ ⊢ X ↘ X ⇓ Ξ(X)}

Ξ ⊢ H ↘ U ⇓ κ → κ′ Ξ ⊢ G ↘ V ⇑ κ = Ξ ⊢ H · G ↘ U V ⇓ κ′

Ξ ⊢ H ↘ U ⇓ ⋆ ; = ; Ξ ⊢ H ↘ U ⇑ ⋆  Ξ, X:κ ⊢ F · X ↘ V ⇑ κ′ ; = ; Ξ ⊢ F ↘ λX:κ. V ⇑ κ → κ′

Further, these reification relations must be deterministic in the following sense: For all Ξ, κ, F (inputs) and neutral or constructed H (input) there is at most one V (output) such that Ξ ⊢ F ↘ V ⇑ κ and at most one U and κ′ (outputs) such that Ξ ⊢ H ↘ U ⇓ κ′.

Seen as logic programs with inputs and outputs as indicated above, these relations denote partial functions, where ↘^{⇑} is defined by cases on the kind κ and and ↘^{⇓} by cases on the neutral value H.

Lemma 4 (Reification returns long normal form). If Ξ ⊢ F ↘ V ⇑ κ, then V is η-long β-normal.

Lemma 5 (Term-like type structure is reifiable). Any term-like type structure T is reifiable.

Proof. In the presence of View, the two relations can simply be defined inductively by the above rules. ⊓ ⊔ Why did we then bother to introduce the concept of a reifiable type structure, instead of just speaking of term-like type structures and define reification inductively? It is because we will show in Sec. 6.3 that the quotient of a reifiable type structure modulo some suitable equality remains reifiable.

We continue by constructing a model of the kinding rules which proves soundness of NbE for types. Kinds κ are interpreted as sets G_{Ξ}^{κ} of pairs (F, T) glued together [CD97] by reification, i. e., the type value F reifies to syntactic type T up to βη-equality. Function kinds are interpreted via Tait’s function space (see Def. 7), thus, the fundamental theorem of kinding yields that G is indeed a type structure.

Definition 12 (Glueing candidate). Fix a reifiable type structure T . We define the families \underline{Gl}, \overline{Gl} ⊆ T × Ty by

\overline{Gl}_{Ξ}^{κ} = \{(F, T) ∈ T_{Ξ}^{κ} × Ty_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇑ κ and Ξ ⊢ T = V : κ\},
\underline{Gl}_{Ξ}^{κ} = \{(H, T) ∈ T_{Ξ}^{κ} × Ty_{Ξ}^{κ} | Ξ ⊢ H ↘ U ⇓ κ and Ξ ⊢ T = U : κ\}.

A family S with \underline{Gl}^{κ} ⊆ S^{κ} ⊆ \overline{Gl}^{κ} is called a glueing candidate.

Lemma 6. Any glueing candidate S contains the constants.

Proof. Since Ξ ⊢ C ↘ C ⇓ Σ(C) we have Cst_{S}(C) = (C, C) ∈ \underline{Gl}_{Ξ}^{Σ(C)} ⊆ S_{Ξ}^{Σ(C)}. ⊓ ⊔

Lemma 7 (Glueing candidate space). \underline{Gl}^{κ}, \overline{Gl}^{κ} form a kind candidate space according to Def. 2.

Proof. Let us write \underline{κ}, \overline{κ} for \underline{Gl}^{κ}, \overline{Gl}^{κ}. We show k-fun-i . Assume (F, T) ∈ (\underline{κ} → \overline{κ′})_{Ξ} and show (F, T) ∈ \overline{κ → κ′}_{Ξ}. We have (X, X) ∈ \underline{κ}_{Ξ,X:κ}, hence, (F · X, T X) ∈ \overline{κ′}_{Ξ,X:κ}. That is, Ξ, X : κ ⊢ F · X ↘ V ⇑ κ′ and Ξ, X : κ ⊢ T X = V : κ′. It follows Ξ ⊢ F ↘ λX: κ. V ⇑ κ → κ′ and Ξ ⊢ λX: κ. T X = λX: κ. V : κ′. Since X ∉ dom(Ξ) we have Ξ ⊢ T = λX:κ. V : κ′. Thus, (F, T) ∈ \overline{κ → κ′}_{Ξ}. ⊓ ⊔

The last proof makes apparent why we work with kinded type structures; if elements of the Kripke function space had not been well-kinded, we would not have the information T ∈ Ty_{Ξ}^{κ→κ′} which is necessary to conclude Ξ ⊢ λX:κ. T X = T : κ′.

Def. and Lem. 3 (Glueing type structure) Given a type structure T , we define G ⊆ T × Ty by

\begin{aligned}G_{Ξ}^{⋆} & := & \underline{⋆}_{Ξ}, \\ G_{Ξ}^{κ→κ′} & := & (G^{κ} →{ \atop T ×Ty} G^{κ′})_{Ξ}. \end{aligned}

G is a glueing candidate, i. e., \underline{Gl}^{κ} ⊆ G^{κ} ⊆ \overline{Gl}^{κ} for all κ.

Proof. By induction on κ. By definition, ⋆ ⊩_{Gl} G^{⋆}, and κ ⊩_{Gl} G^{κ} and κ′ ⊩_{Gl} G^{κ′} imply

\underline{κ → κ′} ⊆ \overline{κ} → \underline{κ′} ⊆ G^{κ} → G^{κ′} ⊆ \overline{κ} → \underline{κ′} ⊆ \overline{κ → κ′}.

⊓ ⊔ Corollary 1. G is induced.

Proof. C_{G} ∈ G_{Ξ}^{Σ(C)} since any glueing candidate contains the constants, and G^{κ→κ′} = G^{κ} → G^{κ′} by definition. ⊓ ⊔

Since G is induced, by the fundamental theorem of kinding it is a type substructure of T × Ty.

Theorem 4 (Soundness of NbE for types). Let T be a reifiable type structure. If Ξ ⊢ T : κ then there is a V ∈ Ty_{Ξ}^{κ} such that Ξ ⊢ T [[T]]_{Var_{T}} ↘ V ⇑ κ and Ξ ⊢ T = V : κ.

Proof. Since (X, X) ∈ \underline{Gl}_{Ξ}^{Ξ(X)} ⊆ G_{Ξ}^{Ξ(X)} for all X ∈ dom(Ξ), for the identity valuation Var_{T ×Ty}(X) = (X, X) we have Var_{G} = Var_{T ×Ty} ∈ G_{Ξ}^{Ξ}.

By the fundamental theorem, G[[T]]_{Var_{G}} = (T [[T]]_{Var_{T}} , T) ∈ G_{Ξ}^{κ}. Since G_{Ξ}^{κ} ⊆ \overline{Gl}_{Ξ}^{κ}, we have that Ξ ⊢ T [[T]]_{Var_{T}} ↘ V ⇑ κ with Ξ ⊢ T = V : κ. ⊓ ⊔

The V returned by reification is the long normal form of T.

6 Type Groupoids

Completeness of NbE means that it models judgmental type equality, i. e., if Ξ ⊢ T = T′ : κ then Ξ ⊢ [[T]] ↘ V ⇑ κ and Ξ ⊢ [[T′]] ↘ V ⇑ κ. Completeness will be shown by a fundamental theorem of type equality. Judgmental equality is usually modelled by partial equivalence relations (PERs), which can be seen as groupoids. Hence, we introduce the notion of a groupoidal type structure, or type groupoid. The advantage over PERs is that we can directly reuse the fundamental theorem of kinding, instantiated to a groupoidal type structure ^{2}T of pairs of types, instead of having to prove this theorem again for kinds modelled as PERs.

Definition 13 (From Wikipedia, 2008-10-30:). A groupoid is a set G with a function −1 : G → G and a partial function ∗ : G ×G → G that have the following properties:

1. Associativity: For all a, b, c ∈ G, if a ∗ b and b ∗ c are defined, then (a ∗ b) ∗ c and a ∗ (b ∗ c) are defined and equal. Conversely, if either of these last two expressions is defined, then so is the other (and again they are equal).

2. Inverse: For all a ∈ G, a^{−1} ∗ a and a ∗ a^{−1} are defined.

3. Identity: For all a, b ∈ G, if a ∗ b is defined, then a ∗ b ∗ b^{−1} = a, and a^{−1} ∗ a ∗ b = b. (The previous axioms already show that these expressions are defined and unambiguous.)

Example 1 (PER as groupoid). A partial equivalence relation R over set S is a groupoid with (s, t)^{−1} = (t, s) and (r, s) ∗ (s, t) = (r, t).

Example 2 (Discrete groupoid). Any set S gives rise to a trivial groupoid with s^{−1} = s and ∗ is defined exactly on the diagonal of S × S, and there s ∗ s = s.

Lemma 8. (b^{−1})^{−1} = b.

Proof. (Uli Schoepp) First, note that b^{−1} = b^{−1} ∗ b ∗ b^{−1}. Hence (b^{−1})^{−1} = (b^{−1})^{−1} ∗ b^{−1} ∗ (b^{−1})^{−1} = (b^{−1})^{−1} ∗ b^{−1} ∗ b ∗ b^{−1} ∗ (b^{−1})^{−1} = b ∗ b^{−1} ∗ (b^{−1})^{−1} = b. ⊓ ⊔

Lemma 9. If a ∗ b is defined then (a ∗ b)^{−1} = b^{−1} ∗ a^{−1}.

Proof. First a = a ∗ b ∗ b^{−1}. Since (a ∗ b)^{−1} ∗ (a ∗ b) is defined, (a ∗ b)^{−1} = (a ∗ b)^{−1} ∗ a ∗ a^{−1} = (a ∗ b)^{−1} ∗ a ∗ b ∗ b^{−1} ∗ a^{−1} = b^{−1} ∗ a^{−1}. ⊓ ⊔

Definition 14 (Subgroupoid). Given a groupoid G, a set H ⊆ G is a subgroupoid if it is closed under inversion and composition, i.e., if

1. a ∈ H implies a^{−1} ∈ H, and

2. a, b ∈ H implies a ∗ b ∈ H if a ∗ b is defined.

6.1 Type Groupoids and the Fundamental Theorem of Type Equality

Definition 15 (Type groupoid). A type structure is groupoidal if each T_{Ξ}^{κ} is a groupoid, constants are preserved under inversion, and inversion and composition distribute over application, i. e.,

C^{−1}  = C

for all C ∈ TyCst,

(F · G)^{−1}  = F^{−1} · G^{−1},
(F · G) ∗ (F′ · G′) = (F ∗ F′) · (G ∗ G′).

Example 3. Each type structure is groupoidal for the trivial choice of inversion (identity) and composition (idempotent, defined on the diagonal).

Def. and Lem. 5 (Square type groupoid) Given a type structure T we define the square type groupoid^{2}T as the product type structure T × T equipped with

\begin{aligned}(F, G)^{−1} & = & (G, F), \\ (F, G) ∗ (G, H) & = & (F, H). \end{aligned}

Proof. The laws of a type groupoid are satisfied, e.g., for the last law we have

((F_{1}, F_{2}) ∗ (F_{2}, F_{3})) · ((G_{1}, G_{2}) ∗ (G_{2}, G_{3}))
= (F_{1}, F_{3}) · (G_{1}, G_{3})
= (F_{1} · G_{1}, F_{3} · G_{3})
= (F_{1} · G_{1}, F_{2} · G_{2}) ∗ (F_{2} · G_{2}, F_{3} · G_{3})
= ((F_{1}, F_{2}) · (G_{1}, G_{2})) ∗ ((F_{2}, F_{3}) · (G_{2}, G_{3}))
⊓ ⊔

Lemma 10 (Function space is groupoid). If K ∈ T̂^{κ} and K′ ∈ T̂^{κ′} are groupoids, so is K →T̂ K′ ∈ T̂^{κ→κ′}.

Proof. Analogous to the proof of Lemma 21. ⊓ ⊔ Definition 16 (Induced type groupoid). Let T be a type structure and E ⊆ ^{2}T . We say E is induced if E is an induced type structure and E_{Ξ}^{⋆} is groupoidal for all Ξ.

Since type equality refers to kinding, we will have to refer to the fundamental theorem of kinding in the proof of the fundamental theorem of type equality.

Lemma 11 (Fundamental theorem of kinding for type groupoids). Let T be a type structure and E ⊆ ^{2}T be induced. Then,

1. E is a type subgroupoid of^{2}T , and

2. if Ξ ⊢ T : κ and (ρ, ρ′) ∈ E_{Θ}^{Ξ} then (T [[T]]_{ρ}, T [[T]]_{ρ′}) ∈ E_{Θ}^{κ}.

Proof. 1. By induction on κ and Lemma 10 we show that E^{κ} is groupoidal.

2. This is just an instance of Theorem 2, since E[[T]]_{(ρ,ρ′)} = (T [[T]]_{ρ}, T [[T]]_{ρ′}). ⊓ ⊔

Definition 17 (Model/respect type equality). Let T be a type structure. We say that E ⊆ ^{2}T models type equality if Ξ ⊢ T = T′ : κ and (ρ, ρ′) ∈ E_{Θ}^{Ξ} imply (T [[T]]_{ρ}, T [[T′]]_{ρ′}) ∈ E_{Θ}^{κ}. A type structure T′ respects type equality if Ξ ⊢ T = T′ : κ implies T′[[T]]_{ρ} = T′[[T′]]_{ρ} for all ρ ∈ T′_{Θ}^{Ξ}.

Lemma 12 (Type structure modulo). Let T and E ⊆ ^{2}T be type structures such that E models type equality. Then T /E is a type structure respecting type equality.

Proof. Application and evaluation are well-defined in T /E since E is a type structure. T /E respects type equality since E models type equality. ⊓ ⊔

Theorem 6 (Fundamental theorem of type equality). Let T be a combinatory type structure and E ⊆ ^{2}T an induced type structure. Then E models type equality.

Proof. By induction on Ξ ⊢ T = T′ : κ. We give a few representative cases. Assume (ρ, ρ′) ∈ E_{Θ}^{Ξ}.

Case

\frac{Ξ ⊢ T : κ → κ′}{Ξ ⊢ λX:κ. T X = T : κ → κ′} X ∉ dom(Ξ)

Since E is induced, it is sufficient to assume arbitrary Θ′ ≤ Θ and (G, G′) ∈ E_{Θ′}^{κ} and show ([[λX:κ. T X]]_{ρ}, [[T]]_{ρ′}) · (G, G′) ∈ E_{Θ′}^{κ′}. Because X ∉ dom(Ξ) we have (ρ_{G}, ρ′) ∈ E_{Θ′}^{Ξ} for ρ_{G} := ρ[X ↦ G]. By induction hypothesis and Lemma 11, ([[T]]_{ρ_{G}}, [[T]]_{ρ′}) ∈ E_{Θ}^{κ→κ′}, hence, ([[T]]_{ρ_{G}} · G, [[T]]_{ρ′} · G′) ∈ E_{Θ′}^{κ′}. We are done, since [[λX:κ. T X]]_{ρ} · G = [[T X]]_{ρ_{G}} = [[T]]_{ρ_{G}} · G. Case

\frac{Ξ, X:κ ⊢ T : κ′ Ξ ⊢ U : κ}{Ξ ⊢ (λX:κ. T) U = T [U/X] : κ′}

Here we use the law [[T [U/X]]]_{ρ} = [[T]]_{ρ[X↦[[U]]_{ρ}]} of combinatory type structures.

Case

\frac{Ξ ⊢ T_{1} = T_{2} : κ Ξ ⊢ T_{2} = T_{3} : κ}{Ξ ⊢ T_{1} = T_{3} : κ}

Let F_{i} = [[T_{i}]]_{ρ} for i = 1, 2, 3. By induction hypothesis, (F_{1}, F_{2}), (F_{2}, F_{3}) ∈ E_{Θ}^{κ}. Since E_{Θ}^{κ} is a subgroupoid of ^{2}T_{Θ}^{κ} and (F_{1}, F_{2}) ∗ (F_{2}, F_{3}) is defined, we have (F_{1}, F_{3}) ∈ E_{Θ}^{κ}. ⊓ ⊔ 6.2 Completeness of NbE for Types

In the following we show that the relation “reify to the same η-long form” gives rise to an equivalence relation on types which models type equality. This implies that NbE is complete.

Def. and Lem. 7 (Kind candidate space for completeness) Let T be reifiable.

\overline{Per}_{Ξ}^{κ} = \{(F, F′) ∈ ^{2}T_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇑ κ and Ξ ⊢ F′ ↘ V ⇑ κ for someV ∈ Ty_{Ξ}^{κ}\}
\underline{Per}_{Ξ}^{κ} = \{(F, F′) ∈ ^{2}T_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇓ κ and Ξ ⊢ F′ ↘ V ⇓ κ for someV ∈ Ty_{Ξ}^{κ}\}

\underline{Per}^{κ} and \overline{Per}^{κ} are Kripke families of subgroupoids, and form a kind candidate space.

Proof. Composition (F_{1}, F_{2})∗(F_{2}, F_{3}) is well-defined since reification is deterministic. ⊓ ⊔

Def. and Lem. 8 (Type groupoid for completeness) Let T be a type structure. We define P^{κ} ⊆ ^{2}T^{κ} by recursion on κ:

\begin{aligned}P^{⋆} & := & \underline{Per}^{⋆}, \\ P^{κ→κ′} & := & P^{κ} →^{ ˆ2}T P^{κ′}. \end{aligned}

P is an induced type groupoid.

Theorem 9 (Completeness of NbE for types). Let T be a reifiable type structure. If Ξ ⊢ T = T′ : κ then Ξ ⊢ [[T]]_{Var} ↘ V ⇑ κ and Ξ ⊢ [[T′]]_{Var} ↘ V ⇑ κ for some V.

Proof. Since (Var, Var) ∈ P_{Ξ}^{Ξ}, by the fundamental theorem of type equality we have ([[T]]_{Var}, [[T′]]_{Var}) ∈ P_{Ξ}^{κ} ⊆ \overline{Per}_{Ξ}^{κ} which entails the goal. ⊓ ⊔

6.3 Type structure modulo reification

In the following we show that a type structure T modulo the equality P induced by Per is still reifiable, i. e., reification is compatible with P-equality. Since P is a kind candidate of space Per, it is clear that for (F, F′) ∈ P_{Ξ}^{κ}, the types F and F′ reify to the same expression under the ⇑-relation. What remains to show that his holds also for the ⇓-relation, provided F and F′ are neutral or constructed. Thus, we need to show that (F, F′) ∈ \overline{Per}_{Ξ}^{κ} implies (F, F′) ∈ \underline{Per}_{Ξ}^{κ} for such F, F′. The proof rests on the following strengthening lemma.

Lemma 13 (Strengthening of reification). Let T be a reifiable structure, F ∈ T_{Ξ}^{κ}, and ⇓⇑ ∈ {⇓, ⇑}. If Ξ′ ⊢ F ↘ T ⇓⇑ κ for some Ξ′ ≤ Ξ, then Ξ ⊢ F ↘ T ⇓⇑ κ.

Proof. By induction on T ∈ Ty_{Ξ}^{κ}, first proving the statement for ⇓, then for ⇑. In the case of a variable X ∈ T_{Ξ}^{κ}, we know Ξ(X) = κ, hence, Ξ ⊢ X ↘ X ⇓ κ. In case Ξ′ ⊢ F ↘ λX : κ_{1}. V ⇑ κ_{1} → κ_{2} we may assume w. l. o. g. that X ∉ dom(Ξ′). Hence, Ξ′, X: κ_{1} ≤ Ξ, X: κ_{1} and by induction hypothesis on V ∈ Ty_{Ξ,X:κ_{1}}^{κ_{2}} we have Ξ, X:κ_{1} ⊢ F · X ↘ V ⇑ κ_{2}, thus, Ξ ⊢ F ↘ λX:κ_{1}. V ⇑ κ_{1} → κ_{2}. ⊓ ⊔

Using strengthening, we can show that ⇑ for neutral and constructed types, which returns the η-long form, embeds into ⇓, modulo η-equality.

Lemma 14 (Reification of neutral and constructed types). Let T be a reifiable type structure. Let H ∈ T_{Ξ}^{κ} be neutral or constructed. If Ξ ⊢ H ↘ V ⇑ κ then Ξ ⊢ H ↘ U ⇓ κ and Ξ ⊢ U = V : κ.

Proof. By induction on κ. Trivial for κ = ⋆. In case κ = κ_{1} → κ_{2}, we have

Ξ, X:κ_{1} ⊢ H · X ↘ V ⇑ κ_{2} = Ξ ⊢ H ↘ λX:κ_{1}. V ⇑ κ_{1} → κ_{2}

Analyzing the induction hypothesis Ξ, X : κ_{1} ⊢ H · X ↘ U′ ⇓ κ_{2}, we get Ξ, X : κ_{1} ⊢ H ↘ U ⇓ κ_{1} → κ_{2} and Ξ, X : κ_{1} ⊢ U X = V : κ_{2}. Since H ∈ T_{Ξ}^{κ}, we get by Lemma 13, Ξ ⊢ H ↘ U ⇓ κ_{1} → κ_{2}, hence, Ξ ⊢ U : κ_{1} → κ_{2}. This entails Ξ ⊢ U = λX:κ_{1}. V : κ_{1} → κ_{2}. ⊓ ⊔

Corollary 2. If (H, T) ∈ \overline{Per}_{Ξ}^{κ} and H is neutral or constructed, then (H, T) ∈ \underline{Per}_{Ξ}^{κ}.

Theorem 10 (Type structure modulo reification). Let T be a reifiable type structure and P defined as above. Then T /P is reifiable and respects type equality.

Proof. Since P models type equality, we only need to show that both reification relations are well-defined on T /P. First, if Ξ ⊢ F ↘ V ⇑ κ and Ξ ⊢ F′ ↘ V′ ⇑ κ and (F, F′) ∈ P_{Ξ}^{κ} ⊆ \overline{Per}_{Ξ}^{κ} then V = V′ since reification is deterministic. Secondly, if Ξ ⊢ H ↘ U ⇓ κ and Ξ ⊢ H′ ↘ U′ ⇓ κ for neutral or constructed (H, H′) ∈ P_{Ξ}^{κ}, then by Cor. 2 (H, H′) ∈ \underline{Per}_{Ξ}^{κ}, hence, U = U′. ⊓ ⊔

Observe however, that T is term-like whereas T /P is not.

7 Object Structures

In this section, we introduce object structures which model both the syntactic object structure Obj indexed by syntactic types in Ty and structures of values D indexed by type values from a structure T . The following development, leading up the fundamental theorem of typing and the soundness of NbE for objects, parallels the preceding one on the type level. However, while we could define the glueing type structure G^{κ} by induction on kind κ, we cannot define a similar glueing objects structure gl by induction on types, due to impredicativity. Hence, we will define gl as a structure of candidates for semantic types.

Definition 18 (Typing context). Given a type structure T , a T_{Ξ}-context Δ ∈ T_{Ξ}^{cxt} is a partial map from the term variables into T_{Ξ}^{⋆}. If Γ ∈ Ty_{Ξ}^{cxt} and ρ ∈ T_{Θ}^{Ξ} then [[Γ]]_{ρ} ∈ T_{Θ}^{cxt} is defined by [[Γ]]_{ρ}(x) = [[Γ (x)]]_{ρ}.

Let Obj_{Γ}^{Ξ ⊢T} = {t | Ξ; Γ ⊢ t : T }.

Definition 19 (Object structure). Let T be a type structure. An object structure over T is a family D^{Ξ ⊢A} (A ∈ T_{Ξ}^{⋆}) of Kripke sets indexed by T_{Ξ}-contexts Δ such that Ξ′ ≤ Ξ implies D_{Δ}^{Ξ ⊢A} = D_{Δ}^{Ξ′ ⊢A}. It respects type equality, i. e., Ξ ⊢ T = T′ : ⋆ implies D^{Θ ⊢[[T]]_{ρ}} = D^{Θ ⊢[[T′]]_{ρ}} for any ρ ∈ T_{Θ}^{Ξ}, and there are operations:

app_{Δ}^{Ξ ⊢A→B} ∈ D_{Δ}^{Ξ ⊢A→B} → D_{Δ}^{Ξ ⊢A} → D_{Δ}^{Ξ ⊢B},
TyApp_{Δ}^{Ξ ⊢∀^{κ}F} ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} → (G ∈ T_{Ξ}^{κ}) → D_{Δ}^{Ξ ⊢F ·G}.

We write · for both of these operations. For Δ, Ψ ∈ T_{Θ}^{cxt}, let η ∈ D_{Δ}^{Θ ⊢Ψ} iff η(x) ∈ D_{Δ}^{Θ ⊢Ψ(x)} for all x ∈ dom(Ψ). We stipulate a family of evaluation functions

⦇ ⦈^{ρ} ∈ Obj_{Γ}^{Ξ ⊢T} → D_{Δ}^{Θ ⊢[[Γ]]_{ρ}} → D_{Δ}^{Θ ⊢[[T]]_{ρ}}

indexed by ρ ∈ T_{Θ}^{Ξ} which satisfy the following equations:

\begin{aligned}⦇x⦈_{η}^{ρ} & = & η(x) \\ ⦇r s⦈_{η}^{ρ} & = & ⦇r⦈_{η}^{ρ} · ⦇s⦈_{η}^{ρ} \\ ⦇t U⦈_{η}^{ρ} & = & ⦇t⦈_{η}^{ρ} · [[U]]_{ρ} \\ ⦇t[u/x]⦈_{η}^{σ} & = & ⦇t⦈_{η[x↦⦇u⦈_{η}^{σ}]}^{σ} & (∗) \end{aligned}  \begin{aligned}⦇λx:U. t⦈_{η}^{ρ} · d & = & ⦇t⦈_{η[x↦d]}^{ρ} & ifd ∈ D_{Δ}^{Θ ⊢[[U]]_{ρ}} \\ ⦇ΛX:κ. t⦈_{η}^{ρ} · G & = & ⦇t⦈_{η}^{ρ[X↦G]} & ifG ∈ T_{Θ}^{κ} \\ ⦇t[U/X]⦈_{η}^{σ} & = & ⦇t⦈_{η}^{σ[X↦[[U]]_{σ}]} & (∗) \end{aligned}

Again, (∗) have to hold only in combinatory object structures.

With parallel substitution, Obj (modulo β, βη, or judgmental equality) forms an object structure over Ty (modulo the same equality).

Definition 20 (Object substructure). Let S, T be type structures with S ⊆ T and let D be an object structure over T . Let E^{Ξ ⊢A} ⊆ D^{Ξ ⊢A} be a Kripke family of subsets indexed by Δ ∈ S_{Ξ}^{cxt} for all A ∈ S_{Ξ}^{⋆}. Then E is an object substructure of D over S if application and evaluation are well defined on E.

app_{Δ}^{Ξ ⊢A→B} ∈ E_{Δ}^{Ξ ⊢A→B} → E_{Δ}^{Ξ ⊢A} → E_{Δ}^{Ξ ⊢B}
TyApp_{Δ}^{Ξ ⊢∀^{κ}F} ∈ E_{Δ}^{Ξ ⊢∀^{κ}F} → (G ∈ S_{Ξ}^{κ}) → E_{Δ}^{Ξ ⊢F ·G}
⦇ ⦈^{ρ}  ∈ Obj_{Γ}^{Ξ ⊢T} → E_{Δ}^{Θ ⊢S[[Γ]]_{ρ}} → E_{Δ}^{Θ ⊢S[[T]]_{ρ}}
for all Δ ∈ S_{Θ}^{cxt} and ρ ∈ S_{Θ}^{Ξ}.

Definition 21 (Reindexed object structure). Let M : S → T be a type structure morphism and D an object structure over T . The type structure E^{Ξ ⊢A} := D^{Ξ ⊢M(A)} over S with

\begin{aligned}f ·_{E} d & := & f ·_{D} d \\ d ·_{E} G & := & d ·_{D} (M(G)) \\ E⦇ ⦈^{ρ} & := & D⦇ ⦈^{M∘ρ} \end{aligned}

is called D reindexed by M.

Definition 22 (Object structure morphism). Let M : S → T be a type structure morphism and D an object structure over S and E one over T . An object structure morphism m : D → E is a Kripke family of maps

m_{Δ}^{Ξ ⊢A} ∈ D_{Δ}^{Ξ ⊢A} → E_{M_{Ξ}^{⋆}∘Δ}^{Ξ ⊢M_{Ξ}^{⋆}(A)}

which commute with application and evaluation, i. e.,

m(f ·_{D} d) = m(f) ·_{E} m(d)
for all f ∈ D_{Δ}^{Ξ ⊢A→B}, d ∈ D_{Δ}^{Ξ ⊢A}
m(d ·_{D} G) = m(d) ·_{E} M(G)
for all d ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} , G ∈ T_{Ξ}^{κ}
m(D⦇t⦈_{η}^{ρ}) = E⦇t⦈_{m∘η}^{M∘ρ}
for all T ∈ Ty_{Ξ}^{⋆}, t ∈ Obj_{Γ}^{Ξ ⊢T} , ρ ∈ S_{Θ}^{Ξ}, η ∈ D_{Δ}^{Θ ⊢S[[Γ]]_{ρ}}.

Definition 23 (Product object structure). Given object structures D_{1} over T_{1} and D_{2} over T_{1} we define the product object structure D_{1}×D_{2} over T_{1}×T_{2} by (D_{1} × D_{2})_{(Δ_{1},Δ_{2})}^{Ξ ⊢(A_{1},A_{2})} := D_{1}_{Δ_{1}}^{Ξ ⊢A_{1}} × D_{2}_{Δ_{2}}^{Ξ ⊢A_{2}} with

\begin{aligned}(f_{1}, f_{2}) ·_{D_{1}×D_{2}} (d_{1}, d_{2}) & := & (f_{1} ·_{D_{1}} d_{1}, f_{2} ·_{D_{2}} d_{2}) \\ (d_{1}, d_{2}) ·_{D_{1}×D_{2}} (G_{1}, G_{2}) & := & (d_{1} ·_{D_{1}} G_{1}, d_{2} ·_{D_{2}} G_{2}) \\ (D_{1} × D_{2})⦇t⦈_{η_{1},η_{2}}^{(ρ_{1},ρ_{2})} & := & (D_{1}⦇t⦈_{η_{1}}^{ρ_{1}}, D_{2}⦇t⦈_{η_{2}}^{ρ_{2}}). \end{aligned}

7.1 Realizability Type Structure and the Fundamental Theorem of Typing Fix some term-like type structure T and an object structure D over T . Let A ∈ D̂_{Ξ}^{A} if A_{Δ} ⊆ D_{Δ}^{Ξ ⊢A} and A is Kripke. D̂_{Ξ}^{A} forms a complete lattice for all Ξ, A. Lemma 15. If Ξ′ ≤ Ξ then D̂_{Ξ}^{A} = D̂_{Ξ′}^{A}. Proof. D_{Δ}^{Ξ ⊢A} = D_{Δ}^{Ξ′ ⊢A}. ⊓ ⊔

Definition 24 (Function space and type abstraction on D̂).

→D̂  ∈ D̂_{Ξ}^{A} → D̂_{Ξ}^{B} → D̂_{Ξ}^{A→B}
(A → B)_{Δ} := {f ∈ D_{Δ}^{Ξ ⊢A→B} | for all d, Δ′ ≤ Δ, d ∈ A_{Δ′} impliesf · d ∈ B_{Δ′}}
( . )^{∀^{κ}F} ∈ (G ∈ T_{Ξ}^{κ}) → D̂_{Ξ}^{F ·G} → D̂_{Ξ}^{∀^{κ}F}
(G.A)_{Δ}^{∀^{κ}F} := {d ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} | d · G ∈ A_{Δ}}

Constructors of higher kind are interpreted as operators on Kripke sets. Definition 25 (Kripke operators of higher kind). We define D̂_{Ξ}^{F:κ} by

\begin{aligned}D̂_{Ξ}^{A:⋆} & := & D̂_{Ξ}^{A}, \\ D̂_{Ξ}^{F:κ→κ′} & := & (G ∈ T_{Ξ}^{κ}) → D̂_{Ξ}^{G:κ} → D̂_{Ξ}^{F ·G:κ′}. \end{aligned}

Definition 26 (Type candidate space). A type candidate space C for D over T consists of two Kripke sets \underline{C}^{Ξ ⊢A}, \overline{C}^{Ξ ⊢A} ∈ D̂_{Ξ}^{A}, (written \underline{A}, \overline{A} if no ambiguities arise) for each type A ∈ T_{Ξ}^{⋆} such that the following conditions hold.

k-ne  \underline{H}  ⊆ \overline{H}  ∈ D̂_{Ξ}^{H}  ifH neutral
k-fun-e \underline{A → B} ⊆ \overline{A} →D̂ \underline{B} ∈ D̂_{Ξ}^{A→B}
k-fun-i \underline{A} →D̂ \overline{B} ⊆ \overline{A → B} ∈ D̂_{Ξ}^{A→B}
k-all-e \underline{∀^{κ}F}  ⊆ G.\underline{F · G} ∈ D̂_{Ξ}^{∀^{κ}F} ifG ∈ T_{Ξ}^{κ}
k-all-i X.\overline{F · X} ⊆ \overline{∀^{κ}F}  ∈ D̂_{Ξ}^{∀^{κ}F} ifX ∉ dom(Ξ)

Definition 27 (Realizable semantic types). If F ∈ T_{Ξ}^{κ} and F ∈ D̂_{Ξ}^{F:κ} then F ⊩_{C}^{κ} F (pronounced F realizes F) is defined by induction on κ as follows:

\begin{aligned}A ⊩_{C}^{⋆} A & :⟺ & \underline{A} ⊆ A ⊆ \overline{A} \\ F ⊩_{C}^{κ→κ′} F & :⟺ & F · G ⊩_{C}^{κ′} F(G, G) for all G ⊩_{C}^{κ} G \end{aligned}

We define the Kripke families T D̂ and C ⊆ T D̂ by

\begin{aligned}T D̂_{Ξ}^{κ} & = & \{(F, F) ∈ T_{Ξ}^{κ} × D̂_{Ξ}^{F:κ}\} \\ C_{Ξ}^{κ} & = & \{(F, F) ∈ T_{Ξ}^{κ} × D̂_{Ξ}^{F:κ} | F ⊩_{C}^{κ} F\}. \end{aligned}

For the remainder of this section, we fix a type candidate space C. Type variables are embedded into the semantic type structure as \underline{X} ∈ D̂_{Ξ}^{X:Ξ(X)}. To define \underline{X}, we have to actually define \underline{H} for all neutral H.

Def. and Lem. 11 (Neutral realizable semantic types) Given a type candidate space, for a neutral H ∈ T_{Ξ}^{κ} we define \underline{H}, \overline{H} ∈ D̂_{Ξ}^{H:κ} by induction on κ. For base kind ⋆, it is already defined, for higher kinds we set

\begin{aligned}\overline{H}(G, G) & := & \overline{H G}, \\ \underline{H}(G, G) & := & \underline{H G}. \end{aligned}

Clearly, H ⊩^{κ} \underline{H} and H ⊩^{κ} \overline{H}.

Definition 28 (Interpretation into D̂). For T ∈ Ty_{Ξ}^{κ} and (σ, ρ) ∈ T D̂_{Θ}^{Ξ} we define D̂[[T]]_{σ,ρ} ∈ D̂_{Θ}^{T [[T]]_{σ}:κ} as follows:

D̂[[X]]_{σ,ρ}  := ρ(X)
D̂[[λX:κ. T]]_{σ,ρ} := ((G, G) ∈ T D̂_{Θ}^{κ}) ↦ D̂[[T]]_{(σ,ρ)[X↦(G,G)]}
D̂[[T U]]_{σ,ρ}  := D̂[[T]]_{σ,ρ}(T [[U]]_{σ}, D̂[[U]]_{σ,ρ})
D̂[[C]]_{σ,ρ}  := CD̂
where →D̂  ∈ D̂_{Ξ}^{→:⋆→⋆→⋆}
→D̂(A, A)(B, B) := A → B
∀κ ; D̂  ∈ D̂_{Ξ}^{∀^{κ}:(κ→⋆)→⋆}
∀κ ; D̂(F, F)  := ⋂_{G⊩^{κ}G} G.F(G, G)

Lemma 16 (Well-definedness of interpretation into D̂). If T ∈ Ty_{Ξ}^{κ} and (σ, ρ) ∈ T D̂_{Θ}^{Ξ} then D̂[[T]]_{σ,ρ} ∈ D̂_{Θ}^{T [[T]]_{σ}:κ}.

Proof.

D̂[[C]]_{σ,ρ}  ∈ D̂_{Θ}^{T [[C]]_{σ}:Σ(C)}
= D̂_{Θ}^{C_{T} :Σ(C)}
D̂[[C]]_{σ,ρ}  = CD̂
D̂[[X]]_{σ,ρ}  ∈ D̂_{Θ}^{T [[X]]_{σ}:κ}
= D̂_{Θ}^{σ(X):κ}
D̂[[X]]_{σ,ρ}  = ρ(X)
D̂[[λX:κ. T]]_{σ,ρ} ∈ D̂_{Θ}^{T [[λX:κ. T]]_{σ}}
= ((G, G) ∈ T D̂_{Θ}^{κ}) → D̂_{Θ}^{T [[λX:κ. T]]_{σ}·G}
= ((G, G) ∈ T D̂_{Θ}^{κ}) → D̂_{Θ}^{T [[T]]_{σ[X↦G]}}
D̂[[λX:κ. T]]_{σ,ρ} = ((G, G) ∈ T D̂_{Θ}^{κ}) ↦ D̂[[T]]_{(σ,ρ)[X↦(G,G)]}
D̂[[T U]]_{σ,ρ}  ∈ D̂_{Θ}^{T [[T U]]_{σ}}
= D̂_{Θ}^{T [[T]]_{σ}·T [[U]]_{σ}}
D̂[[T U]]_{σ,ρ}  = D̂[[T]]_{σ,ρ}(T [[U]]_{σ}, D̂[[U]]_{σ,ρ})

where, in the last line,

\begin{aligned}D̂[[T]]_{σ,ρ} & ∈ & D̂_{Θ}^{T [[T]]_{σ}:κ→κ′} \\ & = & ((G, G) ∈ T D̂_{Ξ}^{κ}) → D̂_{Θ}^{T [[T]]_{σ}·G:κ′}. \end{aligned}

⊓ ⊔

Since the kind function space is the full set-theoretic one, D̂ is combinatory and respects type equality.

Lemma 17 (D̂ is combinatory). Let U ∈ Ty_{Ξ}^{κ}, T ∈ Ty_{Ξ,X:κ}^{κ′} and (σ, ρ), (σ′, ρ′) ∈

T D̂_{Θ}^{Ξ}.

1. D̂[[U]]_{σ,ρ} = D̂[[U]]_{σ′,ρ′} if ρ(X) = ρ′(X) for all X ∈ FV(U).

2. D̂[[T [U/X]]]_{σ,ρ} = D̂[[T]]_{(σ,ρ)[X↦T D̂[[U]]_{σ,ρ}]}.

Proof. The first proposition is needed to establish the second.

1. By induction on U.

2. By induction on T, using 1.

Case κ′ = κ_{1} → κ_{2} and T = λY : κ_{1}. T′. Using the induction hypothesis and 1, we have for all (G, G) ∈ T D̂_{Θ}^{κ_{1}}, since Y ∉ FV(U),

D̂[[T′[U/X]]]_{(σ,ρ)[Y ↦(G,G)]}
= D̂[[T′]]_{(σ,ρ)[Y ↦(G,G)][X↦T D̂[[U]]_{(σ,ρ)[Y ↦(G,G)]}]}
= D̂[[T′]]_{(σ,ρ)[Y ↦(G,G)][X↦T D̂[[U]]_{σ,ρ}]}
= D̂[[T′]]_{(σ,ρ)[X↦T D̂[[U]]_{σ,ρ}][Y ↦(G,G)]}

hence, D̂[[λY :κ_{1}. T′[U/X]]]_{σ,ρ} = D̂[[λY :κ_{1}. T′]]_{(σ,ρ)[X↦T D̂[[U]]_{σ,ρ}]}. ⊓ ⊔ Lemma 18 (D̂ respects type equality). If Ξ ⊢ T = T′ : κ and (σ, ρ) ∈ T D̂_{Θ}^{Ξ} then D̂[[T]]_{σ,ρ} = D̂[[T′]]_{σ,ρ}. Proof. By induction on Ξ ⊢ T = T′ : κ, using Lemma 17. ⊓ ⊔ Lemma 19 (Realizability of type constructors). → ⊩^{⋆→⋆→⋆} → and ∀^{κ} ⊩^{(κ→⋆)→⋆} ∀^{κ}. Proof. Assume A ∈ D̂_{Ξ}^{A} and B ∈ D̂_{Ξ}^{B} with A ⊩^{⋆} A and B ⊩^{⋆} B. We show A → B ⊩^{⋆} A → B.

\underline{A → B} ⊆ \overline{A} → \underline{B} ⊆ A → B ⊆ \underline{A} → \overline{B} ⊆ \overline{A → B}.

Assume F ∈ D̂_{Ξ}^{F:κ→⋆} with F ⊩^{κ→⋆} F. We show ∀^{κ}F ⊩^{⋆} ∀^{κ}(F, F). Let X ∉ dom(Ξ). Then \underline{X} ∈ D̂_{Ξ,X:κ}^{X:κ} and X ⊩^{κ} \underline{X}.

\underline{∀^{κ}F}  ⊆ ⋂_{G∈T_{Ξ}^{κ}} G.\underline{F · G}
⊆ ⋂_{G⊩^{κ}G} G.\underline{F · G} ⊆ ⋂_{G⊩^{κ}G} G.F(G, G)
= ∀^{κ}(F, F) ⊆ X.F(X, \underline{X}) ⊆ X.\overline{F · X}
⊆ \overline{∀^{κ}F}
⊓ ⊔

Theorem 12 (Realizability). T D̂ is a type structure with application (F, F)·(G, G) = (F ·G, F(G, G)) and evaluation T D̂[[T]]_{σ,ρ} = (T [[T]]_{σ}, D̂[[T]]_{σ,ρ}). C is a type substructure of T D̂. Proof. By Def. 27 and Lemma 19, C is induced, hence, by Theorem 2, it is a type structure. ⊓ ⊔ Corollary 3. If T ∈ Ty_{Ξ}^{⋆} and σ ⊩^{Ξ} ρ then \underline{T [[T]]_{σ}} ⊆ \overline{T [[T]]_{σ}}. Proof. By the theorem, T [[T]]_{σ} ⊩^{⋆} D̂[[T]]_{σ,ρ}. ⊓ ⊔ Theorem 13 (Fundamental theorem of typing). Let D be an object structure over T and \underline{C}, \overline{C} ∈ D̂ a type candidate space. Let S ⊆ C be a type substructure of the associated realizability type structure C. Then the family E_{(Δ,Φ)}^{Ξ ⊢(A,A)} := A_{Δ} is an object substructure of D reindexed by π_{1} : S → T . Proof. Note that E_{(Δ,Φ)}^{Ξ ⊢(A,A)} ⊆ D_{Δ}^{Ξ ⊢A}.

1. E respects type equality. For Ξ ⊢ T = T′ : ⋆ and (σ, ρ) ∈ S_{Θ}^{Ξ} we have E_{Δ,Φ}^{Ξ ⊢S[[T]]_{σ,ρ}} = (D̂[[T]]_{σ,ρ})_{Δ} = (D̂[[T′]]_{σ,ρ})_{Δ} = E_{Δ,Φ}^{Ξ ⊢S[[T′]]_{σ,ρ}} since D̂ respects type equality.

2. Object application is well-defined. Let (A, A), (B, B) ∈ S_{Ξ}^{⋆} and f ∈ E_{Δ,Φ}^{Ξ ⊢(A,A)→(B,B)} = (A →D̂ B)_{Δ} and d ∈ E_{Δ,Φ}^{Ξ ⊢(A,A)} = A_{Δ}. By definition of →D̂, f · d ∈ B_{Δ} = E_{Δ,Φ}^{Ξ ⊢(B,B)}.

3. Type application is well-defined. Let (F, F) ∈ S_{Ξ}^{κ→⋆}, (G, G) ∈ S_{Ξ}^{κ}, and d ∈ E_{Δ,Φ}^{Ξ ⊢∀^{κ}(F,F)} = (∀^{κ}F)_{Δ} = (⋂_{G⊩^{κ}G} G.F(G, G))_{Δ} = ⋂_{G⊩^{κ}G}(G.F(G, G))_{Δ}. Since G ⊩ G, d ∈ (G.F(G, G))_{Δ}, hence, d ·_{E} (G, G) = d ·_{D} G ∈ F(G, G) = E_{Δ,Φ}^{Ξ ⊢(F,F)·(G,G)}.

4. Evaluation is well-defined. We show E⦇t⦈_{η}^{σ,ρ} ∈ E_{Δ,Φ}^{Θ ⊢S[[T]]_{σ,ρ}} for (Δ, Φ) ∈ S_{Θ}^{cxt},

(σ, ρ) ∈ S_{Θ}^{Ξ}, and η ∈ E_{Δ,Φ}^{Θ ⊢S[[Γ]]_{σ,ρ}} by induction on Ξ; Γ ⊢ t : T. By definition of E, it is sufficient to show D⦇t⦈_{η}^{σ} ∈ (D̂[[T]]_{σ,ρ})_{Δ} for η ∈ (D̂[[Γ]]_{σ,ρ})_{Δ}. Case

\frac{Ξ ⊢ Γ}{Ξ; Γ ⊢ x : Γ (x)}

We have D⦇x⦈_{η}^{σ} = η(x) ∈ (D̂[[Γ (x)]]_{σ,ρ})_{Δ}.

Case

\frac{Ξ ⊢ T : κ → ⋆ Ξ, X:κ; Γ ⊢ t : T X}{Ξ; Γ ⊢ ΛX:κ. t : ∀^{κ}T} X ∉ dom(Ξ)

To show D⦇ΛX : κ. t⦈_{η}^{σ} ∈ (D̂[[∀^{κ}T]]_{σ,ρ})_{Δ}, assume arbitrary (G, G) ∈ S_{Θ}^{κ}, let σ′ := σ[X ↦ G] and ρ′ := ρ[X ↦ G], and show D⦇ΛX: κ. t⦈_{η}^{σ} ·_{E} (G, G) ∈ (D̂[[T]]_{σ,ρ}(G, G))_{Δ}. Let d := D⦇ΛX:κ. t⦈_{η}^{σ} ·_{E} (G, G) = D⦇t⦈_{η}^{σ′} and note that S[[X]]_{σ′,ρ′} = (G, G). Since (σ′, ρ′) ∈ S_{Θ}^{Ξ,X:κ}, by induction hypothesis d ∈ (D̂[[T X]]_{σ′,ρ′})_{Δ} = (D̂[[T]]_{σ,ρ}(G, G))_{Δ}, because X ∉ F V (T) and Lemma 17.

Case

\frac{Ξ; Γ ⊢ t : ∀^{κ}T Ξ ⊢ U : κ}{Ξ; Γ ⊢ t U : T U}

Let (F, F) := S[[T]]_{σ,ρ} and (G, G) := S[[U]]_{σ,ρ}. By induction hypothesis d :=

D⦇t⦈_{η}^{σ} ∈ (D̂[[∀^{κ}T]]_{σ,ρ})_{Δ} = (∀κ ; D̂(F, F))_{Δ}. Since G ⊩ G, d ·_{E} (G, G) = d ·_{D}

G ∈ F(G, G)_{Δ} = (D̂[[T U]]_{σ,ρ})_{Δ}. Case

\frac{Ξ; Γ ⊢ t : T Ξ ⊢ T = T′ : ⋆}{Ξ; Γ ⊢ t : T′}

Clear, since D̂ respects type equality. ⊓ ⊔

7.2 Soundness of NbE for Objects

Definition 29 (Term-like object structure). An object structure D over T is term-like if:

1. There exists a Kripke family of maps var^{Ξ ⊢Δ} ∈ (x ∈ dom(Δ)) → D_{Δ}^{Ξ ⊢Δ(x)} indexed by Δ ∈ T_{Ξ}^{cxt}. In the presence of var, we can define the neutral objects inductively as follows:

– var^{Ξ ⊢Δ}(x) ∈ D_{Δ}^{Ξ ⊢Δ(x)} is neutral.

– If e ∈ D_{Δ}^{Ξ ⊢A→B} is neutral and d ∈ D_{Δ}^{Ξ ⊢A} then e · d ∈ D_{Δ}^{Ξ ⊢B} is neutral.

– If e ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} is neutral and G ∈ T_{Ξ}^{κ}, then e · G ∈ D_{Δ}^{Ξ ⊢F ·G} is neutral.

2. There exists a Kripke family of computable maps

view_{Δ}^{Ξ ⊢B} ∈ D_{Δ}^{Ξ ⊢B}
→ ObjVar
+ ⋃_{A∈T_{Ξ}^{⋆}} D_{Δ}^{Ξ ⊢A→B} × D_{Δ}^{Ξ ⊢A}
+ ⋃_{F ∈T_{Ξ}^{κ→⋆}} D_{Δ}^{Ξ ⊢∀^{κ}F} × {G ∈ T_{Ξ}^{κ} | F · G = B}
+ {⊥}

such that:

– If view(f) = x then f = var(x).

– If view(f) = (e, d) then f = e · d and e is neutral.

– If view(f) = (e, G) then f = e · G and e is neutral.

– If view(f) = ⊥ then f is not neutral.

If D is a term-like structure over T , we may write D⦇t⦈^{ρ} for D⦇t⦈_{var_{D}}^{ρ}. If T is also term-like we may further abbreviate D⦇t⦈^{Var_{T}} to D⦇t⦈.

Lemma 20 (Injectivity in a term-like object structure). In a term-like object structure, var and neutral application are injective.

Definition 30 (Object reification). Given a term-like type structure T and a term-like object structure D over T , we define the relations

Ξ; Δ ⊢ d ↘ v ⇑ A  d reifies to v at type A,
Ξ; Δ ⊢ e ↘ u ⇓ A  e reifies to u, inferring type A,

(where d, e ∈ D_{Δ}^{Ξ ⊢A} and v, u are syntactical objects) inductively by the following rules:

\overline{Ξ; Δ ⊢ x ↘ x ⇓ Δ(x)}  \frac{Ξ; Δ ⊢ e ↘ u ⇓ A → B  Ξ; Δ ⊢ d ↘ v ⇑ A}{Ξ; Δ ⊢ e d ↘ u v ⇓ B}

\frac{Ξ; Δ ⊢ e ↘ u ⇓ ∀^{κ}F  Ξ ⊢ G ↘ V ⇑ κ}{Ξ; Δ ⊢ e G ↘ u V ⇓ F · G}  \frac{Ξ, X:κ; Δ ⊢ f · X ↘ v ⇑ F · X}{Ξ; Δ ⊢ f ↘ ΛX:κ. v ⇑ ∀^{κ}F}

\frac{Ξ; Δ, x:A ⊢ f · x ↘ v ⇑ B Ξ ⊢ A ↘ U ⇑ ⋆}{Ξ; Δ ⊢ f ↘ λx:U. v ⇑ A → B} \frac{Ξ; Δ ⊢ e ↘ u ⇓ H}{Ξ; Δ ⊢ e ↘ u ⇑ H} H neutral

As for types, object reification is deterministic.

Note that we cannot say now in which Obj_{Γ}^{Ξ ⊢T} the objects u and v live. The conjecture is those Γ, T with Ξ ⊢ Δ ↘ Γ and Ξ ⊢ A ↘ T ⇑ ⋆. However, this does not follow directly from the definition, it is a consequence of Thm. 15. (Not even if we suppose (Δ, Γ) ∈ S_{Ξ}^{cxt} and (A, T) ∈ S_{Ξ}^{⋆}, because of the ∀-elimination rule.)

Def. and Lem. 14 (Glueing type candidate space) Let S ⊆ T × Ty a glueing candidate, ⊩_{Gl} S. For (A, T) ∈ S_{Ξ}^{⋆} we define the Kripke families \underline{gl}^{Ξ ⊢(A,T)}, \overline{gl}^{Ξ ⊢(A,T)} ∈

{ \atop D × Obj}_{Ξ}^{(A,T)} by

\overline{gl}_{(Δ,Γ)}^{Ξ ⊢(A,T)} := \{(d, t) | Ξ; Δ ⊢ d ↘ v ⇑ A and Ξ; Γ ⊢ t = v : T for somev\},
\underline{gl}_{(Δ,Γ)}^{Ξ ⊢(A,T)} := \{(e, t) | Ξ; Δ ⊢ e ↘ u ⇓ A and Ξ; Γ ⊢ t = u : T for someu\}.

gl is a type candidate space.

Proof. We show \underline{gl}^{Ξ ⊢A,T} → \overline{gl}^{Ξ ⊢B,U} ⊆ \overline{gl}^{Ξ ⊢A→B,T →U}.

(f, v) ∈ (\underline{gl}^{Ξ ⊢A,T} → \overline{gl}^{Ξ ⊢B,U})_{Δ,Γ}  assumption

Δ′ = Δ, x:A and Γ′ = Γ, x:T

Δ′ ⊢ x ↘ x ⇓ A and Γ′ ⊢ x = x : T  by def.
(x, x) ∈ \underline{gl}_{Δ′,Γ′}^{Ξ ⊢A,T}  by def.
(f · x, v x) ∈ \overline{gl}_{Δ′,Γ′}^{Ξ ⊢B,U}  from assumption
Δ′ ⊢ f · x ↘ w ⇑ B  and
Γ′ ⊢ v x = w : U  for some w
Δ′ ⊢ A ↘ T′ ⇑ ⋆  and
Γ′ ⊢ T = T′ : ⋆  since (A, T) ∈ S_{Ξ}^{⋆}
Δ ⊢ f ↘ λx:T′. w ⇑ A → B  and
Γ ⊢ v = λx:T′. w : T → U  since x ∉ dom(Γ)
(f, v) ∈ \overline{gl}_{Δ,Γ}^{Ξ ⊢(A,T)→(B,U)}  by def.⊓ ⊔

Theorem 15 (Soundness of NbE for objects). Let D be a term-like object structure over a term-like type structure T . If Ξ; Γ ⊢ t : T then there is a long normal form v such that Ξ; T [[Γ]]_{Var} ⊢ D⦇t⦈_{var}^{Var} ↘ v ⇑ T [[T]]_{Var} and Ξ; Γ ⊢ t = v : T.

Proof. Consider the type candidate space \underline{gl}, \overline{gl} ∈ { \atop D × Obj} for the glueing type structure G. Recall that

gl_{Ξ}^{κ} = \{((F, T), F) ∈ G_{Ξ}^{κ} × { \atop D × Obj}_{Ξ}^{(F,T):κ} | (F, T) ⊩_{gl}^{κ} F\}.

By the fundamental theorem of typing, E_{((Δ,Γ),Φ)}^{Ξ ⊢((A,T),A)} := A_{(Δ,Γ)} is an object substruc-

ture of D × Obj reindexed by π_{1} : gl → G. Since (X, X) ∈ G_{Ξ}^{Ξ(X)} and (X, X) ⊩_{gl}^{Ξ(X)}

\underline{gl}^{Ξ ⊢(X,X)} we have a variable embedding Var_{gl}(X) = ((X, X), \underline{gl}^{Ξ ⊢(X,X)}) ∈ gl_{Ξ}^{Ξ(X)} into type structure gl. Also, since Ξ; Δ ⊢ x ↘ x ⇓ Δ(x) and Ξ; Γ ⊢ x = x : Γ (x) we have (x, x) ∈ \underline{gl}_{(Δ,Γ)}^{Ξ ⊢(Δ(x),Γ (x))}. The setting of Δ such that G[[Γ]] = (Δ, Γ) im-

plies (x, x) ∈ \underline{gl}_{G[[Γ]]}^{Ξ ⊢G[[Γ (x)]]} ⊆ ({ \atop D × Obj}[[Γ (x)]])_{G[[Γ]]} = E_{gl[[Γ]]}^{Ξ ⊢gl[[Γ (x)]]}. Hence, setting

var_{E}^{Ξ ⊢gl[[Γ]]_{_{Var}_{gl}}} (x) = (x, x) we have var_{E}^{Ξ ⊢[[Γ]]} ∈ E_{gl[[Γ]]}^{Ξ ⊢gl[[Γ]]}.

It follows that E⦇t⦈ = E⦇t⦈\begin{matrix}Var & gl \\ var & E \end{matrix} ∈ E_{gl[[Γ]]}^{Ξ ⊢gl[[T]]} = ({ \atop D × Obj}[[T]])_{G[[Γ]]} ⊆ \overline{gl}^{Ξ ⊢G[[T]]}.

With d := D⦇t⦈ we have (d, t) = (D × Obj)⦇t⦈ = E⦇t⦈, thus, Ξ; Δ ⊢ d ↘ v ⇑ T [[T]] and Ξ; Γ ⊢ t = v : T for some v. ⊓ ⊔

8 Object Groupoids

Definition 31 (Object groupoid). An object structure D over a type structure T is an object groupoid if each D_{Δ}^{Ξ ⊢A} is a groupoid and

1. app(f, d)^{−1} = app(f^{−1}, d^{−1}),

2. TyApp(f, G)^{−1} = TyApp(f^{−1}, G), and

3. if f ∗ f′ and d ∗ d′ are defined, then app(f, d) ∗ app(f′, d′) = app(f ∗ f′, d ∗ d′) and TyApp(f, G) ∗ TyApp(f′, G) = TyApp(f ∗ f′, G).

Definition 32 (Groupoidal at higher kinds). Let D be a object groupoid over T . Then A ∈ D̂^{A:⋆} is (⋆-)groupoidal if A_{Δ} is a subgroupoid for each Δ. F ∈ D̂^{F:κ→κ′} is (κ → κ′-)groupoidal if F(G, G) is (κ′-)groupoidal for all G ∈ T_{Ξ}^{κ} and (κ-)groupoidal G ∈ D̂_{Ξ}^{G:κ}. Let

D̃_{Ξ}^{F:κ} := {F ∈ D̂_{Ξ}^{F:κ} | F is κ-groupoidal },
T D̃_{Ξ}^{κ} := {(F, F) ∈ T_{Ξ}^{κ} × T D̃_{Ξ}^{F:κ}}.

Lemma 21 (Function space is groupoidal). If A ∈ D̂^{Ξ ⊢A} and B ∈ D̂^{Ξ ⊢B} are groupoidal, so is A →D̂ B ∈ D̂^{Ξ ⊢A→B}.

Proof. First, we show that (A → B)_{Δ} is closed under inversion. Assume f ∈ (A → B)_{Δ}. To show f^{−1} ∈ (A → B)_{Δ}, assume arbitrary Δ′ ≤ Δ and d ∈ A_{Δ′} and show f^{−1} · d ∈ B_{Δ′}. Since d^{−1} ∈ A_{Δ′} we have f · d^{−1} ∈ B_{Δ′}, hence, B_{Δ′} ∋ (f · d^{−1})^{−1} = f^{−1} · d.

Then, we show that (A → B)_{Δ} is closed under composition. Assume f, f′ ∈ (A → B)_{Δ} and f ∗ f′ defined. Further, assume Δ′ ≤ Δ and d ∈ A_{Δ′} arbitrary and show (f ∗ f′) · d ∈ B_{Δ′}. Note that d = d ∗ d^{−1} ∗ d, hence, it suffices to show (f · d) ∗ (f′ · (d^{−1} ∗ d)) ∈ B_{Δ′}. Yet this holds, since f · d ∈ B_{Δ′} and f′ · (d^{−1} ∗ d) ∈ B_{Δ′} (because d^{−1} ∗ d ∈ A_{Δ′}).

Lemma 22 (Type abstraction is groupoidal). If A ∈ D̂^{Ξ ⊢F ·G} is groupoidal, so is G.A ∈ D̂^{Ξ ⊢∀^{κ}F}.

Proof. Assume f, f′ ∈ (G.A)_{Δ} and f ∗f′ defined. Since f ·G ∈ A_{Δ}, also (f ·G)^{−1} = f^{−1} · G ∈ A_{Δ}. Further, (f · G) ∗ (f′ · G) = (f ∗ f′) · G ∈ A_{Δ}, hence f ∗ f′ ∈ (G.A)_{Δ}.

Corollary 4 (Impredicative quantification is groupoidal). ∀^{κ} ∈ D̂^{Ξ ⊢∀^{κ}:(κ→⋆)→⋆} is (κ → ⋆) → ⋆-groupoidal.

Theorem 16 (Fund. thm. of kinding for type groupoids). Let D be an object groupoid over T . Then T D̃ is a type substructure of T D̂.

Proof. By Lemma 21 and Cor. 4, →_{T D̂}∈ T D̃_{Ξ}^{⋆→⋆→⋆} and ∀_{T D̂}^{κ} ∈ T D̃_{Ξ}^{(κ→⋆)→⋆)}. By

definition of groupoidal, (F, F) ·_{T D̂} (G, G) = (F · G, F(G, G)) ∈ T D̃_{Ξ}^{κ′} for all

(F, F) ∈ T D̃_{Ξ}^{κ→κ′} and (G, G) ∈ T D̃_{Ξ}^{κ}, thus, application is well-defined.

It remains to show that interpretation is well-defined. Let Ξ ⊢ T : κ and (σ, ρ) ∈ T D̃_{Θ}^{Ξ}. One easily shows T D̂[[T]]_{ρ} ∈ T D̃_{Θ}^{κ} by induction on Ξ ⊢ T : κ.

Definition 33 (Square object groupoid). Let D be an object structure over T . Then

D^{2}_{Δ}^{Ξ ⊢A} = D_{Δ}^{Ξ ⊢A} × D_{Δ}^{Ξ ⊢A} with

\begin{aligned}(d, d′)^{−1} & = & (d′, d) \\ (d_{1}, d_{2}) ∗ (d_{2}, d_{3}) & = & (d_{1}, d_{3}) \end{aligned}

is a type groupoid over T .

8.1 Fundamental theorem of object equality

Theorem 17 (Fundamental theorem of object equality). Assume a type structure T that respects type equality and a combinatory object structure D over T . Let \underline{C}, \overline{C} ∈ ˜ D^{2} be a type candidate space and C its associated realizability type structure. If Ξ; Γ ⊢

t = t′ : T and (σ, ρ) ∈ C_{Θ}^{Ξ} and (η, η′) ∈ ˜ D^{2}[[Γ]]_{σ,ρ} then (D⦇t⦈_{η}^{σ}, D⦇t′⦈_{η′}^{σ}) ∈ ˜ D^{2}[[T]]_{σ,ρ}.

Proof. By induction on Ξ; Γ ⊢ t = t′ : T. We show a few representative cases.

Case

\frac{Ξ, X:κ; Γ ⊢ t : T Ξ ⊢ U : κ}{Ξ; Γ ⊢ (ΛX:κ. t) U = t[U/X] : T}

Let (G, G) := T ˜ D^{2}[[U]]_{σ,ρ} ∈ C_{Θ}^{κ} and (σ′, ρ′) := (σ, ρ)[X ↦ (G, G)] ∈ C_{Θ}^{Ξ,X:κ}. By

induction hypothesis, (d, d′) := (⦇t⦈_{η}^{σ′}, ⦇t⦈_{η′}^{σ′}) ∈ ˜ D^{2}[[T]]_{σ′,ρ′}. This entails the goal,

since ˜ D^{2}[[T [U/X]]]_{σ,ρ} = ˜ D^{2}[[T]]_{σ′,ρ′} and (⦇(ΛX: κ. t) U⦈_{η}^{σ}, ⦇t[U/X]⦈_{η′}^{σ}) = (d, d′)

by the combinatory laws. Case

\frac{Ξ; Γ ⊢ t : ∀^{κ}T}{Ξ; Γ ⊢ ΛX:κ. t X = t : ∀^{κ}T} X ∉ FV(t)

Let F := ˜ D^{2}[[T]]_{σ,ρ}, d := ⦇t⦈_{η}^{σ} and d′ := ⦇t⦈_{η′}^{σ}. Let further d̂:= ⦇ΛX:κ. t X⦈_{η}^{σ}. We have to show (d̂, d′) ∈ ∀^{κ}F. Assume arbitrary (G, G) ∈ C_{Θ}^{κ}. It is sufficient to show (d̂, d′) · G ∈ F(G, G). Note that d̂· G = ⦇t X⦈_{η}^{σ[X↦G]} = ⦇t⦈_{η}^{σ[X↦G]} · G = d · G, since X ∉ FV(t) and D is combinatory. The desired (d · G, d′ · G) ∈ F(G, G) now follows from the induction hypothesis (d, d′) ∈ ∀^{κ}F. Case

\frac{Ξ; Γ ⊢ t = t′ : ∀^{κ}T Ξ ⊢ U = U′ : κ}{Ξ; Γ ⊢ t U = t′ U′ : T U}

Let d := ⦇t⦈_{η}^{σ} and d′ := ⦇t′⦈_{η′}^{σ}. Let further (G, G) := (T ˜ D^{2}[[U]]_{σ,ρ}) = (T ˜ D^{2}[[U′]]_{σ,ρ}),

since T (hence also T ˜ D^{2}) respects type equality. First, observe that

\begin{aligned}⦇t U⦈_{η}^{σ} & = & d · G \\ ⦇t′ U′⦈_{η}^{σ} & = & d′ · G \\ ˜D^{2}[[T U]]_{σ,ρ} & = & ˜D^{2}[[T]]_{σ,ρ}(G, G) \end{aligned}

By induction hypothesis,

(d, d′) ∈ ˜ D^{2}[[∀^{κ}T]]_{σ,ρ} = ⋂_{(G,G)∈C_{Θ}^{κ}} G.(˜ D^{2}[[T]]_{σ,ρ}(G, G)).

By the fundamental theorem of kinding, (G, G) ∈ C_{Θ}^{κ}, hence (d, d′)·G = (d·G, d′ · G) ∈ ˜ D^{2}[[T]]_{σ,ρ}(G, G), as expected. Case

\frac{Ξ; Γ ⊢ t = t′ : T Ξ ⊢ T = T′ : ⋆}{Ξ; Γ ⊢ t = t′ : T′}

Trivial, since ˜ D^{2} respects type equality.

8.2 Completeness of Nbe for objects

Definition 34 (Type candidate space for completeness). Let D be a term-like object

structure over term-like T . We define the Kripke families \underline{per}^{Ξ ⊢A}, \overline{per}^{Ξ ⊢A} ∈ ^{ ˜2}D_{Ξ}^{A:⋆} by

\overline{per}_{Δ}^{Ξ ⊢A} := \{(d, d′) ∈ D^{2}_{Δ}^{Ξ ⊢A} | Ξ; Δ ⊢ d ↘ v ⇑ A and
Ξ; Δ ⊢ d′ ↘ v ⇑ A for somev}
\underline{per}_{Δ}^{Ξ ⊢A} := \{(e, e′) ∈ D^{2}_{Δ}^{Ξ ⊢A} | Ξ; Δ ⊢ e ↘ u ⇓ A and
Ξ; Δ ⊢ e′ ↘ u ⇓ A for someu}

Note that composition (d_{1}, d_{2}) ∗ (d_{2}, d_{3}) = (d_{1}, d_{3}) is well-defined in \underline{per}_{Δ}^{Ξ ⊢A} and \overline{per}_{Δ}^{Ξ ⊢A} since reification is deterministic.

Lemma 23. \underline{per}, \overline{per} form a type candidate space for^{2}D.

Theorem 18 (Completeness of NbE for objects). Let D_{0} be a term-like object structure over reifyable T_{0}. If Ξ; Γ ⊢ t = t′ : T then there is a long normal form v such that Ξ; Δ ⊢ ⦇t⦈ ↘ v ⇑ A and Ξ; Δ ⊢ ⦇t′⦈ ↘ v ⇑ A where Δ := T [[Γ]] and A := T [[T]].

Proof. The term structure T := T_{0}/P is reifyable and respects type equality. Let D be defined as D_{0} reindexed by the representation function T → T_{0}. Consider the type structure

per_{Ξ}^{κ} = {(F, F) ∈ T_{Ξ}^{κ} × ˜ D^{2}_{Ξ}^{F:κ} | F ⊩_{per}^{κ} F}.

The variable embedding for per is given by Var_{Ξ} = (X ↦ (X, \underline{per}^{Ξ ⊢X})) ∈ per_{Ξ}^{Ξ}.

E_{(Δ,Φ)}^{Ξ ⊢(A,A)} := A_{Δ}

is an object subgroupoid of ^{2}D reindexed by π_{1} : per → T . Its variable embedding is given by

var_{E}^{Ξ ⊢Δ} = (var_{D}^{Ξ ⊢π_{1}∘Δ}, var_{D}^{Ξ ⊢π_{1}∘Δ}) = (x ↦ (x, x))
∈ \underline{per}_{Δ}^{Ξ ⊢Δ} ⊆ E_{(Δ,Φ)}^{Ξ ⊢(Δ,Φ)}.

By the fundamental theorem of object equality we obtain (D⦇t⦈, D⦇t′⦈) ∈ ˜ D^{2}[[T]] ⊆ \overline{per}_{Δ}^{Ξ ⊢A}, thus, Δ ⊢ ⦇t⦈ ↘ v ⇑ A and Δ ⊢ ⦇t′⦈ ↘ v ⇑ A for some v.

9 Conclusion

We have developed type and object structures, which are sorted applicative structures on type and object level, in order to facilitate generic model constructions for System F^{ω}—which are an alternative to categorical semantics [See87] and Bruce-Meyer-Mitchell models [BM84]. Using special instances of kind candidate spaces we have shown soundness and completeness of an abstract normalization by evaluation algorithm for types. We have gone on to show soundness and completeness of NbE for objects.

We seek to extend NbE to the Calculus of Constructions, using ideas from this work. Due to dependency, type and object levels cannot be defined in sequence, but must be defined simultaneously; this seems to be the main remaining technical difficulty.

Acknowledgments. This work is dedicated to Otto Forster who taught me basic algebraic vocabulary in his excellent lectures on linear algebra in 1994/95 at the Ludwig-Maximilians-University Munich, and to Thierry Coquand who introduced me to abstract semantics of type theory via lambda and PER models.

References

[Abe08] Andreas Abel. Weak βη-normalization and normalization by evaluation for System F. In LPAR’08, volume 5330 of LNAI, pages 497–511. Springer, 2008.

[ACD07] Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In LICS’07, pages 3–12. IEEE CS Press, 2007.

[ACD08] Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βηconversion test for Martin-Löf type theory. In MPC’08, volume 5133 of LNCS, pages 29–56. Springer, 2008.

[ADHS01] Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS’01, pages 303–310. IEEE CS Press, 2001.

[AHS96] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In LICS’96, pages 98–106. IEEE CS Press, 1996.

[AR08] Andreas Abel and Dulma Rodriguez. Syntactic metatheory of higher-order subtyping. In CSL’08, volume 5213 of LNCS, pages 446–460. Springer, 2008.

[Bar84] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984.

[Bar08] Freiric Barral. Decidability for non-standard conversions in lambda-calculus. PhD thesis, Ludwig-Maximilians-University Munich, 2008.

[BCF04] Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL’04, pages 64–76. ACM, 2004.

[BJS07] Frédéric Blanqui, Jean-Pierre Jouannaud, and Pierre-Yves Strub. Building decision procedures in the Calculus of Inductive Constructions. In CSL’07, volume 4646 of LNCS, pages 328–342. Springer, 2007.

[Bla05] Frédéric Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37–92, 2005.

[BM84] Kim B. Bruce and Albert R. Meyer. The semantics of second order polymorphic lambda calculus. In Semantics of Data Types, volume 173 of LNCS, pages 131–144. Springer, 1984.

[BS91] Ulrich Berger and Helmut Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In LICS’91, pages 203–211. IEEE CS Press, 1991.

[CAM07] James Chapman, Thorsten Altenkirch, and Conor McBride. Epigram reloaded: a standalone typechecker for ETT. In TFP’05, volume 6 of Trends in Functional Programming, pages 79–94. Intellect, 2007.

[CD97] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. MSCS, 7(1):75–94, 1997.

[Coq96] Thierry Coquand. An algorithm for type-checking dependent types. In MPC’95, volume 26 of SCP, pages 167–177. Elsevier, 1996.

[CWC07] Jacek Chrzaszcz and Daria Walukiewicz-Chrzaszcz. Towards rewriting in Coq. In Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of LNCS, pages 113–131. Springer, 2007.

[Dan99] Olivier Danvy. Type-directed partial evaluation. In Partial Evaluation Summer School ’98, volume 1706 of LNCS, pages 367–411. Springer, 1999.

[Dyb00] Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. JSL, 65(2):525–549, 2000.

[Gir72] Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII, 1972.

[GL02] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In ICFP’02, volume 37 of SIGPLAN Notices, pages 235–246. ACM, 2002.

[GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in TCS. CUP, 1989.

[INR07] INRIA. The Coq Proof Assistant, Version 8.1. INRIA, 2007. http://coq.inria.fr/.

[Nor07] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers, Göteborg, Sweden, 2007.

[Pol94a] Randy Pollack. The Theory of LEGO. PhD thesis, University of Edinburgh, 1994.

[Pol94b] Robert Pollack. Closure under alpha-conversion. In TYPES’93, volume 806 of LNCS, pages 313–332. Springer, 1994.

[See87] R. A. G. Seely. Categorical semantics for higher order polymorphic lambda calculus. JSL, 52(4):969–989, 1987.

[Tai67] William W. Tait. Intensional interpretations of functionals of finite type I. JSL, 32(2):198–212, 1967.

[WCPW03] Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.