Invariant (computer science)
||This article includes a list of references, related reading or external links, but its sources remain unclear because it lacks inline citations. (September 2010)|
In computer science, an invariant is a condition that can be relied upon to be true during execution of a program. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop.
Invariants are especially useful when reasoning about whether a computer program is correct. The theory of optimizing compilers, the methodology of design by contract, and formal methods for determining program correctness, all rely heavily on invariants in computer programs.
The MU puzzle is a good example of a logical problem where determining an invariant is useful. The puzzle is as follows:
- If a string ends with an I, a U may be appended (xI → xIU)
- Any string after an M may be completely duplicated (Mx → Mxx)
- Any three consecutive I's (III) may be replaced with a single U (xIIIy → xUy)
- Any two consecutive U's may be removed (xUUy → xy)
Is it possible to convert MI into MU using these four transformation rules only?
One could spend many hours applying these transformation rules to strings. However, it might be quicker to find a predicate that's invariant to all rules, and makes getting to MU impossible. Logically looking at the puzzle, the only way to get rid of any I's is to have three consecutive I's in the string. This makes the following invariant interesting to consider:
- The number of I's in the string is not a multiple of 3.
This is an invariant to the problem if for each of the transformation rules the following holds: if the invariant held before applying the rule, it will also hold after applying it. If we look at the net effect of applying the rules on the number of I's and U's we can see this actually is the case for all rules:
Rule #I's #U's Effect on invariant 1 +0 +1 Number of I's is unchanged. If the invariant held, it still does. 2 ×2 ×2 If n is not a multiple of 3, then 2×n isn't either. The invariant still holds. 3 −3 +1 If n is not a multiple of 3, n−3 isn't either. The invariant still holds. 4 +0 −2 Number of I's is unchanged. If the invariant held, it still does.
The table above shows clearly that the invariant holds for each of the possible transformation rules, which basically means that whichever rule we pick, at whatever state, if the number of I's was not a multiple of three before applying the rule, it won't be afterwards either.
Given that there is a single I in the starting string MI, and one is not a multiple of three, it's impossible to go from MI to MU as zero is a multiple of three.
See also 
- C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259 Download PDF
- J.D. Fokker, H. Zantema, S.D. Swierstra (1991). "Iteratie en invariatie", Programmeren en Correctheid. Academic Service. ISBN 90-6233-681-7.