Improving stableKanren's Backward Compatibility

TL;DR

This paper enhances stableKanren's compatibility with miniKanren by implementing contradiction handling and a partial run interface, enabling standard miniKanren programs to run correctly within stableKanren, especially with negation and infinite results.

Contribution

Introduces contradiction handling and a run-partial interface in stableKanren to improve backward compatibility with miniKanren programs involving negation and non-termination.

Findings

Standard miniKanren relations can now produce answers in stableKanren.

The run-partial interface allows execution of non-terminating or unsatisfiable relations.

Faster stratified negation execution without global contradiction checks.

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.