Modal is a matrioshka language based on pattern-matching to rewrite trees

Here is a lecture explaining one specific use of this, writing a symbolic differentiator: https://youtu.be/_fXQ1SwKjDg

For perspective, one might look at the Natural Number Game, an introduction to mathematical proof using the language Lean 4:

https://adam.math.hhu.de/#/g/leanprover-community/NNG4

I recall the feeling, being one of many who "rediscovered" Gröbner bases. This is why one studies history, to recognize the taste when one is a turn away from new history:

There was a leap needed, to generalize Gaussian elimination and the Euclidean algorithm to their common ground of arbitrary polynomials. There's a further leap to noncommuting strings, and then there's typed trees, the "algebraic datatypes" foundation of languages like Haskell and Lean 4. To see term rewriting in these settings as a continuum, one needs to incorporate recursion, to understand how Schützenberger's notions of rational and algebraic languages apply.

The idea of a term ordering is too gnarly here (well past the interstellar frontier of "decideability") for anything besides human intuition or deep learning.

Nevertheless, one sees that term rewriting on typed trees can be the foundation of human thought. Deep learning, while impressive, struggles to simulate recursion using multiple layers. We are discovering exactly how fundamental recursion is to thought. A version of neural nets more closely based on a probability substrate of typed trees might more adeptly model thought.

Looks a bit like "Tcl from first principles".

Term rewriting is woefully overlooked, maybe because the paradigm is rather open-ended. Questions about fixed or variable arity, what rules to apply in what order, what kinds of pattern matching to support, can make the language very limited or intractably inefficient depending on the answer.

I like that Modal just rolls with Peano arithmetic rather than awkwardly bolting on numerics. It's impractical, but it doesn't have to be practical - this is an exploration of a concept

What's nice about rewriting as a concept is that bolt-on extensions to make things fast don't have to be awkward.

Built-in rules that take priority over user-defined ones, as well as special variables in Devine's implementation, allow us to gain back speed while retaining some idea of purity. We know these operations can be phrased in terms of rewrite rules, so let's shortcut them and use built-in arithmetic in place.

You'd never know the difference! There's also a lovely arithmetic library built by d6 that you may enjoy. It does arithmetic digit-by-digit, and they're continually improving it to run faster.

https://git.phial.org/d6/modal/raw/branch/d6/binary/arith.mo...