Strong Normalization for the Calculus of Constructions Chris Casinghino December 2010

2025-05-03 0 0 510.65KB 39 页 10玖币

侵权投诉

Strong Normalization for the Calculus of Constructions

Chris Casinghino

December 2010

1 Introduction

The calculus of constructions (CC) is a core theory for dependently typed programming and

higher-order constructive logic. Originally introduced in Coquand’s 1985 thesis [4], CC has

inspired 25 years of research in programming languages and type theory. Today, extensions

of CC form the basis of languages like Coq [17] and Agda [15, 16].

The popularity of CC can be attributed to the combination of its expressiveness and its

pleasant metatheoretic properties. Among these properties, one of the most important is

strong normalization, which means that there are no inﬁnite reduction sequences from well-

typed expressions. This result has two important consequences. First, it implies that CC

is consistent as a logic. This makes it an attractive target for the formalization of math-

ematics. Second, it implies that there is an algorithm to check whether two expressions

are β-convertible. Thus, type checking is decidable and CC provides a practical basis for

programming languages.

The strong normalization theorem has traditionally been considered diﬃcult to prove [5, 2].

Coquand’s original proof was found to have at least two errors, but a number of later papers

give diﬀerent, correct proofs [5]. In subsequent years, many authors considered how to extend

this result for additional programming constructs like inductive datatypes with recursion, a

predicative hierarchy of universes, and large eliminations [18, 9, 11]. Many of these proofs

are even more challenging, and several span entire theses.

This document reviews three proofs of strong normalization for CC. Each paper we have

chosen proves the theorem by constructing a model of the system in a diﬀerent domain,

and each contributes something novel to the theory of CC and its extensions. The technical

details of the models are often complicated and intimidating. Rather than comprehensively

verifying and reproducing the proofs, we have focused on painting a clear picture of the

beautiful and fascinating mathematical structures that underpin them.

The ﬁrst proof, originally presented by Geuvers and Nederhof [8] and subsequently popu-

larized by Barendregt [3], models CC in the simpler theory of Fω. It demonstrates that the

strong normalization theorems for CC and Fωare equivalent by giving a reduction-preserving

arXiv:2210.11240v1 [cs.PL] 7 Oct 2022

translation from the former to the latter. The second, by Geuvers [7], models CC’s types with

sets of expressions. The paper demonstrates how the model may be extended to cope with

several popular language features, aiming for ﬂexibility. The last proof, from Melli`es and

Werner [13], uses realizability semantics to consider a large class of type theories, known as

the pure type systems, which include CC. The authors’ goal is to prove strong normalization

for any pure type system that enjoys a particular kind of realizability model.

Though each paper has a unique focus and models CC in a diﬀerent semantic system, the

overall structures are very similar. After unifying the syntax, the correspondences between

certain parts of the proofs are quite striking. Readers are encouraged, for example, to

compare the interpretation functions deﬁned in Sections 6.2 and 6.3 with those in Section 5.2.

The similarities between the papers speak to the fundamental underlying structure of CC,

while their diﬀerences illustrate how design choices can push the proof towards varying goals.

The paper is structured as follows: In Sections 2 and 3 we review the deﬁnition and basic

metatheory of pure type systems and the calculus of constructions. We present the high-level

structure of a strong normalization argument in Section 4, then the proofs of Geuvers and

Nederhof [8], Geuvers [7] and Melli`es and Werner [13] in Sections 5, 6 and 7, respectively.

We compare the proofs and conclude in Section 8.

2 Pure Type Systems

The calculus of constructions is one example of a pure type system (PTS). This very general

notion, introduced by Berardi and popularized by Barendregt [3], consists of a parameterized

lambda calculus which can be instantiated to a variety of well-known type systems. For

example, the simply-typed lambda calculus, System F, System Fωand CC are all pure type

systems. The PTS generalization is convenient because it allows us to simultaneously study

the properties of several systems.

A PTS is speciﬁed by three parameters. First, the collection of sorts sis given by a set S.

The typing hierarchy among these sorts is given by a collection of axioms A⊆S2. Finally,

the way product types may be formed is speciﬁed by the set of rules R⊆S3. Figure 1 gives

the complete deﬁnition of the system.

Choosing to explain CC as a PTS settles several questions of presentation. The terms, types

and kinds are collapsed into one grammar. Some authors choose to separate these levels

syntactically for easier identiﬁcation, but we ﬁnd this version more economical and it is

more closely aligned with the three papers under consideration. For the same reasons, we

have used β-conversion in the Conv rule instead of using a separate judgemental equality

(as is done, for example, in [2]). Here, =βis the symmetric, transitive, reﬂexive closure of

;. We do not consider η-conversion.

This context also permits a clean and compartmentalized explanation of CC’s features. In

A, B, a, b ::= s|x|(x:A)→B|λx:A.b|a b

Γ ::= · | Γ,x:A

a;b

(λx:A.b)a;[a/x]bSBeta

A;A0

(x:A)→B;(x:A0)→BSPi1

A;A0

λx:A.b;λx:A0.bSLam1

a;a0

a b ;a0bSApp1

B;B0

(x:A)→B;(x:A)→B0SPi2

b;b0

λx:A.b;λx:A.b0SLam2

b;b0

a b ;a b0SApp2

a;∗b

a;∗aMSRefl

a1;a2

a2;∗a3

a1;∗a3

MSStep

Γ`a:A

`Γ

(s1,s2)∈ A

Γ`s1:s2

TSort

`Γ

(x:A)∈Γ

Γ`x:ATVar

Γ`a:AΓ`B:s

A=βB

Γ`a:BTConv

Γ`A:s1

Γ,x:A`B:s2

(s1,s2,s3)∈ R

Γ`(x:A)→B:s3

TPi

Γ`(x:A)→B:s

Γ,x:A`b:B

Γ`λx:A.b: (x:A)→BTLam

Γ`a: (x:A)→B

Γ`b:A

Γ`a b : [b/x]BTApp

`Γ

` · CNil

x/∈dom(Γ)

Γ`A:s

`Γ,x:ACCons

Figure 1: Deﬁnition of Pure Type Systems

most of the systems we consider, the sorts and axioms are given by the sets:

S={∗,2} A ={(∗,2)}

Intuitively, ∗classiﬁes types and 2classiﬁes kinds. The lone axiom says that ∗is itself a

kind. The rule (∗,∗,∗) permits standard function types, whose domain and codomain are

both types. The system with only this rule is the simply-typed lambda calculus:

R={(∗,∗,∗)}

The rule (2,∗,∗) permits functions whose domain is a kind. For example, when the domain

is ∗these are functions which takes types as arguments (i.e., polymorphism). Thus, adding

this rule yields System F:

R={(∗,∗,∗),(2,∗,∗)}

The rule (2,2,2) eﬀectively duplicates STLC at the type level. It allows functions that

take and return types. Adding it yields System Fω, which has type-level computation:

R={(∗,∗,∗),(2,∗,∗),(2,2,2)}

CC adds dependent types to System Fω. The rule (∗,2,2) permits types to depend on terms

by allowing functions which take terms as arguments but return types. Thus, the complete

speciﬁcation of CC is:

S={∗,2} A ={(∗,2)} R ={(∗,∗,∗),(2,∗,∗),(2,2,2),(∗,2,2)}

3 Simple Metatheory

For completeness, we review a few basic metatheoretic results. We will write Γ `a:Afor

the typing judgement of an arbitrary PTS or when it is clear what system we are discussing,

and otherwise will label the turnstile as in Γ `CC a:Afor CC’s typing relation in particular.

The ﬁrst result, conﬂuence, can be proven using the standard Tait–Martin-L¨of technique [12,

11].

Theorem 3.1 (Conﬂuence).If a;∗a1and a;∗a2then there is a bsuch that a1;∗b

and a2;∗b.

The second property, preservation, is proved by induction on typing derivations, using a

substitution lemma.

Theorem 3.2 (Preservation).If Γ `a:Aand a;bthen Γ `b:A.

The last property is not usually considered for less expressive lambda calculi because they

are presented with separate syntax for terms, types and kinds. The theorem says that CC

expressions can still be classiﬁed in this way with the typing judgement. It is proved by a

straightforward induction on typing derivations.

Theorem 3.3 (Classiﬁcation).If Γ `CC A:B, then exactly one of the following holds:

•Bis 2. In this case, we call Aakind.

•Γ`CC B:2. In this case, we call Aa Γ-constructor.

•Γ`CC B:∗. In this case, we call Aa Γ-term.

When Bis ∗, we will call Aa Γ-type. This is a special case of the second bullet above. In

this document we use the word “expression” to refer to any element of CC’s grammar and

reserve the word “term” for the subclass of expressions identiﬁed here.

Notice that we need a context to distinguish between constructors and terms, but can identify

kinds without one. The ambiguity comes from variables, and some authors avoid it by

splitting them into two syntactic classes (typically x, y, z for term variables and α, β for type

variables). Distinguishing the variables in this way forces duplication or subtle inaccuracy

when discussing binders at diﬀerent levels. For that reason, we prefer to mix the variables

and use a context to identify the terms and constructors.

Finally, we deﬁne the central notion considered below:

Deﬁnition 3.4. An expression is called strongly normalizing if there are no inﬁnite ;

reduction sequences beginning at it. We write SN for the collection of all such expressions.

4 Structure of the proofs

The three proofs we consider each model CC in a diﬀerent domain, but they share a similar

overall structure. In this section we describe the technique at a high level.

Step 1: Deﬁne the interpretations

Each proof begins by deﬁning two interpretations. A “type” interpretation, usually written

JAK, captures the static meaning of types, kinds and sorts. For example, in the second proof

we will model types as sets of expressions so that JAKcontains all the terms of type A. Then

a “term” interpretation is deﬁned to capture the run-time behavior of terms, types and kinds.

This is usually written [a]. In the example where types are interpreted as sets of expressions,

the term interpretation might pick a canonical inhabitant with the right reduction behavior

from the set.

Step 2: Relate the interpretations

After deﬁning the term and type interpretations, we prove a theorem that relates them. For

example, in the second proof we will show that if Γ `a:A, then [a]∈JAK. This theorem is

usually called “soundness”.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

StrongNormalizationfortheCalculusofConstructionsChrisCasinghinoDecember20101IntroductionThecalculusofconstructions(CC)isacoretheoryfordependentlytypedprogrammingandhigher-orderconstructivelogic.OriginallyintroducedinCoquand's1985thesis[4],CChasinspired25yearsofresearchinprogramminglanguagesandtypeth...

展开>> 收起<<

Strong Normalization for the Calculus of Constructions Chris Casinghino December 2010.pdf

共39页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Strong Normalization for the Calculus of Constructions Chris Casinghino December 2010

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: