Completing partial algebra models of term rewriting systems
Gabriela AslÄ± Rino Nesin
Abstract:
The study of partial algebras is the part of universal algebra which
deals with structures whose operations are not defined everywhere. A
natural question to ask if faced with a partial algebra is whether or
not it can be completed, i.e. embedded into a total algebra. If
furthermore we take partial algebras modelling a certain theory T ,
the question of finding a completion also modelling T may be very
hard, depending on the strength of T .
In this thesis we investigate a special case of the difficult problem
stated above. In particular, we show that partial algebras which model
an orthogonal term rewriting system and which satisfy a certain
condition on head-normal forms can be completed. Our result
generalizes a previous result by Inge Bethke, Jan Willem Klop and Roel
de Vrijer presented in [BKdV96]. In the process, we will prove an
abstract confluence theorem which is independent from our particular
choice of term rewriting system and therefore can be taken separately.
Our proof is preceded by a section on completions of partial algebras,
describing the construction of the one-point completion and free
completion of a given partial algebra, and showing the relations
between these completions in category-theoretic terms.