An algebraic view on recursive types

Michael Marz^{∗}

Fachbereich Mathematik Technische Hochschule Darmstadt, Germany May 29, 1996

This is a revised version of Preprint-Nr. 1793 from November 1995.

Introduction

Relatively few λ-terms can be assigned a type in the simple type hierarchy. As is well known, more terms can be typed if recursive types are admitted [Gun92]. In this note a similar extension to simple types is examined.

Our approach is essentially algebraic. We start from the observation that the set of simple types is a totally free algebra with respect to the binary operation →, i.e. a free groupoid. More general groupoids arise as factor structures of free groupoids, so we are lead to discuss free groupoids with a congruence relation. We call these type systems.

Not every type system behaves well with respect to reduction; the crucial subject reduction property may fail. We give a necessary and sufficient condition on type systems, called condition (K), which guarantees subject reduction.

Restricting to finitely many atomic types and finitely generated congruences we can effectively present a type system. Our first result says that it is decidable whether a such presented type system is a K-type system, i.e. whether it satisfies condition (K). Next we show that finitely presented K-type system can always be presented in a particular fashion, namely, by specifying a map from atomic types to type expressions. In other words, the congruence for finitely presented K-type systems is always generated by a list of constraints ι_{1} ∼ τ_{1}, ι_{2} ∼ τ_{2}, …, ι_{n} ∼ τ_{n} where ι_{1}, …, ι_{n} are atomic.

The next question is whether λ-terms typeable in a K-type system are strongly normalizing. This is not always the case. N. Mendler shows in [Men91] that it is precisely the so called positive type systems for which strong normalization holds. In Section 2 we show how to read off positivity from a presentation. In particular, it is decidable whether a finitely presented type system is positive.

∗e-mail: marz@mathematik.th-darmstadt.de

We also show that principle typing is possible using K-type systems. This entails that the question whether a given term admits a type in some positive K-type system is decidable. Since the set of strongly normalizing λ-terms is not recursive, it follows that neither a single nor the union of all positive K-type systems will capture strong normalization.

This paper is a translated extract of my diploma thesis, see [Mar95]. I would like to thank Paweł Urzyczyn for some useful hints, Martin Hofmann, Mathias Kegelmann and Hermann Puhlmann for their careful proof reading, and especially Achim Jung for his stimulating supervision.

1 Free groupoids as type systems for the λcalculus

There are two possible ways of thinking about type systems of the λ-calculus. In Church-style each λ-term contains type annotations in λ-abstractions which permit type reconstruction. On the other hand, in Curry-style the types appear as predicates over the set of untyped terms. We are interested in Curry-style.

In this section we consider a general approach to monomorphic type systems, i.e. type systems consisting only of atomic types and function types. In the simply typed λ-calculus the set of all types forms a groupoid freely generated by the atomic types, the groupoid operation being the arrow →. To allow for more terms to be typed, one approach is to consider type constraints. These are sets of equations of the form ι ∼ τ where ι must be atomic and τ can be any type. From an algebraic point of view this leads to the study of free groupoids with arbitrary congruences as type systems. For our purposes it is more suitable to explicitly handle congruences instead of working with quotient groupoids.

Definition 1.1 A type system (\underline{F}, ≈) consists of a free groupoid \underline{F} = (F, →), i.e. an algebra with one binary operation, and a congruence relation ≈.

In the following X denotes a countably infinite set of variables and (\underline{F}, ≈) stands for a type system.

Definition 1.2 A basis is a finite set Γ of expressions (x : τ) with x ∈ X and τ ∈ F such that for each x ∈ X there is at most one τ ∈ F with (x : τ) ∈ Γ. We use Γ, x : τ as an abbreviation for Γ ∪ {(x : τ)} and we write ⊢ t : τ if Γ is empty. An expression Γ ⊢ t : τ is called a judgement if it is derivable with the following rules:

\overline{(Var)} ; Γ ⊢ x : τ if (x : τ) ∈ Γ  Γ ⊢ s : τ →σ Γ ⊢ t : τ ; \overline{(App)} ; Γ ⊢ st : σ

Γ, x : σ ⊢ t : τ ; \overline{(Abs)} ; Γ ⊢ λx.t : σ →τ  Γ ⊢ t : σ ; \overline{(Con)} ; Γ ⊢ t : τ  if σ ≈ τ

