Enhancing the Power and Performance of Equational Systems

该项目继续并扩大了在设计、开发和实现增强方程系统的能力和性能的技术方面的研究。这项研究的三个关键领域是重写操作、方程编程和方程推导，尽管结果可能也适用于其他领域，如(约束)逻辑编程。重写操作的研究将集中在模式匹配算法的变体上，这些算法专门为函数编程的懒惰评估策略量身定做，并将某些函数的语义构建到用于等式推导的匹配算法中。方程式演绎的研究将集中在PI最近提出的基本补全方法上，在该方法中，不对由先前推理步骤中生成的替换建立的公式中的子表达式进行推理。该提案的等式编程部分将专注于Equals的进一步发展-懒惰语言和积分系统的快速并行实现，该系统使用符号约束求解技术将跨越不同范例的程序分析粘合在一起。***

This project continues and expands the research in the design, development, and implementation of techniques for enhancing the power and performance of equational systems. The three key areas for this research effort are rewrite operations, equational programming, and equational deduction, though the results will likely also be applicable to other areas such as (constraint) logic programming. Research on rewrite operations will focus on variants of pattern matching algorithms that are specifically tailored to lazy evaluation strategies for functional programming and to build the semantics of certain functions into the matching algorithms for equational deduction. The investigations in equational deduction will center on the PI's recently proposed basic completion method, in which no inferences are applied at those subexpressions in formulas that are built up from substitutions generated in previous inference steps. The equational programming component of the proposal will focus on the further development of Equals --- a fast parallel implementation of a lazy language and the Integral system which uses symbolic constraint solving techniques to glue together program analyses across different paradigms. ***