Algebra of constructions. I. The word problem for partial algebras (Q1107515)

The paper presents an algebraic approach to abstract computing systems based on the lambda-calculus and cartesian closed categories. First, axioms of cartesian closed categories are formalized using the language of partial equational logic. Then, constructions of certain categories from words are presented, where partial operations are computable functions. A general formulation of the word problem for a theory in partial equational logic is provided, and the notions of a normal system and an algebra of constructions are defined. Decidability of the word problem for cartesian closed categories is proven in a new way, based on a construction of a normal system which is a recursive partial algebra as a free model of the theory of cartesian closed categories.