UP Lambda-SKI cube

Typed Lambda Logic's (TLambdaL)

Church's Simple Theory of Types

The simple theory of types is probably the simplest logic to describe and to understand. Of course that depends on what you already understand before you start! The hardest bit to understand is the idea of higher order functions, which is present in both pure combinatory logic and in the type-free lambda calculus. If you understand the lambda calculus its a small step to the simple theory of types.

The simple theory of types is arrived at from the lambda calculus by adding a type system, and then some logical constants, and then beefing up the inference rules to reflect the intended meaning of the constants.

First the type system. The type system is based on the premise that there are two collections of elements, the first of which may be thought of as individuals in some domain of discourse (which we will call ind) and the second of which may be thought of either as truth values or as propositions (which we will call bool, anticipating a two valued logic). These two collections are the primitive types.

The full collection of types is obtained by constructing function spaces. From any two types, t and u, not necessarily distinct, a space of functions may be constructed, which we write as t function u and which contains all the functions with domain t and co-domain u, i.e. those functions which are defined for all elements of t and yield values which are elements of u. The types are therefore the closure of the set {ind, bool} under the function space constructor "function".

A grammar for the language of types is as follows:

Type::=bool|ind|(Type function Type)

The terms of the simple theory of types are the terms of the type-free lambda calculus, decorated with types and subject to formation constraints defined using these annotations. A term is either a constant name decorated with a type, or a variable name decorated with a type, or the application of one term to another (shown by juxtaposition with the function on the left), or a lambda abstraction in which the bound variable name is decorated with a type.

A grammar for the terms is as follows:

Term::=Cname:Type|Vname:Type|Term Term|(lambda Vname:Type. Term)
The formation constraints imposed concern function application and functional abstraction. They determine the type of a function formed by abstraction, ensuring that the type of the bound variable in the abstraction is the domain of the function type of the abstraction and also that the type of the body of the lambda expression is the type of the co-domain of the resulting function. When a function is applied the type constraints require that the type of the argument is the same as the domain of the function space type associated with the function.
up home © RBJ created 1995/12/9 modified 1997/12/2