Full primitive recursion on monotone inductive types

Ralph Matthes, LMU München Workshop TYPES ’98 in Kloster Irsee

[figure]

Consider an extension of system F by monotone inductive types as follows: Types: type variables, ρ → σ, ρ × σ, ∀αρ and μαρ. Typed terms in natural deduction formulation without contexts:

(V) x^{ρ}

(→-I) (λx^{ρ}r^{σ})^{ρ→σ}
(→-E) (r^{ρ→σ}s^{ρ})^{σ}
(×-I) ⟨r^{ρ}, s^{σ}⟩^{ρ×σ}
(×-E) (r^{ρ×σ}L)^{ρ}, (r^{ρ×σ}R)^{σ}
(∀-I) (Λαr^{ρ})^{∀αρ} under the usual proviso
(∀-E) (r^{∀αρ}σ)^{ρ[α:=σ]}

[figure]

(μ-I) (C_{μαρ}t^{ρ[α:=μαρ]})^{μαρ}
(μ-E) (r^{μαρ}E_{μ}σm^{∀α∀β.(α→β)→ρ→ρ[α:=β]}s^{ρ[α:=σ]→σ})^{σ}
(μ-E^{+}) (r^{μαρ}E_{μ}^{+}σm^{∀α∀β.(α→β)→ρ→ρ[α:=β]}s^{ρ[α:=μαρ×σ]→σ})^{σ}

m is the witness of monotonicity of λαρ. This witness is here used for the elimination rules. (μ-E) provides for iteration, (μ-E^{+}) gives (full) primitive recursion:

(β_{μ}) (C_{μαρ}t)E_{μ}σms ↦ s(m(μαρ)σ(λx^{μαρ}.xE_{μ}σms)t)
(β_{μ}^{+}) (C_{μαρ}t)E_{μ}^{+}σms ↦

s(m(μαρ)(μαρ × σ)(λx^{μαρ}.⟨x, (λx^{μαρ}.xE_{μ}^{+}σms)x⟩)t)

Theorem: β-reduction is strongly normalizing (incl. β_{→}, β_{×}, β_{∀}).

[figure]

Proof method: reduction-preserving embedding into an extension of Mendler’s LICS ’87 system: Types as before (× not needed), (μ-I) as before.

(μ-E) (r^{μαρ}E_{μ}σs^{∀α.(α→σ)→ρ→σ})^{σ}
(μ-E^{+}) (r^{μαρ}E_{μ}^{+}σs^{∀α.(α→μαρ)→(α→σ)→ρ→σ})^{σ}

The corresponding β-reduction rules:

\begin{matrix}(β_{μ}) & (C_{μαρ}t)E_{μ}σs ↦ & s(μαρ)(λx^{μαρ}.xE_{μ}σs)t \\ (β_{μ}^{+}) & (C_{μαρ}t)E_{μ}^{+}σs ↦ & s(μαρ)(λy^{μαρ}y)(λx^{μαρ}.xE_{μ}^{+}σs)t \end{matrix}

Essential difference to Mendler: No restriction on forming μαρ. Mendler required α to occur only (not necessarily strictly) positively in ρ and based his normalization proof on this assumption.

The reduction-preserving embedding −′ of monotone inductive types into this system: The types are preserved and the terms are translated homomorphically except for the elimination rules.

(μ-E) (r^{μαρ}E_{μ}σms)′ := r′E_{μ}σŝ with
ŝ:= Λαλz^{α→σ}λy^{ρ}.s′(m′ασzy)
(μ-E^{+}) (r^{μαρ}E_{μ}^{+}σms)′ := r′E_{μ}^{+}σŝ with ŝ:=

Λαλz_{1}^{α→μαρ}λz_{2}^{α→σ}λy^{ρ}.s′(m′α(μαρ × σ)(λx^{α}⟨z_{1}x, z_{2}x⟩)y)

This preserves β-reduction: easy calculation.

Theorem: This variant of Mendler’s system is strongly normalizing. Proof: First eliminate iteration by an easy embedding into the system without (μ-E) and (β_{μ}): Simply set (r^{μαρ}E_{μ}σs)′ := r′E_{μ}^{+}σŝ with ŝ:= Λαλz^{α→μαρ}.s′α and everything else homomorphic. (In fact Mendler did not include (μ-E).) Second step: Show strong normalization by extending a suitable proof of strong normalization for system F. Essential tool: vector notation for multiple eliminations. Define rs⃗ for s⃗ being a list of terms, types, symbols L and R. An example: r^{μαρ}s^{∀α.(α→μαρ)→(α→σ_{1}→(σ_{2}×σ_{3}))→ρ→σ_{1}→(σ_{2}×σ_{3})}t^{σ_{1}}R shall denote a term of type σ_{3}.

