Concatenative languages lend themselves to rewriting because they do not bind variables and thus do not incur any confusion with renaming/scope (compositional rather than applicative).

Manfred von Thun has already written on this: there are algebraic laws for concatenative programming like the algebraic laws one has for e.g. groups (\(a \cdot 1 = a\)).

Some simple ones that do not need quotation:

`dip(f) dip(g) = dip(f g)`

`dip(+) + = + +`

(holds because \(+\) is associative; works on all other associative operations)`0 drop = id`

and so on for constants`swap swap = id`

`dup and = id`

`dup or = id`

`dup xor = False`

`swap * = *`

(holds because \( \cdot \) is commutative; works on all other commutative operations)`swap > = <`

(and so on for other operations that have reflect, such as \( > \)).`> not = <=`

(and so on)

I implemented the above lints in my own Kempe compiler. A linting pass is easily implemented with pattern matching one has in ML-style functional languages:

lintAtoms :: [Atom b b] -> Maybe (Warning b)
lintAtoms [] = Nothing
lintAtoms (a@(Dip l _):a'@Dip{}:_) = Just (DoubleDip l a a')
lintAtoms (a@(IntLit l _):(AtBuiltin _ Drop):_) = Just (PushDrop l a)
...