Prologue - a declarative language capable of solving any rebuses and proving theorems

Imagine a high-level language in which you do not need to specify HOW to get the result, instead you just need to specify WHAT you want to receive. At the same time, the scope of the language is not limited and the language is able to solve the same tasks as any other high-level language, like JAVA. Sounds fantastic, doesn't it? However, such a language is and it is called PROLOG. Let's see how PROLOG does this task using the example of guessing the prologue of some riddles and ask PROLOG to give a proof of the theorem.

Riddle 1. Simple, mathematical. "?" - an arbitrary mathematical operation (+, -, *, /), given the equation ((((1? 2)? 3)? 4)? 5)? 6 = 35. Find unknown operations.

')
Let's start describing what we want to get. Since the sign of the operation is unknown, it will be a parameter.

formula (X1, X2, X3, X4, X5, X6, Sign1, Sign2, Sign3, Sign4, Sign5, Result): -
operation (X1, X2, Sign1, PartialResult1),
operation (PartialResult1, X3, Sign2, PartialResult2),
operation (PartialResult2, X4, Sign3, PartialResult3),
operation (PartialResult3, X5, Sign4, PartialResult4),
operation (PartialResult4, X6, Sign5, Result).

This line describes the formula 1? 2? 3? 4? 5? 6 = Result. In fact, it means: the formula is correct if there is a partial result 1, a partial result 2 ... a partial result 4, such that the operations are correct. However, the prologue does not know what an operation is, so we will describe in which cases they are correct:

operation (X1, X2, "+", Result): - Result = X1 + X2.
operation (X1, X2, "*", Result): - Result = X1 * X2.
operation (X1, X2, "/", Result): - Result = X1 / X2.
operation (X1, X2, "-", Result): - Result = X1 - X2.

We have described the formula, and now we can ask any questions about it. For example, we can ask the following questions: 1) if X1 = 1 X2 = 2 ... X6 = 6 Result = 35 then what are possible operations? 2) the part of the numerical parameters and the part of the operations are indicated, as well as the result, to find out what are the missing parameters? 3) all operations, numerical parameters, result are indicated; find out if the formula is correct. You do not need to worry about how the prologue will find the answer - you just need to ask a question.

So the question is:
askMainQuestion (): -
formula (1,2,3,4,5,6, Sign1, Sign2, Sign3, Sign4, Sign5,35),
stdio :: write (Sign1, Sign2, Sign3, Sign4, Sign5),
stdio :: nl,% new line
fail.

Answer: ++ * ++, + ** + -, *** ++ (To ask a question about numeric parameters, you will have to write a couple more lines, but more on that later.)

Riddle 2. Unpretentious, non-mathematical. Given the names of people and kinstenny relations between them. Find all the brothers.

We indicate specific family ties:
parent ("Tom", "Jake").
parent ("Jim", "Jake").
parent ("Timmi", "Tom").
uncle ("Tom", "Peter").
brother ("Timmi", "Cartman").

Now we will describe what a family relationship means:

brother (Man1, Man2): - parent (Man1, Parent), parent (Man2, Parent), Man1 <> Man2.

(Man1 and Man2 are brothers if there is a ManParent who is the parent for Man1 and Man2, and thus Man1 is not Man2).

brother (Man1, Man2): - parent (ChildMan1, Man1), uncle (ChildMan1, Man2).

(Man 1 and Man 2 brothers, if Man 1 has a child, and Man 2 is the uncle of this child).

Now ask the question of who the brothers are:

askMainQuestion (): -
brother (X, Y)
stdIO :: write (X, "", Y),
stdio :: nl,
fail.



Program output: Timmi Cartman, Jake Peter, Tom Jim, Jim Tom. Compare how much code you would have to write in an imperative programming language.
Now let's look at something more complicated than Hello World-based programs and talk about the prologue pitfalls.

Riddle 3. There are 8 queens on the chessboard. No queen beats another queen. Find the location of queens.

First we describe how the queen can walk:

attack (X1, Y1, X2, Y2): - X2 = X1. % queen can attack if the attacked cell and the source on the same vertical
attack (X1, Y1, X2, Y2): - Y2 = Y1. % queen can attack if the attacked cell and the source on the same horizontal
attack (X1, Y1, X2, Y2): - abs (X2 - X1, Abs), abs (Y2 - Y1, Abs). % ... on one diagonal

Now let us indicate in which cases the queen cannot beat another queen:

any (0).
any (1).
any (2).
any (3).
any (4).
any (5).
any (6).
any (7).
dontAttack (X1, Y1, X2, Y2): -
any (X1), any (Y1), any (X2), any (Y2), not (attack (X1, Y1, X2, Y2)).

