Home

Rho calculus

The Rho-calculus is a calculus of pattern matching that embeds the lambda-calculus in a very simple manner, and also naturally accomodates a number of extensions of the lambda-calculus. It encodes the results of pattern matching in a manner that ensures confluence of the whole calculus.

It was proposed by Horatiu Cirstea and Claude Kirchner in 1998, and Matching Power, a 2001 RTA paper, is maybe the nicest introduction to the calculus. Kirchner's research group maintains a list of papers.

Postscript There was an LtU classic story on the rho-calculus as well...

By Charles Stewart at 2006-01-26 21:24 | Theory | other blogs | 15000 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

My interest

It's hard to be general about this, since rewriting is such a flexible technique, but personally I've been interested in finding type systems for various graph rewriting calculi, because otherwise I can't prove the properties I want the systems to have. Type systems are one of the most effective tools for restricting the shape of the structures you are interested in to the ones you care about.

By Charles Stewart at Fri, 2006-02-03 17:02 | login or register to post comments