User loginNavigation 
Reference request: running out of countably many variable namesIn nearly every semantics paper I've seen  notably not Plotkin's CallbyName, Callby 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 betasubstitution 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. By Neil Toronto at 20110311 19:37  LtU Forum  previous forum topic  next forum topic  other blogs  4251 reads

Browse archivesActive forum topics 
Recent comments
2 hours 3 min ago
3 hours 21 min ago
4 hours 7 min ago
4 hours 30 min ago
4 hours 40 min ago
5 hours 39 min ago
6 hours 24 sec ago
7 hours 11 min ago
15 hours 45 min ago
16 hours 17 min ago