权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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.

该项目的目的是开发新的逻辑方法，从数学证明中提取程序。传统上，这样的程序非常复杂，难以理解。我们将通过设计新的技术来改善这种情况，这些技术可以产生用更自然的语言编写的程序，从而使程序提取在目前正在应用的几个领域更加有效。背景：人们早就知道，逻辑和计算之间存在着深刻的联系，数学证明可以转换为计算机程序。证明解释是这样做的一种技术。它们是有用的，原因有很多。当在计算机中实现时，它们为我们提供了一种合成程序的方法，这些程序通过构造是正确的，因此保证没有错误。当应用于复杂的数学证明时，它们有时可以揭示以前没有发现的新算法。现在有一个很大的逻辑子领域致力于使用证明解释从证明中提取程序。问题：证明解释是形式化的数学技术，因此它们经常导致程序与人类编写的程序完全不同。这些程序往往是用一种非常抽象的语言编写的，可能非常长，语法和难以理解。这代表了将证明解释用于实际目的的一个缺点：虽然有一个我们知道可以完成特定任务的程序是有用的，但如果我们能够理解该程序是如何工作的，那就更有用了！我的主要目标：这个项目旨在使使用证明解释获得的程序更接近人类编写的程序。我们的目标是改进当前的最先进的技术，使提取的程序用更自然的语言编写，因此更容易理解。我的方法：我们将采取所有证明解释中最强大和最广泛使用的一个- K。Goedel的Dialectica解释-并对其进行调整，使其在精神上更接近真实世界的编程语言的语言中产生程序。这将涉及将全局状态沿着与控制流语句（如while-loops）合并。这些都是C和Python等日常语言的核心特征，但传统上与证明解释相关的理论语言中却没有这些特征。然后，我们将进一步完善新的解释，使其针对上述两个主要应用进行优化：（i）合成正确的构造程序，以及（ii）从复杂的数学证明中揭示有趣的新算法。这两种应用都需要不同的方法，特别是第二种应用将涉及许多来自数理逻辑的深刻思想。然后，我们将通过开展一系列案例研究来展示我们的新技术，分别针对问题领域（i）和（ii），并针对最能从我们的新方法中受益的特定社区。与此同时，我们将探索我们的新方法的推广，以便它可以潜在地包含来自编程的更多有趣的结构。该项目将要求我们将数理逻辑和编程语言理论的想法结合在一起，并将通过我们的案例研究来举例说明预期的应用，将形式验证和纯数学发挥作用。这使得该项目从根本上跨学科，我们将通过组织访问英国和国际上的一系列相关研究小组，并在项目结束时举办跨学科研讨会来利用这一点。