Undecidable definition of pure function?
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.