Effective Denotational Semantics for Synthesis

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

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.