[figure]

(Lemma on head form) Every term has exactly one of the following forms:

(V) x^{ρ}s⃗
(→-I) λx^{ρ}r

(→-R) (λx^{ρ}r)ss⃗

(×-I) ⟨r, s⟩

(×-R) ⟨r, s⟩Ls⃗, ⟨r, s⟩Rs⃗

(∀-I) Λαr

(∀-R) (Λαr)σs⃗

(μ-I) C_{μαρ}t

(μ-R) (C_{μαρ}t)E_{μ}^{+}σss⃗

[figure]

Definition of the set SN of terms by (strictly positive) induction:

(V) If x^{ρ}s⃗ is a term and the terms in s⃗ are in SN, then

x^{ρ}s⃗ ∈ SN. (→-I) If r ∈ SN, then λx^{ρ}r ∈ SN. (β_{→}) If (λx^{ρ}r)ss⃗ is a term, s ∈ SN and r[x^{ρ} := s]s⃗ ∈ SN, then

(λx^{ρ}r)ss⃗ ∈ SN. (×-I) If r ∈ SN and s ∈ SN, then ⟨r, s⟩ ∈ SN. (β_{×}) If rs⃗ ∈ SN and s ∈ SN, then ⟨r, s⟩Ls⃗ ∈ SN.

If ss⃗ ∈ SN and r ∈ SN, then ⟨r, s⟩Rs⃗ ∈ SN.

[figure]

(∀-I) If Λαr is a term and r ∈ SN, then Λαr ∈ SN. (β_{∀}) If (Λαr)σs⃗ is a term and r[α := σ]s⃗ ∈ SN, then

(Λαr)σs⃗ ∈ SN.

(μ-I) If C_{μαρ}t is a term and t ∈ SN, then C_{μαρ}t ∈ SN.

(β_{μ}^{+}) If s(μαρ)(λy^{μαρ}y)(λx^{μαρ}.xE_{μ}^{+}σs)ts⃗ ∈ SN, x^{μαρ} ∉ FV(s)

and (C_{μαρ}t)E_{μ}^{+}σss⃗ is a term, then (C_{μαρ}t)E_{μ}^{+}σss⃗ ∈ SN.

Lemma: SN is the set of strongly normalizing terms. (The set sn of strongly normalizing terms is defined by (strictly positive) induction via

If for every term r′ with r → r′ we have r′ ∈ sn, then r ∈ sn. Hence, sn is simply the accessible part of →.)

[figure]

Definition of τ-saturated sets. Let M be a set of terms. M is τ-saturated, if the following holds

(SN) If r ∈ M, then r ∈ SN_{τ}.

(V) If x^{ρ}s⃗ is a term of type τ and the terms in s⃗ are in SN, then x^{ρ}s⃗ ∈ M.

(β_{→}) If (λx^{ρ}r)ss⃗ is a term, s ∈ SN and r[x^{ρ} := s]s⃗ ∈ M, then (λx^{ρ}r)ss⃗ ∈ M.

(β_{×}) If rs⃗ ∈ M and s ∈ SN, then ⟨r, s⟩Ls⃗ ∈ M. If ss⃗ ∈ M and r ∈ SN, then ⟨r, s⟩Rs⃗ ∈ M.

(β_{∀}) If (Λαr)σs⃗ is a term and r[α := σ]s⃗ ∈ M, then (Λαr)σs⃗ ∈ M and

[figure]

(β_{μ}^{+}) If s(μαρ)(λy^{μαρ}y)(λx^{μαρ}.xE_{μ}^{+}σs)ts⃗ ∈ M, x^{μαρ} ∉ FV(s) and (C_{μαρ}t)E_{μ}^{+}σss⃗ is a term, then (C_{μαρ}t)E_{μ}^{+}σss⃗ ∈ M.

Trivially, SN_{τ} (the terms of type τ in SN) is τ-saturated. Let M be a set of terms. Let cl_{τ} (M) be the least τ-saturated set containing M ∩ SN_{τ}. (Definable by strictly positive induction) By means of saturated sets we define predicates of strong computability with respect to an assignment of saturated sets for type variables (a candidate assignment) and finally show that every term is strongly computable under substitution. This works if there are constructions for saturated sets corresponding to the type constructs of the system for which the introduction rules and the elimination rules are sound. For →, × and ∀ this is standard. It will be sketched for μ.

