Number representations and Term rewriting
Together with Tim Smit and Wijnand van Woerkom, I worked on term rewriting systems (TRSs) that model integers and integer arithmetic. These systems are more generally known as datatype defining rewrite systems [1] and are studied as formal notations of datatypes. Here, datatypes are canonical term algebras, which means that carriers are non-empty sets of closed terms which are closed under taking subterms. For those familiar with NLP grammars, this means that each non-terminal symbol is eventually rewritten to terminal symbols that are all defined within the system.
As an example of the power of such systems, only 19 rules can encompass an integer representation with addition and multiplication, regardless of n-ary view (binary, decimal, hexadecimal, …).
Our main contributions to the study of these rewriting systems were:
- Shortening of TRSs for the binary and decimal view (less rules used for the same expressiveness).
- Formulating an integer TRS that is independent of n-ary view.
- The development of tools to find new TRSs and to analyze certain system properties, such as confluence (a non-terminal must always eventually be rewritten to the same terminals).
- A graphical analysis of the rewrite rules.