"Science aims to understand reality with as little ideology as possible" (Jorge Wagensberg).
"Mathematical knowledge is knowledge acquired by reason through the construction of concepts" (Kant).
Types of evaluations and reversibility
In MENTAL there is no complete reversible evaluation or computation, since no intermediate steps are recorded in the abstract space. However, there is a reversible evaluation mechanism associated with potential substitution and shape recognition.
The evaluation process is a "forward" process and is associated with the use of current or immediate type substitution expressions, e.g.,
(a = 3)
(b = 4)
(u = a+b) // ev. 7
(v = a*b) // ev. 12
(x = u+v) // ev. 7+12 ev. 19
Also, as we have seen, there can be deferred evaluation, e.g.,
(a = 3)
(b = 4)
(u = (a+b)°) // ev. (u = a+b)
(v = (a*b°)) // ev. (v = a*b)
(x = u+v) // ev. 7+12 ev. 19
However, when we use potential substitution, i.e., representation, the situation changes, producing the phenomenon of reversible evaluation, a "backward" process.
The simplest case is the following:
(x =: a) // x represents a
x // ev. x (x is self-evaluating but represents a)
a // ev. x (a evaluates as its representative, x)
There are really two types of evaluations:
External. It is the superficial, apparent evaluation, the one that appears externally.
Internal. It is the deep, real, true evaluation, the one used internally in the calculations.
When we use immediate substitution, the internal and external evaluation coincide.
When we indicate "ev." in the comment associated with an expression, we are referring to the external evaluation.
The above example, indicating the two types of evaluation:
(x° =: a) // x represents a
x // external ev.: x, internal ev.: a
a // external ev.: x, internal ev.: a
Another example:
(x =: u)
(u =: a)
x // external ev.: x, internal ev.: a
u // external ev.: x, internal ev.: a
a // external ev.: x, internal ev.: a
In the latter case, in the (external) evaluation of a, there are two backward jumps.
The internal evaluation of x, u and a is, in all three cases, the same: a.
Substitution type as parameter
In the following example, we use a parameter, p, to indicate the type of substitution we want to apply. Its value is : or the null expression θ.
(x =p u)°
(u =p a)°
(p = θ) // apply current or immediate substitution
x // ev. a
u // ev. a
a // ev. a
(p = :°) // apply potential substitution
x // ev. x
u // ev. x
a // ev. x
Shape recognition
Potential substitution makes it possible to recognize shapes, i.e. particular expressions corresponding to generic expressions. Examples:
⟨( f(x y) =: (x+yx*y) )⟩
(a+b a*b) // ev. f(a b) (recognizes the form)
(7 12) // self-evaluates (it is not possible, in this case, to go backwards)
⟨( g(x) =: (x xx xxx) )⟩
(1 11 111) // ev. g(1)
(a aa aaa) // ev. g(a)
(ab (ab ab ab) (ab ab ab)) // ev. g(ab)
There must be a direct potential substitution (parameterized or not) and not a process. For example, the sequence (a a a a a a) is not evaluated as a★4 because the definition of repetition is done by a recursive function.
Addendum
Reversible computing
The theory of reversible computing emerged at IBM in the early 1960s. Research has been ongoing ever since.
In practice, the implementation of reversible computing in a microprocessor has drawbacks:
It is a complex task, as it requires a profound modification of the processor design.
The performance is lower. To mitigate this, parallel processing would have to be greatly increased.
It requires more memory.
But it also has advantages:
It expands the possibilities of computation.
Intermediate computations can be reused.
Consumption is reduced, since the energy used in one calculation can be recaptured and reused in the next one, with the consequent lower heat dissipation. This is why reversible computing is also called "adiabatic computing".
The only company that, so far, has designed a reversible processor is Adiabatic Logic.
Bibliography
Bennet, Charles H. Logical Reversibility of Computation. IBM Journal of Research and Development, 17, 525, 1973.
Bennet, Charles H. Notes on the History of Reversible Computation. IBM Journal of Research and Development, 32 (1), 16, 1988.
Feynman, Richard P. Computación reversible y la termodinámica de la computación. Capítulo 5 de Conferencias sobre Computación. Crítica, Barcelona, 2003.
