论文标题
安排交织搜索的复杂性
Scheduling Complexity of Interleaving Search
论文作者
论文摘要
Minikanren是一种用于逻辑和关系编程的轻量级嵌入式语言。它的许多有用功能来自一种独特的搜索策略,称为交织搜索。但是,随着搜索搜索的传统方式,关于逻辑程序的复杂性和表现的推理方式变得无关紧要。我们确定了一个重要的关键组件 - 调度 - 这使Minikanren如此不同,并提出了一种半自动技术,以通过符号执行来估算计划范围的计划影响,以实现相当广泛的程序。
miniKanren is a lightweight embedded language for logic and relational programming. Many of its useful features come from a distinctive search strategy, called interleaving search. However, with interleaving search conventional ways of reasoning about the complexity and performance of logical programs become irrelevant. We identify an important key component -- scheduling -- which makes the reasoning for miniKanren so different, and present a semi-automatic technique to estimate the scheduling impact via symbolic execution for a reasonably wide class of programs.