🚀 go-pugleaf

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 ?