术语重写编程语言允许这样编写规则。术语重写语言将一组重写规则与应用它们的策略相结合。让我们尝试按照您在 Pure 中的建议实现反向，这是一个相当简单且易于访问的术语重写系统。
我们的第一次尝试将尝试反转一个列表，如下所示：
rev [] = [];
(rev (x:xs)) + m = (rev xs) + (x:m)
我们将尝试一些示例查询，反转空列表[]、单例列表[1]和包含 4 个元素的列表[1,2,3,4]。我们期望输出分别为[]、[1]和[4,3,2,1]。
> rev [];
[]
> rev [1];
rev [1]
> rev [1,2,3,4];
rev [1,2,3,4]
我们的第一个规则有效，但第二个规则从未应用。Pure有一个用于将列表连接在一起的内置规则，可能类似于：
xs + [] = xs; // Pure's prelude doesn't actually even include this.
[] + ys = ys;
(x:xs) + ys = x:(xs + ys);
但它的重写策略并没有探索如果将这些步骤中的每一个都颠倒过来会发生什么。为此，对于每个术语xs，都需要考虑可以将术语改写xs + []为xs! 相反，我们将告诉重写系统，当用 重写时rev，考虑附加一个空列表的反向列表是有用的。
rev [] = [];
(rev (x:xs)) + m = (rev xs) + (x:m);
rev (x:xs) = (rev (x:xs)) + [];
这甚至会破坏单个项目列表的堆栈。事实证明，我们的第三条规则一直被应用，直到堆栈溢出，而第二条规则从未停止它。
> rev [1];
<stdin>, line 2: unhandled exception 'stack_fault' while evaluating 'rev [1]'
我们将需要对评估策略进行更多控制。通过引入一个新符号 ，rev2我们可以阻止第三条规则匹配。这些规则与之前的规则相同，只是rev2程序的其余部分不需要看到 for 的规则。
rev [] = [];
rev (x:xs) = (rev2 (x:xs)) + [] with
(rev2 (x:xs)) + m = (rev xs) + (x:m);
end;
这可以正常工作，但没有按照我们的意愿进行评估。
> rev [];
[]
> rev [1];
[]+[1]
> rev [1,2,3,4];
[]+[4]+[3]+[2]+[1]
更糟糕的+是，左关联，所以这仍然有讨厌的n^2运行时间。那是因为，通过rev每次调用 inside rev2，我们每次都引入一个新的[]，并且只在[]. m总是[]。我们需要引用rev2inrev2以便规则可以直接应用于它自己的输出。当我们这样做时，rev2将需要它自己的规则来处理空列表，并且我们开始以一种不愉快的方式重复自己。
rev [] = [];
rev (x:xs) = (rev2 (x:xs)) + [] with
rev2 [] = [];
(rev2 (x:xs)) + m = (rev2 xs) + (x:m);
end;
我们现在得到了，几乎正是我们想要的：
> rev [];
[]
> rev [1];
[]+[1]
> rev [1,2,3,4];
[]+[4,3,2,1]
我们可以[]通过只为rev2.
rev xs = (rev2 xs) + [] with
(rev2 [] ) + m = m;
(rev2 (x:xs)) + m = (rev2 xs) + (x:m);
end;
这完美地工作：
> rev [];
[]
> rev [1];
[1]
> rev [1,2,3,4];
[4,3,2,1]
现在，我们可以更进一步，稍微清理一下我们的代码。由于涉及 rev2 的所有内容都有模式(rev2 a) + b，并且只有符号很重要，所以我们可以用更简单的形式替换该形式的所有内容，rev2 a b。
rev xs = rev2 xs [] with
rev2 [] m = m;
rev2 (x:xs) m = rev2 xs (x:m);
end;
这与您一开始试图避免的 Haskell 定义完全相同
rev xs = rev' xs [] where
rev' [] m = m
rev' (x:xs) m = rev' xs (x:m)