Unification and Matching Modulo Type Isomorphism.
Author: Dan Dougherty and Carlos C. Martínez
March 2004
Abstract::
We present some initial results concerning higher order unification and matching in the presence of type isomorphism. We introduce the notion of term isomorphism under which we aim to develop unification algorithms. It is not hard to show that this equality holds desirable properties such as the decidability of its validity problem. We establish a characterization theorem of term isomorphisms in terms of labelled tree isomorphisms; which we think will lead us to an efficient unification algorithm implementations.
Definition:: (Term Isomorphisms)
Let N and M be lambda terms. We say that N and M are term isomorphic if and only if there exists an invertible lambda term F such that FM = N.
Background::
Type isomorphism has been well studied by R. Di Cosmo, S. Solviev and M. Rittri. It has interesting connections with Logic (Tarski’ high school algebra problem), Category Theory and Information Retrieval from Software Libraries. We say that two types A and B are isomorphic if and only if there exists an invertible term such that maps A bijectively onto B.
In Proceedings of II International Workshop of Higher Order Rewriting, Aachen, Germany, June 2004. Abstract in the Technical report of the Computer Science Department of RWTH Aachen.
© 2012 Carlos C. Martínez | Generated by webgen