Behavioral and Coinductive Rewriting

Behavioral rewriting di ers from standard rewriting in taking account of the weaker inference rules of behavioral logic, but it shares much with standard rewriting, including notions like termination and con uence. We describe an e cient implementation of behavioral rewriting that uses standard rewriting. Circular coinductive rewriting combines behavioral rewriting with circular coinduction, giving a surprisingly powerful proof method for behavioral properties; it is implemented in the BOBJ system, which is used in our examples. These include several lazy functional stream program equivalences and a behavioral re nement.

• Type: Journal
• Year: 2000
• Where: ENTCS
• Authors: Joseph A. Goguen, Kai Lin, Grigore Rosu
• Keywords: Behavioral, Behavioral Rewriting, ENTCS 2000, Standard Rewriting