Does every procedure have a structural equivalent?

Question

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.

Answer 1

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).

Answer 2

But why is it possible to know the two are equivalent?

In general, it is not. As soon as you use a Turing-complete language, deciding equivalence is undecidable; that's a direct consequence of Rice's Theorem.

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?

If every Turing-complete language, every program has infinitely many equivalents. That is a basic property of admissible numberings, a different way of formalizing Turing-completeness.

---

The answers differ, of course, if you consider less powerful models. I have yet to encounter a model of computation that has exactly one "program" per function it can represent; you an always add dead states or useless statements.