Tags:base conversion, numeric bases and term rewriting
Abstract:
We introduce and discuss a term-rewriting technique to convert numbers from any numeric base to any other one without explicitely appealing to division. The rewrite system is purely local and conversion has a quadratic complexity, matching the one of the standard base-conversion algorithm. We prove confluence and termination, and give an implementation and benchmarks in the Dedukti type checker. This work extends and generalizes a previous work by Delahaye, published in a vulgarization scientific review.