Weiermann - Applications of Infinitary Proof Theory (1999).pdf

(335 KB) Pobierz
esslli-tex.dvi
Applications of innitary proof theory
Andreas Weiermann
Institut fur mathematische Logik und Grundlagenforschung
der Westfalischen Wilhelms-Universitat Munster
Einsteinstr. 62, D-48149 Munster, Germany
Summary
This paper consists of four chapters which can be read independently. In Chap-
ter 1 we introduce term rewriting theory for proving non trivial closure prop-
erties of the primitive recursive functions. In Chapter 2 we show that the
derivation lengths for a nite rewrite system for which termination has been
shown by using the lexicographic path ordering are multiple recursive. Chapter
3 provides a termination proof for T using an interpretation of Godel's system
T into the natural numbers. In Chapter 4 we give a simple characterization of
the provably recursive functions of PA.
1 Proving closure properties of the primitive re-
cursive functions via term rewriting
Abstract
The termination of rewrite systems for parameter recursion, simple
nested recursion and unnested multiple recursion is shown by using mono-
tone interpretations on the natural numbers. We show that the resulting
derivation lengths are primitive recursive. As a corollary we obtain trans-
parent and illuminating proofs of the facts that the schemata of parameter
recursion, simple nested recursion and unnested multiple recursion lead
from primitive recursive functions to primitive recursive functions.
1.1 Introduction
A recursive function f is commonly dened by a dening equation (or more
generally a system of equations) of the form
f ( x )= t ( ~y:f ( y ) ;x )
1
where t involves some previously dened recursive functions. The term rewriting
approach orients the dening equations into a rewrite system R f containing the
rule
f ( x )
!
t ( ~y:f ( y ) ;x )
together with some rules for other functions which appear in t . If the rewrite sys-
tem R f is confluent and terminating then R f yields a convenient model for non-
deterministic computations of f . The derivation lengths function, D R f , which
measures the maximal possible lengths of nondeterministic R f -computations,
and hence the maximal lengths of nondeterministic R f computations, then gives
some intrinsic information about the computational complexity of the original
recursive function f . For example, if D R f is bounded by a function in a com-
plexity class
C
which is closed under \elementary in" (hence under coding) then
. Furthermore, this will hold for any evaluation
strategy for f . Obviously, the latter point gives essential information concerning
the computational complexity of f . In particular, if
C
- TIME and so f is in
C
C
is the class of primitive
recursive functions then f is primitive recursive.
The emphasis of this chapter is on investigations of interesting properties of
primitive recursive functions. In our term rewriting approach, the dening
equations for the primitive recursive functions are oriented naturally into rewrite
rules according to the intended computation strategy. It is well known that such
a rewrite system, when it computes only nitely many functions, can be proved
terminating via the multiset path ordering. Hence, as shown by Hofbauer in [22],
the resulting derivation lengths are bounded by a primitive recursive function.
We concentrate on investigations on certain recursive denition schemata where
it is not immediately obvious that they lead from primitive recursive functions
to primitive recursive functions. In particular, we investigate the computa-
tional complexity of the rewrite systems for the schemata of parameter recur-
sion,
PRP
, simple nested recursion,
SNR
, and unnested multiple recursion,
UMR
. The characteristic recursion equations for these schemata are
PRP
: f ( S ( x ) ;y )= h ( x;y;f ( x;p ( x;y )))
SNR
: f ( S ( x ) ;y )= h ( x;y;f ( x;p ( x;y;f ( x;y ))))
UMR
: f ( S ( x ) ;S ( y )) = h ( x;y;f ( x;p ( x;y )) ;f ( S ( x ) ;y ))
whereinallthreecases h and p denote previously dened primitive recursive
functions.
These schemata gure prominently in the literature. That they do not lead
outside the class of primitive recursive functions has been proved, for example,
in Peter [31] or in Felscher [18] using coding techniques and by Feferman [17]
with elaborate proof-theoretic arguments. Simmons [40] has proved similar
results for strong generalisations of
PRP
and
SNR
.
2
f is in
1.2 Basic denitions
(i)
O
n denotes the number-theoretic function m 1 ;:::;m n 7!
0.
(ii) For each n
2
! and for each 1
i
n ,
P
i denotes the number-theoretic
function m 1 ;:::;m n 7!
m i .
(iii)
S
denotes the number-theoretic function m
7!
m +1.
(iv) If f is an m -ary function and if g 1 ;:::;g m are n -ary functions then
SUB
m;n ( f;g 1 ;:::;g m )
denotes the function
m 1 ;:::;m n 7!
f ( g 1 ( m 1 ;:::;m n ) ;:::;g m ( m 1 ;:::;m n )) :
(v) If g is any n -ary function and if h is an n + 2-ary function then
REC
n +1 ( g;h )
denotes the unique n + 1-ary function f which satises the following re-
cursion equations :
f (0 ;m 1 ;:::;m n )= g ( m 1 ;:::;m n )
f ( m +1 ;m 1 ;:::;m n )= h ( m 1 ;:::;m n ;m;f ( m;m 1 ;:::;m n ))
Denition 1.1 The set
PR
of primitive recursive functions is given by the
following inductive denition :
(i)
S2PR
.
(ii)
O
n
2PR
for every natural number n .
(iii)
P
i
2PR
for every natural number n .
(iv) If f
2PR
is an m -ary function and if g 1 ;:::;g m 2PR
are n -ary func-
tions then
SUB
m;n ( f;g 1 ;:::;g m )
2PR
.
(v) If g
2PR
is an n -ary function and h
2PR
is an n +2 -ary function then
REC
n +1 ( g;h )
2PR
.
Denition 1.2 For each natural number n we dene a set N n of primitive
recursive function symbols as follows :
(i) S 1 2
N 1 .
(ii) O n
2
N n .
3
(iii) P i
2
N n .
(iv) If f
2
N m and g 1 ;:::;g m 2
N n then SUB m;n ( f;g 1 ;:::;g m )
2
N n .
(v) If g
2
N n and h
2
N n +2 then REC n +1 ( g;h )
2
N n +1 .
We write 0 for O 0 and S for S 1 . Let N := S f
N n
j
n<!
g
.
Denition 1.3 For each f
2
N , we dene the complexity number of f ,comp ( f ) ,
as follows:
(i) comp ( S 1 ):=1 .
(ii) comp ( O n ):=1 .
(iii) comp ( P i ):=1 .
(iv) comp ( SUB m;n ( f;g 1 ;:::;g m )) :=
max
f
comp ( f ) ; comp ( g 1 ) ;:::; comp ( g m ) ;m;n
g
+2 .
(v) comp ( REC n +1 ( g;h )) := max
f
comp ( g ) ; comp ( h ) ;n
g
+2 .
Denition 1.4 Recursive denition of ( f )
2PR
for f
2
N .
(i) ( S 1 ):=
S
.
(ii) ( O n ):=
O
n .
i .
(iv) ( SUB m;n ( f;g 1 ;:::;g m )) :=
P
SUB
m;n (( f ) ; ( g 1 ) ;:::; ( g m )) .
(v) ( REC n +1 ( g;h )) :=
REC
n +1 (( g ) ; ( h )) .
Lemma 1.1 For every n -ary primitive recursive function f there exists a prim-
itive recursive function symbol g such that ( g )= f .
. An unravelling of this denition
yields the desired primitive recursive function symbol g in a canonical way.
PR
2
We assume familiarity with the basic notions of rewriting theory. For a suitable
overview see Dershowitz and Jouannaud [16].
Denition 1.5 We dene a set R PR of rewrite rules (for calculating primitive
recursive functions) over the signature N as follows :
(i) For n
1 , O n ( x 1 ;:::;x n )
! R PR 0 .
(ii) P i ( x 1 ;:::;x n )
! R PR x i (1
i
n ) .
4
(iii) ( P i ):=
Proof f is dened according to the rules of
! R PR
f ( g 1 ( x 1 ;:::;x n ) ;:::;g m ( x 1 ;:::;x n )) .
(iv) REC n +1 ( g;h )(0 ;x 1 ;:::;x n )
! R PR g ( x 1 ;:::;x n ) .
(v) REC n +1 ( g;h )( S ( x ) ;x 1 ;:::;x n )
! R PR
h ( x 1 ;:::;x n ;x; REC n +1 ( g;h )( x;x 1 ;:::;x n )) .
R PR models the denition schemata of the primitive recursive functions in a
natural way.
Denition 1.6 We dene a set R PRP of rewrite rules as follows.
(i) f (0 ;y )
! R PRP g ( y ) .
(ii) f ( S ( x ) ;y )
! R PRP h ( x;y;f ( x;p ( x;y ))) .
R PRP models the schema of primitive recursion with parameter substitution .
Denition 1.7 We dene a set R SNR of rewrite rules as follows.
(i) f (0 ;y )
! R SNR g ( y ) .
(ii) f ( S ( x ) ;y )
! R SNR h ( x;y;f ( x;p ( x;y;f ( x;y )))) .
R SNR models the schema of simple nested recursion .
Denition 1.8 We dene a set R UMR of rewrite rules as follows.
(i) f (0 ;y )
! R UMR g 1 ( y ) .
! R UMR g 2 ( x ) .
(iii) f ( S ( x ) ;S ( y ))
! R UMR h ( x;y;f ( x;p ( x;y )) ;f ( S ( x ) ;y )) .
R UMR models the schema of unnested multiple recursion (with parameter sub-
stitution) .
All of these schemata can be shown terminating using the lexicographic path or-
dering. This, however, does not give us a sucient information for proving that
they do not go outside the primitive recursive functions, for the lexicographic
path ordering also establishes the termination of the Ackermann function which
is well known for not being primitive recursive.
5
(iii) SUB m;n ( f;g 1 ;:::;g m )( x 1 ;:::;x n )
(ii) f ( x; 0)

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin