[Prev][Next][Index][Thread]
unification in CCC
Date: Fri, 14 Aug 92 10:58:32 +0200
Dear Moderator,
I would like to submit the following question to the attention
of the subscribers of the types list.
yours truly,
Roberto Amadio
=========================================================================
I know of at least two surveys on unification which mention the
problem of unification in the free theory of a cartesian
closed category but do not give any substantial reference.
One of these surveys goes a little bit further and states that
unification in a ccc `corresponds' to higher order unification
(say unification in the simply typed lambda beta eta calculus,
as described in G. Huet [1975] `A unification algorithm for
typed lambda calculus', TCS ).
I am a bit sceptic about this statement and I would appreciate
receiving references to papers where this point is actually worked out.
Roberto Amadio (amadio@loria.loria.fr)
P.S. Here is a sketch of how, I guess, a typical problem could be formalized.
Let us consider the simply typed lambda-beta-eta calculus.
A context G is a list of pairs variable-type where all variables are
distinct.
G |- M:A means that the term M has type A in the context G.
There is a standard interpretation, say [[G |- M:A]] of this judgment
in a CCC as a morphism from the object interpreting G to the object
interpreting A.
Now given two terms of type A in the context G we may ask if there is a
pre-equalizer in the free CCC for the morphisms:
[[G |- M:A ]], [[G |- N:A ]].
This corresponds to the abstract view of a unifier as a pre-equalizer (a cone)
(see for instance, J. Goguen[1989], `What is unification ?', in Resolution
of equations in algebraic structures', Ait-Kaci&Nivat (eds.), Academic Press).
Question: Which kind of relation lies pre-equalizers for [[G |- M:A ]],
[[G |- N:A ]] in the free CCC and unifiers for M, N in the
lambda-beta-eta theory ?