Consider the language of stored binary trees:

Design the -->gc reduction relation, which implements garbage collection. The -->gc reduction relation operates on a configuration that combines the store Σ, a set of “gray” addresses, i.e., σs) to be explored (the addresses of the initially reachable objects, also called roots, plus a set of “black” addresses (initially empty). Each step operates on one gray address, adjusting the gray and black sets based on the address’s value in the store. No more steps are possible when the set of gray addresses goes empty, at which point every address not in the black list can be pruned from the store.