Effective Denotational Semantics for 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.