Reasoning about Syntax-Based Mathematical Algorithms within a Formal Logic

机械化数学的任务是开发支持人们用来创建、探索、连接和应用数学的过程的软件系统。数学在科学和技术中的新应用，特别是在软件开发中，往往需要使用计算机来执行大型而复杂的计算，并检查一长串的逻辑推理。因此，迫切需要能够更好地支持和管理数学过程的机械化数学系统。*在数学实践中，计算和演绎之间存在着强大的协同作用。算法计算机代数系统和公理定理证明系统之间的划分打破了这种协同。为了显著推进机械化数学，这种协同效应需要在单一的机械化数学系统中捕捉到。也就是说，算法数学和公理数学需要集成到一个单一的框架中。*这项研究的短期目标是开发关于符号算法的更好的推理方法，这些方法通过以数学上有意义的方式操作数学表达式来工作。例如，符号微分算法通过将某些语法规则应用于表示函数的表达式来计算函数的导数。这种涉及语法和语义相互作用的算法在传统逻辑中很难描述和证明是正确的，因为没有直接引用表达式语法的机制。*我们打算开发一种在形式逻辑中对基于语法的数学算法进行推理的方法，并证明该方法的有效性。该方法的核心思想是通过添加(1)一组表示逻辑表达式的句法结构的语法值，(2)将表达式映射到语法值的引号运算符，以及(3)将语法值映射到表达式的求值运算符来修改传统逻辑。*我们将产生支持该方法的新逻辑、实现该逻辑的软件系统以及如何使用该逻辑实现来指定和证明基于语法的正确数学算法的示例。如果这种方法被证明对语法和语义的相互作用进行形式化推理是有效的，它将极大地推进我们的长期目标，即整合通过符号计算完成的数学和通过形式演绎完成的数学。

The mission of mechanized mathematics is to develop software systems that support the process people use to create, explore, connect, and apply mathematics. New applications of mathematics in science and technology, especially in software development, often require the use of computers to perform large and complex computations and to check long series of logical deductions. As a result, there is a strong need for mechanized mathematics systems that can better support and manage the process of doing mathematics.***In mathematical practice there is a powerful synergy between computation and deduction. The division between algorithmic computer algebra systems and axiomatic theorem proving systems has broken this synergy. To significantly advance mechanized mathematics, this synergy needs to be captured within a single mechanized mathematics system. That is, algorithmic mathematics and axiomatic mathematics need to be integrated into a single framework.***The short-term objective of this research is to develop better ways of reasoning about symbolic algorithms that work by manipulating mathematical expressions in a mathematically meaningful way. For example, a symbolic differentiation algorithm computes the derivative of a function by applying certain syntactic rules to an expression that represents the function. Algorithms of this type that involve an interplay of syntax and semantics are difficult to specify and prove correct within a traditional logic because there is no mechanism for directly referring to the syntax of expressions.***We intend to develop a method for reasoning about syntax-based mathematical algorithms in a formal logic and then demonstrate the effectiveness of the method. The key idea of the method is to modify a traditional logic by adding to it (1) a set of syntactic values that represent the syntactic structures of the logic's expressions, (2) a quotation operator that maps expressions to syntactic values, and (3) an evaluation operator that maps syntactic values to expressions.***We will produce a new logic that supports the method, a software system that implements the logic, and examples of how the implementation of logic can be used to specify and prove correct syntax-based mathematical algorithms. If the method proves to be effective for reasoning formally about the interplay of syntax and semantics, it will significantly advance our long-term objective of integrating mathematics done by symbolic computation and mathematics done by formal deduction.**