[figure]

Fix λαρ. Let Φ := (Φ_{τ})_{τ} be a family of mappings Φ_{τ} : SAT_{τ} → SAT_{ρ[α:=τ]}. Define for M ∈ SAT_{μαρ} M_{I}(M) := {r ∈ Λ_{μαρ}|∃t ∈ Φ_{μαρ}(M).r = C_{μαρ}t} M_{E}(M) := {r ∈ Λ_{μαρ}|∀σ∀N ∈ SAT_{σ}

∀s ∈ ∀P.(P → M) → (P → N) → Φ(P) → N .rs ∈ N }

and Ψ_{I} : SAT_{μαρ} → SAT_{μαρ} by setting

Ψ_{I}(M) := cl_{μαρ}(M_{I}(M))

and μ_{E}(Φ) := any fixed-point of Ψ_{E} : SAT_{μαρ} → SAT_{μαρ}, defined by

Ψ_{E}(M) := cl_{μαρ}(M_{E}(M)).

Because Ψ_{E} is monotone (it is even non-strictly positive) and SAT_{μαρ} is a complete lattice, such a fixed-point exists. Hence, μ_{E}(Φ) is μαρ-saturated.

[figure]

Lemma 1: M_{E}(M) ∩ SN ∈ SAT (which implies Ψ_{E}(M) = M_{E}(M) ∩ SN). Lemma 2: M_{I}(M) ⊆ SN (which implies Ψ_{I}(M) ⊇ M_{I}(M)). Lemma 3: A μαρ-saturated set M is a pre-fixed-point of Ψ_{I} iff for all t ∈ Φ_{μαρ}(M), we have that C_{μαρ}t ∈ M. A μαρ-saturated set M is a post-fixed-point of Ψ_{E} iff for all r ∈ M, types σ, N ∈ SAT_{σ} and s ∈ ∀P.(P → M) → (P → N) → Φ(P) → N, we have rE_{μ}^{+}σs ∈ N. Theorem: μ_{E}(Φ) is a pre-fixed-point of Ψ_{I} (i.e. Ψ_{I}(μ_{E}(Φ)) ⊆ μ_{E}(Φ)). We therefore have the required rules for calculating with μ_{E}(Φ):

(μ-I) If t ∈ Φ_{μαρ}(μ_{E}(Φ)), then C_{μαρ}t ∈ μ_{E}(Φ).
(μ-E^{+}) If r ∈ μ_{E}(Φ), σ type, N ∈ SAT_{σ} and

s ∈ ∀P.(P → μ_{E}(Φ)) → (P → N) → Φ(P) → N, then

rE_{μ}^{+}σs ∈ N.

[figure]

We thus get a direct proof of strong normalization of the system à la Mendler without iteration. Analysis of the proof gives even more: We only used “any fixed-point of Ψ_{E}” and Ψ_{E} is (non-strictly) positive and does not apply Φ to its argument. It is now easy to define a term rewrite system of non-interleaving positive fixed-point types with some appropriate notion of β-reduction into which our variant of Mendler’s system may be embedded in a reduction preserving way. The clauses for the definition of the embedding on terms may be simply read off the proofs of the above lemmas and the theorem by using modified realizability. The proof of strong normalization for this system of fixed-points goes along the same lines as before but is much more perspicuous. The new proof only allows for the trivial embedding in itself being read off. Hence, the direct proof is faithful to it in the sense of only reflecting the concepts modelled by the system.

[figure]

Other results:

• There is also a direct proof of strong normalization for the system of monotone inductive types (following an idea of Thorsten Altenkirch written down in an ASCII note in 1993).

• Also corecursion (present in Mendler’s original system) embeds into non-interleaving fixed-point types.

• Mendler’s system embeds into non-interleaving strictly positive types including the second-order existential quantifier.

• One may define a system of monotone inductive types by requiring the monotonicity witness to appear in the introduction rule. This system embeds into some “dual” of Mendler’s system and in turn embeds into non-interleaving positive inductive types.

[figure]

• One may also require only special instances of the monotonicity witness leading to seemingly stronger systems (but being reduction equivalent because there is also an embedding of positive inductive types into monotone inductive types).

• Of course, the iterative versions of all of the systems readily embed into system F.

• Embedding non-interleaving fixed-point types into positive inductive types is possible after adding some η-rules. The interleaving of fixed-point types calls for permutative conversions for μ in order to embed them into systems of inductive types. Establishing strong normalization of this extended system is one of my major goals in the next future.

Finis