Rewriting Calculus with(out) Types

The last few years have seen the development of a new calculus which can be considered as an outcome of the last decade of various researches on (higher order) term rewriting systems, and lambda calculi. In the Rewriting Calculus (or Rho Calculus, Cal), algebraic rules are considered as sophisticated forms of "lambda terms with patterns", and rule applications as lambda applications with pattern matching facilities. The calculus can be customized to work modulo sophisticated theories, like commutativity, associativity, associativity-commutativity, etc. This allows us to encode complex structures such as list, sets, and more generally objects. The calculus can either be presented "`a la Curry" or "`a la Church" without sacrificing readability and without complicating too much the metatheory. Many static type systems can be easily plugged-in on top of the calculus in the spirit of the rich typeoriented literature. The Rewriting Calculus could represent a li...

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Horatiu Cirstea, Claude Kirchner, Luigi Liquori
• Keywords: Calculus, ENTCS 2002, Lambda, Rewriting Calculus