Associative Commutative Unification

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Associative Commutative Unification

John D. Ramsdell-3
I'd like to write an obviously correct implementation of a unifier, a
program that when given two terms, finds a substitution that makes the
two terms equal.  The phrase "obviously correct" is meant to imply
that the clarity of the code trumps efficiency.  As near as I can
tell, high performance unifiers are full of side-effects, and
achieving the same performance without side-effects in Haskell is
difficult or impossible.

In contrast, it is easy to write obviously correct Hasklell
implementations of unifiers for freely generated term algebras.  One
can use Lawrence Paulson's code in ML for the Working Programmer as a
template or follow Martelli and Montanari's simple set of rules.

My problem is one of my operators is multiplication, which is
associative and commutative.  These two properties make unification
much more difficult.  Mark Stickel described a complete unification
algorithm for this problem, but the task of translating his
description into an obviously correct Haskell program appears to be
difficult.  For example, the algorithm requires the generation of the
basis of solutions to linear homogeneous diophantine equations.  I
haven't located an algorithm for this part yet.

If you have experience implemented equational unification in Haskell,
please share it.

John
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

Don Stewart-2
ramsdell0:

> I'd like to write an obviously correct implementation of a unifier, a
> program that when given two terms, finds a substitution that makes the
> two terms equal.  The phrase "obviously correct" is meant to imply
> that the clarity of the code trumps efficiency.  As near as I can
> tell, high performance unifiers are full of side-effects, and
> achieving the same performance without side-effects in Haskell is
> difficult or impossible.
>
> In contrast, it is easy to write obviously correct Hasklell
> implementations of unifiers for freely generated term algebras.  One
> can use Lawrence Paulson's code in ML for the Working Programmer as a
> template or follow Martelli and Montanari's simple set of rules.
>
> My problem is one of my operators is multiplication, which is
> associative and commutative.  These two properties make unification
> much more difficult.  Mark Stickel described a complete unification
> algorithm for this problem, but the task of translating his
> description into an obviously correct Haskell program appears to be
> difficult.  For example, the algorithm requires the generation of the
> basis of solutions to linear homogeneous diophantine equations.  I
> haven't located an algorithm for this part yet.
>
> If you have experience implemented equational unification in Haskell,
> please share it.

"Typing Haskell in Haskell" lives here,

    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/thih

"a Haskell program that implements a Haskell typechecker, thus providing
a mathematically rigorous specification in a notation that is familiar
to Haskell users. We expect this program to fill a serious gap in
current descriptions of Haskell, both as a starting point for
discussions about existing features of the type system, and as a
platform from which to explore new proposals"

Might be useful as a starting point.

-- Don
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

John D. Ramsdell-3
The Haskell typechecker contains a nice example of a unifier for
freely generated terms.  My focus is on equational unification, but
thanks anyway.

John

On Sun, Jul 6, 2008 at 10:38 PM, Don Stewart <[hidden email]> wrote:

> ramsdell0:
>> I'd like to write an obviously correct implementation of a unifier, a
>> program that when given two terms, finds a substitution that makes the
>> two terms equal.  The phrase "obviously correct" is meant to imply
>> that the clarity of the code trumps efficiency.  As near as I can
>> tell, high performance unifiers are full of side-effects, and
>> achieving the same performance without side-effects in Haskell is
>> difficult or impossible.
>>
>> In contrast, it is easy to write obviously correct Hasklell
>> implementations of unifiers for freely generated term algebras.  One
>> can use Lawrence Paulson's code in ML for the Working Programmer as a
>> template or follow Martelli and Montanari's simple set of rules.
>>
>> My problem is one of my operators is multiplication, which is
>> associative and commutative.  These two properties make unification
>> much more difficult.  Mark Stickel described a complete unification
>> algorithm for this problem, but the task of translating his
>> description into an obviously correct Haskell program appears to be
>> difficult.  For example, the algorithm requires the generation of the
>> basis of solutions to linear homogeneous diophantine equations.  I
>> haven't located an algorithm for this part yet.
>>
>> If you have experience implemented equational unification in Haskell,
>> please share it.
>
> "Typing Haskell in Haskell" lives here,
>
>    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/thih
>
> "a Haskell program that implements a Haskell typechecker, thus providing
> a mathematically rigorous specification in a notation that is familiar
> to Haskell users. We expect this program to fill a serious gap in
> current descriptions of Haskell, both as a starting point for
> discussions about existing features of the type system, and as a
> platform from which to explore new proposals"
>
> Might be useful as a starting point.
>
> -- Don
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

