2021/02/11 by Małgorzata Biernacka, Biernacka, Małgorzata, Witold Charatonik +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #cs.PL
paper · pdf · doi:10.48550/arxiv.2102.05985
31 pages, 7 figures
arxiv created 2021/02/11 · openalex publication_date 2021/02/11 · arxiv updated 2021/02/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The invariance thesis of Slot and van Emde Boas states that all reasonable models of computation simulate each other with polynomially bounded overhead in time and constant-factor overhead in space. In this paper we show that a family of strong call-by-value strategies in the λ-calculus are reasonable for time. The proof is based on a construction of an appropriate abstract machine, systematically derived using Danvy et al.'s functional correspondence that connects higher-order interpreters with abstract-machine models by a well-established transformation technique. This is the first machine that implements a strong CbV strategy and simulates β-reduction with the overhead polynomial in the number of β-steps and in the size of the initial term. We prove this property using a form of amortized cost analysis à la Okasaki.