Effective Denotational Semantics for Synthesis

用于综合的有效指称语义

• 批准号: 417532197
• 负责人: Professor Dr. Roland Meyer
• 金额: --
• 依托单位: Institut für Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/417532197?language=en
• 关键词: Effective; Denotational; Semantics; Synthesis

Effective denotational semantics is a recent trend in verification. Given a program and aspecification, the idea is to solve the verification task by computing a denotational semantics for the program that is induced by the specification. The specification is typically reactive in that it refers to the interaction of the program with its environment. Our goal is to lift the approach to synthesis. Rather than a program, the synthesis problem considers a program sketch, a program with implementation alternatives left open. The task is to determine a completion of the sketch to a full program that meets the specification. The completion adds to the sketch a controller that selects implementation alternatives based on the history of the computation. A key problem in synthesis is imperfect information, the fact that the program and theenvironment do not see the local state of the other. The existing approaches to synthesis under imperfect information are not satisfactory. The programming models are undecidable or not expressive enough. The present project sets out to improve the situation in the setting of functional programs. The key observation is this. Functional programs do not have local state. Instead, they use choice operators (pattern matching) to locally process data. Hence, it is the choice operators that should give perfect or imperfect information. We propose to develop lambda-plus-plus (L++), a functional programming language with rich support for non-deterministic computation, namely angelic and demonic choices that can be perfect and imperfect. Given these operators, L++ drops the distinction between program and environment. L++ comes with a built-in assertion language for specifications. Formulating a synthesis problem thus amounts to writing a L++ program. We argue that L++ will fill the need for an expressive programming language the synthesis problem of which remains decidable. As for the expressiveness, we will show that problems from various domains (verification, synthesis, automata theory, and graph games) can be understood as L++ synthesis problems. As for the decidability, we will solve L++ synthesis with effective denotational semantics. These semantics will be based on new algebraic structures. The elements of these structures will (finitely) represent computations. The operators will interprete programming constructs. It will be the first time, imperfect information receives a denotational treatment. The central goals of our project are the following. 1. Solve the synthesis problem for the first-order fragment of L++.2. Understand the set of completions of L++ programs.3. Lift the results to the higher-order fragment of L++.4. Generalize the results to infinite storage.5. Formulate problems from other domains as L++ synthesis.

有效的指称语义是验证的最新趋势。给定一个程序和一个规范，其想法是通过计算由规范导出的程序的指称语义来解决验证任务。该规范通常是反应性的，因为它指的是程序与其环境的交互。我们的目标是提升综合方法。综合问题考虑的不是一个程序，而是一个程序草图，一个具有开放的实现替代方案的程序。任务是确定草图是否完成为符合规范的完整程序。完成后会在草图中添加一个控制器，该控制器根据计算历史记录选择实现替代方案。综合中的一个关键问题是信息不完善，即程序和环境看不到对方的本地状态。现有的不完全信息下的合成方法并不令人满意。编程模型是不可判定的或表达能力不够。本项目旨在改善职能项目设置方面的情况。关键的观察是这样的。函数式程序没有本地状态。相反，他们使用选择运算符（模式匹配）来本地处理数据。因此，选择算子应该提供完美或不完美的信息。我们建议开发 lambda-plus-plus (L++)，这是一种函数式编程语言，对非确定性计算提供丰富的支持，即可以完美也可以不完美的天使和恶魔选择。有了这些运算符，L++ 就消除了程序和环境之间的区别。 L++ 带有用于规范的内置断言语言。因此，制定综合问题相当于编写 L++ 程序。我们认为 L++ 将满足对表达性编程语言的需求，而该语言的综合问题仍然是可判定的。至于表达性，我们将证明来自各个领域（验证、综合、自动机理论和图游戏）的问题都可以理解为 L++ 综合问题。至于可判定性，我们将通过有效的指称语义来解决L++综合。这些语义将基于新的代数结构。这些结构的元素将（无限地）代表计算。运算符将解释编程结构。这将是第一次，不完美的信息得到外延处理。我们项目的中心目标如下。 1. 解决L++一阶片段的综合问题。2。理解L++程序的补全集。3．将结果提升到 L++.4 的高阶片段。将结果推广到无限存储。5．将其他领域的问题表述为 L++ 综合。