The Rho Cube

9 years 4 months ago
The Rho Cube
The rewriting calculus, or Rho Calculus (ρCal), is a simple calculus that uniformly integrates abstraction on patterns and nondeterminism. Therefore, it fully integrates rewriting and λ-calculus. The original presentation of the calculus was untyped. In this paper we present a uniform way to decorate the terms of the calculus with types. This gives raise to a new presentation `a la Church, together with nine (8+1) type systems which can be placed in a ρ-cube that extends the λ-cube of Barendregt. Due to the matching capabilities of the calculus, the tems use only one abstraction mechanism and therefore gives an original answer to the identification of the standard “λ” and “Π” ors. As a consequence, this brings matching and rewriting as the first class concepts of the Rho-versions of the Logical Framework (LF) of HarperHonsell-Plotkin, and of the Calculus of Constructions (CC) of CoquandHuet.
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Authors Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Comments (0)