Preliminary Report. Final version to appear in: LFMTP 2010 \begin{matrix}c \\ ◯ \end{matrix} A. Abel & B. Pientka This work is licensed under the Creative Commons Attribution License.

Explicit substitutions for contextual type theory

Andreas Abel

Theoretical Computer Science, Ludwig-Maximilians-University Munich, Germany

                                     andreas.abel@ifi.lmu.de

Brigitte Pientka

School of Computer Science, McGill University, Montreal, Canada

                                      bpientka@cs.mcgill.ca

In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. We then present a weak head normalization procedure which performs both substitutions lazily and in a single pass thereby combining substitution walks for the two different classes of variables. Finally, we describe a bidirectional type checking algorithm which uses weak head normalization and prove soundness.

Keywords: Explicit substitutions, Meta-variables, Logical framework, Contextual modal type theory

1 Introduction

Over the last decade, reasoning and programming with dependent types has received wide attention and several systems provide implementations for dependently typed languages (see for example Agda [BDN09, Nor07], Beluga [PD08, PD10], Delphin [PS08, PS09], Twelf [PS99], etc).

As dependent types become more accepted, it is interesting to better understand how to implement such systems efficiently. While all the systems mentioned support type checking and moreover provide implementations supporting type reconstruction for dependent types, there is a surprising lack in documentation and gap in modelling the theoretical foundations of these implementations. This makes it hard to reproduce some of the ideas, and prevents them from being widely accessible to a broader audience.

A core question in the implementations for dependently typed systems is how to handle substitutions. Let us illustrate the problem in the setting of contextual modal type theory [NPP08], where we not only have ordinary Π-types to abstract over ordinary variables x but also Π^{□} -types which allow us to abstract over meta-variables X, and we find the following two elimination rules:

Δ;Γ ⊢ M : Πx:A.B Δ;Γ ⊢ N : A Δ;Γ ⊢ M N : [N/x]B

Δ;Γ ⊢ M : Π^{□} X:A[Ψ].B Δ;Ψ ⊢ N : A
Δ;Γ ⊢ M (Ψ̂.N) : [[Ψ̂.N/X]]B

In the Π-elimination rule, we do not want to apply the substitution N for x in the type B eagerly during type checking, but accumulate all the individual substitutions and apply them simultaneously, if necessary. Similarly, in the Π^{□} -elimination rule, we do not want to replace eagerly the meta-variable X with N in the type B but accumulate all meta-substitutions and also apply them simultaneously. In fact, we would like to combine substitution walks for meta-variables and ordinary variables, and simultaneously apply ordinary substitution and meta-substitutions to avoid multiple traversals. This will allow us potentially to detect that two terms are not equal without actually performing a substitution, and in the case of a de Bruijn numbering scheme for variables, we would like to avoid unnecessary renumbering.

Explicit substitutions go back to Abadi et al [ACCL91] and are often central when implementing core algorithms such as type checking or higher-order unification [DHK00]. Many existing implementations of proof assistants such as the Twelf system, Delphin, Beluga, Agda or λProlog use explicit substitutions to combine substitution walks for ordinary variables. A different approach with the same goal of handling substitutions efficiently is the suspension calculus [NW98, LNQ05].

However, meta-variables are often modeled via references thereby avoiding the need to explicitly propagate substitutions for meta-variables. Yet there are multiple reasons why we would like to treat meta-variables non-destructively and be able to handle meta-substitutions explicitly. First, such implementations may be easier to maintain and may be more efficient. Second, in several applications we need to abstract over the remaining free meta-variables in the most general solution found by higherorder unification. For example in type reconstruction we need to store a closed most general type or in tabled higher-order logic programming [Pie03] we want to store explicitly the answer substitution for the meta-variables occurring in a query. Abstraction can be expensive since we need to first traverse a term including the types of all the meta-variables occurring in it and collect all references to meta-variables. Subsequently, we again need to traverse the term including the types of meta-variables and compute their appropriate de Bruijn index. A non-destructive implementation of unification could avoid this explicit abstraction step. To achieve a practical, non-destructive implementation of unification, understanding the interaction of ordinary substitutions with meta-substitutions and handling both lazily is crucial.

While meta-variables are often only introduced internally, i.e., there is no abstraction over metavariables using a Π^{□} -type, some languages such as Beluga have taken the step to distinguish ordinary bound variables and meta-variables already in the source language. Consequently, we find different classes of bound variables, bound ordinary variables and bound meta-variables, and different types, Πand Π^{□} -types. When type-checking Beluga programs, we would like to combine substitution walks for these different classes. Understanding how these two substitutions interact is also crucial for type reconstruction in this setting, since omitted arguments may depend on both kinds of variables.

In this paper, we revisit the ideas of explicit substitutions where we combine substitutions for ordinary variables and meta-variables. In particular, we describe an explicit substitution calculus with firstclass meta-variables inspired by contextual modal type theory [NPP08]. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. We omit here the ability to abstract explicitly over meta-variables which is a straightforward addition and concentrate on the interaction of ordinary substitutions and meta-substitutions. We then present a weak head normalization procedure which performs both substitutions lazily and in a single pass thereby combining substitution walks for the two different classes of variables. Finally, we give an algorithm for definitional equality and present a bidirectional type checking algorithm which employs weak head normalization and show soundness. In the future, we plan to use the presented calculus as a foundation for implementing the Beluga language which supports programming and reasoning with formal systems specified in the logical framework LF.

2 The Calculus: Syntax, Typing, and Equality

Let us first introduce the grammar and typing rules for the dependently typed λ-calculus with metavariables based on the ideas in [NPP08]. The system we consider is an extension of the logical framework LF with first-class meta-variables. We design the calculus as an extension of previous explicit substitution calculi such as [ACCL91, DHK00]. These calculi only support ordinary substitutions but not at the same time meta-substitutions.

Our calculus supports general closures on the type and term level. Meta-variables (which sometimes are also called contextual variables) are written as X. Typically, meta-variables occur as a closure [σ]X, but we will treat this as a special case of the general closure [σ]N.

To provide a compact representation of the typing rules, we follow the tradition of pure type systems and introduce sorts and expressions where sorts can be either kind or type and expressions include terms, types and kinds. A single syntactic category of expressions helps us avoid duplication in the typing and equality rules for closures [σ]E and [[θ]]E. We will write M, A, K, if indeed expressions can only occur as terms M, types A or kinds K.

Sorts  s  ::= kind | type
Expressions  E,F ::= s | a | ΠE.F | x_{n} | X_{n} | λ E | F E | [σ]E | [[θ]]E

Special cases of expressions:

Kinds  K  ::= type | ΠA.K | [σ]K | [[θ]]K
Types  A,B ::= a | A M | ΠA.B | [σ]A | [[θ]]A
Terms  M,N ::= x_{n} | X_{n} | λ M | M N | [σ]N | [[θ]]M (n ≥ 1)
Substitutions  σ,τ ::= ↑^{n} | σ,M | [τ]σ | [[θ]]σ  (n ≥ 0)
Meta-substitutions θ  ::= ⇑^{n} | θ,M | [[θ]]θ′  (n ≥ 0)
Contexts  Γ,Ψ ::= · | Ψ,A
Meta-contexts  Δ  ::= · | Δ,Ψ ▷ A

Constants are denoted by letter a, their types/kinds are recorded in a global well-formed signature Σ. We have two different de Bruijn indices x_{n} and X_{n} (n ≥ 1), one for numbering bound variables and one for numbering meta-variables. x_{n} represents the de Bruijn number n and stands for an ordinary bound variable, while X_{n} represents the de Bruijn number n but stands for a meta-variable. Due to the two kinds of substitutions, we also have two kinds of closures; the closure of an expression with an ordinary substitution σ and the closure of an expression with a meta-substitution θ. Following the treatment of meta-variables in [NPP08], we describe the type of a meta-variable as Ψ ▷ A which stands for a metavariable of type A which may refer to variables in Ψ.

Meta-substitutions provide a term M for a meta-variable X of type Ψ ▷ A. Note that M does not denote a closed term, but a term of type A in the context Ψ and hence may refer to variables from Ψ. In previous presentations where we use names for variables, we hence wrote Ψ̂.M/X to be able to rename the variables in M appropriately. Because bound variables are represented using de Bruijn indices in this paper, we simply write M/X but keep in mind that M is not necessarily closed.

