Term rewriting and all that

confluence church rosser termination



[Bool] looks like maude has reflective reasoning

polymorphic operators. Huh

attributes memo - memozie the result otherwise attribute print

a matching equation

load reduce in MYMOD sort A. subsort A < B.

fmod MyNat is
    sort Nat .
    op zero : -> Nat .
    op s_ : Nat -> Nat .
    op _+_ : Nat Nat -> Nat .
    vars N M : Nat .
    eq zero + N = N .
    eq (s N) + M = s (N + M) .
endfm papers

Maude formal environment coherence, temrination, CETA library

full maude is a seperate library thing?

Debugger. That’s interesting. Have it pause at each action? Ematching quantifier logging done right

search command, that’s cool. Takes pattern Search types.

red in STRING : “hello” + “world”.

nonexec eq

ceq cmb commands for conditional equation and conditional membership We can easily enulate these.

(relation is-zero Zero)

I feel like catlab ought to be trivially encodable into this system Brutal.

Maude as a Library: An Efficient All-Purpose Programming Interface

Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework

frozenness. could frozen survive rebuilding? survive hash consing? 20 years of rewriting logic

Programming and symbolic computation in Maude 2020 Theorem Proving for Maude Specifications Using Lean

import maude
m = maude.getModule('NAT')
t = m.parseTerm('2 * 3')

Context-sensitive Rewriting Lucas

There is a sense that we’ve already screwed up context even before we’ve done anything equational just because of hash consing. Hash consing makes trees into dags and now terms are not in unique contexts. Context tagging is a way to undo or prevent work that hash consing does. Maybe rebuilding and hash consing are a kind of rewriting step and therefore may need to be activated only in certain circumstances

TPDB format for termination includes context sensitive anotations it affects termination, so that makes sense.

Memo - can mark terms as memo so they memoize the normal form they write to.

OPerator strategires - can mark which arguments must be evaluated before the total operator is evaluated. Functional modules only

Frozen - can mark whether whole subterms are frozen. Is this that different?

System modules vs functional modules. System modules specify concurrent rewrite systems. Functional modules are assumed church rosser and terminating

K instruction semantics for x86 in K intepreter, compiler, formal prover thing Systems to compare to according to them Redex, Maude, Spoofax, OTT, Rascal, ATL and model driven

popl : matching logic: foundations of K framework

Other Systems

Pure Obj ASF+SDF (superseced by Stratego and Rascal) ELAN (superseded by Tom ) mcrl2

Strategy Stratgo

PLT redex - context sensitive rewriting? term rewriting engine competiton rule engine competition benchamrks but it isn’t responding

dedukti term rewritng engine



String rewriting systems

Word problem Monoid presentation

Knuth Bendix

Termination termination problem database Termcomp 2022

Higher order rewriting


Gershom Bazerman on “Homological Computations for Term Rewriting Systems”