Department of Computer Science and Technology

Technical reports

Categorical abstract machines for higher-order typed lambda calculi

Eike Ritter

April 1993, 149 pages

This technical report is based on a dissertation submitted by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.

DOI: 10.48456/tr-297

Abstract

We define in this thesis categorical abstract machines for the calculus of constructions, a special higher-order lambda-calculus. We start with the derivation of categorical combinators, i.e. an equational theory based on a categorical structure for the calculus. It turns out that only a generalization of Ehrhard’s D-categories can be used for this purpose; all other categorical structures modelling the calculus yield only conditional equations or no equations at all. Next we orient the equations to obtain reduction rules. When we want to show that this reduction corresponds to reduction in the calculus, we run into difficulties in proving strong normalization. We can only show that any reduction that leads first to a combinator corresponding to a weak head-normal form is finite. These results are the key to formulate an eager and a lazy strategy for the reduction of a combinator to its normal form.

We then construct abstract machines for the eager and lazy strategy. Their correctness proof consists of an induction over the definition of the reduction strategies. These machines specialize to the CAM and Krivine’s machine in the first order case respectively. The original construction of the CAM is based on cartesian closed categories (CCCs). They model both environments and terms by morphisms regardless of their conceptual difference, whereas the D-categories separate these two notions. Hence the correspondence between the D-categories and the abstract machines described in this thesis is closer than that between the CAM and the CCCs. We also obtain an abstract machine for type checking of these combinators, which uses the above reduction machines. Preliminary tests suggest that the abstract machines are quite efficient compared to other implementations.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-297,
  author =	 {Ritter, Eike},
  title = 	 {{Categorical abstract machines for higher-order typed
         	   lambda calculi}},
  year = 	 1993,
  month = 	 apr,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-297},
  number = 	 {UCAM-CL-TR-297}
}