Does every procedure have a structural equivalent?

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 screen,
             Vector 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, `fo

Every procedure has a functional equivalent, but not a structural equivalent, going by contextual definitions of functional and structural equivalent based on your question.

That every procedure has a functional equivalent is part of the general result that all “reasonable” methods of defining computation result in the same definition of what is computable. This is the Turing thesis.

A model that is close to your definition of procedures is the RAM machine. It's also possible to define a model based more closely on imperative programming with variable names. Two models based on function calls are µ-recursive functions and the lambda calculus. Both of these models require more than the ability to call a function.

With µ-recursive functions, there is a way to iterate calls to a function (the primitive recursion operator) and a way to call functions recursively until a condition is reached (the minimisation operator). Think of the primitive recursion operator as for loops and of the minimisation operator as while loops (building a general while loop requires more than the minimisation operator because that operator extracts only a specific part of the functionality).

With the lambda calculus, functions can be defined and applied to other functions. This unbridled functionality allows building recursive functions and thus arbitrary computations.

All of these models of computation can be proved to be equivalent. I'll refer you to a textbook for a formal proof; I'll just give the intuition here. Given an imperative program, put all of its variables in a single structure. Where functions use local variables, make a chained list of structures. This way you end up with a single variable in your program. In functional programming, this is known as the world state. Now you can pass this single variable as an argument to all function calls and have the functions returned the modified world state. Express all loops and conditional statements using while, and change while (condition) do_stuff() to a recursive call to do_stuff that minimizes the number of iterations (that's where the primitive recursion and minimisation operators get combined). You no longer need any assignment operator! You've converted your imperative program to a recursive functional program.

This transformation lets you convert an imperative program into a functional one. However, it doesn't really help if what you wanted was to know whether your programs are equivalent, because there are many different ways to implement a particular mathematical function in any framework. It's a general result that functional equivalence (determining whether two programs compute the same result) is undecidable: there is no algorithms that given two programs always says (correctly) “yes, they're equivalent” or “no, they aren't equivalent”. This is a special case of Rice's theorem, which informally speaking says that any decidable property of algorithms that depends only on what the algorithm computes (i.e. the mathematical function that it implements) and not on how it computes it is either the property “true for all algorithms” or “false for all algorithms”. This theorem holds for any Turing-equivalent model of computation (because if there was a way to decide a property for programs written in one model, it could be transposed to any model simply by translating the programs).

StackExchange Computer Science Q#59557, answer score: 4