Our calculus also features closures on the level of substitutions and meta-substitutions. For example, we allow the closure [σ]τ which will allow us to lazily treat ordinary substitution composition and the closure [[θ]]σ which will postpone applying θ to the ordinary substitution σ. Similarly, the closure [[θ]]θ′ for meta-substitutions allows us to lazily compose meta-substitutions. We note the absence of a closure [σ]θ. Applying an ordinary substitution σ to a meta-substitution θ simply reduces to θ, since all objects in the meta-substitution are closed objects and cannot be affected by σ. It is hence not meaningful to include a closure [σ]θ. We also do not introduce a closure of a context Ψ and a meta-substitution θ. Instead we define [[θ]]Ψ eagerly by simply pushing the meta-substitution θ to each declaration as follows: [[θ]]·= ·and [[θ]](Ψ,A) = [[θ]]Ψ, [[θ]]A. The length of a context Γ is denoted by |Γ| and likewise |Δ| for meta-contexts.

Expressions

\frac{Δ ⊢ Γ ctx}{Δ;Γ ⊢ type : kind}  \frac{Δ ⊢ Γ ctx  Σ(a) = K}{Δ;Γ ⊢ a: K}  \frac{Δ;Γ,A ⊢ E : s}{Δ;Γ ⊢ ΠA.E : s}
Δ;Γ ⊢ A: type
Δ;Γ,A ⊢ x_{1} : [↑^{1}]A

Δ;Γ ⊢ x_{n}: A Δ;Γ ⊢ B: type
Δ;Γ,B ⊢ x_{n+1} : [↑^{1}]A
Δ;Γ ⊢ A: type
Δ,Γ ▷ A;[[⇑^{1}]]Γ ⊢ X_{1} : [[⇑^{1}]]A

Δ;Γ ⊢ X_{n}: A Δ;Γ′ ⊢ A′: type
Δ,Γ′▷ A′;[[⇑^{1}]]Γ ⊢ X_{n+1} : [[⇑^{1}]]A
Δ;Γ,A ⊢ M : B Δ;Γ,A ⊢ B: type
Δ;Γ ⊢ λ M : ΠA.B

Δ;Γ ⊢ E : ΠA.F Δ;Γ ⊢ N : A Δ;Γ ⊢ E N : [↑^{0},N]F

Δ;Γ ⊢ σ : Ψ Δ;Ψ ⊢ E : kind
Δ;Γ ⊢ [σ]E : kind

Δ;Γ ⊢ σ : Ψ Δ;Ψ ⊢ E : F Δ;Γ ⊢ [σ]E : [σ]F

Δ ⊢ θ : Δ′ Δ′;Γ ⊢ E : kind

Δ;[[θ]]Γ ⊢ [[θ]]E : kind

Δ ⊢ θ : Δ′ Δ′;Γ ⊢ E : F Δ;[[θ]]Γ ⊢ [[θ]]E : [[θ]]F
Δ;Γ ⊢ E : F_{1} Δ;Γ ⊢ F_{1} ≡ F_{2} : s Δ;Γ ⊢ E : F_{2}

Contexts and meta-contexts

⊢ · mctx Δ;Ψ ⊢ A: type ; ⊢ Δ,Ψ ▷ A mctx  ⊢ Δ mctx ; Δ ⊢ · ctx  Δ;Ψ ⊢ A: type ; Δ ⊢ Ψ,A ctx

Ordinary substitutions

Δ ⊢ Ψ,Γ ctx |Γ| = n
Δ;Ψ,Γ ⊢ ↑^{n}: Ψ

Δ;Γ ⊢ σ : Ψ Δ;Ψ ⊢ A: type Δ;Γ ⊢ M : [σ]A
Δ;Γ ⊢ (σ,M) : (Ψ,A)
Δ;Γ ⊢ τ : Ψ′ Δ;Ψ′⊢ σ : Ψ
Δ;Γ ⊢ [τ]σ : Ψ

Δ ⊢ θ : Δ′ Δ′;Γ ⊢ σ : Ψ
Δ;[[θ]]Γ ⊢ [[θ]]σ : [[θ]]Ψ

Meta-substitutions

⊢ Δ,Δ′mctx |Δ′| = n
Δ,Δ′⊢ ⇑^{n}: Δ

Δ ⊢ θ : Δ′ Δ′;Γ ⊢ A: type Δ;[[θ]]Γ ⊢ M : [[θ]]A
Δ ⊢ (θ,M) : Δ′,Γ ▷ A

\begin{matrix}Δ ⊢ θ : Δ_{0} & Δ_{0} ⊢ θ′: Δ′ \\ Δ ⊢ [[θ]]θ′: Δ′ \end{matrix}

Figure 1: Typing rules for explicit substitution calculus with first-class meta-variables

2.1 Typing rules

In contrast to [HP05], we present the typing rules for LF in pure type system (PTS) style, to avoid rule duplication (which would be substantial for the rules of definitional equality given in the next section).

We will use the following judgments:

⊢ Δ mctx Meta-context Δ is well-typed
Δ  ⊢ Ψ ctx Context Ψ is well-typed
Δ;Γ ⊢ E : F Expression E has “type” F
Δ;Γ ⊢ σ : Ψ Substitution σ has domain Ψ and range Γ
Δ  ⊢ θ : Δ′ Contextual Substitution θ has domain Δ′and range Δ

The judgement Δ;Γ ⊢ E : F subsumes the judgements Δ;Γ ⊢ M : A (term M has type A), Δ;Γ ⊢ A : K (type family A has kind K) and Δ;Γ ⊢ K : kind (kind K is well-formed).

We present the typing rules in Figure 1 as a type assignment system for expressions E. To improve readability, we use the letters M,N instead of E when we know that we are dealing with a term, and similarly A,B for types and K for kinds.

In the typing rule for λM, the hypothesis Δ;Γ,A ⊢ B : type prevents us to form a λ-abstraction on the type level (for this, we would need B : kind). Lambda on the type level does not increase the expressiveness [Ada05, HP05]. Unlike the system in [HP05], we do not assume that the meta-context Δ and the context Γ are well-formed, but ensure that these are well-formed contexts by adding appropriate typing premises to for example the typing rules for bound variables and meta-variables. We establish separately that contexts are well-formed (see Lemma 1 on page 11) and that the inference rules are valid (see Theorem 4 on page 12).

We concentrate here on explaining the typing rules for bound variables and meta-variables. The typing rules for bound variables essentially peel off one type declaration in the context Γ until we encounter the variable x_{1}. The typing premises guarantee that the meta-context Δ and the context Γ and the type A of the bound variable all are well-typed. The rule for meta-variables are built in a similar fashion as the typing rules for bound variables peeling off type declarations from the meta-context Δ until we encounter the meta-variable X_{1}.

2.2 Definitional Equality

In this section, we describe a typed βη-equality judgement on expressions, ordinary substitutions, and meta-substitutions. We will use the following judgments:

Δ;Γ ⊢ E_{1} ≡ E_{2} : F Expressions E_{1} and E_{2} are equal at “type” F
Δ;Γ ⊢ σ_{1} ≡ σ_{2} : Ψ Substitutions σ_{1} and σ_{2} are equal at domain Ψ
Δ ⊢ θ_{1} ≡ θ_{2} : Δ′ Meta-substitutions θ_{1} and θ_{2} are equal at domain Δ′

The judgement Δ;Γ ⊢ E_{1} ≡ E_{2} : F subsumes the judgements Δ;Γ ⊢ K_{1} ≡ K_{2} : kind (kinds K_{1} and K_{2} are equal), Δ;Γ ⊢ A_{1} ≡ A_{2} : K (types A_{1} and A_{2} are equal of kind K) and Δ;Γ ⊢ M_{1} ≡ M_{2} : A (terms M_{1} and M_{2} are equal of type A).

These judgements are all congruences, i. e., we have equivalence rules (reflexivity, symmetry, transitivity) and a congruence rule for each syntactic construction. For instance, this is one of congruence rule for substitutions and the type conversion rule:

Δ;Γ ⊢ M ≡ M′: [σ]A Δ;Γ ⊢ A: type Δ;Γ ⊢ σ ≡ σ′: Ψ
Δ;Γ ⊢ (σ,M) ≡ (σ′,M′) : Ψ,A

Δ;Γ ⊢ E ≡ E′: F Δ;Γ ⊢ F ≡ F′: s Δ; Γ ⊢ E ≡ E′: F′

The remaining rules for definitional equality fall into two classes: the computational laws for ordinary substitutions (Figure 2) and the computational laws for meta-substitutions (Figure 3). Both sets of rules follow the same principle. They are grouped into identity and composition rules, propagation and reduction rules. For ordinary substitutions we also include β-reduction. For meta-substitutions, there is no equivalent β-reduction rule since we do not support abstraction over meta-variables. However, we add propagation into ordinary substitutions. Note that pushing a meta-substitution inside a lambdaabstraction or a Π-type does not require a shift of the indices, since indices of ordinary bound variables are distinct from indices of meta-variables and no capture can occur. There is no reduction for [σ][[θ]]M: an ordinary substitution cannot in general be pushed past a meta-substitution, it has to wait for the metasubstitution to be resolved.