Edsko de Vries
On Tue, Jul 08, 2008 at 08:24:45AM -0400, John D. Ramsdell wrote:
> The Haskell typechecker contains a nice example of a unifier for
> freely generated terms.  My focus is on equational unification, but
> thanks anyway.

Are you aware of "Term Rewriting and all That"? It describes how to do
associative commutative unification; whether it satisfies your
'obviously correct' criterion I don't know.

Edsko
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

John D. Ramsdell-3
> Are you aware of "Term Rewriting and all That"? It describes how to do
> associative commutative unification; whether it satisfies your
> 'obviously correct' criterion I don't know.

Oh yes, I know about term rewriting.  If your equations can be
expressed as a set of confluent rewrite rules, one can use the
Martelli and Montanari's formalization of unification to come up with
an obviously correct equational unifier.  Alas, that simple trick
doesn't work for AC unification.

Have you heard of Maude?  I hear the next version will have support
for AC unification.  If I stay with Haskell, I'd have to use their
support via interprocess communication.  Yuck.

http://maude.cs.uiuc.edu/

John
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

Janis Voigtlaender
John D. Ramsdell wrote:
>>Are you aware of "Term Rewriting and all That"? It describes how to do
>>associative commutative unification; whether it satisfies your
>>'obviously correct' criterion I don't know.
>
>
> Oh yes, I know about term rewriting.

I think Edsko was more specifically referring to the book "Term
Rewriting and all That" by Baader and Nipkow.

--
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

Pepe Iborra-3
In reply to this post by John D. Ramsdell-3
On Fri, Jul 11, 2008 at 2:39 PM, John D. Ramsdell <[hidden email]> wrote:

>> Are you aware of "Term Rewriting and all That"? It describes how to do
>> associative commutative unification; whether it satisfies your
>> 'obviously correct' criterion I don't know.
>
> Oh yes, I know about term rewriting.  If your equations can be
> expressed as a set of confluent rewrite rules, one can use the
> Martelli and Montanari's formalization of unification to come up with
> an obviously correct equational unifier.  Alas, that simple trick
> doesn't work for AC unification.
>
> Have you heard of Maude?  I hear the next version will have support
> for AC unification.  If I stay with Haskell, I'd have to use their
> support via interprocess communication.  Yuck.
>
> http://maude.cs.uiuc.edu/
>
> John
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

You are surely aware that AC unification is much more difficult than
syntactical unification.
CIMe[1] might be useful to solve the generated diophantine equations.
But I don't think you will be able to obtain obvious correctness, and
probably performance neither.

I don't know what you are planning to do, but perhaps you'd be better
served by Maude than by Haskell.
The Maude language is a joy to use and version 2.4 with AC unification
is (expectedly) being released next week in RTA.

Cheers
pepe

[1] - http://cime.lri.fr/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

John D. Ramsdell-3
In reply to this post by Janis Voigtlaender
> I think Edsko was more specifically referring to the book "Term
> Rewriting and all That" by Baader and Nipkow.

Thanks for pointing this out--I was confused.  I notice the book has a
chapter on equational unification that includes a section on AC
unification.  This book looks like a winner.  Thank you.

John
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

John D. Ramsdell-3
In reply to this post by Pepe Iborra-3
> CIMe[1] might be useful to solve the generated diophantine equations.

It also has AC unification, and it probably wouldn't be all that hard
to translate our code into OCaml.  I think CiME isn't supported
anymore.  Still it's worth considering.  It's quite large.  The source
distribution compiled effortlessly on Ubuntu.  That's about all I know
now.

> I don't know what you are planning to do, but perhaps you'd be better
> served by Maude than by Haskell.

Switching to Maude is an option we're considering.

John
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Associative Commutative Unification

Matthieu Sozeau

Le 12 juil. 08 à 04:02, John D. Ramsdell a écrit :

CIMe[1] might be useful to solve the generated diophantine equations.

It also has AC unification, and it probably wouldn't be all that hard
to translate our code into OCaml.  I think CiME isn't supported
anymore.  Still it's worth considering.  It's quite large.  The source
distribution compiled effortlessly on Ubuntu.  That's about all I know
now.

CIMe 2 is not maintained anymore, but a third version is in the works, see:
http://www3.iie.cnam.fr/~urbain/a3pat/a3pat_intro.en.html

-- Matthieu

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe