Higher order functions and Brouwer's thesis. (19th May 2021)

• Record Type: Journal Article
• Authors: STERLING, JONATHAN
• Is Part Of: Journal of functional programming. Volume 31(2021)
• Publication Date: 2021-05-19
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796821000095
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: Extending Martín Escardó's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a functional of type (ℕ→ℕ)→ℕ in Gödel's System T . Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type ℕ→ℕ, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer's famous "mental constructions" of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.