2
$\begingroup$

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
$\endgroup$

1 Answer 1

4
$\begingroup$

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.

$\endgroup$
1
  • $\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
    Commented Oct 7, 2019 at 12:03

Your Answer

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

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