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
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
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
On Fri, Jul 11, 2008 at 2:39 PM, John D. Ramsdell [EMAIL PROTECTED] 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
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
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
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 [EMAIL PROTECTED] wrote:
ramsdell0:
I'd like to write an obviously correct implementation of a
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
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
