$\eta$-reduction is often described as arising from the desire for functions which are point-wise equal to be syntactically equal. In a simply typed calculus with products it is sufficient, but when sums are involved I fail to see how to reduce point-wise equal functions to a common term.

For example, it is easy to verify that any function $f: (1+1) \to (1+1)$ is point-wise equal to $\lambda x.f(fx)$, or more generally $f$ is point-wise equal to $f^{n!}$ when $f: A \to A$ and $A$ has exactly $n$ inhabitants. Is it possible to reduce $f^{n!}$ to $f$? If not, is there an extension of the simply typed calculus which allows this reduction?

  • $\begingroup$ What does "pointwise equal" mean, precisely? $\endgroup$ – Andrej Bauer Jan 9 at 22:35
  • $\begingroup$ two functions $f, g:A \to A$ are point-wise equal if for any $a:A$, $f(a) =_{\beta\eta} g(a)$. $\endgroup$ – Jack Jan 10 at 20:20
  • $\begingroup$ I am afraid this is not a sufficient explanation for type theory. What is $a$ here? Closed term? A term in a context? $\endgroup$ – Andrej Bauer Jan 11 at 7:53
  • $\begingroup$ I would be happy to know a solution for closed terms. How about: two closed terms $f, g:A \to A$ are point-wise equal if for all closed terms $a:A, f(a) =_{\beta\eta} g(a)$? $\endgroup$ – Jack Jan 11 at 16:11
  • $\begingroup$ Nope, you can't get that. $\endgroup$ – Andrej Bauer Jan 11 at 19:17

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.