This is a preprint of a paper to be given at the Normalization by Evaluation Workshop (NBE’98) in Aarhus, Denmark.

Normalization and Functor Categories^{∗}

John C. Reynolds

School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA john.reynolds@cs.cmu.edu

May 9, 1998

Abstract

There is a functor-category model of the simply typed lambda calculus such that the long β-η-normal form of any expression can be obtained from its meaning.

Let Θ be the set Θ ::= ι | Θ → Θ of types of the simply typed lambda calculus (with a single primitive type ι). Let V be the set of variables. Then we define Σ to be the category of type assignments and type-preserving variable maps:

Ob Σ = { π | π ^{∈} F → Θ for some F ⊆^{fin} V }
π ⟶_{Σ} π′ = { ϕ | ϕ ^{∈} dom π → dom π′ and π = ϕ; π′ },

with composition and identities inherited from SET.

It is well known that the functor category SET^{Σ} is Cartesian closed (actually, for any category Σ). The exponentiation of two functors F, G from Σ to SET is the functor F ⇒ G whose action on objects of Σ is

(F ⇒ G)π = Hom_{Σ} π × F ⟶_{SET^{Σ}} G,

where Hom_{Σ} ^{∈} Σ^{op} → (Σ → SET) is the Curried hom-functor for the category Σ. Thus, if η ^{∈} (F ⇒ G)π then ηπ′ ^{∈} (π ⟶_{Σ} π′) × F π′ → Gπ′. The action of F ⇒ G on morphisms of Σ is

(F ⇒ G)(ϕ ^{∈} π ⟶_{Σ} π′)(η ^{∈} (F ⇒ G)π)π′′⟨ϕ′ ^{∈} π′ ⟶_{Σ} π′′, a ^{∈} F π′′⟩ = ηπ′′⟨ϕ; ϕ′, a⟩.

∗This research was sponsored in part by National Science Foundation Grant CCR-9804014.

The fact that SET^{Σ} is Cartesian closed leads directly to a semantics for the simply typed lambda calculus. Types denote functors from Σ to SET, and the type constructor → is interpreted by ⇒:

[[θ → θ′]] = [[θ]] ⇒ [[θ′]].

Type assignments denote functors defined by products in SET^{Σ}

[[π]] = \begin{matrix}∏ & ^{SET^{Σ}} \\ v^{∈}dom π \end{matrix}[[πv]].

Since these products are defined pointwise, we have

\begin{aligned}[[π]]π′(v ^{∈} dom π) & = & [[πv]]π′ \\ [[π]](ϕ ^{∈} π′ ⟶_{Σ} π′′)(η ^{∈} [[π]]π′)(v ^{∈} dom π) & = & [[πv]]ϕ(ηv). \end{aligned}

When an expression e satisfies the typing judgement π ⊢ e : θ, its meaning [[e]]_{πθ} is a natural transformation from [[π]] to [[θ]]. These natural transformations satisfy the following semantic equations:

\begin{aligned}[[v]]_{π,πv}π′η & = & ηv \\ [[e e′]]_{πθ′}π′η & = & [[e]]_{π,θ→θ′}π′ηπ′⟨I_{π′}^{Σ}, [[e′]]_{πθ}π′η⟩ \\ [[λv. e]]_{π,θ→θ′}π′ηπ′′⟨ϕ ^{∈} π′ ⟶_{Σ} π′′, a ^{∈} [[θ]]π′′⟩ & = & [[e]]_{[π|v:θ],θ′}π′′[ [[π]]ϕη | v: a]. \end{aligned}

Here I_{π′}^{Σ} is the identity morphism on π′ in Σ, and [ f | v: a] denotes the function with domain dom f ∪ {v} that maps v into a and all other arguments w into fw.

To complete our semantics, we need only define the functor [[ι]] that gives meaning to the primitive type ι. Before doing so, however, we must digress to define some sets of expressions in the simply typed lambda calculus.

To avoid confusing expressions of the lambda calculus with metalinguistic abstractions and applications, we write appl for the function that maps expressions e and e′ into the application e e′, and abstr for the function that maps a variable v and an expression e into the abstraction λv. e. Then we define M and N to be the least families of sets of expressions, each indexed by a type assignment π and a type θ, such that