This raises the question of why the enumeration of all possible coordinates of the queen (any) is necessary. The point is that the prologue is designed in such a way that it cannot iterate through all possible numeric or string values. All possible values ​​of the value for which the question is asked should be either listed in the code (such as the characters in the example about finding characters), or directly calculated based on the input data in the question (such as the result of the formula in the example about finding characters if the formula does not include rounding errors). Of course, such a restriction makes the prologue not the most convenient language for solving equations; however, this was never the main purpose of this language.

So, we have described what “one queen does not beat another queen”, now you need to specify that each of the 8 queens does not beat the other 7 queens, but writing 8 * 7 = 56 rules is exhausting, therefore we will describe this rule recursively. We define an empty array and we will iteratively add one queen to it one by one.

dontAttack ([]).

(if there are no queens, then no queen beats any other)

dontAttack (X, Y, []): - any (X), any (Y).

(if there is one single queen, then he does not beat other queens)

dontAttack (X1, Y1, [X2, Y2 | OtherElements]): -
dontAttack ([X2, Y2 | OtherElements]), dontAttack (X1, Y1, X2, Y2), dontAttack (X1, Y1, OtherElements).

(if there is a queen with X1 and Y1 coordinates and an array of queens, then none of the queen beats the other, if 1) inside the array of queens none of the queen beats the other 2) queen (X1, Y1) beats the first queen from an array of queens 3) if you remove the first queen from an array of queens, then none of the queens in the received set of queens beat another either)

dontAttack ([X1, Y1 | OtherElements]): -
dontAttack (X1, Y1, OtherElements).

(if there is a queen with X1 and Y1 coordinates and an array of queens, and no queen beats the other, then if you add a queen to an array of queens, then no queen will still beat the other)

Now it remains to ask a question about the coordinates of these queens. However, in order not to get many identical answers, differing only in the number of queens, let's say that the first queen is in the first column, the second - in the second, and so on:

askMainQuestion (): -
X1 = 0, X2 = 1, X3 = 2, X4 = 3, X5 = 4, X6 = 5, X7 = 6, X8 = 7,
dontAttack ([X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8]),
stdio :: write (X1, ":", Y1, "-", X2, ":", Y2, "-", X3, ":", Y3, "-", X4, ":", Y4, " - ", X5,": ", Y5," - ", X6,": ", Y6," - ", X7,": ", Y7," - ", X8,": ", Y8),
stdio :: nl,% new line
fail.

Starting the program and in the same second we get all possible arrangements of queens on the chessboard.

Now let's ask the prologue to prove a simple theorem.

We prove that a subset of a group is a subgroup if and only if, for any elements of A and B from this subset, the result of the product of A and its inverse to B lies in this subset. In order to prove that a subset is a subgroup, it is necessary to prove three points: 1) the neutral element lies in the subset 2) for each element of the subset its inverse element lies in the subset 3) the product of any two elements of the subset lies in the subset.

Denote the neutral element as “E” and define the neutral element:

operation (A, "E", A): - any (A).
operation ("E", A, A): - any (A).

An element is neutral, if, when multiplying any element by a neutral element, the original element is obtained. (for example, in integers 1 is the neutral element).

Add a couple of specific items.

any ("E").
any ("M").
any ("A").
any ("B").
any ("notA").
any ("notB").

There were introduced some other elements, besides “E”, we will explain what these elements are, describing their properties:

ofGroup ("M", "Set").
ofGroup ("A", "SubSet").
ofGroup ("B", "SubSet").

A and B are elements from a subset, M is an element from a set.

obratni ("B", "notB").
obratni ("notB", "B").
obratni ("A", "notA").
obratni ("notA", "A").
obratni ("E", "E").

“NotA” - back to “A”, “notB” - back to “B”

Now we give the definition of the inverse element:

operation (A, B, "E"): - obratni (A, B).
operation (B, A, “E”): - obratni (A, B).

And the opposite of B, if multiplying A by B results in a neutral element (for example, 2 * 0.5 = 1). As you can see, A and B do not have quotes here, which means that there are not specific elements “A” and “B”, but any elements.

Subset definition:

ofGroup (X, "Set"): - ofGroup (X, "SubSet").

(an element belongs to a set if it belongs to a subset)

Now we point out that for any elements of A and B from a subset, the result of the product of A and its inverse to B lies in this subset (by the condition of the theorem).

ofGroup (C, "SubSet"): - obratni (B, NotB), operation (A, NotB, C), ofGroup (A, "SubSet"), ofGroup (B, "SubSet"), stdio :: write (C , "is from subset, because", A, "*", NotB, "=", C, "."), stdio :: nl.

As you can see, here we added the output to the screen (stdio :: write), this is done to trace the actions of the prologue, to learn how the prologue used this rule to see the progress of the proof of the theorem.

Now it remains to prove three points from the theorem.
Ask a question about the neutral element “E”:

