Suppose I have a basic mathematical function like:
$ f(x) = x^2 + 2$
implemented in typed pseudo-code as:
int f(x) {
return x*x + 2;
}
If we were to break out this procedure into a step-by-step sequence of actions, we have the following:
f: procedure(int x) returns int:
set int(temp) as multiply(x, x);
set int(temp2) as add(x, int(2));
set int(return-value) as temp2;
return;
However, say we have an equivalent "function" that is not a procedure but is equivalent in functionality (as in, it describes the same mutations, just differently--by structure):
f: function(int x) returns int:
define(return-value
add(
2
multiply(
x
x
)
)
)
This is essentially a mathematical expression written as a tree of operators and operands, Lisp-style.
It is very clear that the two are equivalent and describe the same mathematical expression: one by procedure, and the other, by structure/definition.
But why is it possible to know the two are equivalent? This mapping between procedure and functional is not always very clear. For even this pair of constructs, they are not equivalent simple "because they are." There must exist some sort of algorithm or procedure to describe how to map a procedure to a function (and, hopefully, not simply enumerating all of the possible values of output from a procedure and comparing it to a function).
Now, suppose we have a procedure as such:
g: procedure(Vector<{int red, int blue, int green}> screen,
Vector<{int red, int blue, int green}> buffer) returns void:
for-each {int, int, int} pixel, screen-pixel in buffer, screen:
copy screen-pixel into pixel;
return;
Is there a system in which a structural/functional equivalent for $g$ can exist?
Generally; for a set of procedures, does there exist a system in which each procedure has a functional/structural equivalent?
Semantics-wise, we usually know what a string of actions/instructions coupled with a set of data will do. For example, for-each
will usually loop over a set of data performing some sort of sequences of instructions for each element in a set. However, the actual implementation of for-each
can often differ, which means that proving that several implementations are equivalent in functionality can be non-trivial unless there is a universal way of mapping several procedures to their functional/structural form that all exist in a common system.
Generalized, if every procedure has a structural equivalent that share a common system for description, it may be possible to compare each procedure by value and then prove each are equivalent to a single function or not. This is the justification for why I am asking this question.