An official website of the United States government
Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, Nebula, proves equivalences of programs written in Haskell. We demonstrate Nebula's practical effectiveness at both proving equivalence and producing counterexamples automatically by applying Nebula to existing benchmark properties.
more »
« less
Checking equivalence in a non-strict language
Abstract Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation,nebula, proves equivalences of programs written in Haskell. We demonstratenebula’s practical effectiveness at both proving equivalence and producing counterexamples automatically by applyingnebulato existing benchmark properties.
more »
« less
- PAR ID:
- 10651042
- Publisher / Repository:
- Cambridge University Press
- Date Published:
- Journal Name:
- Journal of Functional Programming
- Volume:
- 35
- ISSN:
- 0956-7968
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Abstract Recent wide-field integral-field spectroscopy has revealed the detailed properties of high-redshift Lyαnebulae, most often targeted due to the presence of an active galactic nucleus (AGN). Here, we use VLT/MUSE to resolve the morphology and kinematics of a nebula initially identified due to strong Lyαemission atz∼ 3.2 (LABn06). Our observations reveal a two-lobed Lyαnebula, at least ∼173 pkpc in diameter, with a light-weighted centroid near a mid-infrared source (within ≈17.2 pkpc) that appears to host an obscured AGN. The Lyαemission near the AGN is also coincident in velocity with the kinematic center of the nebula, suggesting that the nebula is both morphologically and kinematically centered on the AGN. Compared to AGN-selected Lyαnebulae, the surface-brightness profile of this nebula follows a typical exponential profile at large radii (>25 pkpc), although at small radii, the profile shows an unusual dip at the location of the AGN. The kinematics and asymmetry are similar to, and the Civand Heiiupper limits are consistent with, other AGN-powered Lyαnebulae. Double-peaked and asymmetric line profiles suggest that Lyαresonant scattering may be important in this nebula. These results support the picture of the AGN being responsible for powering a Lyαnebula that is oriented roughly in the plane of the sky. Further observations will explore whether the central surface-brightness depression is indicative of either an unusual gas or dust distribution or variation in the ionizing output of the AGN over time.more » « less
-
We present an enumerative program synthesis framework calledcomponent-based refactoringthat can refactor “direct” style code that does not use library components into equivalent “combinator” style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code calledequivalence by canonicalizationthat does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such asmapandfilterin the staticallytyped functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool calledCobblerand evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.more » « less
-
We propose a new synthesis algorithm that canefficientlysearch programs withlocalvariables (e.g., those introduced by lambdas). Prior bottom-up synthesis algorithms are not able to evaluate programs withfree local variables, and therefore cannot effectively reduce the search space of such programs (e.g., using standard observational equivalence reduction techniques), making synthesis slow. Our algorithm can reduce the space of programs with local variables. The key idea, dubbedlifted interpretation, is to lift up the program interpretation process, from evaluating one program at a time to simultaneously evaluating all programs from a grammar. Lifted interpretation provides a mechanism to systematically enumerate all binding contexts for local variables, thereby enabling us to evaluate and reduce the space of programs with local variables. Our ideas are instantiated in the domain of web automation. The resulting tool,Arborist, can automate a significantly broader range of challenging tasks more efficiently than state-of-the-art techniques includingWebRobotand Helena.more » « less
-
A<sc>bstract</sc> We establish an equivalence between two different quantum quench problems, the joining local quantum quench and the Möbius quench, in the context of (1 + 1)-dimensional conformal field theory (CFT). Here, in the former, two initially decoupled systems (CFTs) on finite intervals are joined att= 0. In the latter, we consider the system that is initially prepared in the ground state of the regular homogeneous Hamiltonian on a finite interval and, aftert= 0, let it time-evolve by the so-called Möbius Hamiltonian that is spatially inhomogeneous. The equivalence allows us to relate the time-dependent physical observables in one of these problems to those in the other. As an application of the equivalence, we construct a holographic dual of the Möbius quench from that of the local quantum quench. The holographic geometry involves an end-of-the-world brane whose profile exhibits non-trivial dynamics.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1017/S0956796825100099
