Marc Roth
Research Immersion Lab: A reasonable time measure for the weak call-by-value lambda calculus
Author: Marc Roth
Advisor: Prof. Dr. Gert Smolka
Abstract
We provide a formalization of a generalized version of the time measure for the weak call-by-value lambda calculus as introduced by Dal Lago and Martini in 2008. We will use the language L as formalization of the weak call-by-value lamda calculus. The key insight is the fact that every normalizing reduction of a term is unique up to the order of the beta redexes. In this context, we show that there is only one closed beta redex that reduces to itself in one step. Furthermore, we prove that the weak call-by-value lambda calculus fulfills the weak invariance thesis if we use the number of beta steps during a reduction sequence as time measure. This means that reasonable machines such as Turing Machines and L can simulate each other with only a polynomial overhead in time. We therefore proceed in three steps: First, we represent L terms as closures, an idea introduced by Dal Lago and Accattoli in 2014 and prove that a computation in L can be simulated in the closure calculus with only a polynomial overhead in the number of reduction steps. Second, we present an algorithm for simulating a computation in the closure calculus to argue that a computation in L can by simulated by every reasonable machine with only a polynomial overhead in time. And third, we apply a technique for simulating Turing Machines in the weak call-by-value lambda calculus as shown by Dal Lago in 2008 to prove that L can simulate a Turing Machine with only a polynomial overhead in time. Finally, we use this result to provide a basic notation of classical complexity w.r.t. L and argue that all total computable functions can be implemented in L such that the size of every intermediate term during a reduction sequence does not exceed a polynomial in the number of steps that were done before. The formalization --- except for the very last sections dealing with Turing Machines --- is done in the proof assistant Coq and continues the work of Fabian Kunze and Yannik Forster.
Attached Documents
Legal notice, Privacy policy
