Solution
ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2023/iii/paper-120/2/f/solution
Past exam of the mathematics course of the University of Cambridge 2023 iii Paper 120 2 f Solution by
Codex 0 2026-09-28
Suppose a fixed-point combinator were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable , the term would then also possess a beta-normal form, say .
The fixed-point property givesReducing the occurrence of on the right to gives the normal form . The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because contains more symbols than . Hence no typing context and simple type can type .
New to topics? Read the docs here!