To illustrate the definitional equality rules, we show how to derive Δ;Γ ⊢ [σ,M]x_{n+1} ≡ [σ]x_{n}: [σ]A which also demonstrates that such a rule is admissible. Transitivity is essential to assemble the following sub-derivations.

Step 1:

{Δ;Ψ ⊢ x_{n}: A \atop Δ;Ψ,B ⊢ x_{n+1} : [↑^{1}]A} Weakening
Δ;Ψ,B ⊢ x_{n+1} ≡ [↑^{1}]x_{n}: [↑^{1}]A

Reduction

Δ;Γ ⊢ [σ,M]x_{n+1} ≡ [σ,M][↑^{1}]x_{n}: [σ,M][↑^{1}]A

Congruence

Δ;Γ ⊢ [σ,M]x_{n+1} ≡ [σ,M][↑^{1}]x_{n}: [[σ,M]↑^{1}]A

Composition, Conversion

Step 2:

Δ;Γ ⊢ σ,M : Ψ,B Δ;Ψ,B ⊢ ↑^{1} : Ψ Δ;Ψ ⊢ x_{n}: A Δ;Γ ⊢ [σ,M][↑^{1}]x_{n} ≡ [[σ,M]↑^{1}]x_{n}: [[σ,M]↑^{1}]AComposition \begin{matrix}D \\ Δ;Γ ⊢ [σ,M]↑^{1} ≡ σ : Ψ \end{matrix} Δ;Γ ⊢ [[σ,M]↑^{1}]A ≡ [σ]A: type Congruence
Δ;Γ ⊢ [σ,M][↑^{1}]x_{n} ≡ [[σ,M]↑^{1}]x_{n}: [σ]A

Conversion

Step 3:

\begin{matrix}D \\ Δ;Γ ⊢ [σ,M]↑^{1} ≡ σ : Ψ \end{matrix} ; Δ;Γ ⊢ [[σ,M]↑^{1}]x_{n} ≡ [σ]x_{n}: [σ]ACongruence

where

D =

{Δ;Γ ⊢ σ,M : Ψ,B \atop Δ;Γ ⊢ [σ,M]↑^{1} = [σ]↑^{0} : Ψ} Pairing {Δ;Γ ⊢ σ : Ψ \atop Δ;Γ ⊢ [σ]↑^{0} ≡ σ : Ψ} Category Laws
Δ;Γ ⊢ [σ,M]↑^{1} ≡ σ : Ψ

Transitivity

Similarly, we can show that Δ;Γ ⊢ [[θ,M]]X_{n+1} ≡ [[θ]]X_{n}: [[θ]]A is admissible.

2.2.1 Extensionality Laws

As mentioned earlier, we take into account β-reductions and η-expansions. In particular, we consider η-rules for ordinary substitutions as well as meta-substitutions.

\frac{Δ;Γ ⊢ M : ΠA.B}{Δ;Γ ⊢ M ≡ λ(([↑^{1}]M) x_{1}) : ΠA.B}

\frac{Δ ⊢ Γ,A,Γ′ctx  |Γ′| = n}{Δ;Γ,A,Γ′ ⊢ ↑^{n} ≡ (↑^{n+1} ,x_{n+1} ) : Γ,A}  \frac{⊢ Δ,Γ ▷ A,Δ′mctx  |Δ′| = n}{Δ,Γ ▷ A,Δ′ ⊢ ⇑^{n} ≡ (⇑^{n+1} ,X_{n+1} ) : Δ,Γ ▷ A}

β-Reduction

\frac{Δ;Γ,A ⊢ M : B Δ;Γ,A ⊢ B: type Δ;Γ ⊢ N : A}{Δ;Γ ⊢ (λM)N ≡ [↑^{0},N]M : [↑^{0},N]B}

Substitution Propagation: Identity and Composition

\frac{Δ;Γ ⊢ E : F}{Δ;Γ ⊢ [↑^{0}]E ≡ E : F} \frac{Δ;Γ ⊢ σ : Γ′ Δ;Γ′ ⊢ τ : Ψ Δ;Ψ ⊢ E : F}{Δ;Γ ⊢ [σ][τ]E≡ [[σ]τ]E : [[σ]τ]F}

Substitution Propagation: Constants

\frac{Δ;Γ ⊢ σ : Ψ}{Δ;Γ ⊢ [σ]type ≡ type : kind} \frac{Δ;Γ ⊢ σ : Ψ Δ;Γ ⊢ a: K}{Δ;Γ ⊢ [σ]a ≡ a: [σ]K}

Substitution Propagation: Variable Lookup

\frac{Δ;Γ ⊢ σ : Ψ Δ;Ψ ⊢ A: type Δ;Γ ⊢ M : [σ]A}{Δ;Γ ⊢ [σ,M]x_{1} ≡ M : [σ]A} \frac{Δ;Γ ⊢ x_{n+1} : A}{Δ;Γ ⊢ x_{n+1} ≡ [↑^{1}]x_{n}: A}

Substitution Propagation: Pushing into Expression Constructions

\frac{Δ;Γ ⊢ σ : Ψ Δ;Ψ,A ⊢ F : s}{Δ;Γ ⊢ [σ](ΠA.F) ≡ Π[σ]A.[[↑^{1}]σ,x_{1}]F: s}

\frac{Δ;Γ ⊢ σ : Ψ  Δ;Ψ,A ⊢ M : B  Δ;Ψ,A ⊢ B: type}{Δ;Γ ⊢ [σ](λM) ≡ λ[[↑^{1}]σ,x_{1}]M: Π[σ]A.[[↑^{1}]σ,x_{1}]B}
\frac{Δ;Γ ⊢ σ : Ψ  Δ;Ψ ⊢ E : ΠA.F  Δ;Ψ ⊢ N : A}{Δ;Γ ⊢ [σ](E N) ≡ [σ]E [σ]N : [σ,[σ]N]F}

Substitution Reductions: Pairing and Shifting

\frac{Δ;Γ ⊢ (σ,M) : Ψ,Ψ′,A |Ψ′| = n}{Δ;Γ ⊢ [σ,M]↑^{n+1} ≡ [σ]↑^{n}: Ψ}  \frac{Δ;Γ ⊢ σ : Ψ′ Δ;Ψ′ ⊢ (τ,M) : Ψ,A}{Δ;Γ ⊢ [σ](τ,M) ≡ ([σ]τ,[σ]M) : Ψ,A}

\frac{Δ ⊢ Γ,Γ_{1},Γ_{2} ctx |Γ_{1}| = m |Γ_{2}| = n}{Δ;Γ,Γ_{1},Γ_{2} ⊢ [↑^{n}]↑^{m}≡ ↑^{n+m} : Γ}

Substitution Reductions: Category Laws

\frac{Δ;Γ ⊢ σ : Ψ}{Δ;Γ ⊢ [↑^{0}]σ ≡ σ : Ψ}  \frac{Δ;Γ ⊢ σ : Ψ}{Δ;Γ ⊢ [σ]↑^{0} ≡ σ : Ψ}

\frac{Δ;Γ_{1} ⊢ σ_{1} : Γ_{2} Δ;Γ_{2} ⊢ σ_{2} : Γ_{3} Δ;Γ_{3} ⊢ σ_{3} : Γ_{4}}{Δ;Γ_{1} ⊢ [σ_{1}][σ_{2}]σ_{3} ≡ [[σ_{1}]σ_{2}]σ_{3} : Γ_{4}}

Figure 2: Computational Laws I: β and substitutions Meta-Substitution Propagation: Identity and Composition

\frac{Δ;Γ ⊢ E : F}{Δ;Γ ⊢ [[⇑^{0}]]E ≡ E : F}  \frac{Δ ⊢ θ : Δ′ Δ′ ⊢ θ′: Δ′′ Δ′′;Γ ⊢ E : F}{Δ;[[[[θ]]θ′]]Γ ⊢ [[θ]][[θ′]]E ≡ [[[[θ]]θ′]]E : [[[[θ]]θ′]]F}

Meta-Substitution Propagation: Constants and Ordinary Variables

\frac{Δ ⊢ θ : Δ′ Δ′ ⊢ Γ ctx}{Δ;[[θ]]Γ ⊢ [[θ]]type ≡ type : kind} \frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ a: K}{Δ;[[θ]]Γ ⊢ [[θ]]a ≡ a: [[θ]]K} \frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ x_{n}: A}{Δ;[[θ]]Γ ⊢ [[θ]]x_{n}≡ x_{n}: [[θ]]A}

Meta-Substitution Propagation: Meta-variable Lookup

\frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ A: type Δ;[[θ]]Γ ⊢ M : [[θ]]A}{Δ;[[θ]]Γ ⊢ [[θ,M]]X_{1} ≡ M : [[θ]]A} \frac{Δ;Γ ⊢ X_{n+1} : A}{Δ;Γ ⊢ X_{n+1} ≡ [[⇑^{1}]]X_{n}: A}

Meta-Substitution Propagation: Pushing into Expression Constructions

\frac{Δ ⊢ θ : Δ′ Δ′;Γ,A ⊢ F : s}{Δ;[[θ]]Γ ⊢ [[θ]](ΠA.F) ≡ Π[[θ]]A.[[θ]]F : s}  \frac{Δ ⊢ θ : Δ′ Δ′;Γ,A ⊢ M : B  Δ′;Γ,A ⊢ B: type}{Δ;[[θ]]Γ ⊢ [[θ]](λM) ≡ λ[[θ]]M: Π[[θ]]A.[[θ]]B}
\frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ E : ΠA.F  Δ′;Γ ⊢ N : A}{Δ;[[θ]]Γ ⊢ [[θ]](E N) ≡ [[θ]]E [[θ]]N : [↑^{1},[[θ]]N]F}  \frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ σ : Ψ  Δ′;Ψ ⊢ E : F}{Δ;[[θ]]Γ ⊢ [[θ]][σ]E≡ [[[θ]]σ][[θ]]E: [[[θ]]σ][[θ]]F}

Meta-Substitution Propagation: Pushing into Ordinary Substitutions

\frac{Δ ⊢ θ : Δ′ Δ′ ⊢ Γ,Γ′ctx |Γ′| = n}{Δ;[[θ]]Γ,[[θ]]Γ′ ⊢ [[θ]]↑^{n} ≡ ↑^{n}: [[θ]]Γ}

\frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ σ : Ψ Δ′;Ψ ⊢ A: type Δ′;Γ ⊢ M : [σ]A}{Δ;[[θ]]Γ ⊢ [[θ]](σ,M) ≡ ([[θ]]σ,[[θ]]M) : [[θ]]Ψ,[[θ]]A}

\frac{Δ ⊢ θ : Δ′ Δ′;Γ ⊢ τ : Ψ′ Δ′;Ψ′ ⊢ σ : Ψ}{Δ;[[θ]]Γ ⊢ [[θ]][τ]σ≡ [[[θ]]τ][[θ]]σ : [[θ]]Ψ}  \frac{Δ ⊢ θ : Δ′ Δ′ ⊢ θ′: Δ′′ Δ′′;Γ ⊢ σ : Ψ}{Δ;[[[[θ]]θ′]]Γ ⊢ [[θ]][[θ′]]σ ≡ [[[[θ]]θ′]]σ : [[[[θ]]θ′]]Ψ}

Meta-Substitution Reductions: Pairing and Shifting

\frac{Δ ⊢ (θ,M) : Δ_{0},Δ′_{0},Γ ▷ A |Δ′_{0}| = n}{Δ ⊢ [[θ,M]]⇑^{n+1} ≡ [[θ]]⇑^{n}: Δ_{0}} \frac{Δ ⊢ θ : Δ′_{0} Δ′_{0} ⊢ (θ′,M) : Δ_{0},Γ ▷ A}{Δ ⊢ [[θ]](θ′,M) ≡ ([[θ]]θ′,[[θ]]M) : Δ_{0},Γ ▷ A}

\frac{⊢ Δ,Δ_{1},Δ_{2} mctx |Δ_{1}| = m |Δ_{2}| = n}{Δ,Δ_{1},Δ_{2} ⊢ [[⇑^{n}]]⇑^{m}≡ ⇑^{n+m} : Δ}

Meta-Substitution Reductions: Category Laws

\frac{Δ ⊢ θ : Δ_{0}}{Δ ⊢ [[⇑^{0}]]θ ≡ θ : Δ_{0}} \frac{Δ ⊢ θ : Δ_{0}}{Δ ⊢ [[θ]]⇑^{0} ≡ θ : Δ_{0}} \frac{Δ_{1} ⊢ θ_{1} : Δ_{2} Δ_{2} ⊢ θ_{2} : Δ_{3} Δ_{3} ⊢ θ_{3} : Δ_{4}}{Δ_{1} ⊢ [[θ_{1}]][[θ_{2}]]θ_{3} ≡ [[[[θ_{1}]]θ_{2}]]θ_{3} : Δ_{4}}

Figure 3: Computational Laws II: Meta-substitution 9 2.2.2 Compatibility and Equivalence Rules Substitution Congruence

Δ ⊢ Γ,Γ′ctx |Γ′| = n
Δ;Γ,Γ′⊢ ↑^{n} ≡ ↑^{n}: Γ

Δ;Γ ⊢ M ≡ M′: [σ]A Δ;Γ ⊢ σ ≡ σ′: Ψ
Δ;Γ ⊢ (σ,M) ≡ (σ′,M′) : Ψ,A

etc. + equivalences

Simultaneous Congruence

{Δ;Γ,A ⊢ M ≡ N : B \atop Δ;Γ ⊢ λ M ≡ λ N : ΠA.B}

\begin{matrix}Δ;Γ ⊢ M_{1} ≡ N_{1} : ΠA_{2}. A_{1} & Δ;Γ ⊢ M_{2} ≡ N_{2} : A_{2} \\ ΔΓ ⊢ M_{1}M_{2} ≡ N_{1}N_{2} : [↑^{0},M_{2}]A_{1} \end{matrix}

\begin{matrix}Δ;Γ ⊢ σ_{1} ≡ σ_{2} : Ψ & Δ;Ψ ⊢ M_{1} ≡ M_{2} : A \\ Δ;Γ ⊢ [σ_{1}]M_{1} ≡ [σ_{2}]M_{2} : [σ_{1}]A \end{matrix}

Δ;Γ ⊢ X_{n} ≡ X_{n}: A  Δ;Γ ⊢ x_{n} ≡ x_{n}: A

Equivalence

{Δ; Γ ⊢ N ≡ M : A \atop Δ; Γ ⊢ M ≡ N : A}  \begin{matrix}Δ; Γ ⊢ M ≡ N : A & Δ; Γ ⊢ N ≡ M′: A \\ Δ; Γ ⊢ M ≡ M′: A \end{matrix}

Type conversion

Δ; Γ ⊢ M ≡ N : A Δ;Γ ⊢ A ≡ B: type
Δ; Γ ⊢ M ≡ N : B

Family congruence

{a:E in Σ \atop Δ;Γ ⊢ a ≡ a: E}  \begin{matrix}Δ;Γ ⊢ A ≡ B: ΠC.K & Δ;Γ ⊢ M ≡ N : C \\ Δ;Γ ⊢ AM ≡ BN : [↑^{0},M]K \end{matrix}
Δ;Γ ⊢ A_{1} ≡ B_{1} : type {Δ;Γ ⊢ A_{1} : type} Δ;Γ,A_{1} ⊢ A_{2} ≡ B_{2} : type
Δ;Γ ⊢ ΠA_{1}.A_{2} ≡ ΠB_{1}.B_{2} : type

Family equivalence

{Δ;Γ ⊢ A ≡ B: K \atop Δ;Γ ⊢ B ≡ A: K}  \begin{matrix}Δ;Γ ⊢ A ≡ B: K & Δ;Γ ⊢ B ≡ C : K \\ Δ;Γ ⊢ A ≡ C : K \end{matrix}

Kind conversion

Δ;Γ ⊢ A ≡ B: K Δ;Γ ⊢ K ≡ L: kind
Δ;Γ ⊢ A ≡ B: L

Kind congruence

Δ;Γ ⊢ type ≡ type : kind

Δ;Γ ⊢ A ≡ B: type {Δ;Γ ⊢ A: type} Δ;Γ,A ⊢ K ≡ L: kind

Δ;Γ ⊢ ΠA.K ≡ ΠB.L: kind

Kind equivalence

Δ;Γ ⊢ K ≡ L: kind
Δ;Γ ⊢ L ≡ K : kind

Δ;Γ ⊢ K ≡ L′: kind Δ;Γ ⊢ L′≡ L: kind

Δ;Γ ⊢ K ≡ L: kind 10

2.3 Properties

Next, we prove some standard properties about the presented type assignment system. First, we show that contexts are indeed well-formed.

Lemma 1 (Context well-formedness)

1. If Δ,Δ′ ⊢ J or Δ,Δ′;Γ ⊢ J then ⊢ Δ mctx.

2. If Δ ⊢ θ : Δ′or Δ ⊢ θ ≡ θ′: Δ′then ⊢ Δ′mctx.

3. If Δ;Γ,Γ′ ⊢ J then Δ ⊢ Γ ctx.

