“A Predicative Strong Normalisation Proof for a λ-Calculus with Interleaving Inductive Types”

Errata and New Ideas

Andreas Abel

April 23, 2004

The aforementioned article appeared in 2000 in Coquand et al., Types for Proofs and Programs (TYPES’99), pp. 21–40, LNCS 1956, Springer-Verlag. I found the following errors:

p. 28 Definition of weak head reduction. The correct definition is:

{t ⊳_{β} u \atop t ⊳_{whd} u}  {t ⊳_{whd} u \atop E[t] ⊳_{whd} E[u]}

p. 28 Lemma 1. Proposition 3

{t ⊳_{whd} t′ E[t′] ∈ SN \atop E[t] ∈ SN}

is wrong. Counterexample: Let Ω be a diverging term, t ≡ (λx.y) Ω and t′ = y. The correct proposition is

{t ⊳_{whd} t′ t, E[t′] ∈ SN \atop E[t] ∈ SN}

Proof by induction on t, E[x] ∈ SN, analysing the reducts of E[t]. Since t has a head redex and cannot be in constructor form, each reduction of E[t] has to take place in E[x] or t. The interesting case is t ⊳_{1} u with u ≢ t′. Then by proposition 1 there exists an u′ such that u ⊳_{whd} u′ and t′ ⊳^{∗} u′. The last fact implies that E[u′] ∈ SN. Hence, we can invoke the induction hypothesis on u ⊳_{whd} u′ and obtain E[u] ∈ SN. □

p. 36 A typo in rule (non-rec) at bottom of page: The superscript to U_{i} in the conclusion must be νX.ρ (instead of μX.ρ).

Addendum

Here is some new ideas on details of the paper.

On the type Fin

An inductive type of the form μX. μY. F (X, Y) is isomorphic to μX. F (X, X). Hence, the type of unlabelled finitely branching (and finite-depth) trees

Fin = μX. μY. 1 + X × Y

is isomorphic to the type of unlabelled binary trees μX.1+X×X. (Implementing arbitrary trees by binary trees is folklore in computer science.)

On empty and unit type

In the presentation of the calculus the empty type 0 with its eliminator case_{0} are explicitely added. In the presence of inductive types, both constants are also definable:

\begin{aligned}0 & ≡ & μX.X \\ case_{0} & ≡ & It^{X.X}(λx^{σ}.x) : 0 → σ \end{aligned}

It holds that

case_{0}(c t) ≡ It(λx.x)(c t) = (λx.x)(It(λx.x)t) = case_{0} t.

In the extended calculus which includes coinductive types the singleton set is definable as well:

\begin{aligned}1 & ≡ & νX.X \\ unit & ≡ & Co^{X.X, 0→0}(λx^{0→0}.x)(λy^{0}.y) : 1 \end{aligned}

We have

d unit ≡ d(Co(λx.x)(λy.y)) = Co(λx.x)((λx.x)(λy.y)) = unit.

On the Interpretation of Coinductive Types

In Section 6.2 we have defined the interpretation of coinductive types eliminationbased as the greatest fixed-point of the destructor-rule. If we define it introduction-based instead, we do not even require the urelement relation U for a predicative definition. The changes are the following:

We first add a new definition.

Let ρ ∈ Ty(X⃗, X) a strictly-positive type, n := |X⃗| and P_{1}, …, P_{n} saturated sets. A term set S is called self-supported w.r.t. ρ and P⃗ if S ∈ SAT and ds ∈ [[ρ]](P⃗ , S) for all terms s ∈ S.

Introducing the notation dS = {ds | s ∈ S} we could also have required dS ⊆ [[ρ]](P⃗ , S). Disregarding the destructor d which comes from the “iso”- formulation of coinductive types we could say that a self-supported set w.r.t. ρ and P⃗ is a post-fixed point of the operator [[ρ]](P⃗ , ).

The name self-supported comes from the notion of support of Pierce [Pie02, p.290] which coincides with our urelement relation U. Using Prop. 1 we can split the post-fixed point condition on S into the two conditions dS ⊆ [[ρ]](P⃗ , SN^{νX.ρ}) and U_{n+1}^{ρ}(dS) ⊆ S, using the generalization U(S) := ⋃_{s∈S} U(s). In Pierce’s terms, the first condition expresses that the support of dS is defined and the second condition expresses that the support of dS is contained in S. Hence we speak, again ignoring the “iso”-issue, of a self-supporting set.

The introduction rule for greatest fixed-point (co-elim, p. 3) states that each post-fixed point is contained in the greatest fixed point. We turn that into a introduction rule for coinductive types:

S self-supported w.r.t. ρ and P⃗ t ∈ S

\overline{(coind)}
t ∈ [[νX.ρ]](P⃗)

Lemma 21 If S is self-supported then S ⊆ [[νX.ρ]](P⃗).

Proof. Immediately by (coind). □

The rule (destr’) is now admissible:

Lemma 22 If t ∈ [[νX.ρ]](P⃗) then dt ∈ [[ρ]](P⃗ , [[νX.ρ]](P⃗)).

Proof. By inversion of the assumption we have that t ∈ S for some selfsupported set S. By definition of self-support, dt ∈ [[ρ]](P⃗ , S). By the previous lemma and monotonicity of [[ρ]] we conclude dt ∈ [[ρ]](P⃗ , [[νX.ρ]](P⃗)). □

The remainder of Section 6 stays unaffected by these changes. But to improve clarity, we should say we prove that a set is self-supported instead of that it is closed under (destr’). This applies to the formulation of the proofs of Prop. 12, Lemma 3 and Prop. 15, but technically, the proofs remain unchanged.

Summarizing, we now handle coinductive types in a predicative meta-theory without coinduction, which simplifies the setting a bit. It shows that the urelement relation U is only required to give a predicative interpretation of inductive types. Note that here a trick similar to using a self-supportive set would not work. We could define inductive types elimination-based, but this would result in the impredicative rule

{∀S ∈ SAT, f ∈ [[σ]](P⃗ , S) ⇒ S. It f t ∈ S \atop t ∈ [[μXσ]](P⃗)}.

How does one check whether t ∈ [[νX.ρ]](P⃗)? How does one construct a selfsupported set S in this case? Pierce gives a semi-algorithm in his book on page 292: Start with the singleton S_{0} = {t} and then enrich it by its support S_{n+1} = S_{n} ∪ U_{n+1}^{ρ}(S_{n}) until it is self-supported. When it becomes inconsistent on the way, i.e., S_{n} ⊆ [[ρ]](P⃗ , SN^{νX.ρ}) does not hold, then t is not in the interpretation of the coinductive type, otherwise, it is. Of course, over infinite domains, this may never terminate. E.g., we could not check whether the stream of all natural numbers is in the semantics.

References

[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.