Home » forums » LtU Forum

Rewrite.js – a minimalist s-expr based term rewriting system

Rewrite.js is estimated to be a Turing complete, s-expression based term rewriting system. It may be used as a curiosity computing platform, formula application system, proof checker, problem solver, and pretty much anywhere where any kind of computation is required, as long as slower performance on intensive computations doesn't go beyond limits of user patience.

Rewrite.js is designed as a creation with only one kind of rules: substitution rules. Being such a minimalist creation, complete rewrite.js implementation fits in a bit more than 400 Javascript lines of code.

To get a feeling about rewrite.js appearance, this is a math expression rewriting code in rewrite.js:

    (
        (
            REWRITE
            (
                MATCH
                (VAR <a>)
                (RULE (READ  <a> + <a>) (WRITE 2 * <a>))
            )
            (
                MATCH
                (VAR <a>)
                (RULE (READ  <a> * <a>) (WRITE <a> ^ 2))
            )
        )

        (x + x) * (x + x)
    )

The above example evaluates to:

    ((2 * x) ^ 2)

Rewrite.js is hosted on https://github.com/contrast-zone/rewrite.js with convenient online playground.

Aside from criticism, I'm particularly interested in possible rewrite.js usage ideas.

By Ivan V. at 2022-12-27 19:13 | LtU Forum | previous forum topic | next forum topic | other blogs | 4137 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Maybe I'm mixing things up, but

Maybe I'm mixing things up, but this furiously reminds me of what's at the core of the processing model of XSLT (1.0) - current node list, current node in the former, matching rule, and substitution into a result node list - and/or, although probably more loosely, of Turchin's Refal.

Have you heard about the latter?

By Cyril at Wed, 2023-03-08 04:42 | login or register to post comments

You're right

You're right, it is very similar to XSLT, only that it operates on s-exprs instead of XML.

I've heard of Refal (just reminded myself a bit), and you're right again - it is similar to Refal too.

After decades of coding in imperative languages, I find it a bit hard to wrap my head around rules that systematically apply similar to math formulas instead of step-by-step instruction flow. But I guess this is how theorem proving works, and I'm not sure if there is an alternative solution for theorem proving.

By Ivan V. at Sun, 2023-03-12 10:11 | login or register to post comments

The problem with term

The problem with term rewriting systems is that they tend to exhibit combinatorial explosion, so we have to be very careful when composing rewrite rules. And it is very easy to enter an infinite recursion (if constructs may help to avoid the recursion).

By Ivan V. at Sun, 2023-03-12 13:51 | login or register to post comments

Infinite recursions are evitable

edit: double post removed.

By Ray Dillinger at Mon, 2023-03-20 16:25 | login or register to post comments

Most Infinite recursions are evitable with ony a small effort

In RETE driven inference systems, I usually coded the rewrite/inference rules to execute if and only if the inferred term was NOT already in the set.

This doesn't prevent all infinite recursions, especially if reasoning about what a system knows (I know THIS, and now I know that I KNOW this, and now I know that I KNOW that I know this, etc, and each loop is entering a slightly different inferred truth into the set), but it does avoid most of the elementary ones.

By Ray Dillinger at Mon, 2023-03-20 16:28 | login or register to post comments

Gödel's incompleteness

I subjectively suspect that unavoidable infinite recursion is, if not the only one, then among a few examples because of which Gödel's incompleteness theorems hold. I have the same hunch for the Halting problem.

By Ivan V. at Sun, 2023-04-23 09:37 | login or register to post comments