4. If Δ;Γ ⊢ σ : Ψ or Δ;Γ ⊢ σ ≡ σ′: Ψ then Δ ⊢ Ψ ctx.

The height of the output derivation is bounded by the height of the input derivation, in all cases.

Proof. By simultaneous induction over all judgments. □

The following inversion theorem for typing is standard for PTSs and are necessary due to the type conversion rule which makes inversion a non-obvious property. It allows us to classify expressions into terms, types, kinds, and the sort kind. We write Δ;Γ ⊢ E ≡ E′ if there exists a sort s such that Δ;Γ ⊢ E ≡ E′: s.

Theorem 2 (Inversion of typing)

1. There is no derivation of Δ;Γ ⊢ kind : E.

2. If Δ;Γ ⊢ type : E then E = kind.

3. If Δ;Γ ⊢ a: E then Δ;Γ ⊢ E ≡ Σ(a).

4. If Δ;Γ ⊢ ΠA.E : F then Δ;Γ ⊢ A: type and Δ;Γ,A ⊢ E : F and either F = kind or Δ;Γ ⊢ F ≡ type.

5. If Δ;Γ ⊢ x_{n+1} : A then Γ = Γ_{1},A′,Γ_{2} with |Γ_{2}| = n and Δ;Γ ⊢ A ≡ [↑^{n+1} ]A′.

6. If Δ;Γ ⊢ X_{n+1} : A then Δ = Δ_{1},Γ′▷A′,Δ_{2} with |Δ_{2}| = n and Γ = [[⇑^{n+1} ]]Γ′ and Δ;Γ ⊢ A ≡ [[⇑^{n+1} ]]A′.

7. If Δ;Γ ⊢ λM : C then there are A,B such that Δ;Γ ⊢ C ≡ ΠA.B and Δ;Γ ⊢ A: type and Δ;Γ,A ⊢ B: type and Δ;Γ,A ⊢ M : B.

8. If Δ;Γ ⊢ E N : C then there are A,F such that Δ;Γ ⊢ E : ΠA.F and Δ;Γ ⊢ N : A and Δ;Γ ⊢ C ≡ [↑^{0},N]F.

9. If Δ;Γ ⊢ [σ]E : F then there are Ψ,F′such that Δ;Γ ⊢ σ : Ψ and Δ;Ψ ⊢ E : F′ and Δ;Γ ⊢ E ≡ [σ]F′.

10. If Δ;Γ ⊢ [[θ]]E : F then there are Δ′,Γ′,F′such that Δ ⊢ θ : Δ′and Δ;Γ′ ⊢ E : F′and Γ = [[θ]]Γ′ and Δ;Γ ⊢ F ≡ [[θ]]F′.

Proof. By induction on the typing derivation, peeling off the type conversion steps and combining them with transitivity. □

Expression E is a kind if Δ;Γ ⊢ E : kind for some Δ,Γ, it is a type family if Δ;Γ ⊢ E : K for some kind K and some Δ,Γ, and it is a term if Δ;Γ ⊢ E : A for some A,Δ,Γ with Δ;Γ ⊢ A: type.

The following inversion statement for meta-variables under a substitution is crucial for the correctness of algorithmic equality (Sec. 3.2) and bidirectional type checking (Sec. 4).

Corollary 3 If Δ;Γ ⊢ [σ]X_{m}: A then Δ = Δ_{1},Ψ ▷ A′,Δ_{2} with |Δ_{2}| = m − 1 and Δ;Γ ⊢ σ : [[⇑^{m}]]Ψ and Δ;Γ ⊢ A ≡ [σ][[⇑^{m}]]A′.

Theorem 4 (Syntactic Validity)

1. If Δ;Γ ⊢ E : F or Δ;Γ ⊢ E_{1} ≡ E_{2} : F then Δ;Γ ⊢ F : s for some sort.

2. If Δ;Γ ⊢ E ≡ E′: F then Δ;Γ ⊢ E : F and Δ;Γ ⊢ E′: F.

3. If Δ ⊢ θ ≡ θ′: Δ′then Δ ⊢ θ : Δ′and Δ ⊢ θ′: Δ′.

4. If Δ;Γ ⊢ σ ≡ σ′: Ψ then Δ;Γ ⊢ σ : Ψ and Δ;Γ ⊢ σ′: Ψ. Proof. By simultaneous induction over all judgments. □

3 Evaluation and Algorithmic Equality

In this section, we define a weak head normalization strategy together with algorithmic equality. The goal is to treat ordinary substitutions and meta-substitutions lazily; in particular, we aim to postpone shifting of substitutions until necessary. For the treatment of LF, an untyped algorithmic equality is sufficient. The design of the algorithm follows Coquand [Coq91] with refinements from joint work with the first author [AC07]. In this article, we only show soundness of the algorithm; completeness can be proven using techniques of the cited works. However, an adaptation to de Bruijn style and explicit substitutions is necessary; we leave the details to future work, a sketch can be found in the appendix.

We first characterize our normal forms by defining normal and neutral expressions where expressions include terms, types, and kinds. Normal forms are exactly the expressions we can type-check with a bidirectional algorithm (see Section 4). Note that type checking normal forms is sufficient in practice, since the input to the type checker, written by a user, is almost always in β-normal form (or can be turned into normal form by introducing typed let-definitions).

Normal substitutions are built out of normal expressions. However, it is worth keeping in mind that our typing rules will ensure that they only contain terms and not types, since we do not support typelevel variables. Our normal forms are only β-normal, not necessarily η-long. Only meta-variables are associated with an ordinary normal substitution, all other closures have been eliminated.

Normal expressions V ::= s | ΠV.V′| λV | U
Neutral expressions U ::= a | x_{n} | [ν]X_{n}| U V
Normal substitutions ν ::= ↑^{n} | (ν,V)

Next, we define weak head normal forms (whnf). Since we want to treat ordinary substitutions and meta-substitutions lazily and in particular want to postpone the complete computation of their compositions, we cannot require that substitutions and meta-substitutions are already in normal form. Hence, we introduce environments ρ for ordinary substitutions and similarly meta-substitutions η for describing substitutions and meta-substitutions that are in weak head normal form. Closures are expressions E in an environment ρ and a meta-environment η. It is convenient to also treat variables x_{n} as closures. These arise when stepping under a binder in type and equality checking and are the synonym of Coquand’s generic values [Coq96].

Weak head normal forms  W ::= type | [ρ][[η]]ΠA.B | [ρ][[η]]λM | H
Neutral weak head normal forms H ::= a | x_{n} | [ρ]X_{n}| H L
Closures  L ::= x_{n} | [ρ][[η]]E
Environments  ρ ::= ↑^{n} | (ρ,L) | [↑^{n}]ρ
Meta-environments  η ::= ⇑^{n} | (η,M)

Our weak head normal forms and closures combine substitutions and meta-substitutions and our whnf-reduction strategy simultaneously treats substitutions and meta-substitutions. Instead of coupling expressions with two suspended substitutions, we could have introduced a joint simultaneous substitutions and closures built with them. The path taken in this paper builds on the individual substitution operations instead of defining a new joint substitution operation. To clarify the nature and the interplay of ordinary substitutions and meta-substitutions it is helpful to consider the typing rule of closures [ρ][[η]]E:

Δ;Ψ ⊢ ρ : [[η]]Ψ′ Δ ⊢ η : Δ′ Δ′;Ψ′⊢ E : F
Δ;Ψ ⊢ [ρ][[η]]E : [ρ][[η]]F

Intuitively, this means to obtain an expression E′which makes actually sense in Δ and Ψ, we first compute [[η]]E and subsequently apply the ordinary substitution ρ to arrive at E′≡ ([ρ][[η]]E).

Shift propagation. While we treat shifts in the environment as an explicit operation—to avoid a traversal when lifting an environment under a binder—, shifting a closure or a neutral weak head normal form can be implemented inexpensively. Let shifting shift^{n}L of a closure L be defined by shift^{n}x_{m}= x_{n+m} and shift^{n}([ρ][[η]]E)= [[↑^{n}]ρ][[η]]E. It is extended to shifting of neutral weak head normal forms H by shift^{n}(H L)= (shift^{n}H) (shift^{n}L) and shift^{n}([ρ]X_{m})= [[↑^{n}]ρ]X_{m}and shift^{n}a = a.

3.1 Weak head evaluation

Our weak head evaluation strategy will postpone propagation of substitutions into an expression until necessary. Treating substitutions lazily seems to be beneficial as also supported by the experimental analysis on lazy vs eager reduction strategies for substitutions by Nadathur and his collaborators [LNQ05]. We present the algorithm for weak head normalization in Figure 4. We define a function whnf L where L is either a variable x_{n} or a proper closure [ρ][[η]]E. The function whnf is then defined recursively on E.

