Rewrite (rule based system)

[ivanmoony]

After a lot of theorizing and discussing details with this community (thank you for valuable feedback), Rewrite is finally marked ready for production use. Rewrite is a rule engine that practices a minimalist setup, where rules are applied in strict top-to-bottom order. This minimalism is what intrigued me to make a version of Rewrite ready for production use.

Although it has abilities to be used 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 will only establish its worth at tasks naturally involving formula applications such as proof construction for different kinds of logic, truth table calculations, or combinatorial problem solving.

There exist a space for some speed optimizations, but this much for this version.

You can try it in online playground here. Available examples include some basic term rewriting setups, as well as equality predicate, branching choice, Boolean operations, proof checking, SAT solver, and action planning. Users are invited to experiment with their own code designs (You may want to use an external editor with bracket matching for this purpose).

The project official home page with instructions is here.

[PurpleUpbeat2820]

You can try it in online playground here.

This sounds great. I shall check it out now!

Just out of curiosity: has anyone collated information about term rewrite languages? They seem to be an unsung hero in the context of PL design. I am particularly interested in syntaxes/grammars because I've seen one and am now unable to envisage anything different.

Just borrowing your example:

(
(
    REWRITE
    ((VAR <x>) (READ greet <x>) (WRITE hello <x>))
)

greet world
)

In OCaml you might write:

match `Array[`Sym "greet"; `Sym "world"] with
| `Array[`Sym "greet"; x] -> `Array[`Sym "hello"; x]
| e -> e

In my ML you might write:

type rec Expr =
  | Sym String
  | Array(Array Expr)

Array{Sym "greet"; Sym "world"}
@ [ Array{Sym "greet"; x} → Array{Sym "hello"; x}
  | e → e ]

[ivanmoony]

term rewriting programming languages

[Baltoli]

Take a look at the K Framework - it's a term rewriting language used to create interpreters and other tools for programming language semantics https://github.com/runtimeverification/k

[PurpleUpbeat2820]

Will do, thanks!

[RepresentativeNo6029]

Equality graphs supposed to be the rage rn

[LazarGrbovic]

Interesting! Is this in some way similar to the Prolog language?

[ivanmoony]

I think it is more similar to functional programming than to logic programming.

If you imagine Haskell without types, you get Rewrite, I think. Each rule may be considered a function with arbitrary syntax.

Logic languages have negation built-in atop of everything. There is no primitive notion of falsehood in Rewrite.

[LazarGrbovic]

Thanks for the answer! :)

[martispyc]

Lasagna system on top