[Prev][Next][Index][Thread]
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