Gorogoa

Blog of the designer

Three years passed... when will this game be released?

Tricks in solving common programming problems

O(1)-space collision detection

At times, you need to detect for once whether a collision occurs. For example, you may need to enumerate a sequence$$ x_0,\ x_1=f(x_0),\ x_2=f(x_1),\ \dots,\ x_i=f(x_{i-1}),\ \dots $$until either a desired element is found or a cycle is detected. A naive method to detect a cycle requires storing all elements ever enumerated in a hash table. This method however would need to store the entire sequence in the worst case. Instead, you can utilize one of the cycle detection techniques to reduce the space to O(1) at the cost of possibly longer search time.

(more to come...)

Quantifier elimination

A theory has quantifier elimination if for every formula f of the theory, there exists another formula f' without quantifiers that is equivalent to it (modulo the theory).

A common technique to show that the validity of a theory is decidable is to show that the theory admits decidable quantifier elimination and then prove the decidability of quantifier-free sentences. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable.

Note that theories could be decidable yet not admit quantifier elimination. For example, Example: Nullstellensatz in ACF and DCF. On the other hand, whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations to ensure that it admits quantifier elimination.