The Barendregt Cube with Definitions and Generalised Reduction

Abstract

In this paper, we propose to extend the Barendregt Cube by generalising β-reduction and by adding definition mechanisms. Generalised reduction allows contracting more visible redexes than usual, and definitions are an important tool to allow for a more flexible typing system. We show that this extension satisfies most of the original properties of the Cube including Church-Rosser, Subject Reduction and Strong Normalisation. © 1996 Academic Press, Inc.