TOC Seminar -- Philippe Le Chenedec -- Thur., May 25

Date: Thu, 11 May 89 15:12:52 EDT

To: theory-seminars@theory.LCS.MIT.EDU

			DATE: Thursday, May 25, 1989
			   TIME: Refreshments: 4PM
			       Lecture: 4:15PM
			      PLACE: NE43-512A

			 On the Logic of Unification

			    Philippe Le Chenadec
	Institut National de Recherche en Informatique et Automatique
		  B.P. 105, 78153 Le Chesnay Cedex, France
		       e-mail: lechenad@inria.inria.fr

Unification, or solving equations on finite trees, is a P-complete problem
central to symbolic manipulation, especially in Resolution, Type Inference
and Rewriting. We present a natural logic dedicated to unification. This
logic enjoys the classical proof-theoretic properties: atomicity; strong
normalization; Church-Rosserness; left/right introduction/elimination, and
positive/negative, symmetries.

Motivated by the Type Inference problem for Polymorphic lambda-calculus, we
introduce, besides a model-theoretic semantics and its completeness, a
geometrical interpretation of deductions in the fundamental group of the
hypotheses graph. This semantics describes the operational content of the
deductions, and allows the design of a normalization process.

This unification logic provides significant tools in investigations of
higher-order unification, especially for the Type Inference problem for
Polymorphic Lambda-Calculus, via fixed-point equations deducible from the
given equations in Unification Logic. We also present some results on the
classification problem of these fixed-point equations.

HOST: Prof. Meyer