Rewriting Calculus with Fixpoints: Untyped and First-order Systems

Horatiu Cirstea (1) , Luigi Liquori (2, 3) , Benjamin Wack (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs
2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems
3 MIRHO - Objects, types and prototypes : semantics and validation

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.

Mots clés: type theory; rewriting calculus; lambda-calculus; object calculus; pattern matching; fixpoints; lambda-calcul

Mots clés: théorie des types; points fixes; calculs à objets; filtrage; calcul de réécriture

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]; Informatique et langage [cs.CL]

Horatiu Cirstea, Luigi Liquori, Benjamin Wack. Rewriting Calculus with Fixpoints: Untyped and First-order Systems. Types for Proofs and Programs International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, Apr 2003, Turin, Italy. pp.147-161, ⟨10.1007/978-3-540-24849-1_10⟩. ⟨inria-00100113⟩