Reasoning about Syntax-Based Mathematical Algorithms within a Formal Logic

点击翻译按钮获取中文摘要

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.