firstQuestion (): -
ofGroup ("E", "SubSet"),
stdio :: write ("E is from subset"),
! ..
firstQuestion (): - stdio :: write ("E is NOT from subset").

About the inverse element:

secondQuestion (): -
ofGroup ("notA", "SubSet"),
stdio :: write ("notA is from subset"),
! ..
secondQuestion (): - stdio :: write ("NotA is NOT from subset").

Here you might have a question: you need to prove that for any element of the subset, its inverse element belongs to the subset, but in the prologue question we indicated one single specific element - “notA”. In fact, since we did not impose any restrictions on the “notA” element (except that it is the inverse element of an element belonging to a subset), then if we take any inverse element, then the same arguments will be true for it applied to "notA". Mathematicians often use this technique in proving theorems. This technique is especially important for Prolog, because it cannot iterate through all string and numeric values.

Well, now we will ask a question about belonging to a subset of the result of the product of two elements from a subset:

operation ("A", "B", "AB").
thirdQuestion (): -
operation ("A", "B", AB),
ofGroup (AB, "SubSet"),
stdio :: write ("A * B is from subset"),
! ..
thirdQuestion (): - stdio :: write ("A * B is NOT from subset").

We start ... And the program crashes, hanging, from stack overflow! Let's see why this happened. In fact, the prologue tries to find a solution by looking at the facts entered into it. When searching for the answer to the main question, the prologue goes through all the facts, at least somehow connected with the question. If it is not known whether a fact is true, he in turn goes through all the facts related to this fact. And so, until it reaches unconditional facts, for example, obratni (“A”, “notA”) - “notA” is inverse to “A”. The question was asked: does the neutral element belong to the subset? The prologue sees the rule ofGroup (C, "SubSet"): - obratni (B, NotB), operation (A, NotB, C), ofGroup (A, "SubSet"), ofGroup (B, "SubSet") and understands that if we substitute a neutral element for C and find A and B that satisfy the rule, then according to the rule the neutral element will belong to a subset. The first element among the existing ones is the reverse one (any (“E”)), so Prolog chooses it as B. So, obratni (“E”, NotB). After this, Prolog asks the question: which element is inverse to “E”? - and finds the answer (obratni ("E", "E")). So, NotB = "E". After this, Prolog goes further according to the rule and sees the operation (A, NotB, C), in this case the operation (A, "E", "E") and asks the question: what element when multiplied by "E" gives "E" - and finds the answer “E” (from the rule of operation (A, “E”, “E”): - obratni (A, “E”) and the fact obratni (“E”, “E”).). So, A = “E”. We follow the source rule further: ofGroup (A, “SubSet”), in this case ofGroup (“E”, “SubSet”). And here Prolog tries to answer the same question that we asked at the beginning - but does “E” belong to “SubSet” (neutral to a subgroup)? The program loops and begins again to sort through the same facts and rules, walking in a vicious circle. Well, let's rewrite the original rule:

ofGroup (C, "SubSet"): - obratni (B, NotB), NotB <> "E", NotB <> "M", operation (A, NotB, C), ofGroup (A, "SubSet"), ofGroup (B, "SubSet"), stdio :: write (C, "is from subset, because", A, "*", NotB, "=", C, "."), Stdio :: nl.

Now, you cannot use “E” and “M” as NotB, and the program will not hang (yes, and it also hangs on “M”).
After that, the program at the same second gives proof of the three points of the theorem:

E is from subset, because B * notB = E.
E is from subset
(A and B are in a subset, so the product of A and the inverse of B lies in a subset. In this case, the same element "B" is used instead of A and B. The proof can be made more detailed by adding more write commands to the rules )

E is from subset, because B * notB = E.
notA is from subset, because E * notA = notA.
notA is from subset

E is from subset, because B * notB = E.
notB is from subset, because E * notB = notB.
AB is from subset, because A * B = AB.
A * B is from subset

Conclusion

Prolog is a wonderful declarative language, but the constant hanging does not do him honor (if anyone knows how to deal with this, please share in the comments). In fact, the task of searching for cycles in graphs has been solved a long time ago, and the elimination of a problem at the language level is a completely solvable problem! If this problem were solved, it would be possible to compile a knowledge base of all known mathematical facts, and ask any questions! Or, for example, change one of the basic axioms of mathematics and instantly find out how other laws will change (a la Lobachevsky's geometry in the blink of an eye)! Of course, I am somewhat optimistic, and the language needs a little more refinement, but still ... For example, one of the possible improvements: Prolog should be able not only to get out of the loop, but also to be able to handle the looping according to certain rules in order to operate with endless sequences satisfying condition of the theorem, such as in the Bolzano-Weierstrass theorem . However, in the current state, Prolog is vryat suitable for anything at all: it took me even longer to search for the causes of loops than to prove the theorem itself! (IMHO, just my opinion)