-
A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus
Authors:
Yannick Forster,
Fabian Kunze
Abstract:
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $λ$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying tran…
▽ More
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $λ$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for Ł, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.
△ Less
Submitted 17 July, 2019; v1 submitted 26 April, 2019;
originally announced April 2019.
-
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Authors:
Yannick Forster,
Fabian Kunze,
Marc Roth
Abstract:
We study the weak call-by-value $λ$-calculus as a model for computational complexity theory and establish the natural measures for time and space -- the number of beta-reductions and the size of the largest term in a computation -- as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas [STOC~84]. More precisely, we show that, using those measures, Turing machines an…
▽ More
We study the weak call-by-value $λ$-calculus as a model for computational complexity theory and establish the natural measures for time and space -- the number of beta-reductions and the size of the largest term in a computation -- as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas [STOC~84]. More precisely, we show that, using those measures, Turing machines and the weak call-by-value $λ$-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations that terminate in (encodings) of 'true' or 'false'. We consider this result as a solution to the long-standing open problem, explicitly posed by Accattoli [ENTCS~18], of whether the natural measures for time and space of the $λ$-calculus are reasonable, at least in case of weak call-by-value evaluation.
Our proof relies on a hybrid of two simulation strategies of reductions in the weak call-by-value $λ$-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of $\log n$, which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space and a polynomial overhead in time.
△ Less
Submitted 20 February, 2019;
originally announced February 2019.
-
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
Authors:
Fabian Kunze,
Gert Smolka,
Yannick Forster
Abstract:
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three…
▽ More
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.
△ Less
Submitted 2 January, 2019; v1 submitted 8 June, 2018;
originally announced June 2018.
-
Towards the Integration of an Intuitionistic First-Order Prover into Coq
Authors:
Fabian Kunze
Abstract:
An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intuitionistic prover generates a certificate based on the matrix characterization of intuitionistic first-order logic; the certificate is then translated into a sequent-style proof.
An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intuitionistic prover generates a certificate based on the matrix characterization of intuitionistic first-order logic; the certificate is then translated into a sequent-style proof.
△ Less
Submitted 19 June, 2016;
originally announced June 2016.
