Two applications of analytic functors
We apply the theory of analytic functors to two topics related to theoretical computer science. One is a mathematical foundation of certain syntactic well-quasi-orders and well-orders appearing in graph theory, the theory of term rewriting systems, and proof theory. The other is a new verification of the Lagrange-Good inversion formula using several ideas appearing in semantics of lambda calculi, especially the relation between categorical traces and fixpoint operators. (C) 2002 Published by Elsevier Science B.V.
analytic functor lagrange-good inversion formula recursive path ordering