UP

Barendregt's Lambda Cube

cubemap

The lambda cube is a way of presenting the fine structure of Coquand's Calculus of Constructions relating that system to a variety of other typed lambda calculi. This idea is due to Henk Barendregt, and is presented in his Introduction to Generalised Type Systems which is my principle source in preparing this material.

The eight systems at the vertices of the cube are obtained by extending the simply typed lambda calculus (lambdafun) at the origin of the cube along one or more of the axes of the cube. The cube has six faces.

To understand the following presentation of the lambda cube you must first refer to the page on Pure (or generalised) Type Systems. The deductive system given there is parameterised by a triple (S,A,R), in which S is a set of sorts, A is a set of axioms and R is a set of triples of sorts. The relation R determines which products are available in the system.

For the systems on the lambda cube the sorts are always {*,box} (it may be helpful to think of these as the sorts of types and kinds respectively) and the set A is always {<> box *:box} (which says that the sort of types is a kind).

The systems on the lambda cube are here defined by enumeration of the relation R for each of the systems. In all these systems the second and third sorts in the triples which define the relationship R are the same, so we omit the third and define R by enumeration of a set of pairs for each system.

Since there are only two sorts, there are just four possible ordered pairs. One of these (*,*) is present in all the systems on the lambda cube. Each system is therefore uniquely associated with a subset of the remaining three pairs. The organisation into a cube arises from using these three pairs as labels for three axes. The position on the cube of the system determines its coordinates which in turn determine the relation R giving the instances of the Pi rules which are available in the system. These tell you the sort of a dependent product type depending on the sorts of its domain and range types.

Axes:

The axes provide a coordinate system spatially locating the systems according which instances of the Pi rules are available in each system.
  The (*,*) rule, which asserts that the types are closed under the (dependent) function space constructor, is common to all eight systems, and so might be thought of as labelling the origin.

Three other pairs appear, each of which corresponds to an axis of the coordinate system.

  Face Without Axis Face With  
  "Standard" Models (box,*) Types dependent on Kinds 2
    (box,box) Kinds Dependent on Kinds w
->   (*,box) Kinds Dependent on Types P

Faces:

  (box,*)    
not(*,box) not(box,box) (*,box) (box,box)
  not(box,*)    

Vertices:

(box,*)(box,box)
(*,*) 
    Lambda omega   Lambda c
(box,*)(box,box)
(*,*)(*,box)
(box,*) 
(*,*) 
  Lambda2 LambdaP2    
(box,*) 
(*,*)(*,box)
 (box,box)
(*,*) 
    Lambdauw Lambdapuw  
 (box,box)
(*,*)(*,box)
  
(*,*) 
  Lambdafun   Lamp    
  
(*,*)(*,box)

Lambdafun

The Simply Typed Lambda Calculus

Coordinates
funPw2
(*,*)      
This is said by Barendregt to correspond to Church's simply typed lambda calculus, but that system does not admit dependent types. It is also sometimes alleged to be "hol", possibly meaning by that the logical system supported by the Cambridge HOL interactive theorem prover. This is even wider off the mark, most importantly because all the systems on the lambda cube can only be construed as logics via the propositions as types paradigm, under which a proof that a term has some type is taken as a proof of a proposition understood to be expressed by the type (in the case of a product type, for example, a proposition quantifying over the domain of the product and asserting over that domain the proposition corresponding to the type of the codomain). However, the logic commonly called HOL is a polymorphic version (though not the same kind of polymorphism as is found on the lambda-cube) of the classical logic known as Church's Simple Theory of Types, which is obtained from the simply typed lambda calculus by using certain types of terms of the calculus as propositions in a Hilbert-style axiomatic theory. This is logically quite different, and very much stronger than, the system at the origin of the lambda cube.

Lambdauw

Weak Lambda Omega
Related to the system POLYREC studied by Renardel de Lafalette [1985].

Coordinates
->Pw2
(*,*)   (box,box)  

Lambda2

Polymorphic or Second Order, Typed Lambda Calculus

Coordinates
->Pw2
(*,*)     (box,*)

Lambda omega

The System Fomega

Coordinates
->Pw2
(*,*)   (box,box) (box,*)

Lamp

LF
Also corresponds to one of the AUTOMATH systems.

Coordinates
->Pw2
(*,*) (*,box)    

Lambdapuw

Weak Lambda P omega

Coordinates
->Pw2
(*,*) (*,box) (box,box)  

LambdaP2

Lambda P2

Coordinates
->Pw2
(*,*) (*,box)   (box,*)

Lambda c

The Calculus of Constructions

Coordinates
->Pw2
(*,*) (*,box) (box,box) (box,*)


UP HOME © RBJ created 1995-11-12 modified 2011-05-23