Reversing a list
Background
For an overview of Logos, see the getting_started
Livebook.
The problem of reversing a list is a simple, but illustrative demonstration of the expressiveness of logic programming, as well as certain practical considerations. To lay the conceptual and concrete groundwork for a solution in Logos, it makes sense to first develop a solution in pure Elixir. For both the Elixir and Logos implementations, two different recursive algorithms will be presented. One approach is straightforward, but relatively inefficient. The second algorithm makes use of an accumulator and is a more computationally efficient strategy.
Let’s install Logos for later use:
Mix.install([{:logos, git: "https://github.com/epfahl/logos.git"}])
Elixir solution
defmodule Reverse.Elixir do
@doc """
List reversal using a simple recursive approach where the solution is built by
adding the head of the current list to the end of the reverse of the tail. This
appraoch is not tail recursive, and the list concatenation step is relatively
expensive for linked lists.
"""
def reverse1([]), do: []
def reverse1([h | t]), do: reverse1(t) ++ [h]
@doc """
List reversal using a recursive approach where the solution is built by prepending
the head of the current list onto an initially empty accumulator list. This approach
is tail recursive and uses the linked list efficiently.
"""
def reverse2(l), do: reverse2(l, [])
def reverse2([h | t], acc), do: reverse2(t, [h | acc])
def reverse2([], acc), do: acc
end
# Function to roughly estimate execution time in seconds
timer = fn fun ->
fun
|> :timer.tc()
|> elem(0)
|> Kernel./(1_000_000)
end
The docstrings above briefly describe the two solutions and their differences. Let’s verify that they produce the same expected results:
l = [1, 2, 3, 4]
IO.inspect(Reverse.Elixir.reverse1(l))
Reverse.Elixir.reverse1(l) == Reverse.Elixir.reverse2(l)
A simple timing experiment shows that the performance of the two algorithms is very different.
l = 1..10_000 |> Enum.to_list()
t1 = timer.(fn -> Reverse.Elixir.reverse1(l) end)
t2 = timer.(fn -> Reverse.Elixir.reverse2(l) end)
t1 / t2
The accumulator-based algorithm is orders of magnitude faster for sufficiently large lists.
Logos solution
The Logos interpretations of the two algorithms are given below.
defmodule Reverse.Logos do
use Logos
@doc """
Logos interpretation of naive recursive algorithm in `Reverse.Elixir.reverse1`.
"""
defrule reverse1(l, res) do
# An empty list `l` means the result `res` is also empty.
[empty(l), empty(res)]
# For a non-empty list, define 3 new variables: the head `h` and tail `t` of
# the list `l`, as well as a variable `tr` that represents the reverse of `t`.
with_vars [h, t, tr] do
[
# The list `l` is obtained by prepending the head `h` onto the tail `t`.
prepend(h, t, l),
# Recursive step that defines the reverse of the tail as `tr`.
reverse1(t, tr),
# The concatenation of the reverse of the tail `tr` and the list `[h]` with
# only the head is the final result `res`.
concat(tr, [h], res)
]
end
end
@doc """
Logos interpretation of accumulator-based algorithm in `Reverse.Elixir.reverse2`.
"""
defrule reverse2(l, res) do
# Call `reverse2/2` with the accumulator (third arg) initialized to an
# empty list.
reverse2(l, res, [])
end
defrule reverse2(l, res, acc) do
# When the list `l` is empty, the result `res` is bound to the accumulator `acc`.
# This is the only clause that binds `res` or any part of `res` to a value.
[empty(l), equal(res, acc)]
# For a non-empty list, define 2 new variables: the head `h` and tail `t` of the
# list `l`.
with_vars [h, t] do
[
# The list `l` is obtained by prepending the head `h` onto the tail `t`.
prepend(h, t, l),
# Recursive step that reverses the tail `t` and updates the accumulator by
# prepending the head `h` of the list `l`.
reverse2(t, res, [h | acc])
]
end
end
end
The comment annotations above briefly describe the different components of the algorithms.
There are clear parallels with the Elixir implementations. For instance, the clauses that
handle the case where l
is empty are almost direct translations. Also, when an Elixir
function clause pattern matches [h | t]
in the argument, the corresponding Logos clause
is prepend(h, t, l)
, another straightforward translation.
Let’s ensure that these Logos rules behave as expected. First, access the high-level Logos interface:
use Logos
Test the naive implemention:
ask [r] do
Reverse.Logos.reverse1([1, 2, 3, 4], r)
end
|> Enum.take(1)
Good so far. Now for the accumulator-based algorithm:
ask [r] do
Reverse.Logos.reverse2([1, 2, 3, 4], r)
end
|> Enum.take(1)
Both algorithms work as expected for these inputs. As with other Logos rules, it should be
possible to run reverse
in reverse, by putting the “result” in the second argument and
asking for the first argument. Do both algorithms still behave as expected?
ask [l] do
Reverse.Logos.reverse1(l, [4, 3, 2, 1])
end
|> Enum.take(1)
ask [l] do
Reverse.Logos.reverse2(l, [4, 3, 2, 1])
end
|> Enum.take(1)
Excellent! Now let’s take a peak at the relative computational performance of these two approaches:
l = 1..10_000 |> Enum.to_list()
q1 =
ask [r] do
Reverse.Logos.reverse1([1, 2, 3, 4], r)
end
q2 =
ask [r] do
Reverse.Logos.reverse2([1, 2, 3, 4], r)
end
t1 = timer.(fn -> q1 |> Enum.take(1) end)
t2 = timer.(fn -> q2 |> Enum.take(1) end)
t1 / t2
The runtime ratio isn’t nearly as dramatic as in the pure Elixir case, but it’s still true that the accumulator-based solution is much faster. The details of the absolute and relative performances of the Elixir and Logos versions will not be investigated here, but this would be an interesting project.
Both algorithms work as expected in these tests. But these tests are very basic; they don’t
take advantage of the pull power of logic programming. Below is a series of experiments
that dig a little deeper into the expressiveness of Logos. In what follows, only the
accumulator version of reverse (reverse2
) will be used.
# Verify success for given, grounded input and output lists
ask [x] do
Reverse.Logos.reverse2([1, 2, 3], [3, 2, 1])
end
|> Enum.take(1)
# Infer the values in the reverse list
ask [x, y] do
Reverse.Logos.reverse2([1, 2], [x, y])
end
|> Enum.take(1)
# Infer the missing values in the list/reverse-list pair
ask [x, y] do
Reverse.Logos.reverse2([1, 2, x], [3, y, 1])
end
|> Enum.take(1)
# Create a rule that succeeds if a list is a palindrome
defmodule Palindrome do
use Logos
import Reverse.Logos, only: [reverse2: 2]
defrule palindrome(l) do
with_vars [r] do
[reverse2(l, r), equal(l, r)]
end
end
end
import Palindrome
# Verify that the given given list is a palindrome
ask [x] do
palindrome([1, 2, 3, 2, 1])
end
|> Enum.take(1)
# Show the variable structure of all possible palindromes
ask [p] do
palindrome(p)
end
|> Enum.take(10)
# Infer the missing values in the given palindrome
ask [x, y] do
palindrome([1, x, 3, 2, y])
end
|> Enum.take(1)
# Generate 3-letter palindromes from a set of letters
letters = ["p", "a", "e", "i", "o", "u"]
ask [p] do
with_vars [x, y, z] do
[
member(x, letters),
member(y, letters),
member(z, letters),
equal([x, y, z], p),
palindrome(p)
]
end
end
|> Enum.take(10)
Interminable problems
WIP
Check the call stack for take(1) for the naive and accumulated versions.
See The Art of Prolog p109 for backstory.
It looks like this always works when both args are “complete” lists (see The Art of Prolog). Can we have a version of reverse that dispatches to the right version when one or the other side is a complete list?
Resolutions:
- Choose only first solution, regardless of goal ordering
- Ensure both inputs are “complete” lists.
-
A dispatch-based solution that chooses a branch depending on the inputs.
- Can this be done purely logically?