Relational programming: pain, interest, and pain again

In the previous post we told in detail what we teach students in the field of "Industrial Programming". For those whose area of ​​interest lies in a more theoretical field, for example, attracted by new programming paradigms or abstract mathematics used in theoretical research on programming, there is another specialization - “Programming languages”.

Today I will talk about my research in the field of relational programming, which I do at the university and as a student-researcher in the laboratory of language tools JetBrains Research.

What is relational programming? Usually we run a function with arguments and get the result. And in the relational case, you can do the opposite: fix the result and one argument, and get the second argument. The main thing is to write the code correctly and be patient and have a good cluster.

About myself

My name is Dmitry Rozplokhas, I am a first-year student of the St. Petersburg HSE, and last year I graduated from the bachelor's program of the Academic University in the field of “Programming Languages”. Since the third year of undergraduate studies, I am also a research student at the JetBrains Research language tools laboratory.

Relational programming

General facts

Relational programming is when, instead of functions, you describe the relationship between arguments and the result. If the language is sharpened for this, you can get certain bonuses, for example, the ability to run the function in the opposite direction (restore the possible values ​​of the arguments as a result).

In general, this can be done in any logical language, but interest in relational programming arose simultaneously with the advent of a minimalistic pure logical language miniKanren about ten years ago , which made it possible to conveniently describe and use such relations.

Here are some of the most advanced use cases: you can write a proof checker and use it to find evidence ( Near et al., 2008) or create an interpreter of some language and use it to generate programs for a set of tests ( Byrd et al., 2017 ).

Syntax and Toy Example

miniKanren is a small language; only basic mathematical constructions are used to describe relations. This is an embedded language, its primitives are a library for some external language, and small miniKanren programs can be used inside a program in another language.

Foreign languages ​​suitable for miniKanren, a whole bunch. Initially, there was Scheme, we are working with the version for Ocaml ( OCanren ), and the full list can be viewed at minikanren.org . Examples in this article will also be on OCanren. Many implementations add helper functions, but we will focus only on the core language.

Let's start with the data types. Conventionally, they can be divided into two types:

• Constants are some data from the language into which we are embedded. Strings, numbers, even arrays. But for the basic miniKanren, this is all a black box, constants can only be checked for equality.
  
• A "term" is a tuple of several elements. Commonly used in the same way as data constructors in Haskell: data constructor (string) plus zero or more parameters. OCanren uses regular data constructors from OCaml.
  

For example, if we want to work with arrays in miniKanren itself, then it must be described in terms of terms similar to functional languages ​​- as a singly connected list. A list is either an empty list (indicated by some simple term), or a pair of the first element of the list (“head”) and other elements (“tail”).

let emptyList = Nil
let list_123 = Cons (1, Cons (2, Cons (3, Nil)))

A miniKanren program is the relationship between some variables. At startup, the program gives all possible values ​​of the variables in a general form. Often implementations allow you to limit the number of answers in the output, for example, find only the first one - the search does not always stop after finding all the solutions.

You can write several relationships that are defined through each other and even called recursively as functions. For example, below we instead of function$$ define the relation $$: list $$ is a concatenation of lists $$ and $$. Functions that return relationships traditionally end with an “o” to distinguish them from ordinary functions.

A relation is written as some statement regarding its arguments. We have four basic operations :

• Unification or equality (===) of two terms, terms can include variables. For example, you can write the relation “list$$ consists of one element $$":
  
  

  let isSingletono x l = l === Cons (x, Nil)
  

• Conjunction (logical “and”) and disjunction (logical “or”) - as in ordinary logic. OCanren are referred to as &&& and |||. But there is basically no logical denial in MiniKanren.
  
• Adding new variables. In logic, it is a quantifier of existence. For example, to check the list for non-emptyness, you need to check that the list consists of a head and a tail. They are not arguments of the relationship, so you need to create new variables:
  
  

  let nonEmptyo l = fresh (h t) (l === Cons (h, t))
  

A relationship can invoke itself recursively. For example, you need to define the relationship "element$$lies on the list. " We will solve this problem by analyzing trivial cases, as in functional languages:

1. Or the head of the list is $$
   
2. Or $$ lies in the tail
   

let membero l x =
    fresh (h t) (
        (l === Cons (h, t)) &&&
        (x === h ||| membero t x)
    )

The basic version of the language is built on these four operations. There are also extensions that allow you to use other operations. The most useful of them is disequality constraint for setting the inequality of two terms (= / =).

Despite the minimalism, miniKanren is quite expressive language. For example, look at the relational concatenation of two lists. The function of two arguments turns into a triple relation "$$ is a concatenation of lists $$ and $$".

let appendo a b ab =
    (a === Nil &&& ab === b) |||
    (fresh (h t tb) (* Синтаксический сахар: после fresh неявно добавляются &&& *)
        (a = Cons (h, t))
        (appendo t b tb)
        (ab === Cons (h, tb)))

