"Domain algebra, quantum algebra, refinement algebra"

《领域代数、量子代数、细化代数》

• 批准号: 89769-2012
• 负责人: Desharnais, Jules
• 金额: $ 2.04万
• 依托单位: Université Laval
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2016
• 资助国家: 加拿大
• 起止时间: 2016-01-01 至 2017-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=593188
• 关键词: Domain; algebra; quantum; refinement

This research is about the mathematics of program construction, a branch of formal methods. It consists in finding methods for rigorously (mathematically) specifying what we want a computer to do, and then deriving a correct program from the specification (the program is said to refine the specification). The goal of these methods is to obtain programs that are correct by construction, rather than verifying them later to correct bugs. This research uses algebraic techniques to describe specifications, programs and refinement. It has five main objectives. (1) Determining whether so-called refinement algebras with a domain operator are decidable, i.e., whether there exists an algorithm deciding if two expressions of the algebra are equal. This property is important when using the algebras in practice, since automated deductions can be carried out. (2) Find algebras modelling the behaviour of quantum automata. These automata are abstract quantum computers with a rather weak computing power, but understanding them better is a way to improve our knowledge of what quantum computation will bring when quantum computers are available. (3) Devise refinement algebras for probabilistic and quantum programming. (4) Find an algorithm for calculating controllers for visibly pushdown automata, another abstract type of computer that is useful for modelling some properties of programs. If this research is successful, it will yield applications to program security. (5) Mathematically derive efficient programs (i.e., fast and using little memory) for solving problems in digital geometry. An example of a 2-D digital geometry is that of a computer screen, made of discrete pixels rather than a continuous set of points. Surprisingly, not much research on computational complexity (the branch of computing science targeting efficient programs) has been done in this area, at least when compared to continuous geometry. This is thus a good occasion to invent new algorithms while proving their correctness in the rigorous style of the mathematics of program construction.

本文研究的是形式化方法的一个分支--程序构造数学。它包括找到严格（数学上）指定我们希望计算机做什么的方法，然后从规范中导出正确的程序（该程序被称为细化规范）。这些方法的目标是通过构造获得正确的程序，而不是稍后验证它们以纠正错误。这项研究使用代数技术来描述规格，程序和细化。它有五个主要目标。(1)确定具有域算子的所谓的精化代数是否可判定，即，是否存在一个算法来决定代数的两个表达式是否相等。这个性质在实际使用代数时很重要，因为可以进行自动演绎。(2)寻找模拟量子自动机行为的代数。这些自动机是计算能力相当弱的抽象量子计算机，但更好地理解它们是一种提高我们对量子计算机可用时量子计算将带来什么的知识的方法。(3)为概率和量子规划设计精化代数。(4)找到一个算法来计算控制器的可见下推自动机，另一种抽象类型的计算机，是有用的建模程序的一些属性。如果这项研究是成功的，它将产生应用程序的安全性。(5)数学上推导出有效的程序（即，快速且使用很少的内存）来解决数字几何中的问题。二维数字几何的一个例子是计算机屏幕，它由离散的像素而不是连续的点组成。令人惊讶的是，至少与连续几何相比，在该领域对计算复杂性（计算科学中针对高效程序的分支）的研究并不多。因此，这是一个很好的机会，发明新的算法，同时证明他们的正确性，在严格的风格的数学程序的建设。