Adderall: appendᵒ, firstᵒ and restᵒ

This time I have been playing around with lists and various relations that are defined with them.

First example is with appendᵒ. This construct is used in conjunction with lists. Essentially “these two lists appended will form the third list”. The example below is used to find all ways of creating list [“a” “b” “c” “d”] with two lists and it will produce 5 different solutions:

(run* [q]
  (fresh (x y)
    (appendᵒ x y ["a" "b" "c" "d"])
    (≡ #t(x y) q)))

[([], ['a', 'b', 'c', 'd']),
(['a'], ['b', 'c', 'd']),
(['a', 'b'], ['c', 'd']),
(['a', 'b', 'c'], ['d']),
(['a', 'b', 'c', 'd'], [])]

Closely related to appendᵒ is firstᵒ and restᵒ. firstᵒ takes the first element of a sequence and restᵒ takes everything else, except the first (so, rest of them, hence the name).

For example, if q is the first element of a sequence and it has value of 1, what possible solutions exists? The answer of course is that there are inifinite amount of solutions, but they can be expressed as [(1 . <‘_.0’>)]. A pair, where first element is 1 and the second element can be anything.

(run* [q]
  (firstᵒ q 1))
[(1 . <'_.0'>)]

Likewise, it is possible to say “if there is a sequence [1 2 3 4] and q is the rest of it, what value q has?” There is only one answer [2 3 4].

(run* [q]
  (restᵒ [1 2 3 4] q))
[[2, 3, 4]]

Now comes something nifty (lifted from Since there is no way to specify the second element of a sequence, we have to write that by ourselves. We could just write required logic every time we needed it, but it is handier to write it as a reusable function:

(defn secondᵒ [l x]
  (fresh [r]
    (restᵒ l r)
    (firstᵒ r x)))

secondᵒ takes two parameters, then it creates a new logical variable as a helper. r is defined to be all but first element of given sequence. x is then defined to be the first element r, which is the second element of l (the original list).

Armed with this new relation, we can revise the original program to consider only answers where first or second element of y is “c”. This effectively limits the possible ansers to two, as shown below:

(run* [q]
  (fresh (x y)
    (appendᵒ x y ["a" "b" "c" "d"])
        [(firstᵒ y "c")]
        [(secondᵒ y "c")])
    (≡ #t(x y) q)))

[(['a'], ['b', 'c', 'd']),
(['a', 'b'], ['c', 'd'])]

This isn’t exactly rocket science, but still couple steps further than in the previous post. We know couple more tools more and can create new ones if existing ones aren’t enough.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s