The solution is structurally no different from how we would write it in a functional language. We analyze two cases united by a clause:

1. If the first list is empty, then the second list and the result of concatenation are equal.
   
2. If the first list is not empty, then we parse it into the head and tail and construct the result using a recursive call of the relation.
   

We can make a request to this relation, fixing the first and second argument - we get the concatenation of lists:

run 1 (λ q -> appendo (Cons (1, Cons (2, Nil))) (Cons (3, Cons (4, Nil))) q)

⇒

q = Cons (1, Cons (2, Cons (3, Cons (4, Nil))))

We can fix the last argument - we get all the partitions of this list into two.

run 4 (λ q r -> appendo q r (Cons (1, Cons (2, Cons (3, Nil)))))

⇒

q = Nil, r = Cons (1, Cons (2, Cons (3, Nil)))  |
q = Cons (1, Nil), r = Cons (2, Cons (3, Nil))  |
q = Cons (1, Cons (2, Nil)), r = Cons (3, Nil)  |
q = Cons (1, Cons (2, Cons (3, Nil))), r = Nil 

You can do anything else. A slightly more non-standard example, in which we fix only part of the arguments:

run 1 (λ q r -> appendo (Cons (1, Cons (q, Nil))) r (Cons (1, Cons (2, Cons (3, Cons (4, Nil))))))

⇒

q = 2, r = Cons (3, Cons (4, Nil))

How it works

From the point of view of theory, there is nothing impressive here: you can always just start searching all possible options for all arguments, checking for each set whether they behave with respect to a given function / relation as we would like (see "The British Museum Algorithm" ) . Of interest is the fact that here the search (in other words, the search for a solution) uses only the structure of the described relationship, due to which it can be relatively effective in practice.

The search is in relation to accumulating information about various variables in the current state. We either don’t know anything about each variable, or we know how it is expressed in terms, values ​​and other variables. For instance:

b = Cons (x, y)
c = Cons (10, z)
x = ?
y = ?
z = ?

Passing through unification, we look at two terms with this information in mind and either update the state or terminate the search if two terms cannot be unified. For example, completing the unification b = c, we get new information: x = 10, y = z. But the unification b = Nil will cause a contradiction.

We search in conjuncts sequentially (so that information accumulates), and in a disjunction we divide the search into two parallel branches and move on, alternating steps in them - this is the so-called interleaving search. Thanks to this alternation, the search is complete - every suitable solution will be found after a finite time. For example, in the Prolog language this is not so. It does something like a deep crawl (which can hang on an infinite branch), and interleaving search is essentially a tricky wide crawl modification.

Let's now see how the first query from the previous section works. Since appendo has recursive calls, we will add indexes to variables to distinguish them. The figure below shows the enumeration tree. Arrows indicate the direction of dissemination of information (with the exception of the return from recursion). Between disjunctions, information is not distributed, and between conjunctions is distributed from left to right.

1. We start with an external call to appendo. Left branch of disjunction dies due to controversy: list$$ not empty.
   
2. In the right branch auxiliary variables are introduced, which are then used to “parse” the list $$ on the head and tail.
   
3. After this, the appendo recursive call occurs for a = [2], b = [3, 4], ab =?, In which similar operations occur.
   
4. But in the third call to appendo, we already have a = [], b = [3,4], ab = ?, and then the left disjunction just works, after which we get the information ab = b. But in the right branch there is a contradiction.
   
5. Now we can write out all the available information and restore the answer by substituting the values ​​of the variables:
   
   a_1 = [1, 2]
b_1 = [3, 4]
ab_1 = Cons h_1 tb_1
h_1 = 1
a_2 = t_1 = [2]
b_2 = b_1 = [3, 4]
ab_2 = tb_1 = Cons h_2 tb_2
h_2 = 2
a_3 = t_2 = Nil
b_3 = b_2 = b_1 = [3, 4]
ab_3 = tb_2 = b_3 = [3, 4]

   
6. It follows that $$ = Cons (1, Cons (2, [3, 4])) = [1, 2, 3, 4], as required.
   

What I did in undergraduate

Everything slows down

As always: they promise you that everything will be super declarative, but in reality you need to adapt to the language and write everything in a special way (keeping in mind how everything will be executed) in order for at least something to work, except for the simplest examples. This is disappointing.

One of the first problems that a novice miniKanren programmer faces is that it very much depends on the order in which you describe the conditions (conjuncts) in the program. With one order, everything is OK, but two conjunctions were swapped and everything began to work very slowly or did not finish at all. This was unexpected.

Even in the example with appendo, launching in the opposite direction (generating splits of the list into two) does not end unless you explicitly specify how many answers you want (then the search will end after the required number is found).

