Is it possible to add computational facilities to otherwise "mathematical" formal systems by adjoining identities to types?

Question

The following thought has been on my mind for years.

Think of $\mathbb{N}$ as the type of all well-formed expressions representing natural numbers. And think of $$\tilde{\mathbb{N}} := \frac{\mathbb{N}}{x \in \mathbb{N} \vdash x + 0 = x \mid x,y \in \mathbb{N} \vdash x + S(y) = S(x+y)}$$

as the type of all well-formed expressions representing natural numbers that have been put into normal form by repeatedly applying the identities in the denominator. There's functions $$\alpha : \mathbb{N} \rightarrow \tilde{\mathbb{N}}, \qquad \beta : \tilde{\mathbb{N}} \rightarrow \mathbb{N}$$ defined as follows: $\alpha$ turns an arbitrary well-formed expression of type $\mathbb{N}$ into a task for your computer to solve, in which the computer must repeatedly apply the rules until the expression is in normal form. And $\beta$ simply includes $\tilde{\mathbb{N}}$ into $\mathbb{N}$. To reduce an expression like $3 + 4$ to normal form, we can write $\beta(\alpha(3 + 4))$. This constructs the job $3 + 4$ for our computer (this is what $\alpha$ does), waits until the problem has been solved (this is just how the underlying computational framework operates), and then "forgets" the fact that it's now in normal form (this is what $\beta$ does). In this way, we compute $3 + 4 = 7$.

Of course, this makes no sense. You can't systematically compute $3 + 4 = 7$ without knowing a bit more. For example:

1. You also can't prove $3 + 4 = 7$ in this way without knowing $3$ is supposed to be replaced by its definition $S(S(S(0))),$ whereas $+$ is not supposed to be replaced by its definition, because after all, we're going to deal with $+$ using equations, not definitions.

2. You also can't prove $3 + 4 = 7$ unless you realize that the expression you've constructed, namely $S(S(S(S(S(S(S(0)))))))$, is supposed to be reported to the end-user as the numeral $7$.

As a result of not being able to address these issues, I find myself unable to see how one might start with a "mathematical" formal system and then adjoin computational facilities by allowing the end-user to "attach" identities to types, thereby constructing "computational types" that automatically reduce their terms to normal form.

Question. Is it possible to add computational facilities to mathematical formal systems by adjoining identities to types, and if so, how are issues (1) and (2) above addressed?

Answer 1

Algebraic theories (and their extensions) may be augmented by rewriting rules, like the ones you describe. For example, we could have a rule $$\frac{\vdash n : \mathbb N \quad \vdash m : \mathbb N}{\vdash \mathsf{s\text{-}add\text{-}cong} : \mathsf{add}(\mathsf{s}(n), m) \Rightarrow \mathsf{s}(\mathsf{add}(m, n))}$$ and so on. These are studied in rewriting theory. Note that, in general, rewriting systems specified in this way may not have unique normal forms for terms: this requires proof.

There are two straightforward solutions to the problems you raise (leaving aside the question of efficiency).

1. Either new nullary operators $3$, $4$ and $7$ can be introduced into the system, and rewrites $$\frac{}{\vdash \mathsf{3\text{-}def} : 3 \Rightarrow \mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{z})))}$$ introduced to give a canonical representation (though note that such a system will not be finitely axiomatisable). Alternatively, this can simply be treated as a parsing problem, with $3$ simply being a name for $\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{z})))$, which is used in the input language, but which the underlying rewriting system will have no knowledge of.
2. The system dealing with the rewriting system can have pretty-printing facilities to automatically convert certain terms into canonical representations, i.e. it would convert $\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{z})))$ to $3$ when outputting to a user. The rewriting system itself would have no knowledge of $3$.

Thus, we can separate the question of purely formal computation and the question of concrete syntax, rather than attempting to construct a system that handles both.