# Is it possible to prove a function is idempotent?

Is it possible to use static or dependent types to prove a function is idempotent?

Unfortunately, that discussion is a little over my head.

• I'm not posting this as an answer because I'm not 100% sure, but I believe this is impossible due to Rice's Theorem. Sep 26, 2016 at 20:37
• This is a fascinating question, and my intuition indicates this should be possible in a restricted, non-Turing-complete language. However, Programmers focusses on questions regarding the software development life cycle (see out help center for details), whereas this seems to be a computer science question. The Computer Science site may be a better fit and lead to better answers.
– amon
Sep 26, 2016 at 20:58
• @gardenhead Rice's theorem states that given any property that the behavior of a program could have, it's sometimes impossible to determine whether or not a program has that property. There's a big difference between "this is sometimes impossible" and "this is impossible". Sep 26, 2016 at 23:16
• My last comment was pretty vague. In any case, here's what Rice's theorem has to say: there is no algorithm which correctly classifies all functions as being idempotent or not idempotent. However, there are still useful algorithms which classify some functions as being idempotent or not. Sep 27, 2016 at 0:56
• The OP asked about proving that a function is idempotent, not having an algorithm classify functions as idemptotent or not. The main difference being that a proof can be written by a person. As for Turing completeness, it is indeed not a problem. Sep 27, 2016 at 8:07

If you mean by your question "is there an algorithm to decide automatically if an arbitrary function is idempotent or not", the answer is no, due to the theorems already mentioned in the comments. However, for specific classes of functions, one can - in theory - very easily decide if the function is idempotent or not. For example, if the function is pure (means: without any side effects), and one knows it always returns a value in a finite amount of time for any given input, then idempotency can be decided simply by trying out if `f(f(x))=f(x)` for any possible input `x` to the function. Not that this will be very efficient, it could run until the end of the universe.