Suppose we fix the original variables as follows: a =?, B =?, Ab = [1, 2, 3] (see the figure below) In the second branch, this information will not be used in any way during a recursive call (the variable ab and restrictions on $$ and $$appear only after this call). Therefore, at the first recursive call, all its arguments will be free variables. This call will generate all kinds of triples from two lists and their concatenation (and this generation will never end), and then among them will be chosen those for which the third element is exactly the one we need.



Everything is not as bad as it might seem at first glance, because we will sort through these triples in large groups. Lists with the same length but different elements do not differ from the point of view of the function, therefore they will fall into one solution - there will be free variables in place of the elements. Nevertheless, we will still iterate over all possible lengths of lists, although we only need one, and we know which one. This is a very irrational use (non-use) of information in the search.

This specific example is easy to fix: you just need to move the recursive call to the end and everything will work as it should. Prior to the recursive call, unification with the variable ab will take place and the recursive call will be made from the tail of the given list (as a normal recursive function). This definition with a recursive call at the end will work well in all directions: to the recursive call, we manage to accumulate all the possible information about the arguments.

However, in any slightly more complex example, when there are several meaningful calls, one specific order for which everything will be fine does not exist. The simplest example: expanding a list using concatenation. We fix the first argument - we need this particular order, we fix the second - we need to swap the calls. Otherwise, it is searched for a long time and the search does not end.

reverso x xr =
    (x === Nil &&& xr == Nil) |||
    (fresh (h t tr)
        (x === Cons (h, t))
        (reverso t tr)
        (appendo tr (Cons (h, Nil)) xr))

This is because interleaving search processes conjuncts sequentially, and no one could think of how to do it differently without losing acceptable efficiency, although they tried. Of course, all solutions will someday be found, but with the wrong order, they will be searched for so unrealistically long that there is no practical sense in this.

There are techniques for writing programs to avoid this problem. But many of them require special skill and imagination to use, and the result is very large programs. An example is the term size bounding technique and the definition of binary division with remainder through multiplication with its help. Instead of stupidly writing a mathematical definition

divo n m q r =
    (fresh (mq)
        (multo m q mq)
        (pluso mq r n)
        (lto r m))

I have to write a recursive definition of 20 lines + a large auxiliary function that is unrealistic to read (I still do not understand what is being done there). It can be found in Will Bird's dissertation in the Pure Binary Arithmetic section.

In view of the foregoing, I would like to come up with some kind of search modification so that simple and naturally written programs also work.

Optimize

We noticed that when everything is bad, the search will not end unless you explicitly indicate the number of answers and break it. Therefore, they decided to fight precisely with the incompleteness of the search - it is much easier to concretize than “it works for a long time”. In general, of course, I just want to speed up the search, but it is much more difficult to formalize, so we started with a less ambitious task.

In most cases, when the search diverges, a situation occurs that is easy to track. If a function is called recursively, and in a recursive call, the arguments are the same or less specific, then in the recursive call another such subtask is generated again and infinite recursion occurs. Formally, it sounds like this: there is a substitution, applying which to the new arguments, we get the old ones. For example, in the figure below, a recursive call is a generalization of the original: you can substitute$$ = [x, 3], $$= x and get the original call.



It can be traced that this situation also occurs in the divergence examples we have already met. As I wrote earlier, when you run appendo in the opposite direction, a recursive call will be made with free variables instead of all variables, which, of course, is less specific than the original call, in which the third argument was fixed.

If we run reverso with x =? and xr = [1, 2, 3], it can be seen that the first recursive call will again occur with two free variables, so new arguments can again obviously be transferred to the previous ones.

reverso x x_r  (* x = ?, x_r = [1, 2, 3] *)
    fresh (h t t_r)
        (x === Cons (h, t))
          (* x_r = [1, 2, 3] = Cons 1 (Cons 2 (Cons 3 Nil)))
             x = Cons (h, t) *)
        (reverso t t_r)
          (* критерий: можно подставить t=x, t_r=[1,2,3], получили исходный вызов *)

Using this criterion, we can detect divergence in the process of program execution, understand that everything is bad with this order, and dynamically change it to another. Thanks to this, ideally, just the right order will be selected for each call.
You can do it naively: if divergence is found in the conjunct, then we hammer in all the answers that he already found and postpone its execution until later, “skipping ahead” the next conjunct. Then, perhaps, when we continue to execute it, more information will already be known and divergence will not arise. In our examples, this will lead to the desired swap conjuncts.

There are less naive ways that allow, for example, not to lose the work already done, postponing the performance. Already with the most stupid variant of changing the order, divergence has disappeared in all simple examples suffering from the non-commutativity of the conjunction, which we know, including:

• sorting the list of numbers (it is also the generation of all permutations of the list),
  
• Peano arithmetic and binary arithmetic,
  
