7
$\begingroup$

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.png

As 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.

Improve this question
$\endgroup$
3
  • $\begingroup$ You won't be able to prove anything only on those two encoding of NOT, but the result you may want to prove would be something like : given $f$ a boolean lambda term, $NOT\ f\ true\ false$ should reduce to the same normal form, no matter which encoding of NOT you choose. $\endgroup$
    – Tpecatte
    Sep 17, 2013 at 8:55
  • $\begingroup$ Hmm, sooo... you suggest to use Church-Rosser Theorem to show confluence of both reductions? But doesn't it suggest that there could be some transformation involved? (maybe some which hasn't been discovered yet) $\endgroup$
    – SasQ
    Sep 17, 2013 at 17:47
  • $\begingroup$ I'm not sure there is any transformation involved, the confluence just means that the choice of not doesn't really matter. It's the same as Church integer, you can swap the two parameters to define integers, and both are valid and are equivalent in some way when "evaluated" but not equivalent using transformations. $\endgroup$
    – Tpecatte
    Sep 18, 2013 at 7:50

2 Answers 2

Reset to default
3
$\begingroup$

In order to prove the two NOT forms are not generally equivalent, all you have to do is find a term that when each is applied, returns a different result such as:

$NOT1 \; \lambda x.\; x \; \;\;=\;\; (\lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t )) \; \lambda x.\; x \;\; =\;\; \lambda x. \; x \; $

$NOT2 \; \lambda x.\; x \; \;\;=\;\; (\lambda x.\lambda t.\lambda f.xft) \; \lambda x.\; x\;\; =\;\; \lambda t.\lambda f. ft \; $

Improve this answer
$\endgroup$
-3
$\begingroup$

Let the first not be called not1 and the second not2. Then you have the following:

$$\mathsf{not1} \, M \to_\beta M \, \mathsf{false} \, \mathsf{true}$$ and $$\mathsf{not2} \, M \to_\beta \lambda t \, f . M \, f \, t \to_\eta \lambda t . M \, t \to_\eta M$$

Now, if we suppose that $$M = \mathsf{true}$$ then the top reduction would give us false while the bottom reduction would give us true -- so that making the identification would seem to give a strange result.

Improve this answer
$\endgroup$
4
  • $\begingroup$ That's because you've made an error. As far as I know, you cannot eta-reduce that way. $\mathsf{not2} \, M \to_\beta \lambda t \, f . M \, f \, t$ is OK, and this is the correct normal form until you know $M$. But this is not: $\lambda t \, f . M \, f \, t \to_\eta \lambda t . M \, t$; you cannot get rid of $\lambda f$ because it is not the last parameter in the subordinate function application. If you call the function reduced that way with the same parameters, it will return $M t$, which in turn will be called on the other parameter (formerly $f$), which gives $M t f$, not $M f t$. $\endgroup$
    – SasQ
    Sep 17, 2013 at 18:13
  • $\begingroup$ I believe you are incorrect. Eta is a rewrite so it must be a congruence -- closed under substitution and context. This should allow the reduction given. I can also do it the other way if you like. Set $S = \lambda f . M f)$. Then $\lambda t . S t \to^{\eta} S$ and then again, $\lambda f . M f \to^{\eta} M$. $\endgroup$
    – Jonathan Gallagher
    Sep 18, 2013 at 20:45
  • 1
    $\begingroup$ @JonathanGallagher: $\lambda t f . M f t$ should be read as $\lambda t . \lambda f . ((M f) t)$ and not as $\lambda t. (\lambda f . (M f)) t$. You got your parenheses wrong, which is why you think you can perform the $\eta$-reduction. $\endgroup$
    – Andrej Bauer
    Sep 19, 2013 at 13:10
  • $\begingroup$ Ah. I see. Thank you for the clarification. My response is incorrect. $\endgroup$
    – Jonathan Gallagher
    Sep 19, 2013 at 23:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.