I've seen two different lambda expressions for the logical NOT function.One of them just applies its parameter to constants true and false internally in a reverse order:$NOT \;\;=\;\; \lambda x.\; x \; \mbox{false}\; \mbox{true} \;\;=\;\; \lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t ) $and the other one which captures two more parameters instead of passing them to the returned function externally, and applies $x$ to them in reverse order too:$NOT \;\;=\;\; \lambda x. \; \lambda t.\lambda f.xft$of which the other one seems a bit simpler (and it is also simpler when encoded in binary).So my question is this:Is there any transformation which could get me from one of these representations to the other?I see they are equivalent extensionally, that is, both produce the same results. But I'd like to prove it somehow by algebraic transformations, such as those for alpha, beta and eta conversions. Unfortunately, none of these can help me in this case: Alpha is just for renaming. Beta works only for function calls, but we don't have any function call here which could be reduced, since $x$ is free in the function body (not the whole expression, though) in all these expressions until we actually call NOT on something. The most close one seems to be the eta, which is related to extensional equivalence and forwarding parameters, but when the parameters are being reversed, it's not a simple forwarding anymore and eta doesn't seem to apply here.Is there any more conversion rule I'm missing?(Well, I guess they won't just skip two Greek letters from no particular reason, wouldn't they?)P.S.: This question is actually a model one, since there are many other definitions for other functions which have several different forms which seem to be extensionally equivalent, but completely different with regard to the known reduction rules. I've chosen the simplest example of this problem.Edit:To better clarify what I'd like to know, here's a diagram showing the reduction steps for both versions of the not function:http://sasq.comyr.com/Stuff/Lambda/Not.pngAs you can see, they really both reduce to the same results (contrary to what @Jonathan Gallagher was saying below). This is what I already know: that they are confluent, and so they're Church-Rosser equivalent. What I don't know however is if there is any conversion rule (similar to alpha, beta & eta) which could allow me to transform one form of not to the other. This would allow me to at least make sure if some other functions (more complicated than these two here), are also equivalent, which could be hard when they can reduce to more than just two possible answers. I'd like to know if there's some conversion rule which could allow me to convert one intensional definition into another when two functions are already extensionally equivalent (i.e. they give the same results for the same parameters). Or (which would be better) if some function can be converted somehow to the other even if I don't know whether they're extensionally equivalent.
Equivalence of two lambda expressions for NOT
lambda calculus