There is one more way to make sure that variables do not stand of bottom -- make sure that you only write terminating functions. Then the equational theory for

There is one more way to make sure that variables do not stand of bottom -- make sure that you only write terminating functions. Then the equational theory for strict and lazy evaluation becomes the same. I think this is the main reason that people don't worry too much about bottom: in practice all functions should terminate anyway. If your program gets stuck in an infinite loop, you probably have bug.