Lambda the Ultimate

Suppose you are defining a language based on the lambda calculus, and for some reason you must have strict data constructors. Are there any compelling reasons to have non-strict application?

What book should I buy to get a foundation for following the discussions at lambda-the-ultimate.org? I often feel there's some theoretical stuff I'm missing to fully follow the discussions. Ps. I'm not looking for a 800 page bible.. Something slightly more easy to approach maybe..

thanks in advance!

In nearly every semantics paper I've seen - notably not Plotkin's Call-by-Name, Call-by Value and the Lambda Calculus - the semantics obtains a fresh variable name by simply declaring "x fresh". It's almost a joke, actually. The names come from a countable set, so they're practically inexhaustible, and we know we could either thread a counter (aka gensyms) or examine some term to find the lexically greatest and choose the next one. So we smirk and just write "x fresh".

This week, I decided to write the beta-substitution metafunction for an operational semantics, making sure every operation was explicitly defined. According to Plotkin, I can take a new name from the set of all names that aren't free in both the expression being substituted in, N, and the expression being substituted, M. Then I realized, because of how I defined the language, that either N or M could contain every name as a free variable!

The language contains infinite terms. It's a theoretical device, not intended to be implemented. An example of an expression that uses every name is the set of functions N = {(lambda x1 . x0), (lambda x0 . x1), (lambda x3 . x2), (lambda x2 . x3), ...}. If X = {x0, x1, x2, x3, ...} is the set of variable names, every name in X is free in N.

I might be able to find a tricky way around this or prove that it never happens (under some reasonable conditions). But I've settled on using De Bruijn indexes instead of names.

Here are my questions: Has anybody run out of variable names or heard of running out of variable names before? What did you or the other person do about it?

EDIT: I'm softening the question. Has "x fresh" ever not worked for you, for whatever reason?

EDIT (again): I'm not necessarily looking for new solutions, because I think I have a really good one. I'm looking more for analogies - other experience I can cite when I write about this. I also want to know whether this "x fresh doesn't work" problem is new.