UP Lambda-SKI cube

Typed Lambda Calculi (TLambdac)

Pure Typed Lambda Calculus

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 codomain u, i.e. those functions which are defined for all elements of t and yeild 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 codomain 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 1999/9/19 c