**Problem Detail:**

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 isimpureif

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

###### Asked By : minexew

#### Answered By : Gilles

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

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/42439

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback