Does there exist a normal-form lambda calculus program $f$ such that

  • $f (\lambda x . x)$ normalizes
  • For all normal form $e \ne \lambda x . x$, $f e$ does not normalize

Well nevermind this has an easy answer.

Let $r_n = \lambda x_1 ... x_n . \lambda p . p \: x_1 ... x_n$

Note that for $m < n$, $r_n\: A_1 ... A_m$ normalizes for any normal $A_1 ... A_m$.

Then for any $f$, let $n$ be larger than the number of subterms in $f$.

$f \:r_n$ normalizes, so therefore no $f$ exists which only normalizes for a specific input.

| cite | improve this answer | |
  • $\begingroup$ Did you use the fact that $f$ normalizes on $\lambda x.\ x$? Does this actually prove that any normalizing $f$ must normalize on infinitely many normalized arguments? $\endgroup$ – chi Oct 7 '19 at 12:03

Your Answer

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

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