Using Church's $\lambda x.(\lambda y.y))$ as false and $\lambda x.(\lambda y.x))$ as true, and given two free variables $g$ and $h$:

Could there exist a function $eq?$ such that $(eq?\ g\ h)$ is false, and $(eq?\ g\ g)$ is true?

I typically would show my work here, but as of right now, I honestly have nothing except a hunch that it's categorically impossible.

  • 1
    $\begingroup$ What do you mean by the truth value of an expression like $(eq?\ g\ h)$ when $g,h$ are free? I don't believe that's well-defined. The natural definition would be to say that it reduces to true; but that doesn't make sense for an expression with free variables. $\endgroup$ – D.W. Mar 27 at 2:21
  • $\begingroup$ @D.W. I want to determine whether two free variables are literally the same variable or not. In Scheme, I can write (eq? 'A 'A) and it returns #t, whereas (eq? 'A 'B) returns #f. ('A and 'B are atoms, not strings, meaning that they behave like $\lambda$-calculus free variables.) I'm open to any edits or suggestions that would make that clearer. $\endgroup$ – Ben I. Mar 27 at 2:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.