The relationship between stratified $\lambda$-calculus and usual type theories

In the previous section, we introduced the term constructions and axioms of a stratified $\lambda$-calculus without motivation in terms of more familiar mathematical approaches. In this section, we will describe a motivation for this system and indicate its relationship with more familiar type systems.

Stratified $\lambda$-calculus is not a type system at all in the usual sense. Terms in stratified $\lambda$-calculus do not have types. The scheme of relative types serves only to restrict what $\lambda$-terms (functions) can be defined. For example, the term x(x), which would not make sense in a typed system, is meaningful in stratified $\lambda$-calculus, but the term $(\lambda x.x(x))$ is not.

Although stratified $\lambda$-calculus is an untyped system itself, it has a close relationship with a typed system, consideration of which can help us to see what is going on. We briefly introduce a quite conventional typed $\lambda$-calculus, then indicate how it can be restricted to get a system related to our stratified $\lambda$-calculus.

We restrict ourselves to pairing, function application and abstraction as term constructions for the sake of simplification. We assume a base type $\iota$ of individuals. If $\alpha$ and $\beta$ are types, $\alpha \times \beta$ and $\alpha \rightarrow \beta$ are types, called product types and arrow types respectively. The inhabitants of $\alpha \times \beta$ are to be understood to be pairs with first projection of type $\alpha$ and second projection of type $\beta$. The inhabitants of $\alpha \rightarrow \beta$ are understood to be functions from type $\alpha$ to type $\beta$. The types are exactly those which can be constructed from $\iota$ using the given type constructors.

This motivates the following restrictions on our term constructions: variables require type labels (we still have a countable supply of each type); the projection functions $\pi_1$ and $\pi_2$ are replaced by infinitely many different versions with type superscripts of the forms $(\alpha\times\beta)\rightarrow \alpha$ and $(\alpha\times\beta)\rightarrow \beta$, respectively; any pair term is still well-formed, but requires the appropriate product type superscript; a function application term T(U) is only well-formed if T has an arrow type $\alpha \rightarrow \beta$ and U has type $\alpha$ (the application term is then of type $\beta$); a $\lambda$-term $(\lambda x.T)$ is always well-formed if T is well-formed, and has type $\alpha \rightarrow \beta$, where $\alpha$ is the type of x and $\beta$ is the type of T.

In this system, a term like x(x) cannot be well-formed because no type superscript appropriate to x can be constructed. A hint of the advantage which we see in the stratified $\lambda$-calculus can be seen in the proliferation of projection functions in different types. Similarly, there is a different identity function $(\lambda x^{\alpha}.x^{\alpha})$ on each type $\alpha$ (inhabiting $\alpha \rightarrow \alpha$); this is a general phenomenon.

The restricted version of this type scheme which is related to stratified $\lambda$-calculus is obtained as follows. Its types are labelled by natural numbers. Type 0 is to be identified with $\iota$. Type n+1 is to be identified with $n \rightarrow n$(where n stands for the type already labelled by n). Further, we identify type n with the product type $n \times n$ (this assumption is harmless if types are understood to have infinitely many inhabitants).

The inhabitants of type 0 are individuals, and enjoy a surjective pairing function under which each individual is identified with some pair of individuals. The inhabitants of type n+1 are the functions from type n to type n, for each n; it is easy to define the surjective pair on type n+1 in a uniform manner in terms of the pair on type n.

There is a great deal of polymorphism in this restricted type system. In fact, every theorem which can be proved about types 0,1,2$\ldots$has a precise analogue with each type label raised by one which can be proved about types 1,2,3$\ldots$, and each definable object in the system using types 0,1,2$\ldots$ has an analogue defined in the same way using types 1,2,3$\ldots$. This polymorphism motivates the idea of collapsing the type structure entirely: suppose that all the types are in fact the same domain, but keep the restrictions on the formation of abstractions inherited from the typed system, and we obtain a stratified $\lambda$-calculus.

The practical application of this to working with Watson is to keep in mind the relationship between relative types of objects in the definition of a function in stratified $\lambda$-calculus and the concrete types of individuals, functions from individuals to individuals (type 1), functions from type 1 functions to type 1 functions (type 2), etc., in this typed calculus.

It might seem we lose expressive power through not allowing types such as $(\iota \rightarrow \iota) \rightarrow \iota$ or $\iota \rightarrow (\iota \rightarrow \iota)$ (functions from type 1 to type 0 and vice versa), but these types are both readily coded into type 2. A function from type 1 to type 0 is represented by a function of type 2 taking a type 1 function to the (type 1) constant function of the type 0 value of the coded function. A function from type 0 to type 1 is coded by a function of type 2: values at constant functions of its intended type 0 arguments of the coded function are the intended type 1 values, while values at nonconstant functions are ignored (they may be taken to be a default value). A combination of these devices and similar considerations about product types allows the coding of any type in the simple type theory of Church. Experience suggests to us that there is not any serious loss of mathematical fluency.

The use of the term ``stratified'' for well-formed $\lambda$ terms can be motivated by considering the fact that we have to organize the functions and arguments appearing in the specification of a new function by a $\lambda$ term into ``strata'' corresponding to the integer types of our restricted type system. When considering a complex term, it can be helpful to draw a diagram with horizontal levels into which each object appearing in the $\lambda$-term is placed, and make sure that functions on one level are applied only to arguments on the next level down.

A final comment: the common practice of ``currying'' (replacing a function of type $(\alpha \times \beta) \rightarrow \gamma$ whose typical value might be written f(x,y) with the related function of type $\alpha \rightarrow (\beta \rightarrow \gamma)$ whose typical (iterated) value might be written f(x)(y)) used in conventional systems of typed and untyped $\lambda$-calculus is not used in stratified $\lambda$-calculus because it is not sound in terms of relative type: in f(x,y) the relative types of x and y are the same, while they are different in f(x)(y). This is the reason why we have used the conventional notation f(x) for function application rather than the notation fx more usual in combinatory logic and $\lambda$-calculus (the latter notation lends itself better to currying).