12

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

I've searched Google and various places on StackOverflow/StackExchange for the answer with no luck. The closest I've found was this conversation about Idris: https://groups.google.com/forum/#!topic/idris-lang/yp7vrspChRg

Unfortunately, that discussion is a little over my head.

Improve this question
14
  • 3
    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.
    – gardenhead
    Sep 26, 2016 at 20:37
  • 4
    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
  • 2
    @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".
    – Tanner Swett
    Sep 26, 2016 at 23:16
  • 2
    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.
    – Tanner Swett
    Sep 27, 2016 at 0:56
  • 2
    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.
    – gallais
    Sep 27, 2016 at 8:07

1 Answer 1

Reset to default
3

For certain functions it is. Especially when you know the function ;-)

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.

So if that is not the answer you were looking for, write a better question, currently it is pretty unclear what exactly you are really looking for.

Improve this answer
2
  • Thanks for the answer. The ability to "decide automatically" was exactly what I was looking for.
    – bmaddy
    Oct 28, 2016 at 12:08
  • 2
    To expand on the 'for certain functions it is' statement: Idempotency can be proven for any function that either only accepts a finite amount of inputs (by trying out all of them), or a type of input that is defined recursively (like natural numbers, or linked lists), which means that you only need to prove that the idempotency is true for the base case(es) and the recursive case(es).
    – Qqwy
    Jan 2, 2017 at 21:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.