Ask HN: Design and Implementation of Term Rewriting Systems

https://news.ycombinator.com/item?id=21797009

by i_don_t_know • 7 years ago

7 4 7 years ago

news.ycombinator.com

Hello!

I’m looking for resources on the design and implementation of Term Rewriting Systems. I’m particularly interested in systems for use in discrete math and computer algebra systems, but any resource is welcome.

Also, how do these systems relate to graph reduction in lazy functional languages?

Thank you!

triska• 7 years ago

The book Term Rewriting and All That by Baader and Nipkow includes a lot of code in ML, I highly recommend it.

The code is available online:

https://www21.in.tum.de/~nipkow/TRaAT/

The book also contains many useful references, which I also recommend to check out for your other questions.

Also, in my experience, logic programming languages like Prolog are especially useful for reasoning about term rewriting systems, because they provide built-in features such as unification, subsumption checks and implicit search and backtracking which are very useful when working with and reasoning about term rewriting systems.

i_don_t_know2• 7 years ago

Thank you for the recommendation.

chewxy• 7 years ago

How these systems relate to graph reduction: graph reduction is one way to implement term rewriting.

Laziness is an orthogonal issue related to your operational semantics.

The designs of TRS implementations are mainly to address an issue - your reduction rules as written are not ordered. In implementing them you need to impose an order. This is not so desirable, so parallel reduction may be required, but that introduces a whole new bunch of issues.

Baader and Nipkow is pretty good, but I would also highly suggest writing a lambda calculus in an imperative programming language to get a feel for the operational semantics

i_don_t_know2• 7 years ago

Thank you.

Ask HN: Design and Implementation of Term Rewriting Systems

Related Stories