UP Lambda-SKI cube

Typed Combinatory Calculi (Tc)

Pure Typed Combinatory Logic

There are two main historical reasons for the introduction of types.

The first type system was that devised by Russell for use in Principia Mathematica, and published in a paper entitled Mathematical Logic as based on the Theory of Types. Russell's motivation in introducing this theory was to overcome the problems causing inconsistency in Frege's previous attempt to reduce mathematics to logic, in a way which was both technically and philosophically satisfactory.

The motivation for introducing types into the systems of the Lambda-SKI cube is similar. The introduction of type constraints reduces the expressiveness of the systems sufficiently to make it possible to introduce quantifiers without rendering the systems inconsistent. In particular, the introduction of a type system constrains the domains over which functions may be defined in a manner similar to the constraints which are necessary in set theory for the theory to be consistent with the semantics of the iterative heirarchy of sets.

We will consider in the systems around the Lambda-SKI cube the very simple type system introduced by Church for his Simple Theory of Types, together with some small elaborations of that system which have proven desirable in practical implementations and which were introduced in LCF and inherited by HOL.

up home © RBJ created 1995-12-9 modified 2005-12-28