Self-aware Program Analysis in stableKanren

doi:10.1007/978-3-031-99751-8_8

Self-aware Program Analysis in stableKanren

2026-01-01

0

PRE

AI

DOI：10.1007/978-3-031-99751-8_8

原文链接

原文求助

摘要

En 中文

本文提出两项改进以提升stableKanren在单调程序上的兼容性和性能。miniKanren支持单调推理，其中一个程序产生恰好一个模型。stableKanren扩展miniKanren至非单调推理，程序可有零至多个模型。stableKanren通过其run接口中的扩展非单调归结处理非单调推理的主要元素：循环和否定。当前stableKanren中的非单调归结也适用于单调程序，并引发两个问题：首先，无限答案的单调程序在stableKanren下无法产生答案；其次，单调程序在stableKanren下运行变慢，因额外的非单调归结。这些单调程序无需非单调归结。我们在stableKanren中构建无非单调归结的run-partial接口。使用run-partial可解决上述两个问题；但用户需具备专业知识判断程序是否单调并选择对应接口。我们进一步为stableKanren的run接口引入两项程序分析以隐式识别单调程序。我们通过宏在语法层面处理第一个问题，使run接口不对无否定的单调程序应用非单调归结。此外，我们提出四个语法级宏构建输入程序的两组较小孪生程序。每组孪生程序在循环与否定上的语义不同，通过运行这两组孪生程序解决第二个问题。单调程序的孪生程序产生相同结果，但非单调程序则不同。我们更新的run接口可在语法层面识别单调程序，但仍需进一步工作以在执行期间识别此类程序。

Keyword:

logic programming

miniKanren

stableKanren

macros

Self-aware Program Analysis in stableKanren

摘要

期刊

机构

引用论文