Semantics Modifiers and Reversible Computations: What We Have Been Doing All That Time

Докладчик: Дмитрий Булычев

One of the most spectacular applications of miniKanren, which showcases its potential, is the implementation of relational interpreters. With a relational interpreter for a general-purpose programming language, it becomes possible to evaluate regular programs in this language in relational semantics. A typical example includes a Scheme over miniKanren over Scheme tower of interpreters, and the typical application includes program synthesis (“quines”, “twines”, “trines”, test-based synthesis, etc.) Another use case is turning verifiers into provers using relational conversion —- a direct syntactic transformation of functional programs into corresponding relational ones. In all these cases, the desirable properties of the solutions have to be ad-hoc justified anew. Meantime, at the edge of the century, Robert Glück and Sergey Abramov have developed a general framework of “semantics modifiers” which seems to address all these questions (and some others). In the talk, we give an overview of the semantics modifiers framework, relate it to the problems relevant for the relational programming domain, and discuss how the latter can benefit from the former (and vice versa).

???? Sergey Abramov, Robert Glück. From Standard to Non-Standard Semantics by Semantics Modifiers // International Journal of Foundations of Computer Science,Vol. 12, No. 02, pp. 171-211 (2001)
???? Sergey Abramov, Robert Glück. Principles of Inverse Computation and the Universal Resolving Algorithm // The Essence of Computation. Complexity, Analysis, Transformation (2002)
???? Sergey Abramov, Robert Glück. Combining Semantics with Non-Standard Interpreter Hierarchies // FSTTCS (2000)