Cichon and Weiermann introduced the notion of term rewriting characterizations, a rewriting theoretic framework which allows the application of techniques from the field of rewriting in the study of recursive function theory. In this report we introduce the reader to the topic by reflecting the results and reasoning carried out in two papers by Isabelle Oitavem, leading to a characterization of PSPACE, the functions computable in polynomial space.

We present a rewrite system R that naturally models the functions in PSPACE. It is shown that every R reduction strategy yields an algorithm that runs in polynomial space. Therefore R exactly describes the functions in PSPACE.