M_{πθ} = { v | v ^{∈} dom π and πv = θ } ∪ { appl(e, e′) | e ^{∈} M_{π,θ̂→θ} and e′ ^{∈} N_{πθ̂} }
N_{πι} = M_{πι}
N_{π,θ→θ′} = { abstr(v, e) | v = new(dom π) and e ^{∈} N_{[π|v:θ],θ′} }.

Here new(dom π) is the first variable not belonging to dom π, in some standard ordering of the variables in V. It is easy to see that N_{πθ} is the set of long β-η-normal forms e that satisfy the typing π ⊢ e : θ. (The use of new imposes a canonical choice of a single normal form in each equivalence class under α-conversion.)

Each type-preserving variable map ϕ ^{∈} π ⟶_{Σ} π′ induces a substitution −/ϕ that maps each e ^{∈} M_{πθ} into e/ϕ ^{∈} M_{π′θ} and each e ^{∈} N_{πθ} into e/ϕ ^{∈} N_{π′θ}:

v/ϕ = ϕv
(appl(e, e′))/ϕ = appl(e/ϕ, e′/ϕ)
(abstr(v, e))/ϕ = abstr(v′, e/[ ϕ | v: v′]),

where v′ = new(dom π′).

It is easy to see that e/(ϕ; ϕ′) = (e/ϕ)/ϕ′ and e/I_{π}^{Σ} = e. Thus we may complete our semantics by defining the functor [[ι]]:

[[ι]]π = N_{πι} [[ι]](ϕ ^{∈} π ⟶_{Σ} π′)(e ^{∈} N_{πι}) = e/ϕ.

Next we define two families of transfer functions between sets of expressions and sets obtained from the meanings of types:

τ_{πθ} ^{∈} M_{πθ} → [[θ]]π μ_{πθ} ^{∈} [[θ]]π → N_{πθ},

by

τ_{πι}e = e
τ_{π,θ→θ′}(e ^{∈} M_{π,θ→θ′})π′⟨ϕ ^{∈} π ⟶_{Σ} π′, a ^{∈} [[θ]]π′⟩ = τ_{π′θ′}(appl(e/ϕ, μ_{π′θ}a))
μ_{πι}e = e
μ_{π,θ→θ′}(p ^{∈} [[θ]]π ⇒ [[θ′]]π) = abstr(v, μ_{π′θ′}(pπ′⟨J, τ_{π′θ}v⟩)),

where v = new(dom π), π′ = [ π | v: θ], and J ^{∈} π ⟶_{Σ} π′ is the identity injection from dom π to dom π′.

By induction on the structure of the type θ, one can show

Proposition 1 If ϕ ^{∈} π ⟶_{Σ} π′ then

[figure: M_{πθ}; M_{π′θ}; [[θ]]π; [[θ]]π′; τ_{πθ}; τ_{π′θ}; −/ϕ; [[θ]]ϕ]

commutes in SET.

Now suppose we define the environment

η̂_{π} = λv ^{∈} dom π. τ_{π,πv}v ^{∈} [[π]]π.

From the above proposition (taking ϕ to be J), and the action of [[π]] on morphisms of Σ, one can show

η̂_{π′} = [ [[π]]Jη̂_{π} | v: τ_{π′θ}v],

where v = new(dom π), π′ = [ π | v: θ], and J ^{∈} π ⟶_{Σ} π′ is the identity injection from dom π to dom π′.

Finally, by simultaneous induction on the structure of the expression e, we obtain Proposition 2

1. If e ^{∈} M_{πθ} then [[e]]_{πθ}πη̂_{π} = τ_{πθ}e.

2. If e ^{∈} N_{πθ} then μ_{πθ}([[e]]_{πθ}πη̂_{π}) = e. Then, since an expression has the same meaning as its normal form, the second part of this proposition gives

Proposition 3 If π ⊢ e : θ then μ_{πθ}([[e]]_{πθ}πη̂_{π}) is the long β-η-normal form of e.