Undecidable definition of pure function?

I am trying to come up with a formal definition for functional purity in a simple programming language (think JavaScript). What I've got so far is this:


DEFINITION: A statement is impure if

• it is an assignment, unless it assigns to a local variable

• OR, it evaluates a call to a function, unless that function is pure

• OR, it is a block containing an impure statement

DEFINITION: A function is pure if it doesn't contain any impure statement.

For simplicity, let's ignore assignments altogether and assume that a block is simply an ordered set of statements. (it shouldn't make a difference)

Now, this definition seems to work great until somebody defines a function that refers to itself, e.g.

function fibonacci(n)  {
    if(n == 0)
        return 0;
    else if(n == 1)
        return 1;
    else
        return fibonacci(n - 1) + fibonacci(n - 2);
}

or

function f() { return g(); }
function g() { return f(); }

By the proposed definition, to prove that fibonacci is pure, you need to prove that fibonacci is pure. Similarly in the second example. Thus, the purity of fibonacci, f and g is undecidable, yet intuitively we know that all 3 of these are pure, so this definition must be flawed.

How would I modify this definition to be decidable (and give the intuitively expected answer) even in the presence of recursion?

This question refers to some definitions of functional purity, but they don't seem formal enough to be used as a base for further reasoning.

On undecidability

You attempt to prove that fibonacci is pure in a particular way, and you fail to do so. This does not prove that purity is an undecidable property. All it shows is that this particular way of determining the purity of fibonacci doesn't work.

A property is undecidable if no matter what method you use to calculate it, there is a parameter for which it fails. The possible methods are algorithms implemented on a Turing machine or any equivalent framework (recursive functions, etc.).

Purity is undecidable in general, but you need more language constructs than what you showed. For example, it is easy to reduce purity to halting, which is a well-known undecidable problem:

f;
global := 3;

This code is pure iff global := 3 is never executed, which is equivalent to saying that f doesn't terminate. So if you can decide purity, you can decide halting.

On recursive definitions

Your definition of purity is incomplete. You need to explain in more detail how to deal with recursive functions. To illustrate this, let's consider the following axioms for a property which I'll call cuteness:

• If A and B are cute then A; B is cute.

• If A, B and C are cute then if A then B else C is cute.

• If A, B1, …, Bn are cute then A(B1,…,Bn) is cute.

• +, -, == are cute.

Is fibonacci cute? If the list of axioms above is complete, then no, fibonacci is not cute, because a recursive function definition is not cute. All of the axioms above work if I replace “cute” by “terminating”, which shows that adding recursive functions to the mix can radically change the definition.

If I add the following axiom:

• If A is cute then function f () { A } is cute.

Then all cute functions are, in fact, pure in the sense of not having assignments as side effects. The axioms above in fact completely capture a strong notion of purity, i.e. if a function is pure then you can prove it using these axioms. The notion of purity defined here forbids all assignments, even if they don't escape their scope.

On defining purity

If you want to allow internal side effects, you need a more complex definition, with a context. Above all axioms were of the form “if these programs have the property then that program has the property too”. More complex properties need to consider programs in context, to describe the variables, types, memory locations, etc. used in the program. The following rules capture purity in a context which defines what variables are allowed to be modified:

• If A and B are pure in the context Γ then so is A; B.

• If A, B and C are pure in the context Γ then so is if A then B else C is cute.

• If A, B1, …, Bn are cute in the context Γ then so is A(B1,…,Bn).

• +, -, == are pure in any context.

• If A is pure in the context Γ then A is also pure in any superset of Γ.

• If A is pure in the context Γ, x1,…,xn then function f (x1,…,xn) { A } is pure in the context A.

• If A is pure in the context Γ then x := A is pure in the context Γ, x.

A better way to say “A is pure in the context Γ” might be “Γ captures all the side effects of A”. A program is pure if the empty context captures its side effects.

StackExchange Computer Science Q#42439, answer score: 6