Recursion-closed algebraic theories

摘要

A class of algebraic theories called “recursion-closed,” which generalize the rational theories studied by J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B. Wright in [in “Proceedings, 17th IEEE Symposium on Foundations of Computer Science, Houston, Texas, October 1976,” pp. 147–158; in “Mathematical Foundations of Computer Science, 1978,” Lecture Notes in Computer Science, Vol. 64, Springer-Verlag, New York/Berlin, 1978; “Free Continuous Theories,” Technical Report RC 6906, IBM T. J. Watson Reserch Center, Yorktown Heights, N.Y., December 1977; “Notes on Algebraic Fundamentals for Theoretical Computer Science,” IBM Technical Report, 1979], is investigated. This work is motivated by the problem of providing the semantics of arbitrary polyadic recursion schemes in the framework of algebraic theories. It is suggested by Goguen et al. (“Proceedings, 17th IEEE Symposium”) that the semantics of arbitrary polyadic recursion schemes can be handled using algebraic theories. The results show that this is indeed the case, but that “rational theories” are insufficient and that it is necessary to introduce a new class of “recursion-closed” algebraic theories. This new class of algebraic theories, is defined and studied, and “free recursion-closed algebraic theories” are proved to exist.