FOM: 55:Term Rewriting/Proof Theory

[Harvey Friedman]

This is the 55th in a series of self contained postings to fom covering a
wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM

This is a draft which strengthens the known connections between term
rewriting and proof theory. It is being checked over by the experts in this
matter in Europe. In the meantime, I post it here.

TERM REWRITING AND ORDINAL RECURSION
by
Harvey M. Friedman
Department of Mathematics
Ohio State University
August 4, 1999

ABSTRACT

The relationship between rewriting systems and proof theory has been
developing through work of Dershowitz, Weierman, Tezout, etcetera. The
ordinal LAMBDA = theta_capitalomega^omega(0) appears naturally in this
theory. However, the <LAMBDA recursive functions have not made a natural
appearance. We show that the length of termination in ordered rewriting
with respect to LPO is measured by the <LAMBDA recursive functions. Also
the problem of whether one ground term can be derived from another via
ordered rewriting with respect to LPO has complexity measured by the
<LAMBDA recursive functions.

1. BACKGROUND

An important connection between term rewriting and proof theory is through
a natural ordering on terms called the lexicographic path ordering. This
was first defined and used to prove an important termination theorem by N.
Dershowitz. We mostly follow the treatment of LPO and rewriting systems
given in:

Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge
University Press, 1998

but we modify the notation a bit for our purposes.

A signature Sigma is a finite set of function symbols, each with a
particular arity >= 0. Constant symbols are viewed as function symbols of
arity 0. An ordered signature is a signature together with a strict
ordering > on its elements. Let T(Sigma,V) be the set of terms built up
from Sigma and any variables x1,x2,... . It is always assumed that Sigma
contains no variables. Let T(Sigma) be the set of ground terms of
T(Sigma,V); i.e., those terms that do not contain variables.

A rewrite rule in T(Sigma,V) is an expression

l arrows r

where l,r are in T(Sigma,V), l is not a variable, and every variable in r
is a variable in l.

A term rewriting system R consists of a signature Sigma, and a finite set
of rewrite rules in T(Sigma,V).

We now discuss the implementation of a rewrite rule l arrows r in
T(Sigma,V). Let s,t in T(Sigma,V). We say that

s arrows* t

by

l arrows r

if and only if there is a way to obtain s from l by substituting terms for
variables in such a way that we obtain t from r by substituting terms for
variables in the same way. (Of course, we require that different
occurrences of the same variable be replaced by the same term).

An R-derivation consists of a finite or infinite sequence of terms
t1,t2,... in T(Sigma,V) of length 1 <= n <= infinity, such that for all 1
<= i < n, ti arrows* ti+1.

We say that R is terminating if and only if every R-derivation is finite.

Let Sigma be an ordered signature. We define the lexicographic path order
>lpo on T(Sigma,V) as follows. s >lpo t if and only if at least one of the
following holds:

1. t is a variable of s that is distinct from s. Otherwise, let s =
f(s1,...,sm) and t = g(t1,...,tn).
2. Some si is >=lpo t.
3. f > g and s is >lpo every tj.
4. f = g, s is >lpo every tj, and (s1,...,sm) >lpo (t1,...,tn) under the
lexicographic extension of >lpo to T(Sigma,V)^m = T(Sigma,V)^n.

This is a recursive definition of a strict order.

Dershowitz showed that by Kruskal's theorem, lpo on T(Sigma,V) is always a
well quasi ordering.

Dershowitz used this result to show the following. We say that R is lpo
decreasing if and only if every rewrite rule l arrows r of R obeys l >lpo
r. If R is lpo decreasing then R is terminating. The idea is that if s
arrows* t then s >lpo t.

It is known in the folklore (Diana Schmidt, Andreas Weierman,...) that the
ordinals of the lpo's on ground terms in the T(Sigma,V) approach the proof
theoretic ordinal of Kruskal's theorem, which is
theta_capitalomega^omega(0) = LAMBDA.

We wish to measure the lengths of termination. Let N be the set of all
positive integers. For any term t, we write #(t) for the depth of t. (This
is defined by induction, where the depth of constants are 0, and the depth
of F(t1,...,tn) is one more than the maximum of the depths of the t's). The
termination function of R is the function f:N into N where for n >= 0, f(n)
is the length of the longest R-derivation that begins with a term t with
#(t) <= n if there is a longest such; infinity otherwise. In case there are
no constant symbols, f(0) is 0.

By a finitely branching tree argument, if R is lpo decreasing then its
termination function is finitely valued.

