Improving stableKanren's Backward Compatibility
Xiangyu Guo, Ajay Bansal
TL;DR
This work tackles the backward-compatibility problem of stableKanren when running standard miniKanren programs, which fail due to coarse handling of contradictions under stable-model semantics. It introduces a compile-time has-negation? analysis to identify definite programs and updates the defineo macro to avoid unnecessary unavoidable-contradiction checks for these cases, enabling standard miniKanren programs to run within stableKanren. A run-partial interface is added to restore miniKanren's run semantics in environments where stableKanren relations may be non-terminating or unsatisfiable, and to accelerate stratified negation programs by bypassing global contradiction checks. Empirical results show substantial performance gains for stratified programs, particularly in final-SCC scenarios, and demonstrate that standard miniKanren relations can coexist with stableKanren relations in the same environment. The authors also outline future work on dependency-graph-based decision mechanisms to automatically choose the appropriate execution mode, further enhancing usability and efficiency.
Abstract
We improve the backward compatibility of stableKanren to run miniKanren programs. stableKanren is a miniKanren extension capable of non-monotonic reasoning through stable model semantics. However, standard miniKanren programs that produce infinite results do not run as expected in stableKanren. According to stable model semantics, the contradictions are created by negations. A standard miniKanren's relations do not involve negation, and the coarse contradictions handling in stableKanren causes this compatibility issue. Therefore, we provide a find-grinded contradiction handling to restrict the checking scope. As a result, standard miniKanren relations can produce answers. We also add a ``run-partial'' interface so that standard miniKanren's relations implemented with ``define''/``defineo'' can generate answers even if they coexist with non-terminating or unsatisfiable stableKanren relations in the same environment. The ``run-partial'' interface also supports running stratified negation programs faster without checking global unavoidable contradictions. A dependency graph analysis can be applied to the input query in the future, so the ``run'' interface can implicitly decide whether to perform unavoidable contradictions checking to improve usability.