Optimal Derivation in Term Rewriting Systems, 1/29, 10:45am

Date: Wed, 16 Jan 91 10:31:56 EST


		Date: Tuesday, January 29, 1991
		Time: Refreshments at 10:45 a.m.
		Place: Second Floor Lounge

	Optimal Derivation in Term Rewriting Systems
		Without Critical Pairs

			Luc Maranget


	This work introduces a new notion of labeled Term
Rewriting Systems (labeled TRS).  This notion expresses sharing
in TRS.  A new notion of conditional TRS is also introduced.
Conditional TRS allows us to extend the properties of TRS
without critical pairs to a class of Systems wider than the
usual one.  In this extended notion of systems without critical
pairs, optimal derivations are characterized.  Furthermore, for
any normalizable term, it is possible to compute an optimal
normalizing derivation.

	These results are applied to two systems describing weak
lambda-calculi.  The call-by-name-with-sharing or lazy strategy
is shown to be optimal in these systems.

Host: Professor Arvind