The recursive equations are the means by which you obtain a mapping from one ___domain to the other (eg. from the programming symbols to the program values). For equations there are many ways in which you can give meaning to each equation in the same way, such that the mechanical process makes sense.
For example:
a x = b (text) --> x is unknown, it is the right one if f(x) = a x equals f'(x) = b; both functions are programs you can compute and play with
from there you go mechanically to:
x = b/a (text) --> x is unknown, it is the right one if f(x) = x equals f'(x) = b/a
while in the first step it was hard to tell much about x, now we can see that it is trivial to guess which is the right x; x must be b/a
This is the first mapping from the ___domain of symbols to another ___domain that I could think of. There must be more natural mappings that can be used like this.
Check out abstract interpretation and Galois connections. These require a different kind of mechanical manipulations than simple algebra. I wonder if there is a gamification to be found in this direction.
For example:
a x = b (text) --> x is unknown, it is the right one if f(x) = a x equals f'(x) = b; both functions are programs you can compute and play with
from there you go mechanically to:
x = b/a (text) --> x is unknown, it is the right one if f(x) = x equals f'(x) = b/a
while in the first step it was hard to tell much about x, now we can see that it is trivial to guess which is the right x; x must be b/a
This is the first mapping from the ___domain of symbols to another ___domain that I could think of. There must be more natural mappings that can be used like this.