Infinite sets in practice

We present a C++ library allowing computation over infinite sets. The programmer is able to represent infinite sets (in finite memory), as well as loop over them (in finite time). The elements of these sets can be "atoms" from some (usually infinite) structure, as well as integers (and other constants), pairs, tuples, and infinite sets of elements, allowing one to naturally implement the finite automata with atoms, for example. In theory, the system can be extended to work with any underlying structure, as long as its first order theory is decidable, and the iteration/recursion depth is bounded in the given program; currently, dense order, infinite random graph, and random tree theories are implemented. This work is partially based on ideas by Mikolaj Bojanczyk and Szymon Torunczyk.