2020-02-02
One of the greatest Star Trek episodes is titled Darmok in Star Trek: The Next Generation. It has the hallmarks of a great Star Trek: TNG episode: a first contact between two civilizations and a dilemma that is not solved by violence but by thinking and understanding.
One of the nicest logic programming languages is miniKanren. This is due to the fact that it is a small, relatively easy to understand Logic Programming (LP) language and has implementations in many programming languages. This later feature allows for logic programming features to be used in many different environments, as a logic programming Domain-Specific language (DSL).
A popular implementation of miniKanren is the core.logic library of the Clojure programming language. In this article we aim to introduce miniKanren/core.logic by encoding story elements of the Darmok episode of Star Trek: TNG (some spoilers for the episode will follow).
The episode is based around the fact that the Federation and the Tamarian people aim to establish successful first contact with each other. From the Federation, the crew of the starship Enterprise are sent to the planet El-Adrel where a Tamarian ship awaits them. Unfortunately attempts at communication fail from both sides and lead to some dangerous situations. The difficulty of communication arises from the fact that Tamarians communicate exclusively through allegory. This means that it is not enough to just decipher the words and grammar used in the Tamarian language, but the crew of the Enterprise must also understand the myths and historical events to which these allegories refer to. Within the episode multiple allegories are used by the Tamarians, such as with the phrase "Darmok and Jalad at Tanagra", that utterly baffle the crew at first. However due to shared dangers and cooperation by the captain of the Enterprise, Picard, and the captain of the Tamarian ship, Darmok, they start to understand each other. In the end a successful first contact is made. This is captured by the newly coined allegory for first contact in the Tamarian language: "Picard and Dathon at El-Adrel".
In this article we will use core.logic to write a logic program to represent the allegories used in the Darmok episode and to generate templates of the Darmok story through a sequence of allegories. A logic program is a bit different than the programs most people are used to. Instead of giving precise instructions to the computer one instead writes a goal, or a group of goals, that provide some logical restrictions on what one intends to achieve. With these goals the logic programming system can find the right answers. Note that the source for the code used this article can be found here in case you want to experiment along while reading this article.
Let's start off with a small logic program that can translate the Tamarian allegory that represents cooperation, the phrase "Darmok and Jalad at Tanagra". We aim to translate this allegory to an equivalent allegory based on a human myth, as well as the English translation for it: "cooperation".
In order to do this we give the Clojure definition of this goal as a logic program, then explain each element of it and how to use it.
(defn cooperation [tam hum eng]
(l/conde [(l/== [tam] ["Darmok and Jalad at Tanagra."])
(l/== [hum] ["Gilgamesh and Ekidu at Uruk."])
(l/== [eng] ["cooperation"])]))
First lets decipher the above definition. For people, unfamiliar with Clojure, the form (defn cooperation [tam hum eng] ... ) defines a function named cooperation with the parameters tam hum eng. The part with (l/conde ... ) is a shorthand for (core.logic/conde ... ); we will use l as the abbreviation for the core.logic namespace in the rest of this article. This l/conde part functions as a way to connect various goals together. It creates a disjunction (elements separated by OR) of separate vectors of goals which it considers as conjunction (elements separated by AND). For people a bit familiar with boolean logic this a way to write a Disjunctive Normal Form. To give a very simplified example the form (l/conde [A B] [C] ) with the goals A, B, C can be seen as a way to find the case where (A 'AND' B) 'OR' C holds. In the previous example l/conde is called on a single vector of elements [(l/== [tam] ["Darmok and Jalad at Tanagra."]) (l/== [hum] ["Gilgamesh and Ekidu at Uruk."]) (l/== [eng] ["cooperation"])], meaning that this function wants each of the goals: (l/== [tam] ["Darmok and Jalad at Tanagra."]) AND (l/== [hum] ["Gilgamesh and Ekidu at Uruk."]) AND (l/== [eng] ["cooperation"]) fulfilled.
So now we know that this function takes three parameters and wants to ensure that the three goals all have to be met. But what do the goals themselves mean? They all have a similar structure in that they are using the equality in core.logic, l/==, to unify elements. Unification is a core part of a logic programming system and it is used to constrain elements to the same possible values. For the first example (l/== [tam] ["Darmok and Jalad at Tanagra."]), the unification aims to ensure that the variable tam has the value of the string "Darmok and Jalad at Tanagra.", which can be seen as the Tamarian phrase for cooperation. The other goals do this unification for the human mythology equivalent: "Gilgamesh and Ekidu at Uruk." of this allegory, as well for the English word "cooperation", for the variables hum and eng, respectively.
We have now given an anatomy of this logic program that does unification on phrases relating to cooperation, but how do we use it? For this we need two things: a set of logic variables and a way to tell the system to run the logic program. The function l\run* does exactly that, which for the given set of parameters tries to find all examples where the goals are fulfilled.
So if we evaluate the following code:
(l/run* [tam hum eng]
(cooperation tam hum eng))
we get the following:
(["Darmok and Jalad at Tanagra." "Gilgamesh and Ekidu at Uruk." "cooperation"])
What l\run* is doing is taking a given list of logic variables and tries to list all the possible values these variables can take. Here it only lists a single possible set of values for the variables tam, hum and eng. This should not be surprising as there is only exactly one way each of the variables tam, hum, and eng can be fulfilled by the "cooperation" goal based on the definition we gave above. The variable tam gets unified with the string value "Darmok and Jalad at Tanagra.", hum with "Gilgamesh and Ekidu at Uruk." and eng with "cooperation".
In the previous case we used only 'fresh' logic variables (variables that have no constraints placed upon their possible values yet), but instead we can also use a specific value in our goal instead. In the following example we only have two variables. Instead of a variable for first parameter used in the cooperation goal we give the string `"Darmok and Jalad at Tanagra." as follows:
(l/run* [hum eng]
(cooperation "Darmok and Jalad at Tanagra." hum eng))
which gives the result:
(["Gilgamesh and Ekidu at Uruk." "cooperation"])
There are only two variables listed in the answer, as there are only two variables given for l/run* to check in our initial case. Otherwise the answer is exactly what we would expect as there is only one possible way these variables can be bound in our logic program.
Now lets try a run where there are no possible valid answers, giving the word "challenge" as a parameter:
(l/run* [tam hum eng]
(cooperation tam hum "challenge"))
This returns an empty list of answers: (), as there are no ways to unify the word "challenge" inside the goal of cooperation.
Given we got the basics of logic programs covered, lets expand our example into something more complex.
Instead of one single allegory, we now define five of them based on the various allegories used in the Darmok episode. The functions representing these goals are all named after the English word translation: failure, common-enemy, cooperation, successful-cooperation and successful-first-contact. They all follow the same structure as the cooperation allegory we previously examined in detail. In addition we also define a function for representing any allegory, aptly named allegory. This is a goal that can be fulfilled by any of the allegories named above.
(defn failure [tam hum eng]
(l/conde [(l/== [tam] ["Shaka, when the walls fell."])
(l/== [hum] ["Gilgamesh, his plant eaten by a snake."])
(l/== [eng] ["failure"])]))
(defn common-enemy [tam hum eng]
(l/conde [(l/== [tam] ["Beast at Tanagra."])
(l/== [hum] ["Bull of Heaven."])
(l/== [eng] ["common-enemy"])]))
(defn cooperation [tam hum eng]
(l/conde [(l/== [tam] ["Darmok and Jalad at Tanagra."])
(l/== [hum] ["Gilgamesh and Ekidu at Uruk."])
(l/== [eng] ["cooperation"])]))
(defn successful-cooperation [tam hum eng]
(l/conde [(l/== [tam] ["Darmok and Jalad on the ocean."])
(l/== [hum] ["Gilgamesh and Ekidu, after the Bull's defeat."])
(l/== [eng] ["successful-cooperation"])]))
(defn successful-first-contact [tam hum eng]
(l/conde [(l/== [tam] ["Picard and Dathon at El-Adrel."])
(l/== [hum] ["Picard and Dathon at El-Adrel."])
(l/== [eng] ["successful-first-contact"])]))
(defn allegory [tam hum eng]
(l/conde [(failure tam hum eng)]
[(common-enemy tam hum eng)]
[(cooperation tam hum eng)]
[(successful-cooperation tam hum eng)]
[(successful-first-contact tam hum eng)]))
There should not be any very surprising elements in this part, but we give two quick observations before continuing.
First, the human equivalent for Tamarian allegories are based on the Gilgamesh story, which is also explicitly mentioned in the episode, that provides a way for captain Picard to connect with the Tamarian captain Dathon. The only exception to this is "Picard and Dathon at El-Adrel." which is an allegory coined at the end of the episode as a term for first contact between cultures. It seems fitting to use this as an allegory from a human perspective as well.
Second, to reiterate how l/conde works with choices, we remark that each of the named allegories in the allegory function are in their own vector (indicated by each goal inside their own [] brackets). This indicates that any of failure, common-enemy, cooperation, successful-cooperation or successful-first-contact can fulfill the goal of allegory.
We can test this later notion by running a short logic program for finding all possible allegories:
(l/run* [tam hum eng]
(allegory tam hum eng))
which returns:
(["Shaka, when the walls fell."
"Gilgamesh, his plant eaten by a snake."
"failure"]
["Beast at Tanagra." "Bull of Heaven." "common-enemy"]
["Darmok and Jalad at Tanagra." "Gilgamesh and Ekidu at Uruk." "cooperation"]
["Darmok and Jalad on the ocean."
"Gilgamesh and Ekidu, after the Bull's defeat."
"successful-cooperation"]
["Picard and Dathon at El-Adrel."
"Picard and Dathon at El-Adrel."
"successful-first-contact"])
This shows five possible answers because, as mentioned, any of the above allegories can fulfill the given goal.
By default l/run* will list all possible answers for a given logic program, which is a very powerful feature for exhaustively searching for all the solutions to a given problem. However this list can be large, and even infinite! In such scenarios there is a way to limit the answers to a certain number when searching by using l/run (note the lack of the * character) directly followed by the number of answers we want returned.
For example, the call:
(l/run 2 [tam hum eng]
(allegory tam hum eng))
will return only two possible answers:
(["Shaka, when the walls fell."
"Gilgamesh, his plant eaten by a snake."
"failure"]
["Beast at Tanagra." "Bull of Heaven." "common-enemy"])
Now as we are getting a bit more familiar with the allegories in this example, we do not want to write out all three versions of each allegory each time. We can do this by defining a new goal allegory-short that succeeds for any phrase that identifies one of the five allegories:
(defn allegory-tam [tam]
(l/fresh [x y]
(allegory tam x y)))
(defn allegory-hum [hum]
(l/fresh [x y]
(allegory x hum y)))
(defn allegory-eng [eng]
(l/fresh [x y]
(allegory x y eng)))
(defn allegory-short [x]
(l/conde [(allegory-tam x)]
[(allegory-hum x)]
[(allegory-eng x)]))
The allegory-short function was defined by writing out the three scenarios by which a phrase could be part of an allegory: it is either the Tamarian allegory, the Human allegory or the English translation. The only new structure we use here from core.logic is l/fresh which lets us introduce new (fresh) logic variables which have no binding as of yet. When using the various forms of l/run the parameters for the function are automatically given as fresh variables, but this function allows us to create them inside other parts of the logic program as well.
Now if we want to list, for example, five possible phrases that form part of an allegory we can call:
(l/run 5 [x]
(allegory-short x))
which will return five of the possible terms that are used as part of allegories.
("Shaka, when the walls fell."
"Beast at Tanagra."
"Darmok and Jalad at Tanagra."
"Gilgamesh, his plant eaten by a snake."
"failure")
With all the functions for logic programming we built up, lets try our hand at creating a logic program that generates variants of the Darmok story expressed through a sequence of allegories. In this scenario, much like in the episode any phrase, a Tamarian- or Human allegory or their English equivalent, could be used to describe parts of the story. In essence we can represent the story as a list of phrases, for example: ("failure", "Beast at Tanagra." "Darmok and Jalad at Tanagra." "successful-first-contact" ).
We could put many restrictions on the order of the phrases, but for the sake of brevity we just want to ensure that each story starts with a phrase for failure and ends with a phrase for successful-first-contact much like the structure of the actual episode. In addition let's assume our stories are only five phrases long.
We can now define logic program to generate such stories as follows:
(defn failure-any [x]
(l/fresh [a1 a2 a3]
(l/conde [(failure x a1 a2)]
[(failure a1 x a2)]
[(failure a1 a2 x)])))
(defn successful-first-contact-any [x]
(l/fresh [a1 a2 a3]
(l/conde [(successful-first-contact x a1 a2)]
[(successful-first-contact a1 x a2)]
[(successful-first-contact a1 a2 x)])))
(defn five-element-story [x1, x2, x3, x4, x5]
(l/fresh [a1 a2 a3]
(l/conde [(failure-any x1)
(allegory-short x2)
(allegory-short x3)
(allegory-short x4)
(successful-first-contact-any x5)])))
Every construct we used to build these functions should be familiar based on the previous examples. We just needed to define two special versions of our goals for the shorthand version of allegories: one for failure and one for successful first contact.
For example if we want five solutions that fulfill all the criteria for such stories we can call the following code:
(l/run 5 [x1 x2 x3 x4 x5]
(five-element-story x1 x2 x3 x4 x5))
which for example could return:
(["Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Picard and Dathon at El-Adrel."]
["Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Picard and Dathon at El-Adrel."]
["Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"successful-first-contact"]
["Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Beast at Tanagra."
"Picard and Dathon at El-Adrel."]
["Shaka, when the walls fell."
"Shaka, when the walls fell."
"Shaka, when the walls fell."
"Beast at Tanagra."
"Picard and Dathon at El-Adrel."])
As one can see the logic program will exhaustively go through all the possible ways the goals can fulfilled and list them up to limit given as a parameter for l/run. The results are not necessarily unique if there are multiple ways to fulfill the goals. This can be seen in the first and second answers as the phrase "Picard and Dathon at El-Adrel." is both the Tamarian and Human allegory for successful first contact.
The above restrictions allow for a lot of the same allegories used within the story. For this, one can define new restrictions and further fine tune the story generation. For example, one can create restrictions on the number of duplicate phrases used, or could ensure that there is more diversity in the phrase type (Tamarian, Human, English) is used. Declaring new restrictions, combining them with existing ones and using the same mechanism to derive any number of answers is one of the core strengths of a logic programming system such as core.logic.
As a final example to show how logic programming can be embedded into a (regular) program, we create a logic program inside a regular Clojure function that creates n-number of stories of a given length. Take a quick look at the following code:
(defn n-element-story [nr-of-elements stories]
(let [vars (repeatedly nr-of-elements l/lvar)
first-var (first vars)
middle (drop-last (rest vars))
last-var (last vars)]
(l/run stories [q]
(l/conde [(l/== q vars)
(l/distincto q)
(failure-any first-var)
(successful-first-contact-any last-var)
(l/everyg allegory-short middle)]))))
Without going too in-depth on every part of this function, it programmatically creates n-number of fresh variables based on the given parameter. It then unifies these with the parameters of a run execution inside the function and returns them. For example, six stories of four elements can be requested by the call:
(n-element-story 4 6)
which will result in the stories:
(("Shaka, when the walls fell."
"Beast at Tanagra."
"Darmok and Jalad at Tanagra."
"Picard and Dathon at El-Adrel.")
("Shaka, when the walls fell."
"Beast at Tanagra."
"Darmok and Jalad on the ocean."
"Picard and Dathon at El-Adrel.")
("Shaka, when the walls fell."
"Beast at Tanagra."
"Gilgamesh, his plant eaten by a snake."
"Picard and Dathon at El-Adrel.")
("Shaka, when the walls fell."
"Beast at Tanagra."
"failure"
"Picard and Dathon at El-Adrel.")
("Shaka, when the walls fell."
"Beast at Tanagra."
"Bull of Heaven."
"Picard and Dathon at El-Adrel.")
("Shaka, when the walls fell."
"Darmok and Jalad at Tanagra."
"Beast at Tanagra."
"Picard and Dathon at El-Adrel."))
There you have it, a very quick overview of using core.logic for logic programming. If you would like to experiment further the code used in this article is available. Here we only scratched the surface of what is possible in a logic programming environment such as core.logic. Feel free to check it out, or any other miniKanren implementation available in your language.
I hope that, much like the Darmok episode, this article has expanded your horizons on communicating. Logic programming is a very interesting, and often underutilized programming paradigm. The core.logic/miniKanren logic programming language is a great system to get started with it. I hope that this, perhaps first, contact with Logic Programming or core.logic aids you in your future endeavors.