Four Complete Datatype Defining Rewrite Systems for an Abstract Datatype of Natural Numbers
Jan Aldert Bergstra · Data Archiving and Networked Services (DANS) · 2014
Natural numbers with zero, one, successor, addition and multiplication, constitute a classic example of an abstract datatype amenable for equational initial algebra specification. Datatype defining rewrite systems provide a specification which at the same time is a complete, that is confluent and strongly terminating, rewrite system thereby providing means for automatic implementation. Syntax for unary, binary, decimal, and hexadecimal notation is introduced and corresponding rewrite systems are designed.