Most of the main syntactic properties of the simply typed λ-calculus remain true for type systems as presented here. Notably, we have the following two lemmas which can be proved by induction:

Lemma 1.3 (Generation Lemma) Let Γ be a basis such that Γ ⊢ t : τ is a judgement.

a) If t = x ∈ X, then (x : τ_{1}) ∈ Γ for some τ_{1} with τ_{1} ≈ τ.

b) If t = t_{1}t_{2}, then there is a τ_{1} ∈ F such that Γ ⊢ t_{1} : τ_{1} → τ and Γ ⊢ t_{2} : τ_{1} are judgements.

c) If t = λx.t_{1}, then there are τ_{1}, τ_{2} ∈ F such that τ ≈ τ_{2} →τ_{1} and Γ, x : τ_{2} ⊢ t_{1} : τ_{1} is a judgement.

Lemma 1.4 (Substitution Lemma) Let Γ be a basis such that Γ, x : σ ⊢ t : τ and Γ ⊢ s : σ are judgements for λ-terms s and t. Then Γ ⊢ t[s/x] : τ is also a judgement.

The β-reduction is defined as usual (see e.g. [Bar92]), we write s [figure: β] t if s reduces to t. Unfortunately, the judgements are not always stable under β-reduction.

Definition 1.5 Let (\underline{F}, ≈) be a type system. The λ_{(\underline{F},≈)}-calculus has the β-subject reduction property if, for any judgement Γ ⊢ s : τ and for any reduction s [figure: β] t, the expression Γ ⊢ t : τ is a judgement.

Proposition 1.6 The following are equivalent:

(1) The λ_{(\underline{F},≈)}-calculus has the β-subject reduction property.

(2) The following property holds for every σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F:

(K) σ_{1} → τ_{1} ≈ σ_{2} → τ_{2} ⇒ σ_{1} ≈ σ_{2} and τ_{1} ≈ τ_{2}

Proof: (1) implies (2): Straightforward using the Generation Lemma and the Substitution Lemma.

(2) implies (1): First, we show that σ_{1} → τ_{1} ≈ σ_{2} → τ_{2} implies τ_{1} ≈ τ_{2} (for σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F). For x, y, z ∈ X there is a deduction for y : τ_{1}, z : σ_{2} ⊢ (λx.y)z : τ_{2}. Since we have the β-subject reduction property we get y : τ_{1}, z : σ_{2} ⊢ y : τ_{2}. Hence, τ_{1} ≈ τ_{2} follows from the Generation Lemma.

For the second part, we take again σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F with σ_{1} → τ_{1} ≈ σ_{2} → τ_{2}. Choosing Γ = {u : σ_{1} → τ_{1}, v : σ_{1} → σ_{1}, y : σ_{2}} we can derive Γ ⊢ (λx.u(vx))y : τ_{2}. Since we assume the subject reduction property, Γ ⊢ u(vy) : τ_{2} is also a judgement. Because of the Generation Lemma there is a ψ ∈ F with Γ ⊢ u : ψ → τ_{2} and Γ ⊢ vy : ψ. Again we apply the Generation Lemma, hence, we have σ_{1} → σ_{1} ≈ σ_{2} → ψ.

As shown in the first part this leads to σ_{1} ≈ ψ, thus σ_{1} → σ_{1} ≈ σ_{2} → σ_{1} follows. Because y : σ_{2} ⊢ (λx.x)y : σ_{1} is a judgement we get y : σ_{1} ⊢ y : σ_{2} by the subject reduction property. This leads to σ_{1} ≈ σ_{2}. □

We have shown that (K) is a sufficient and necessary condition for the β-subject reduction property. The idea of this proof is due to R. Statman, see [Sta94], however, the proof as presented here is much shorter.

If we add η-reduction to the system we do not get any problems: the calculus is stable under η-reduction.

Type systems that satisfy (K) are called K-type systems. There are many properties of the untyped λ-calculus that remain true for the λ_{(\underline{F},≈)}-calculus. In case the calculus has a K-type system, we get the Church-Rosser-Theorem as a consequence of the subject reduction property.

As can be easily shown there are no non-trivial finite K-type systems:

Remark 1.7 The number of congruence classes of a K-type system is 1 or infinite.