To support the lazy evaluation of substitutions, our weak head normalization algorithm relies on the definition of two functions, namely Env η θ and env ρ η σ. Both functions are defined recursively over the last argument, i.e., Env is inductively defined over θ and env is inductively defined over σ. When we encounter a closure of [σ]τ (or [[θ]]θ′resp.), we compute first the environment corresponding to σ and subsequently we compute the environment for τ. This strategy allows us to avoid unnecessary shifting of de Bruijn indices.

In addition, whnf relies on a lookup function to retrieve the i-th element of a substitution which corresponds to the index i. Such lookup functions are defined for both, ordinary variables and metavariables.

Next, we prove that types are preserved when computing weak head normal forms and that the computation is sound with regard to the specification of definitional equality. Note that at this point termination is only clear for the lookup and substitution evaluation functions. For whnf and evaluating application @, soundness is conditional on termination.

Theorem 5 (Subject reduction) Let Δ ⊢ η : Δ′.

1. If Δ′ ⊢ θ : Δ′′then Δ ⊢ Env η θ ≡ [[η]]θ : Δ′′.

2. If Δ′;Ψ ⊢ σ : Ψ′and Δ;Γ ⊢ ρ : [[η]]Ψ then Δ;Γ ⊢ env ρ η σ ≡ [ρ][[η]]σ : [[η]]Ψ′.

3. If Δ′;Ψ ⊢ X_{m}: A then Δ;[[η]]Ψ ⊢ Lookup η X_{m}≡ [[η]]X_{m}: [[η]]A.

4. If Δ;Ψ ⊢ x_{m}: A and Δ;Γ ⊢ ρ : Ψ then Δ;Γ ⊢ lookup ρ x_{m}≡ [ρ]x_{m}: [ρ]A.

Meta-substitution evaluation Env η θ computes the meta-environment form of [[η]]θ.

Env ⇑^{m} ⇑^{n}  = ⇑^{m+n}
Env (η,M) ⇑^{n+1}  = Env η ⇑^{n}
Env η (θ,M)  = (Env η θ,[[η]]M)
Env η [[θ]]θ′  = Env (Env η θ) θ′

Substitution evaluation env ρ η σ computes the environment form of [ρ][[η]]σ .

env ([↑^{k}]ρ) η σ  = [↑^{k}](env ρ η σ)
env ρ η ↑^{0}  = ρ
env ↑^{k} η ↑^{n}  = ↑^{k+n}
env (ρ,L) η ↑^{n+1}  = env ρ η ↑^{n}
env ρ η (σ,M)  = (env ρ η σ,[ρ][[η]]M)
env ρ η ([σ]τ)  = env (env ρ η σ) η τ
env ρ η ([[θ]]σ)  = env ρ (Env η θ) σ

Meta-variable lookup Lookup η X_{m}retrieves the binding of X_{m} in meta-environment η.

Lookup ⇑^{n} X_{m}  = X_{n+m}
Lookup (η,E) X_{1}  = E
Lookup (η,E) X_{m+1} = Lookup η X_{m}

Variable lookup lookup ρ x_{m}computes the closure form of [ρ]x_{m}.

lookup ↑^{n} x_{m}  = x_{n+m}
lookup (ρ,L) x_{1}  = L
lookup (ρ,L) x_{m+1} = lookup ρ x_{m}
lookup ([↑^{n}]ρ) x_{m} = shift^{n}(lookup ρ x_{m})

Weak head evaluation whnf L computes the weak head normal form of closure L.

whnf x_{m}  = x_{m}
whnf [ρ][[η]]s  = s
whnf [ρ][[η]]a  = a
whnf [ρ][[η]]x_{m}  = whnf (lookup ρ x_{m})
whnf [ρ][[⇑^{0}]]X_{m}  = [ρ]X_{m}
whnf [ρ][[η]]X_{m}  = whnf [ρ][[⇑^{0}]](Lookup η X_{m})
whnf [ρ][[η]](ΠA.E) = [ρ][[η]](ΠA.E)
whnf [ρ][[η]](λM) = [ρ][[η]](λM)
whnf [ρ][[η]](M N) = (whnf [ρ][[η]]M) @ [ρ][[η]]N
whnf [ρ][[η]][σ]M = whnf [env ρ η σ][[η]]M
whnf [ρ][[η]][[θ]]M = whnf [ρ][[Env η θ]]M

Evaluating application W @ L computes the weak head normalform of W L.

[ρ][[η]](λM) @ L  = whnf [ρ,L][[η]]M
H @ L  = H L

Figure 4: Weak head evaluation 5. Let Δ′;Ψ ⊢ E : F and Δ;Γ ⊢ ρ : [[η]]Ψ.

If whnf [ρ][[η]]E is defined then Δ;Γ ⊢ whnf [ρ][[η]]E ≡ [ρ][[η]]E : [ρ][[η]]F.

6. Let Δ;Γ ⊢ W : ΠA.F and Δ;Γ ⊢ L: A. If W @ L is defined then Δ;Γ ⊢ W @ L ≡ W L: [↑^{0},L]F.

Proof. Each by induction on the trace of the function and inversion on the typing derivations, the first four statements in isolation and the remaining two simultaneously. □

3.2 Algorithmic equality

Building on the weak head normalization algorithm introduced in the previous section, we now give an algorithm for deciding equality of expressions. This is a key piece in the bi-directional type checking algorithm which we present in Section 4. Two closures, where L = [ρ][[η]]E and L′= [ρ′][[η′]]E′, are algorithmically equal if their weak head normal forms are related, i.e., whnf [ρ][[η]]E ∼^{w} whnf [ρ′][[η′]]E′.

As we check that two expressions are equal, we lazily normalize them using our weak head normalization algorithm from the previous section and our algorithmic equality algorithm alternates between applying a whnf step and actually comparing two expressions or substitutions.

The actual equality algorithm is defined using three mutual recursive judgments. 1) checking that two expressions in whnf are equal 2) checking that two neutral weak head normal forms are equal and 3) checking that two environments, i.e., ordinary substitutions in whnf, are equal.

W ∼^{w} W′  weak head normal forms W,W′are algorithmically equal
H ∼^{n} H′  neutral weak head normal forms H,H′are algorithmically equal
[↑^{k}]ρ ∼^{r} [↑^{k′}]ρ′ environments ρ,ρ′are algorithmically equal under shifts by k,k′resp.

Many of the algorithmic equality rules are straightforward and intuitive, although a bit veiled by the abundance of explicit shifting that comes with de Bruijn style. When checking whether two metavariables are equal, we need to make sure that respective environments are equal. When we check whether two lambda-abstractions are equal, we must lift their environments under the lambda-binding. This amounts to shifting them by one and extending them with a binding for the first variable. To handle eta-equality, we eta-expand the neutral weak head normal form H on the fly when comparing it to a lambda-closure.

Comparing two environments for equality simply recursively analyzes the substitutions. In addition, we handle just-in-time eta-expansion on the level of substitutions (see the last two rules).

Algorithmic equality of neutral weak head normal forms.

\overline{a ∼^{n} a} \overline{x_{m} ∼^{n} x_{m}}

\frac{[↑^{0}]ρ ∼^{r} [↑^{0}]ρ′}{[ρ]X_{m}∼^{n} [ρ′]X_{m}} H ∼^{n} H′ whnf L ∼^{w} whnf L′

H L ∼^{n} H′L′

Algorithmic equality of weak head normal forms.

\overline{s ∼^{w} s}

whnf [ρ][[η]]A ∼^{w} whnf [ρ′][[η′]]A′ whnf [[↑^{1}]ρ,x_{1}][[η]]B ∼^{w} whnf [[↑^{1}]ρ′,x_{1}][[η′]]B′

[ρ][[η]](ΠA.B) ∼^{w} [ρ′][[η′]](ΠA′.B′)

\frac{H ∼^{n} H′}{H ∼^{w} H} whnf [[↑^{1}]ρ,x_{1}][[η]]M ∼^{w} whnf [[↑^{1}]ρ′,x_{1}][[η′]]M′

[ρ][[η]](λM) ∼^{w} [ρ′][[η′]](λM′)

whnf [[↑^{1}]ρ,x_{1}][[η]]M ∼^{w} (shift^{1}H) x_{1}

[ρ][[η]](λM) ∼^{w} H

(shift^{1}H) x_{1} ∼^{w} whnf [[↑^{1}]ρ,x_{1}][[η]]M

H ∼^{w} [ρ][[η]](λM)

Algorithmic equality of environments.