What can we say about the termination functions of the lpo decreasing term
rewriting systems? It would seem that they should be cofinal in the <LAMBDA
recursive functions, as given by the Hardy hierarchy on LAMBDA. But
Weierman has shown that this is false. In fact, they are cofinal in the
<omega^omega^omega recursive functions, as given by the Hardy hierarchy on
omega^omega^omega.

2. LPO ORDERED REWRITING

By ordered rewriting with respect to LPO, we mean the following. Let R be a
term rewriting system in T(Sigma,V), where Sigma is ordered. An lpo
decreasing R-derivation is an R-derivation where each term is greater than
the next term under >lpo with respect to Sigma. Obviously, every lpo
decreasing R-derivation is finite.

We wish to measure the lengths of lpo decreasing derivations. The lpo
termination function of R is the function f:N into N where for n >= 0, f(n)
is the length of the longest lpo decreasing R-derivation that begins with a
term t with #(t) <= n if there is a longest such; infinity otherwise.

Using a finitely branching tree argument, we see that the lpo decreasing
termination function of R is finitely valued.

We now show that the lpo termination functions climb up the Hardy hierarchy
on LAMBDA.

The quickest way to see the upper bound - i.e., that every lpo decreasing
R-derivation function is <LAMBDA recursive - is to use proof theory.

THEOREM 2.1. Every max lpo termination function of every term rewriting
system is <LAMBDA recursive.

Proof: Simply observe that every lpo termination function of every term
rewriting system is a provably recursive function of ACA_0 plus Kruskal's
theorem for bounded valence. Therefore by Rathjen/Weierman

M. Rathjen, A. Weiermann: Proof-theoretic investigations on Kruskal's theorem.
Annals of Pure and Applied Logic 60 (1993) 49-88

it is a provably recursive function of pi-1-2-BI_0. And again by this
paper, it must be <LAMBDA recursive. QED.

3. LOWER BOUNDS FOR GROUND TERM REWRITING

In this section we consider the lpo termination functions of term rewriting
systems, where we allow only ground terms in the lpo decreasing
R-derivations. Thus the ground lpo termination function of R is the f:N
into N where for n >= 1, f(n) is the length of the longest lpo decreasing
R-derivation that begins with a ground term t with #(t) <= n that consists
entirely of ground terms. We will write R# for the ground lpo termination
function of R.

THEOREM 3.1. Let f:N into N be a <LAMBDA recursive function. There exists a
term rewriting system R such that R# is everywhere greater than f.

We will prove this result with the help of several lemmas.

