Enhancing the Power and Performance of Equational Systems

该项目继续并扩展了在设计，开发和实施技术，以提高方程系统的功率和性能的研究。 这项研究工作的三个关键领域是重写操作，方程式编程和方程式推导，尽管结果可能也适用于其他领域，如（约束）逻辑编程。 重写操作的研究将集中在模式匹配算法的变体上，这些算法专门针对函数式编程的惰性评估策略，并将某些函数的语义构建到等式推导的匹配算法中。 在方程推导的调查将集中在PI的最近提出的基本完成方法，其中没有推理适用于那些子表达式的公式，建立从先前的推理步骤中产生的替代。 该提案的等式编程部分将侧重于Equals的进一步发展-一种懒惰语言和Integral系统的快速并行实现，该系统使用符号约束求解技术将不同范式的程序分析粘合在一起。 ***

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. ***