The type system with the congruence relation F × F induces the untyped λcalculus. Using the free groupoid \underline{F}_{J} with the smallest congruence relation we get the simply typed λ-calculus with J as the set of atomic types.

For a decidability result for K-type systems we need two lemmas:

Lemma 1.8 Let (\underline{F}_{J} , ≈) be a type system that is generated by a symmetric relation ∼. Then (\underline{F}_{J} , ≈) is a K-type system iff the following condition is true:

σ_{1} →τ_{1} ∼ ι_{1} ∼ … ∼ ι_{n} ∼ σ_{2} →τ_{2} implies σ_{1} ≈ σ_{2} and τ_{1} ≈ τ_{2}

for all σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} , n ∈ ℕ_{0}, and ι_{1}, …, ι_{n} ∈ J.

Proof: If σ_{1} → τ_{1} ∼ ι_{1} ∼ … ∼ ι_{n} ∼ σ_{2} → τ_{2} holds for σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} and ι_{1}, …, ι_{n} ∈ J and (\underline{F}_{J} , ≈) is a K-type system then σ_{1} ≈ σ_{2} and τ_{1} ≈ τ_{2} hold as well.

Let σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} be types such that σ_{1} → τ_{1} ≈ σ_{2} → τ_{2}. We have to show σ_{1} ≈ σ_{2} and τ_{1} ≈ τ_{2}. As well known from universal algebra we can get from σ_{1} →τ_{1} to σ_{2} →τ_{2} by replacing occurrences of subtypes δ by δ′ in σ_{1} →τ_{1} with δ ∼ δ′. Thus, we get a sequence σ_{1} → τ_{1} ⇝ φ_{1} ⇝ … ⇝ φ_{n} ⇝ σ_{2} → τ_{2}. Consider subsequences of the form φ_{i} = σ′_{1} → τ′_{1} ⇝ φ_{i+1} = ι_{1} ⇝ … ⇝ φ_{i+k} = ι_{k} ⇝ φ_{i+k+1} = σ′_{2} → τ′_{2} with ι_{1}, …, ι_{k} ∈ J. For k ≥ 1 the condition of the proposition yields σ′_{1} ≈ τ′_{1} and σ′_{2} ≈ τ′_{2}. So we only have to deal with the case k = 0: we must show that σ′_{1} → τ′_{1} ⇝ σ′_{2} → τ′_{2} implies σ′_{1} ≈ σ′_{2} and τ′_{1} ≈ τ′_{2} when σ′_{2} → τ′_{2} is the result of the replacement of one occurrence of a subtype δ as described above. This is clear if δ is a proper subtype of σ′_{1} or τ′_{1}. The case δ = σ′_{1} → τ′_{1} follows from the assumption choosing k = 0. □

Lemma 1.9 For any freely generated groupoid \underline{F} with a finite binary relation ∼ it is decidable whether σ ≈ τ holds for σ, τ ∈ F.

Proof: Let S := {δ ∈ F | ∃δ′ ∈ F : δ ∼ δ′ or δ′ ∼ δ} ∪ {σ, τ} and T be the set of all subtypes of elements of S. The relation ≈′ is defined as the smallest reflexive, symmetric and transitive extension of ∼ that satisfies

σ_{1} ≈′ τ_{1}, σ_{2} ≈′ τ_{2}, σ_{1} →σ_{2}, τ_{1} →τ_{2} ∈ T  ⇒  σ_{1} →σ_{2} ≈′ τ_{1} →τ_{2}

for all σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ T . Since T is finite, so is ≈′. Given σ ≈ τ, there are σ_{0}, σ_{1}, …, σ_{n+1} ∈ F with σ = σ_{0} ≈ σ_{1} ≈ … ≈ σ_{n+1} = τ such that σ_{i+1} can be obtained from σ_{i} (i = 0, …, n) by replacing a subtype δ by some δ′ with δ ∼ δ′ or δ′ ∼ δ. By induction on the sum of the length of the σ_{i} one can be prove σ_{0} ≈′ σ_{n+1} which is left to the reader. This completes the proof because ≈′ is finite. □

Of particular interest are presentations for type systems using a functional relation which maps atomic types to arbitrary ones. In other words, the generating relation is of the form \{ι_{i} ∼ τ_{i} | ι_{i} ∈ J , τ_{i} ∈ F_{J} \}. If a type system (\underline{F}_{J} , ≈) is finitely presented, i.e. J is finite and there is a finite relation ∼ generating ≈, we get the following results as consequences of the two lemmas:

