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
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
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
10 matches
Mail list logo