Rewriting calculus with fixpoints: untyped and first-order systems

Abstract

The rewriting calculus, also called ρ-calculus, is a framework embedding α-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the α-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the α-calculus can be generalized to the ρ-calculus: in this paper, we study extensively a first-order ρ-calculus àla Church, called ρ→stk The type system of ρ→stk allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting - based language. © Springer - Verlag 2004.