Redex long tutorial beta-eta equivalence is false

[samth]

Consider the following term in the language of Lambda from https://docs.racket-lang.org/redex/redex2015.html : ((lambda () ((lambda (x) 1))) 2). This term is not beta-equivalent to anything, because it's stuck. But it is eta-equivalent to ((lambda (x) 1) 2) which beta-reduces to 1. So the statement in the tutorial

The βη semantics is equivalent to the β variant. Formulate this theorem as a metafunction. Use redex-check to test your theorem.

is wrong.

This error was found by random testing, here: http://drdr.racket-lang.org/69138/racket/share/pkgs/redex-doc/redex/scribblings/long-tut/code/lab-tue-mor.rkt

[mfelleisen]

I thought we had found this problem before, some N years ago.

[samth]

There's a comment in the file saying that terms with duplicate variables falsify the theorem, but this is a different issue.

[rfindler]

I probably should have opened an issue, but there was a counterexample found around september 6th, 2022

> (term (theorem:eval-β=eval-βη ((lambda () ((lambda (c) 7))) K)))
#f

[rfindler]

If I'm reading over the email chain between me and Matthias correctly, the conclusion we came to is that n-ary lambda just doesn't work out and thus the right thing to do is to change the long tutorial to use unary lambda and application expressions. I think I dropped the ball at that point, however, ☹

[mfelleisen]

That’s precisely the conclusion we came to.

[samth]

I don't think just switching to unary functions is enough, you probably need to take out numbers as well. This term: ((lambda (z) z) (lambda (x) (5 x)))) is a counterexample to the equivalence of beta-eta and beta since it's beta-eta equivalent to 5, although the precise way the theorem is implemented in redex means it doesn't fail. Probably there's a way to make an actual counterexample with just numbers, though.

[mfelleisen]

Why don’t you try to get redex to fai?

[samth]

I'm not sure what you mean. Consider the following:

(define bad-term
  (term ((lambda (z) z) (lambda (x) (5 x)))))
(traces s-->β bad-term)
(traces s-->βη bad-term)
(traces -->βη bad-term)

The first traces call reduces the term to (lambda (x) (5 x)) whereas the second and third both reduce to 5. This demonstrates that the reduction relations are not the same, contrary to the statement I quoted.

However, the way the theorem is phrased uses a metafunction to implement the transitive closure of the reduction relation in a way that (I think) causes eta reduction never to be used, except in the wrong-arity cases that the bug report starts with.

Also, the definition of eta reduction omits the side condition that the bound variable of the lambda being eliminated can't be free in the term we reduce to, and thus you can get this kind of bad reduction, but again it can't be turned into a counterexample because of the way the theorem is phrased.

lab-tue-mor.rkt> (apply-reduction-relation -->βη (term (lambda (x) (x x))))
'(x)

[mfelleisen]

I am on my way to Germany w/o time to look at the statement. BUT, the Redex book clrearly distinguishes between _evaluation_ by standard reduction and _calculation_ by calculating. My hunch is that we used evaluation, which is why a meta-function is just okay. I can see why calculating wouldn’t work for a unary calculus. I’ll try to dig into this when I get back unless someone figures it out first.

[samth]

The Redex book part 1 stops having eta as soon as it gets to ISWIM, and doesn't ever have multi-argument functions, avoiding these problems. In fact footnote 2 (p49) says basically that we can't have eta any more because we've added numeric constants, which is exactly the problem here. Part 2 of the book starts with ISWIM and never mentions eta.

[rfindler]

However, the way the theorem is phrased uses a metafunction to implement the transitive closure of the reduction relation in a way that (I think) causes eta reduction never to be used, except in the wrong-arity cases that the bug report starts with.

Implicit in this, are you thinking that apply-reduction-relation is guaranteed to use the rules in order? I think it isn't promised to go in order, but it might be hard to get it to go out of order (I'm not sure how to do that, just that it isn't obvious that it won't!)p

[samth]

Well, there's both the ordering issue and the fact that the metafunction returns immediately when given a lambda, so (lambda (x) (5 x)) doesn't reduce even though it has an eta-redex.

[shhyou]

Looks like changing to unary functions is #258 but it is still open.