Imperative programs from proofs

证明中的命令式程序

基本信息

批准号：
EP/W035847/1
负责人：
Thomas Powell
金额：
$ 39.68万
依托单位：
University of Bath
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2023
资助国家：
英国
起止时间：
2023 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FW035847%2F1
关键词：
Imperative programs proofs

项目摘要

The aim of this project is to develop new logical methods for extracting programs from mathematical proofs. Traditionally, such programs are extremely complicated and difficult to understand. We will improve the situation by devising novel techniques that produce programs written in a more natural language, thereby making program extraction more effective in several areas in which it is currently being applied.Background: It has long been known that there is a deep connection between logic and computation, and that mathematical proofs can be converted to computer programs. Proof interpretations are a technique for doing this. They are useful for many reasons. When implemented in a computer, they provide us with a way of synthesising programs that are correct-by-construction and therefore guaranteed to be bug free. When applied to complex mathematical proofs, they can sometimes reveal new algorithms that have not been previously discovered. There is now a large subfield of logic dedicated to using proof interpretation to extract programs from proofs.The problem: Proof interpretations are formal mathematical techniques, and as such they often result in programs that are quite different from those a human would write. These programs tend to be written in a very abstract language and can be extremely long, syntactic, and difficult to understand. This represents a drawback to using proof interpretations for practical purposes: While it is useful to have a program that we know accomplishes a particular task, it would be more useful if we were able to understand how that program worked!My main goal:This project aims to bring programs obtained using proof interpretations closer to those a human would write. The aim is to improve the current state-of-the-art so that extracted programs are written in a more natural language and therefore easier to understand.My approach: We will take one of the most powerful and widely used of all proof interpretations - K. Goedel's Dialectica interpretation - and adapt it so that it produces programs in a language that is much closer in spirit to a real-world programming language. This will involve incorporating a global state along with control flow statements such as while-loops. These are all core features of everyday languages such as C and Python but are absent from the kind of theoretical languages traditionally associated with proof interpretations. We will then further refine the new interpretation so that it is optimized for the two main applications outlined above: (i) synthesising correct-by-construction programs, and (ii) revealing interesting new algorithms from complex mathematical proofs. These two applications will each require a different approach, and the second in particular will involve a number of deep ideas from mathematical logic. We will then demonstrate our new technique by carrying out a series of case studies, targeting problem areas (i) and (ii) respectively and aimed at specific communities who would most benefit from our new method. In parallel, we will explore generalisations of our new method so that it could potentially incorporate further interesting structures from programming.The project will require us to bring together ideas from both mathematical logic and the theory of programming languages, and the intended applications, which will be exemplified through our case studies, bring formal verification and pure mathematics into play. This makes the project fundamentally cross-disciplinary, and we will exploit this by organising visits to a range of relevant research groups in the UK and internationally, and by hosting a cross-disciplinary workshop towards the end of the project.

该项目的目的是开发从数学证明中提取程序的新逻辑方法。传统上，这样的程序非常复杂且难以理解。我们将通过设计新颖的技术来改善这种情况，以制作更自然的语言编写的程序，从而使程序提取在目前正在应用的几个领域中更有效。background：长期以来，人们一直知道逻辑和计算之间存在着深厚的联系，并且数学证明可以转换为计算机程序。证明解释是这样做的一种技术。它们有很多原因有用。当在计算机中实施时，它们为我们提供了合成正确构造的程序，因此保证无错误的方法。当应用于复杂的数学证明时，它们有时可以揭示以前未发现的新算法。现在，有一个巨大的逻辑子领域，专门用于使用证明解释从证据中提取程序。问题：证明解释是正式的数学技术，因此它们通常导致程序与人类会写的那些截然不同。这些程序倾向于用非常抽象的语言编写，并且可能非常长，句法和难以理解。这代表了用于实际目的使用证明解释的缺点：虽然拥有一个我们知道完成一项特定任务的程序很有用，但是如果我们能够了解该程序的工作方式，这将更有用！我的主要目标：该项目的目的是将使用与人类会写的那些人接近的证明解释获得获得的程序。目的是改善当前的最新原始程序，以更自然的语言编写，因此更容易理解。我的方法：我们将采用所有证明解释中最强大，最广泛使用的方法之一 - K. Goedel的辩证法解释 - 并适应它，以使其以一种在精神上与现实的语言更接近的语言产生程序。这将涉及将全球状态和控制流语句（例如While-Loops）结合起来。这些都是日常语言（例如C和Python）的核心特征，但传统上与证明解释相关的理论语言不存在。然后，我们将进一步完善新的解释，以便对上述两个主要应用程序进行优化：（i）合成正确的构造程序，以及（ii）从复杂的数学证明中揭示有趣的新算法。这两个应用程序将每个应用都需要不同的方法，而第二个应用程序将涉及数学逻辑的许多深刻想法。然后，我们将通过进行一系列案例研究，针对问题领域（i）和（ii），并针对特定的社区来证明我们的新技术，这些社区最能从我们的新方法中受益。同时，我们将探讨我们新方法的概括，以便它有可能纳入编程中的进一步有趣的结构。该项目将要求我们从数学逻辑和编程语言理论中汇集出想法，以及通过我们的案例研究，正式验证和纯粹的数学来体现的预期应用程序，这些应用程序将被阐明。这使该项目从根本上跨学科了，我们将通过组织访问英国和国际的一系列相关研究小组，并在项目结束时举办跨学科研讨会来利用这一点。