Theorem 1.10 It is decidable whether a finitely presented type system is a K-type system.

Corollary 1.11 Each type system generated by a functional relation is a K-type system.

Proof: Follows from Lemma 1.8 because there are no nontrivial sequences. □

Because of Proposition 1.6, type systems generated functional relation lead to calculi with the subject reduction property. For finitely presented K-type systems, even the converse direction of Corollary 1.11 is true:

Theorem 1.12 Each finitely presented K-type system is generated by a functional relation.

Proof: We sketch an algorithm that takes a finite presentation ∼ of (\underline{F}_{J} , ≈) and gives a functional relation ∼′ on J × F_{J} such that ≈ is the closure of ∼′. Each pair σ_{1} → σ_{2} ∼ τ_{1} → τ_{2} is replaced by σ_{1} ∼ τ_{1} and σ_{2} ∼ τ_{2}. This is done at the very beginning of the algorithm and whenever such a pair occurs. Every two pairs ι ∼ σ and ι ∼ τ with len(σ) ≥ len(τ) are replaced by σ ∼ τ and ι ∼ τ, where len(τ) denotes the number of arrows in τ.

For proving the termination let l denote the maximal length of types related by ∼ and m_{k} := | {τ ∈ F_{J} | len(τ) = k and ∃i = 1, …, n with ι_{i} ∼ τ or τ ∼ ι_{i}}| for k = 2, …, l. One has to verify that the weight (m_{l}, m_{l−1}, …, m_{2}) ∈ ℕ^{l−1} decreases w.r.t. to the lexicographical order during each loop, i.e. while doing one replacement of the second form followed by several ones of the first. Since the lexicographical order is well founded the algorithm terminates. □

2 Strong normalization of λ_{(\underline{F},≈)}-terms

N. Mendler has given a condition characterizing the normalization of a special kind of K-type systems. In this section we generalize this for arbitrary finitely presented Ktype systems by using the results of Section 1. Moreover, we give a graph theoretical characterization for checking this condition. As in Section 1, we consider type systems (\underline{F}_{J} , ≈).

Definition 2.1 Let τ ∈ F be a type. The sets Pos(τ) and Neg(τ) are defined by structural recursion: For atomic types ι ∈ J we set

Pos(ι) = {ι},
Neg(ι) = o /,

and for function types σ →τ:

Pos(σ →τ) = {σ →τ} ∪ Neg(σ) ∪ Pos(τ),
Neg(σ →τ) = Pos(σ) ∪ Neg(τ).

A type σ occurs positively in τ if σ ∈ Pos(τ) and negatively if σ ∈ Neg(τ). A relation ∼ is negative if there are σ, τ ∈ F_{J} with σ ≈ τ such that σ occurs negatively in τ. Otherwise ∼ is positive.

In [Men91], N. Mendler has shown the normalization property for calculi with positive type systems:

Proposition 2.2 Let (\underline{F}_{J} , ≈) be a type system generated by a functional relation ∼ on J × F_{J}. Then the λ_{(\underline{F},≈)}-calculus is strongly normalizing iff ∼ is positive.

Unfortunately, it is not obvious whether an arbitrary relation {ι_{i} ∼ τ_{i} | i ∈ I} on a free groupoid \underline{F}_{J} is positive or not. In order to characterize the positivity of ∼ we consider the type graph of the induced type system.

Definition 2.3 Let (\underline{F}_{J} , ≈) be a type system generated by a functional relation ∼. The generating type graph E_{J}^{∼} of (\underline{F}_{J ,≈}) consists of the set of vertices J ∪ \{τ ∈ F | ∃ι ∈ J: ι ∼ τ} and the edges

• σ ^{−1}^{}τ if σ occurs negatively in τ,

• σ ^{1}^{}τ if σ ≠ τ and σ occurs positively in τ,

• σ ^{}^{1}^{}τ if σ ≠ τ and σ ∼ τ or τ ∼ σ.

(We write σ ^{}^{1}^{}τ for σ [figure: 1; 1] τ.)

Lemma 2.4 Let (\underline{F}_{J} , ≈) be a type system where ≈ is generated by the relation ∼. Then the following are equivalent:

