Self-aware Program Analysis in stableKanren
摘要
This paper presents two improvements to the compatibility and performance of stableKanren on monotonic programs. miniKanren supports monotonic reasoning, in which one program produces exactly one model. stableKanren extends miniKanren to nonmonotonic reasoning, where a program can have zero to multiple models. stableKanren handles loops and negations, the main elements of nonmonotonic reasoning, through an extended nonmonotonic resolution in its “run” interface. The current nonmonotonic resolution in the stableKanren also applies to monotonic programs and creates two issues. Firstly, a monotonic program with infinite answers could not produce an answer under stableKanren. Secondly, a monotonic program runs slower under stableKanren due to the additional nonmonotonic resolution. The nonmonotonic resolution is unnecessary for these monotonic programs. We construct a “run-partial” interface in stableKanren without nonmonotonic resolution. Using “run-partial” resolves the above two issues; however, expert knowledge is required to identify whether the program is monotonic or nonmonotonic and to choose the corresponding interface by the users. We further introduce two program analyses to the stableKanren “run” interface to identify the monotonic program implicitly. We use a macro to handle the first issue at the syntax level, so the “run” interface does not apply nonmonotonic resolution on monotonic programs without any negations. Furthermore, we present four syntax-level macros to construct two smaller twins of the input program. Each twin has different semantics on loops over negations, so we resolve the second issue by running these two twins. The twins of the monotonic programs produce identical outcomes, but the nonmonotonic programs do not. Our updated “run” interface can identify monotonic programs at the syntax level; there is still more work to identify such programs during execution.