• generation of binary trees of a given size.
  

This was an unexpected surprise for us. In addition to divergence, optimization also fights against program slowdowns. The diagrams below show the execution time of programs with two different orders in conjunctions (relatively speaking, one of the best and one of many bad). It was launched on a computer with the configuration of Intel Core i7 CPU M 620, 2.67GHz x 4, 8GB RAM with the Ubuntu 16.04 operating system.

When the order is already optimal (we select it by hand), optimization slows down execution a little, but it is not critical.


But when the order is not optimal (for example, suitable only for launching in the opposite direction), optimization is much faster. The crosses mean that we just could not wait for the end, it works much longer

How to break nothing

All this was based purely on intuition and we wanted to prove it strictly. Theory after all.

In order to prove something, we need formal semantics of the language. We described operational semantics for miniKanren. This is a simplified and mathematized version of a real language implementation. It uses a very limited (therefore easy to use) version, in which you can specify only the final execution of programs (the search should be final). But for our purposes this is exactly what is needed.

To prove the criterion, the lemma is first formulated: program execution from a more general state will work longer. Formally: the output tree in semantics has a large height. This is proved by induction, but the statement must be very carefully generalized, otherwise the inductive hypothesis will not be strong enough. It follows from this lemma that if a criterion worked during program execution, then the output tree has its own subtree of greater or equal height. This gives a contradiction, since for inductively given semantics all the trees are finite. This means that in our semantics the execution of this program is inexpressible, which implies that the search in it does not end.

The proposed method is conservative: we change something only when we are convinced that everything is already completely bad and impossible to do worse, therefore we do not break anything in terms of program completion.

The main proof contains a lot of details, so we had the desire to formally verify it by writing to Coq . However, it turned out to be quite difficult technically, so we cooled off our ardor and seriously engaged in automatic verification only in the magistracy.

Publication

In the middle of the work, we presented this study at the poster session of ICFP-2017 at the Student Research Competition . There we met with the creators of the language - Will Bird and Daniel Friedman - and they said that it is meaningful and we need to look at it in more detail. By the way, Will is generally friends with our laboratory at JetBrains Research. All of our research on miniKanren began when, in 2015, Will held a summer school in relational programming in St. Petersburg .

A year later, we brought our work to a more or less complete form and presented the article at the Principles and Practice of Declarative Programming 2018.

What do I do in graduate school

We wanted to continue to engage in formal semantics for miniKanren and rigorous proof of all its properties. In the literature, usually properties (often far from obvious) are simply postulated and demonstrated using examples, but no one proves anything. For example, the main book on relational programming is a list of questions and answers, each of which is devoted to a specific piece of code. Even for the statement of completeness of interleaving search (and this is one of the most important advantages of miniKanren over standard Prolog), it is impossible to find a strict wording. You can’t live like that, we decided, and, having received a blessing from Will, we set to work.

Let me remind you that the semantics that we developed at the previous stage had a significant limitation: only programs with finite search were described. In miniKanren, running programs are also interesting because they can list an infinite number of answers. Therefore, we needed more cool semantics.

There are many different standard ways to define the semantics of a programming language, we only had to choose one of them and adapt it to a specific case. We described semantics as a labeled transition system - a set of possible states in the search process and transitions between these states, some of which are marked, which means that at this stage of the search, another answer was found. The execution of a particular program is thus determined by the sequence of such transitions. These sequences can be finite (coming to a terminal state) or infinite, describing simultaneously terminating and not completing programs. In order to completely specify such an object mathematically, one needs to use a coinductive definition.

The semantics described above isoperational - it reflects the true implementation of the search. In addition to it, we also use denotational semantics, which associates some mathematical objects with natural programs in language programs and constructions (for example, relations in a program are considered as relations on many terms, conjunction is the intersection of relations, etc.) The standard way to define such semantics is known as the smallest Erbran model, and for miniKanren it has already been done earlier (also in our laboratory).

After that, completeness of the search in the language, and along with correctness, can be formulated as the equivalence of these two semantics - the coincidence of the sets of answers for a specific program in them. We managed to prove it. It is interesting (and a little sad) that we did without co-induction, using several nested inductions with different parameters.
As a corollary, we also obtain the correctness of some useful language transformations (in terms of the set of obtained solutions): if the transformation obviously does not change the corresponding mathematical object, for example, reordering conjunctions or using distributive conjunctions or disjunctions, then the search results do not change.

Now we want to use semantics to prove other useful properties of the language, for example, criteria for the completeness / divergence or the correctness of additional language constructions.

We also took a more detailed look at a rigorous description of our formalization using Coq. Having overcome many different difficulties and invested a lot of effort, we were able at the moment to set the operational semantics of the language and conduct some evidence, which on a piece of paper had the form “Obviously. Qed. " We do not lose faith in ourselves.