(1) The relation ∼ is positive.

(2) The product of the labels of the edges of every circle

ι_{i_{1}}  ^{x_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{x_{2}}^{}… ^{}^{1}^{}ι_{i_{n}}  ^{x_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

in the generating type graph E_{J}^{∼} of (\underline{F}_{J} , ≈) is even.

Proof: The proof of (1) implies (2) is clear. For the reverse direction let us assume that ∼ is negative. We construct a circle in the generating type graph where the product of the labels is negative. Consider the total type graph G_{J}^{∼} of (\underline{F}_{J ,≈}) which is defined as follows:

• The vertices of G_{J}^{∼} are all the types of F_{J}.

• The labelled edges σ ^{1}^{}τ and σ ^{−1}^{}τ are defined as in the generating type graph.

• σ ^{}^{1}^{}τ is an edge if σ ≠ τ and τ can be obtained by replacing a subtype φ of σ by some ψ with φ ∼ ψ or ψ ∼ φ.

W.l.o.g we assume that no ι_{i} occurs negatively in τ_{i} and τ_{i} ∉ J (for ι_{i} ∼ τ_{i}). We use σ^{k} as an abbreviation for

σ_{k,1} ^{}^{1}^{}σ_{k,2} ^{}^{1}^{}… ^{}^{1}^{}σ_{k,n_{k}}.

If the relation ∼ is negative, there is a circle

K = σ_{1,n_{1}} ^{x_{1}}^{}σ^{2} ^{x_{2}}^{}… ^{x_{m−1}}^{}σ^{m} ^{x_{m}}^{}σ^{1}

such that x_{1} · . . . · x_{m} is negative. We sketch an algorithm that computes a closed path

ι_{i_{1}}  ^{y_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{y_{2}}^{}… ^{}^{1}^{}ι_{i_{n}}  ^{y_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

in the generating type graph E_{J}^{∼} such that x_{1} · . . . · x_{m} = y_{1} · . . . · y_{n} = −1. If there is a path τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ in K with σ′ ∉ J, there are four cases:

• If x = 1 and ι_{i} occurs positively in σ′:

replace τ_{i} ^{}^{1}^{}ι_{i} ^{1}^{}σ ^{}^{1}^{}σ′ by τ_{i} ^{}^{1}^{}ι_{i} ^{1}^{}σ′.

• If x = −1 and ι_{i} occurs negatively in σ′:

replace τ_{i} ^{}^{1}^{}ι_{i} ^{−1}^{}σ ^{}^{1}^{}σ′ by τ_{i} ^{}^{1}^{}ι_{i} ^{−1}^{}σ′.

• If σ′ can be obtained by replacing some τ_{j} by ι_{j} in σ such that for x = 1 the type ι_{i} does not occur positively, for x = −1 it does not occur negatively in σ′: replace τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ by τ_{i} ^{}^{1}^{}ι_{i} ^{y}^{}τ_{j} ^{}^{1}^{}ι_{j} ^{z}^{}σ′. If the occurrence of τ_{j} that has to be replaced is positive then choose y = x and z = 1, otherwise y = −x and z = −1.

• If σ′ can be obtained by replacing ι_{i} by τ_{i} in σ such that ι_{i} is not a subtype of τ_{i}: replace τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ by τ_{i} ^{x}^{}σ′.

If K does not contain any atomic type we have σ_{k,i} = φ_{k,i} →ψ_{k,i} for all k = 1, …, m, i = 1, …, n_{k}. In this case, replace every sequence

σ^{k} ^{x_{k}}^{}φ_{k+1,1}→ψ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}φ_{k+1,n_{k+1}}→ψ_{k+1,n_{k+1}} ^{x_{k+1}}^{}σ^{k+2}

(k = 1, …, m) by

• σ^{k} ^{−x_{k}}^{}φ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}φ_{k+1,n_{k+1}} ^{−x_{k+1}}^{}σ^{k+2}, if σ^{k} is contained in φ_{k+1,k},

• σ^{k} ^{x_{k}}^{}ψ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}ψ_{k+1,n_{k+1}} ^{x_{k+1}}^{}σ^{k+2}, if σ^{k} is contained in ψ_{k+1,k}.

Deleting trivial edges σ ^{}^{1}^{}σ and contracting edges σ_{1} ^{x}^{}σ_{2} ^{y}^{}σ_{3} to σ_{1} ^{x·y}^{}σ_{3} completes the algorithm. During each loop the number of edges σ ^{}^{1}^{}σ′ with σ ∼ / σ′ and σ′ ∼ / σ or the length of types that are related by ^{}^{1}^{}increases, hence, the algorithm terminates. □

As a consequence of Lemma 2.4 we get:

Corollary 2.5 It is decidable whether a finite functional relation is positive.

In the light of Theorem 1.12 and Proposition 2.2, Corollary 2.5 implies:

Theorem 2.6 Let (\underline{F}_{J} , ≈) be a finitely presented K-type system. Then it is decidable whether the λ_{(\underline{F}_{J} ,≈)}-calculus is strongly normalizing.

3 Typeability and principle typing with positive K-type systems

We study the subject of typeability of terms in K-type systems. We call a λ-term t typeable if there is a K-type system such that we can derive a judgement Γ ⊢ t : τ. In [Urz95], P. Urzyczyn has shown that the λ-term \overline{2} \overline{2}K with \overline{2} := λyx.y(yx) and K := λxy.x is not typeable in System F. However, using the positive K-type system (\underline{F}_{J} , ≈) generated by J := \{ι_{1}, ι_{2}\} and ι_{1} ∼ ι_{2} →ι_{1}, there is a deduction for ⊢ \overline{2} \overline{2}K : ι_{1} →ι_{1}. On the other hand, the λ-term λx.xx is easily typeable in System F, but not with a positive K-type system.

As shown in [Wel94], the typeability problem is undecidable in System F. In the following we will show that this is not the case for positive K-type systems.

Definition 3.1 Let (\underline{F}, ≈) and (\underline{F}′, ≈′) be type systems and φ: \underline{F} → \underline{F}′ a groupoid homomorphism (i.e. φ(σ → τ) = φ(σ) → φ(τ)). We call φ: (\underline{F}, ≈) → (\underline{F}′, ≈′) a type system homomorphism if σ ≈ τ implies φ(σ) ≈′ φ(τ).

Let t be a λ-term. A K-type system (\underline{F}, ≈) is called principle K-type system for t if t is typeable in (\underline{F}, ≈) and for every other such type K-type system (\underline{F}′, ≈′) there is a type system homomorphism φ: (\underline{F}, ≈) → (\underline{F}′, ≈′).

Lemma 3.2 Let t be a λ-term and (\underline{F}, ≈) a K-type system such that Γ ⊢ t : σ and Γ ⊢ t : τ are judgements. If Γ contains all (free and bound) variables of t then σ ≈ τ holds.

Proof: By induction on the structure of t. □

Now, we are able to prove the main result of this section:

Theorem 3.3 (Principle Typing Theorem) For each λ-term t exists a principle K-type system.

Proof: We assume that no variable in t occurs freely and bounded or bounded more than once. Given the set {x_{i} | i ∈ I} of all variables contained in t we define J := {ι_{i} | i ∈ I} and Γ := {(x_{i} : ι_{i}) | i ∈ I}. For a subterm s of t, the type σ_{s} is defined by structural recursion:

• If s is a variable with (s : ι) ∈ Γ, then σ_{s} := ι.

• If s is an application s_{1}s_{2}, take a fresh variable κ, define σ_{s} := κ, and let σ_{s_{1}} ∼ σ_{s_{2}}→κ.

• If s is an abstraction λx.s_{1} with (x : ι) ∈ Γ, then σ_{s} := ι→σ_{s_{1}}.

For all subterms s of t, we get judgements Γ ⊢ s : σ_{s} in the type system (\underline{F}_{J ∪L}, ≈) where L is the set of all fresh variables κ used in the definition above and ≈ being the K-closure of ∼ (i.e. the smallest symmetric, transitive extension of ∼ satisfying condition (K)).

Let (\underline{F}′, ≈′) be a K-type system with a basis Γ′ and a type τ ∈ F′ such that Γ′ ⊢′ t : τ is a judgement in this type system. Assume Γ′ to contain every (free or bound) variable in t. We define a map φ_{0} : J → F′ by φ_{0}(ι_{i}) = τ_{i} where {(x_{i} : τ_{i})} ∈ Γ′. This map can be extended to φ: F_{J ∪L} → F′ in the following way:

φ(σ) = \{ \begin{matrix}φ_{0}(σ) & if σ ∈ J \\ τ & if σ = σ_{s_{1}s_{2}} ∈ L for τ ∈ F with Γ′ ⊢′ s_{1}s_{2} : τ \\ φ(σ_{1})→φ(σ_{2}) & if σ = σ_{1} →σ_{2} \end{matrix}

Clearly, φ defines a groupoid homomorphism. For proving that φ is a type system homomorphism it is sufficient to prove that σ ∼ σ′ implies φ(σ) ≈′ φ(σ′).

Let s be a subterm of t and Γ ⊢ s : σ_{s}. It can be shown by induction of the structure of s that Γ′ ⊢′ s : φ(σ_{s}) is a judgement for s in (\underline{F}′, ≈′).

Now assume σ ∼ σ′ for σ, σ′ ∈ F_{J ∪L}. Because of the definition of ∼ there is a subterm s = s_{1}s_{2} of t and a variable κ ∈ L such that σ = σ_{s_{1}}, σ′ = σ_{s_{2}} → κ, and σ_{s} = κ. As shown above, Γ′ ⊢′ s_{1} : φ(σ), Γ′ ⊢′ s_{2} : φ(σ_{s_{2}}), and Γ′ ⊢′ s_{1}s_{2} : φ(κ) are judgements. Because of the Generation Lemma 1.3 there is a ϱ ∈ F′ with Γ′ ⊢′ s_{1} : ϱ → φ(κ) and Γ′ ⊢′ s_{2} : ϱ. By Lemma 3.2 we get φ(σ) ≈′ ϱ → φ(κ) and φ(σ_{s_{2}}) ≈′ ϱ. This implies φ(σ) ≈′ φ(σ_{s_{2}}) → φ(κ) = φ(σ_{s_{2}} → κ) = φ(σ′) which shows that φ is a type system homomorphism. This completes the proof. □

Corollary 3.4 It is decidable whether there is a positive K-type system in which an arbitrary λ-term t is typeable.

Proof: Suppose the principle K-type system (\underline{F}, ≈) for t being negative and let (\underline{F}′, ≈′) be another K-type system in which t is typeable. Since the relation ≈ is negative there are types σ, τ ∈ F with σ ≈ τ such that σ occurs negatively in τ. Because of Theorem 3.3 there is a type system homomorphism φ: (\underline{F}, ≈) → (\underline{F}′, ≈′) with φ(σ) ≈′ φ(τ). The type φ(σ) occurs negatively in φ(τ), thus, the type system (\underline{F}′, ≈′) is negative as well. Since the generating relation ∼ of ≈ satisfies the Kproperty, so does ≈ (this follows from Lemma 1.8 because every pair σ_{1} ∼ σ_{2} contains an atomic type). Moreover, ∼ is finite, thus we can apply Corollary 2.5 and check whether the principle K-type system (\underline{F}, ≈) is positive. □

In this paper we have examined positive type congruences for the λ-calculus. As shown by P. Urzyczyn in [Urz95] these are equivalent to positive recursive types with respect to typeability, i.e. a λ-term is typeable using positive recursive types iff it is typeable in a positive K-type system. In this light we have given a new proof for the decidability of typeability with positive recursive types.

References

[Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118–309. Clarendon Press, 1992.

[Gun92] C. Gunter. Semantics of Programming Languages. Structures and Techniques. Foundations of Computing. MIT Press, 1992.

[Mar95] M. Marz. Monomorphe Typsysteme des λ-Kalküls, Juni 1995. Diplomarbeit, 46pp.

[Men91] N. P. Mendler. Inductive types and type constraints in the second-order lambda-calculus. Annals of Pure and Applied Logic, 51:159–172, 1991.

[Sta94] R. Statman. Recursive types and the subject reduction theorem. Technical Report 94-164, Carnegie Mellon University, March 1994.

[Urz95] P. Urzyczyn. Positive recursive type assignment. Technical Report 95-03(203), Instytut Informatyki, Uniwersytet Warszawski, 1995.

[Wel94] J. B. Wells. Typability and type checking in the second order λ-calculus are equivalent and undecidable. In 9th LICS conference, pages 176–185. IEEE Computer Society Press, 1994.