Talk:Alpha-equivalence

From The Twelf Project

The definition is not correct. It's not enough to say that y is not a free variable of e. You must also have y free for x in e.

Not sure where you're taking issue here: a counterexample might be helpful, and you're welcome to edit the actual page to clarify if you'd like. Certainly it is the case that alpha equivalence is quite subtle, which is one of the reasons we like that Twelf takes care of all of it for us :-) — Rob (and his talk) 14:21, 27 February 2011 (EST)

The usual definition has the additional condition that y != x. Is that what you meant? Drl 22:46, 15 March 2011 (EDT)