\frac{k + n = k′+ n′}{[↑^{k}]↑^{n} ∼^{r} [↑^{k′}]↑^{n′}}  \frac{[↑^{k+n}]ρ ∼^{r} [↑^{k′}]ρ′}{[↑^{k}][↑^{n}]ρ ∼^{r} [↑^{k′}]ρ′}  \frac{[↑^{k}]ρ ∼^{r} [↑^{k′+n′}]ρ′}{[↑^{k}]ρ ∼^{r} [↑^{k′}][↑^{n′}]ρ′}

[↑^{k}]ρ ∼^{r} [↑^{k′}]ρ′ whnf (shift^{k}L) ∼^{w} whnf (shift^{k′}L′)

[↑^{k}](ρ,L) ∼^{r} [↑^{k′}](ρ′,L′)

[↑^{k}]ρ ∼^{r} [↑^{k′}]↑^{n′+1} whnf (shift^{k}L) ∼^{w} x_{k′+n′+1}

[↑^{k}](ρ,L) ∼^{r} [↑^{k′}]↑^{n′}

[↑^{k}]↑^{n+1} ∼^{r} [↑^{k′}]ρ′ x_{k+n+1} ∼^{w} whnf (shift^{k′}L′)

[↑^{k}]↑^{n} ∼^{r} [↑^{k′}](ρ′,L′)

Theorem 6 (Soundness of algorithmic equality)

1. If H ∼^{n} H′and Δ;Γ ⊢ H : F and Δ;Γ ⊢ H′: F′then Δ;Γ ⊢ F ≡ F′and Δ;Γ ⊢ H ≡ H′: F.

2. If W ∼^{w} W′and Δ;Γ ⊢ W : F and Δ;Γ ⊢ W′: F then Δ;Γ ⊢ W ≡ W′: F.

3. If [↑^{k}]ρ ∼^{r} [↑^{k′}]ρ′and Δ;Γ ⊢ [↑^{k}]ρ : Ψ and Δ;Γ ⊢ [↑^{k′}]ρ′: Ψ then Δ;Γ ⊢ [↑^{k}]ρ ≡ [↑^{k′}]ρ′: Ψ.

Proof. Simultaneously by induction on the derivation of algorithmic equality and inversion on the typing. □

4 Bidirectional Type Checking

In this section, we show how to use our explicit substitution calculus to type-check expressions. As mentioned in the introduction, accumulating substitution walks in type-checking is one of the key applications of this work. We only describe the algorithm and leave its theoretical properties for future work.

We design the algorithm in a bidirectional way [Coq96, AC07] which allows us to omit type annotations at lambda-abstractions. We use the following three judgments:

Δ;Γ ⊢ V ⇇ s Type normal form V checks against sort s
Δ;Γ ⊢ V ⇇ L Normal form V checks against “type” closure L
Δ;Γ ⊢ U ⇉ L The type of neutral normal form U is inferred as closure L
Δ;Γ ⊢ ν ⇇ Ψ Normal substitution ν checks against domain Ψ

In these judgements, Γ is a list of type closures L. On Δ we pose no restrictions; an entry Ψ▷A of Δ is as before a list of type expressions Ψ and a type expression A. Inferring the type of neutral normal forms U.

\overline{Δ;Γ ⊢ a ⇉ [↑^{0}][[⇑^{0}]]Σ(a)}  \frac{Δ;Γ ⊢ U ⇉ L  whnf L = [ρ][[η]](ΠA.B)  Δ;Γ ⊢ V ⇇ [ρ][[η]]A}{Δ;Γ ⊢ U V ⇉ [ρ,V][[η]]B}

\frac{|Γ′| = n}{Δ;Γ,L,Γ′ ⊢ x_{n+1} ⇉ shift^{n+1} L}  \frac{Δ = Δ_{1},Ψ ▷ A,Δ_{2}  |Δ_{2}| = n  Δ;Γ ⊢ ν ⇇ [↑^{0}][[⇑^{n+1} ]]Ψ}{Δ;Γ ⊢ [ν]X_{n+1} ⇉ [ν][[⇑^{n+1} ]]A}

Checking the type of normal forms V.

whnf L = [ρ][[η]](ΠA.B) Δ;Γ,[ρ][[η]]A ⊢ V ⇇ [↑^{1}ρ,x_{1}][[η]]B Δ;Γ ⊢ λV ⇇ L

Δ;Γ ⊢ U ⇉ L whnf L ∼^{w} whnf L′
Δ;Γ ⊢ U ⇇ L′

Checking well-formedness of types and kinds V.

Δ;Γ ⊢ type ⇇ kind

Δ;Γ ⊢ V ⇇ type Δ;Γ,[↑^{0}][[⇑^{0}]]V ⊢ V′⇇ s
Δ;Γ ⊢ ΠV.V′⇇ s

\frac{Δ;Γ ⊢ U ⇉ L whnf L = type}{Δ;Γ ⊢ U ⇇ type}

Checking normal substitutions ν. In this judgement Δ;Γ ⊢ ν ⇇ Ψ, the context Ψ is also in closure form.

\frac{|Γ| = n}{Δ;Γ ⊢ ↑^{n} ⇇ ·}  \frac{Δ;Γ ⊢ ν ⇇ Ψ  Δ;Γ ⊢ V ⇇ L}{Δ;Γ ⊢ (ν,V) ⇇ Ψ,L}

5 Conclusion

We have presented an explicit substitution calculus together with algorithms for weak head normalization, definitional equality, and bi-directional type checking where both ordinary variables and metavariables are modelled using de Bruijn indices and both kinds of substitutions are handled lazily and simultaneously.

We also have proven subject reduction and soundness of the definitional equality algorithm. A sketch of the normalization proof, which guarantees that the described algorithm is complete, can be found in the appendix. Finally, we describe a bi-directional type-checking algorithm which treats ordinary substitutions and meta-substitutions at the same time. In the future, we plan to adapt the presented explicit substitutions in the implementation of the programming and reasoning environment Beluga.

References

[AC07] Andreas Abel and Thierry Coquand. Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundamenta Informaticae, 77(4):345–395, 2007. TLCA’05 special issue.

[ACCL91] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

[Ada05] Robin Adams. A Modular Hierarchy of Logical Frameworks. PhD thesis, University of Manchester, 2005.

[BDN09] Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs’09), volume 5674 of Lecture Notes in Computer Science, pages 73–78. Springer-Verlag, 2009.

[Coq91] Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 255–279. Cambridge University Press, 1991.

[Coq96] Thierry Coquand. An algorithm for type-checking dependent types. In Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), volume 26 of Science of Computer Programming, pages 167–177. Elsevier, May 1996.

[DHK00] Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher order unification via explicit substitutions. Information and Computation, 157(1-2):183–235, 2000.

[HP05] Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic, 6(1):61–101, 2005.

[LNQ05] Chuck Liang, Gopalan Nadathur, and Xiaochu Qi. Choices in representation and reduction strategies for lambda terms in intensional contexts. Journal of Automated Reasoning, 33(2):89–132, 2005.

[Nor07] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden, September 2007.

[NPP08] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1–49, 2008.

[NW98] Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1-2):49–98, 1998.

[PD08] Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In ACM SIG-PLAN Symposium on Principles and Practice of Declarative Programming (PPDP’08), pages 163– 173. ACM Press, July 2008.

[PD10] Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Jürgen Giesl and Reiner Hähnle, editors, 5th International Joint Conference on Automated Reasoning (IJCAR’10), Lecture Notes in Computer Science. Springer-Verlag, 2010.

[Pie03] Brigitte Pientka. Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2003. CMU-CS-03-185.

[PS99] Frank Pfenning and Carsten Schürmann. System description: Twelf — a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, pages 202–206. Springer, 1999.

[PS08] Adam B. Poswolsky and Carsten Schürmann. Practical programming with higher-order encodings and dependent types. In Proceedings of the 17th European Symposium on Programming (ESOP ’08), volume 4960, page 93. Springer, March 2008.

[PS09] Adam Poswolsky and Carsten Schürmann. System description: Delphin - a functional programming language for deductive systems. Electronic Notes in Theoretical Computer Science, 228:113–120, 2009.

A Normalization

The proof of normalization follows the blue print laid out in earlier work [AC07]. To show normalization and completeness of algorithmic equality, we interpret types A as partial equivalence relations (PERs) A between expressions, i. e., relations that are symmetric and transitive. By establishing A ⊆ (∼^{w}) which means that two elements related by A are algorithmically equal, and by the fundamental theorem which states that definitionally equal terms Δ;Γ ⊢ M ≡ M′: A evaluate to elements related by A, obtain completeness of algorithmic equality. The model construction also yields termination of algorithmic equality, thus, as a final result we can show that algorithmic equality decides definitional equality for well-typed terms.