LEMMA 3.2. Let Sigma be a finite set of function symbols. There is a term
rewriting system R and a primitive recursive function f:N into N such that
the following holds. For all t in T(Sigma) there exists a ground
R-derivation of t from 0 of any length >= f(#(t)).

Proof: Let F be a binary function symbol not in Sigma. For t1,...,tn in
T(Sigma union {F},V), we define F[t1,...,tn] inductively by F[t1] = t1,
F[t1,t2] = F(t1,t2), F[t1,...,tn+1] = F[F(t1,t2),t3,...,tn+1], n >= 2.

We start with the following rewrite rules:

x arrows x
0 arrows s

where s is a ground term in Sigma union {F,0} of depth <= 1.

Commutativity and associativity of F:

F(x,y) arrows F(y,x)
F(F(x,y),z) arrows F(x,F(y,z))
F(x,F(y,z)) arrows F(F(x,y),z)

Repetition:

F(x,y) arrows F[x,x,y,y]

Breakdown:

F(x,y) arrows x
F(x,y) arrows y

Buildup:

F[x1,...,xn] arrows G(x1,...,xn)

where n >= 1 and G is an n-ary element of Sigma union {F,0}.

By standard techniques, there is an R-derivation from F[t1,...,tn] to
F[t1',...,tn'], where t1',...,tn' is any permutation of t1,...,tn.

We can prove by induction on n >= 0 that for all listings of the ground
terms t1,...,tm in T(Sigma) of depth at most n without repetition, there is
an R-derivation from 0 to F[t1,...,tn]. And we can get obvious double
exponential bounds. QED

For n >= 0, let n* be the term S...S0, where there are exactly n S's.

LEMMA 3.3. Let g:N into N be primitive recursive. There is a term rewriting
system R' such that for all n >= 1, there is a ground R'-derivation from
F(n*,n*) to F(0,0) of length at least g(n), with all terms of the form
F(m*,r*), where the pairs lexicographically decrease.

Proof: Use the following rewrite rules. F(0,x) arrows SSx. F(Sx,0) arrows
SS0. F(Sx,Sy) arrows F(x,F(Sx,y)). This is a version of the Ackerman
function. QED

LEMMA 3.4. Let g:N into N be primitive recursive and Sigma be given
containing 0,S, and let G be a new 4-ary function symbol. There is a term
rewriting system R'' such that the following holds. Let t1 >lpo t2 >lpo ...
>lpo tn be ground terms in T(Sigma), where #(ti+1) <= g(#(ti)). There is an
lpo decreasing ground R''-derivation of length n starting with
G(t1,F(#(t1)*,#(t1)*),0,0). Here lpo is with respect to any strict order on
the symbols used for which G is the strict maximum.

Proof: Let g,Sigma,G be as given. Let R be a term rewriting system and f:N
into N be a primitive recursive function according to Lemma 3.2. We may
assume that g >= f everywhere and G is not used in R. Let R' be as given by
Lemma 3.4, where G is not used in R'.

Before defining the required term rewriting system R'', we informally
describe the R''-derivation of length n starting with
G(t1,F(#(t1)*,#(t1)*),0,0).

First we go from G(t1,F(#(t1)*,#(t1)*),0,0) to G(t1,F(0,0),t2,#(t2)*). Each
intermediate term is of the form G(t1,F(m*,p*),s,j*). The second terms,
F(m*,p*), go from F(#(t1)*, #(t1)*) to F(0,0) of length at least g(#(t1))
>= #(t2), using R', with lexicographically decreasing pairs. The third
terms go from 0 to t2 using R. The fourth terms go from 0* = 0 to #(t2)*. G
will appear only in outermost position.

Then we go from G(t2,F(#(t2)*,#(t2)*),0,0) to G(t2,F(0,0),t3,#(t3)*). Each
intermediate term is of the form G(t2,F(m*,p*),s,j*). The second terms,
F(m*,p*), go from F(#(t2)*,#(t2)*) to F(0,0) of length at least g(#(t2)),
using R', with lexicographically decreasing pairs. The third terms go from
0 to t2 using R. The fourth terms go from 0* = 0 to #(t3)*. G will appear
only in outermost position.

We can continue in this way n-1 times, ending with
G(tn-1,F(0,0),tn,#(tn)*). Thus we view this construction as consisting of
n-1 blocks. To accomodate the moves in each block, we use the rewrite rules

G(x,s,t,y) arrows G(x,s',t',y)
G(x,s,t,y) arrows G(x,s',t',Sy)

where s arrows s' is a rewrite rule in R' and t arrows t' is a rewrite rule
in R. Here we disjointify the variables so that the rules from R' and R are
used independently.

To accomodate the starting of a new block, we use the rewrite rule

G(x,y,z,w) arrows G(z,F(w,w),0,0).

QED

LEMMA 3.5. Let Sigma be an ordered signature. There exists a linearly
ordered signature Sigma' extending Sigma such that the following holds. Let
f:N into N be a primitive descent recursive function on lpo with respect to
Sigma'. There exists a term rewriting system R in T(Sigma,V) such that R#
is everywhere greater than f.

Proof: Immediate from Lemma 3.4. QED

To complete the proof of Theorem 3.1, we need only show that the primitive
descent recursive functions on the linearly ordered lpo's are cofinal in
the <LAMBDA recursive functions. This is clear from any reasonable proof of
the folklore result that the ordered types of the linearly ordered lpo's
climb up to LAMBDA. For the sake of completeness, we give such a treatment
here.

Here is a presentation of a particularly simple sequence of ordinal
notation systems cofinal in LAMBDA. They are easily viewed as fragments of
the usual Feferman/Aczel notation system.

Let n >= 1. Define Fn:capitalomega^n into capitalomega as follows.
Fn(alpha1,...,alphan) is the least power of omega, lambda, such that

i) lambda > alpha1,...,alphan;
ii) for all beta1,...,betan < lambda, if (beta1,...,betan) is
lexicographically less than (alpha1,...,alphn) then Fn(beta1,...,betan) <
lambda.

LEMMA 3.6. For n >= 1, let LAMBDAn be the least ordinal such that Fn maps
LAMBDAn into LAMBDAn. LAMBDAn is generated by Fn,0,+.

We can obviously order the terms over Fn,0,+ by ordering according to their
evaluation as ordinals.

The normal terms over Fn,0,+ are the terms generated by the clauses

a) 0 is a normal term;
b) if k >= 2 and t1,...,tk are normal terms each of which start with Fn,
and t1 >= ... >= tk, then t1 + ... + tk is a normal term;
c) if t1,...,tn are normal terms then Fn(t1,...,tn) is a normal term.

LEMMA 3.7. For n >= 1, every ordinal < LAMBDAn is given by a unique normal
term over Fn,0,+.

Note that we are using + as a function symbol of indefinite arity. We now
wish to use + only as a binary function symbol. Obviously every normal term
over Fn,0,+ can be converted into a term where + is used only as a binary
function symbol by left associating any use of +. We call these the binary
normal terms over Fn,0,+.

LEMMA 3.8. For n >= 1, the ordering on the binary normal terms over Fn,0,+
is the same as lpo restricted to the binary normal terms over Fn,0,+ with
respect to the ordering 0 < + < Fn.

The Hardy hierarchy on LAMBDA are defined in terms of fundamental
sequences, but depend only on certain minimal properties of these
fundamental sequences. An equivalent way of treating the <LAMBDA recursive
functions is in terms of elementary descent recursive functions. This is
the approach taken in

H. Friedman and M. Sheard, Elementary descent recursion and proof theory,
Annals of Pure and Applied Logic 71 (1995), 1-45.

Along the lines of this treatment, let E(m,x) be an exponential stack of
2's of height m >= 0 with x >= 0 put on top. Thus E(0,x) = x and E(1,x) =
2^x.

For each n >= 1 we associate the function gn:omegaxomega into omega defined
as follows. gn(m,0) = the greatest binary normal term t over Fn,0,+ with
#(t) <= E(m,0). gn(m,p+1) = the greatest binary normal term t < gn(m,p)
over Fn,0,+ with #(t) <= E(m,p+1), provided gn(m,p) is not 0; 0 otherwise.

And for each n >= 1, we associate the function hn:omega into omega, where
hn(m) is the least p such that gn(m,p) is 0.

Then according to considerations in Friedman/Sheard, we see that the
functions hn are cofinal in the <LAMBDA recursive functions as given by the
Hardy hierarchy.

4. LPO GROUND DERIVATION PROBLEM

The lpo ground derivation problem is as follows.
GIVEN: A rewriting system R on T(Sigma), where Sigma is strictly ordered.
Two terms s,t in T(Sigma).
DETERMINE: Is there an lpo decreasing ground R-derivation from s to t?

It is clear from the previous discussion that for each R, this problem is
<LAMBDA recursive. The uniform problem is, in an appropriate sense, LAMBDA
recursive. We now show that for each <LAMBDA recursive function f, there
exists R such that this problem for R is not in time complexity <= f. As a
consequence, the uniform problem is not <LAMBDA recursive.

LEMMA 4.1. Let f:N into N be recursive. There is a term rewriting system R
with signature Sigma containing 0 such that the following problem cannot be
solved with time complexity <= cf(dn), for any positive integer constants
c,d. GIVEN: t in T(Sigma). DETERMINE: Is there a ground R-derivation from t
to 0. Furthermore, if the answer is yes then there is such a derivation of
length primitive recursive in #(t) and f.

Proof: We refer to the encoding of Turing machines into term rewriting
systems such as in Baader/Nipkow. We can choose R whose Sigma contains 0,S,
based on the action of a specific Turing machine TM, such that the
following holds.

i) For all t in T(Sigma) representing an initial instantaneous tape
description, all terms in all R-derivations starting with t mention S and
represent the instantaneous tape descriptions according to the action of TM;
ii) For all t in T(Sigma) representing an initial instantaneous tape
description, the problem of whether there is an R-derivation from t to a
term representing an instantaneous tape description for which no quadruple
applies, is not of time complexity <= cf(dn), for any positive integer
constants c,d;
iii) If the answer is yes then there is such a derivation of length
primitive recursive in #(t) and f.

We can then add rewrite rules which introduces a new poisonous constant
symbol c when applied to a term representing an instantaneous tape
description for which no quadruple applies, which can continue to swallow
up everything surrounding it to finally obtain c alone, and with a final
rewrite rule, c arrows 0, allowing 0 to be derived. There will be no other
way to derive 0. QED

THEOREM 4.2. Let f:N into N be <LAMBDA recursive. There is a term rewriting
system R* such that the lpo ground derivation problem is not of time
complexity <= f.

Proof: Fix f and let R,Sigma be as given by Lemma 4.1. The upper bound of
lengths of derivations is obviously <LAMBDA recursive. Choose a rewriting
system R' according to Theorem 3.1 whose lpo decreasing termination
function is sufficiently large. Then R and R' can be combined
lexicographically in the obvious way to create the desired R*. We lpo
decrease with R at the same time we go up/down with R'. We can arrange
things so that the part going down with R always can stabilize with all
zeros. So the suitably hard problem is whether we can get to all zeros
using (R,R') = R*. QED