Higher-order unification

[Russell Wallace]

I'm currently struggling (operative word) with higher-order
unification, and wondering if anyone might be able to help. Specific
questions:

It makes sense in the abstract that higher-order unification is
undecidable, but it would help to make it a bit more concrete. Does
anyone have any specific examples of cases where the usual first-order
algorithm fails?

I now believe unification is the key to making combinator logic work.
Is Huet's algorithm likely to be the best one for this case, or a
tweaked version thereof?

Does anyone have an explanation of Huet's algorithm for nonmathematicians?

[Abram Demski]

Russel,

My understanding so far:

Higher-order equational unification can proceed by putting two terms
in normal form before attempting to unify them. However, the act of
putting the two in normal form is potentially nonterminating, so the
unification is undecidable. The task is further complicated by the
substitutions themselves, which may allow for further reductions;
thus, even when one has put both terms into normal form, I take it you
can't conclude that the two can't be unified just because they don't
appear to be unifiable.

Does this fit with what you've read about it?

--Abram

> --
>
> You received this message because you are subscribed to the Google Groups "One Logic" group.
> To post to this group, send email to one-...@googlegroups.com.
> To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.
>
>
>

--
Abram Demski
http://dragonlogic-ai.blogspot.com/
http://groups.google.com/group/one-logic

[Russell Wallace]

I don't think so, or rather, what you say is true, but I don't think
that covers the difficulty.

From a one-page document entitled:
Higher Order Unification
Chris Kau ffman
Fall 2004

I get the following:

In the first order framework a pair of terms like
t1 = (F A)
t2 = (f x)
could not be unified as their function symbols di ffer. In the
higher-order setting, if f and x are
treated as variables, substituting F for f and A for x unifies the
two terms. However, it is not
the only solution to the unification problem: substituting \y:FA for
f and anything for x will
also unify the two terms.

I don't think you can put file attachments in Google groups messages,
so I'll send you the PDF directly.

[Abram Demski]

Russel,

Ok, so the difficulty in this and similar cases comes from the
so-called "flexible terms," right? Because a free variable occurs in
the head position, it's not possible to just compare the heads to see
if a match can be made; one must make substitutions. The problem is
that these substitutions can allow further reductions... and since
there's a great deal of freedom in what one can put into that head
position, the further reductions can lead in many directions.

Thanks for the references. Right now I'm still getting through the
book chapter by Dowek. It is making sense now that I decided to read
it in order. :)

--Abram

On Tue, Dec 22, 2009 at 10:01 AM, Russell Wallace

[Abram Demski]

Russel,

Ah. :) I just got to the part about Huet's lemma. Nevermind what I
said about flexible terms being the problem!

--Abram