The basic PERs are the algorithmic equality relations. We define a relation on environments by ρ ∼^{r} ρ′ ⟺ ∀k.[↑^{k}]ρ ∼^{r} [↑^{k}]ρ′. The k is actually irrelevant, as witnessed by the following lemma:

Lemma 7 (Environment equality) For all k_{1},k_{2} we have [↑^{k_{1}}]ρ ∼^{r} [↑^{k_{1}}]ρ′iff [↑^{k_{2}}]ρ ∼^{r} [↑^{k_{2}}]ρ′.

Lemma 8 (Shifting equal elements) 1. If whnfL ∼^{w} whnf L′then whnf shift^{k}L ∼^{w} whnf shift^{k}L′.

2. If H ∼^{n} H′then shift^{k}H ∼^{n} shift^{k}H′.

In both cases, the output derivation has the same height as the input derivation.

Lemma 9 The algorithmic equality relations (∼^{w}),(∼^{n}),(∼^{r} ),(∼^{r} ) are PERs.

Constructions on PERs. If A is a PER on closures and B a PER on weak head normal forms we define the closure \overline{B} and the function space A → B by

\overline{B}  = \{(L,L′) | (whnf L,whnf L′) ∈ B\}
A → B = {(W,W′) | (W @ L,W′@ L′) ∈ B for all (L,L′) ∈ A }.

Closure is a monotone operator on PERs, and function space → is an operator on PERs which is antitone in the domain and monotone in the codomain.

Contexts will be interpreted as PERs over environments. For G a PER on environments, A a PER on closures and B a PER on weak head normal forms let

(∼^{i} )  = {(↑^{n},↑^{n}) | n ∈ ℕ}
G × A = {(ρ,ρ′) | (env ρ ⇑^{0} ↑^{1},env ρ′⇑^{0} ↑^{1}) ∈ G and (lookup ρ x_{1},lookup ρ′x_{1}) ∈ A)}
G ▷ B = {(E,E′) | (whnf [ρ][[⇑^{0}]]E,whnf [ρ′][[⇑^{0}]]E′) ∈ B for all (ρ,ρ′) ∈ G }.

Product × is a monotone operator on PERs. Entailment ▷ , like function space, is a PER operator that is antitone in the domain and monotone in the codomain.

To interpret meta-contexts, we define a meta-product D ⊗ E between a PER over meta-contexts D and a PER over expressions E.

D ⊗ E = {(θ,θ′) | (Env θ ⇑^{1},Env θ′⇑^{1}) ∈ D and (Lookup θ X_{1},Lookup θ′X_{1}) ∈ E }

Type interpretation. In terms of proof theoretic strength, LF equals the simply-typed lambda calculus. Dependencies in LF can be erased in the normalization proof, hence types can be interpreted as “simplytyped” PERs (as opposed to using families of PERs [AC07]) . Also, since we have no λ on the type level, we do not have to model operators on PERs, and we model kinds simply as PERs over type expressions. We arrive at the following definition of type interpretation:

⦇E⦈  = (∼^{w})  if E is a term
⦇ΠA.E⦈ = \overline{⦇A⦈}→ ⦇E⦈
⦇[σ]E⦈ = ⦇E⦈
⦇[[θ]]E⦈ = ⦇E⦈
⦇E⦈  = (∼^{w})  otherwise

The interpretation of terms does not really matter, we set them to (∼^{w}) for conformity. Because of erasure and since we have no type variables, interpretation can ignore substitutions and redexes altogether. Lemma 10 (Semantic type equality) If Δ;Γ ⊢ E ≡ E′: F then ⦇E⦈ = ⦇E′⦈. Proof. By induction on the derivation of equivalence. The lemma is trivial because we have no type or kind variables and all computation is happening on the term level and is ignored by the operation ⦇E⦈. □

Context and meta-context interpretation.

⦇·⦈  = (∼^{r} )  empty context
⦇Ψ,A⦈  = ⦇Ψ⦈ × ⦇A⦈
⦇Ψ ▷ A⦈  = ⦇Ψ⦈ ▷ ⦇A⦈
⦇·⦈ = {(⇑^{0},⇑^{0})} empty meta-context
⦇Δ,Ψ ▷ A⦈ = ⦇Δ⦈ ⊗ ⦇Ψ ▷ A⦈

Note that ⦇[[θ]]Ψ⦈ = ⦇Ψ⦈.

The constructions on PERs satisfy the following inclusions. Lemma 11

1. (∼^{n}) ⊆ \overline{(∼^{w})} → (∼^{n}) ⊆ \overline{(∼^{n})} → (∼^{w}) ⊆ (∼^{w}).

2. (∼^{i} ) ⊆ (∼^{i} ) × \overline{(∼^{n})} ⊆ (∼^{r} ) × \overline{(∼^{w})} ⊆ (∼^{r} ).

3. (∼^{n}) ⊆ ⦇E⦈ ⊆ (∼^{w}).

4. (∼^{i} ) ⊆ ⦇Ψ⦈ ⊆ (∼^{r} ).

As a consequence, semantic types are sandwiched between the algorithmic equality relation (∼^{n}) on neutral weak head normal forms and the algorithmic equality (∼^{w}) on weak head normal forms. In particular, each semantic type contains the variables, (x_{m},x_{m}) ∈ ⦇A⦈, and only algorithmically equal elements are related by a semantic type. The presence of the variables in the semantic types is crucial to show a normalization property for open expressions. In our case, it is needed to establish that the identity environment ↑^{0} is a valid inhabitant of each semantic context ⦇Ψ⦈, or more precisely (↑^{0},↑^{0}) ∈ ⦇Ψ⦈.

Semantic judgements. In the following, we establish that our PERs actually model typing and equality rules of LF.

Δ;Γ ⊧ E : F ⟺ Δ;Γ ⊧ E ≡ E : F
Δ;Γ ⊧ E ≡ E′: F ⟺  (whnf [ρ][[η]]E,whnf [ρ′][[η′]]E′) ∈ ⦇F ⦈ for all (η,η′) ∈ ⦇Δ⦈ and (ρ,ρ′) ∈ ⦇Γ⦈
Δ;Γ ⊧ σ : Ψ  ⟺  Δ;Γ ⊧ σ ≡ σ : Ψ
Δ;Γ ⊧ σ ≡ σ′: Ψ  ⟺  (env ρ η σ,env ρ′η′σ′) ∈ ⦇Ψ⦈ for all (η,η′) ∈ ⦇Δ⦈ and (ρ,ρ′) ∈ ⦇Γ⦈
Δ ⊧ θ : Δ′  ⟺  Δ ⊧ θ ≡ θ : Δ′
Δ ⊧ θ ≡ θ′: Δ′  ⟺  (Env η θ,Env η′θ′) ∈ ⦇Δ′⦈ for all (η,η′) ∈ ⦇Δ⦈

Theorem 12 (Fundamental theorem) If Δ;Γ ⊢ J then Δ;Γ ⊧ J. Proof. Simultaneously by induction on the derivations. □

From the model, it is now easy to derive decidability of equality. Lemma 13 (Identity environments) (↑^{0},↑^{0}) ∈ ⦇Γ⦈ and (⇑^{0},⇑^{0}) ∈ ⦇Δ⦈. Theorem 14 (Completeness of algorithmic equality)

1. If Δ;Γ ⊢ E = E′: F then whnf [↑^{0}][[⇑^{0}]]E ∼^{w} whnf [↑^{0}][[⇑^{0}]]E′.

2. If Δ;Γ ⊢ σ = σ′: Ψ then env ↑^{0} ⇑^{0} σ ∼^{r} env ↑^{0} ⇑^{0} σ′.

Proof. By Lemma 13 and the fundamental theorem we have (whnf [↑^{0}][[⇑^{0}]]E,whnf [↑^{0}][[⇑^{0}]]E′) ∈ ⦇F ⦈, which by Lemma 11 entails whnf [↑^{0}][[⇑^{0}]]E ∼^{w} whnf [↑^{0}][[⇑^{0}]]E′. Similarly env ↑^{0} ⇑^{0} σ ∼^{r} env ↑^{0} ⇑^{0} σ′.

□

Lemma 15 (Termination) If W ∼^{w} W and W′ ∼^{w} W′then the query W ∼^{w} W′terminates.

Theorem 16 (Decidability of equality) If Δ;Γ ⊢ E,E′: F then Δ;Γ ⊢ E ≡ E′: F iff whnf [↑^{0}][[⇑^{0}]]E ∼^{w} whnf [↑^{0}][[⇑^{0}]]E′.

Proof. By a combination of Theorem 12 and Lemma 15 we know that the algorithmic equality test terminates. If E,E′ are definitionally equal, then the algorithmic equality terminates successfully by Theorem 14. The opposite direction follows by soundness (Theorem 6). □