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  5884 reads

Browse archives
Active forum topics 
Recent comments
3 days 15 hours ago
3 days 19 hours ago
3 days 19 hours ago
22 weeks 5 days ago
26 weeks 6 days ago
28 weeks 4 days ago
28 weeks 4 days ago
31 weeks 1 day ago
35 weeks 6 days ago
35 weeks 6 days ago