Hello, declarative world

Basic goals

There are only four kinds of goal in the language we’re building, and two of them are very basic.

The first kind, called equal, is the only kind of goal that isn’t made out of other goals. An equal goal contains two values, and when it’s pursued in a particular state, it tries to make its two values equal by unifying them in that state.

Here’s an example. We’ll make a new state that has some variables in it, and then use a Goal.equal factory method to make a goal that says x is equal to 5:

>> state = State.new
=> #<State @variables=[], @values={}>

>> state, (x, y, z) = state.create_variables [:x, :y, :z]
=> [#<State @variables=[x, y, z], @values={}>, [x, y, z]]

>> goal = Goal.equal(x, 5)
=> #<Goal @block=#<Proc>>

If we pursue that goal in our original empty state, we get back a stream of results:

>> states = goal.pursue_in(state)
=> #<Enumerator: #<Enumerator::Generator>:each>

(We’re using an enumerator to represent a stream here. An enumerator is just an object we can call #next on and keep getting more values out.)

The first result in the stream is a state that says the value of x is 5:

>> state = states.next
=> #<State @variables=[x, y, z], @values={x=>5}>

>> state.values
=> {x=>5}

>> state.value_of x
=> 5

So the goal has succeeded in making x equal to 5.

If we try to retrieve another result from the stream we get a StopIteration exception, because the goal only produced one state:

>> states.next
StopIteration: iteration reached an end

Here’s how Goal.equal is implemented:

def Goal.equal(a, b)
  Goal.new do |state|
    state = state.unify(a, b)

    Enumerator.new do |yielder|
      yielder.yield state if state
    end
  end
end

To construct an equal goal we have to provide the two values, a and b. When the goal is pursued in a particular state, it unifies a and b in that state and produces a stream of states — an enumerator — as its result.

The code inside the Enumerator.new block yields an output state if unification was successful, otherwise it does nothing, so the resulting stream either contains a single state or is empty.

Explicitly creating variables just to pass them to a goal is a bit inconvenient, which is why we have the other kind of basic goal, called with_variables. The job of a with_variables goal is to run an existing goal and automatically provide it with as many local variables as it needs.

For example, we can take an equal goal that expects to use a variable called x, and wrap it up into a with_variables goal so that the local variable x is automatically created when we need it:

>> goal = Goal.with_variables { |x| Goal.equal(x, 5) }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> state = states.first
=> #<State @variables=[x], @values={x=>5}>

>> state.values
=> {x=>5}

This time we didn’t have to create the variable x ourselves — when we pursue the goal and inspect the resulting states, we can see that it’s been created for us.

This is pretty easy to implement in Ruby because we can examine a block with Proc#parameters:

def Goal.with_variables(&block)
  names = block.parameters.map { |type, name| name }

  Goal.new do |state|
    state, variables = state.create_variables(names)
    goal = block.call(*variables)
    goal.pursue_in state
  end
end

We can call Goal.with_variables with a block and get back a goal. When that goal is pursued, it automatically creates the right number of variables for our block, calls it with them, and pursues whatever goal is returned.

Combining goals

So those are the two basic goals: making values equal, and introducing local variables automatically. There are two other kinds of combining goal that we can use to plug together the basic goals to make larger and more interesting ones.

The first combining goal is called either. It combines two goals by pursuing each of them independently and combining their output streams. Every output state from an either goal satisfies either its first or its second subgoal.

Here’s an example of that. We want to be able to say either x equals 5, or x equals 6:

>> goal = Goal.with_variables { |x|
     Goal.either(
       Goal.equal(x, 5),
       Goal.equal(x, 6)
     )
   }
=> #<Goal @block=#<Proc>>

When we pursue that goal in an empty state, the stream we get back has two result states in it:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.values
=> {x=>5}

>> states.next.values
=> {x=>6}

One of them says that x is 5, and the other one says x is 6.

The implementation of Goal.either is very short:

def Goal.either(first_goal, second_goal)
  Goal.new do |state|
    first_stream = first_goal.pursue_in(state)
    second_stream = second_goal.pursue_in(state)

    first_stream.interleave_with(second_stream)
  end
end

It pursues each goal separately, then combines the resulting streams by interleaving them. Unfortunately, there is no Enumerator#interleave_with method in Ruby, so we have to implement that too.

We should be able to interleave, say, a stream of letters and a stream of numbers to get a stream of both letters and numbers:

>> letters = 'a'.upto('z')
=> #<Enumerator: "a":upto("z")>

>> numbers = 1.upto(10)
=> #<Enumerator: 1:upto(10)>

>> letters.interleave_with(numbers).entries
=> ["a", 1, "b", 2, "c", 3, "d", 4, "e", 5, "f", 6, "g", 7, "h", 8,
    "i", 9, "j", 10, "k", "l", "m", "n", "o", "p", "q", "r", "s",
    "t", "u", "v", "w", "x", "y", "z"]

Notice that we get a letter, then a number, then another letter, then another number and so on, and when the numbers run out we just get the rest of the letters.

It would be helpful if this worked even when the streams are infinite. So if we have an infinite stream of the letters 'a', 'b' and 'c' repeating over and over, and an infinite stream of the numbers from 1 up to infinity, we should still be able to interleave them:

>> letters = ['a', 'b', 'c'].cycle
=> #<Enumerator: ["a", "b", "c"]:cycle>

>> numbers = 1.upto(Float::INFINITY)
=> #<Enumerator: 1:upto(Infinity)>

>> letters.interleave_with(numbers).take(50)
=> ["a", 1, "b", 2, "c", 3, "a", 4, "b", 5, "c", 6, "a", 7, "b", 8,
    "c", 9, "a", 10, "b", 11, "c", 12, "a", 13, "b", 14, "c", 15,
    "a", 16, "b", 17, "c", 18, "a", 19, "b", 20, "c", 21, "a", 22,
    "b", 23, "c", 24, "a", 25]

Here’s how to implement it:

class Enumerator
  def interleave_with(other)
    enumerators = self, other

    Enumerator.new do |yielder|
      until enumerators.empty?
        loop do
          enumerator = enumerators.shift
          yielder.yield enumerator.next
          enumerators.push enumerator
        end
      end
    end
  end
end

The inner loop of this implementation bounces back and forth between the two enumerators until they’ve both finished. It relies on Enumerator#next raising a StopIteration exception when each stream runs out, which breaks out of the inner loop and discards the finished stream. If either enumerator is infinite it just keeps going forever.

The other combining goal is called both. It’s slightly more complicated.

It combines two goals by pursuing the first goal to get a stream of states, then pursuing the second goal in each of those states and combining the many resulting streams together. So each state in the final stream satisfies both goals, because it was produced by incrementally satisfying the first goal and then the second one.

Here’s a simple example. We should be able to combine two goals that each produce one state to get one final state; let’s say we want both x to equal 5 and y to equal 7:

>> goal = Goal.with_variables { |x, y|
     Goal.both(
       Goal.equal(x, 5),
       Goal.equal(y, 7)
     )
   }
=> #<Goal @block=#<Proc>>

Sure enough, we get one state back that says x is 5 and y is 7:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.values
=> {x=>5, y=>7}

We can use both can build up more complex goals as well. Here’s a goal that says we want a to equal 7 and b to equal either 5 or 6:

>> goal = Goal.with_variables { |a, b|
     Goal.both(
       Goal.equal(a, 7),
       Goal.either(
         Goal.equal(b, 5),
         Goal.equal(b, 6)
       )
     )
   }
=> #<Goal @block=#<Proc>>

If we pursue that in an empty state, we should get back one state where a is 7 and b is 5, and another where a is 7 and b is 6:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.values
=> {a=>7, b=>5}

>> states.next.values
=> {a=>7, b=>6}

And if we try to pursue two incompatible goals simultaneously, we should get an empty stream back:

>> goal = Goal.with_variables { |x|
     Goal.both(
       Goal.equal(1, x),
       Goal.equal(x, 2)
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.values
StopIteration: iteration reached an end

Pursuing that goal doesn’t produce any results, because there’s no way to make x be both 1 and 2.

Again, Goal.both has a short implementation:

def Goal.both(first_goal, second_goal)
  Goal.new do |state|
    states = first_goal.pursue_in(state)
    second_goal.pursue_in_each(states)
  end
end

It pursues the first goal in the initial state to get a stream of results, and then pursues the second goal in each of those. But again we’re relying on an unimplemented method, this time Goal#pursue_in_each, so here it is:

class Goal
  def pursue_in_each(states)
    Enumerator.new do |yielder|
      first, remaining = states.next, states

      first_stream, remaining_streams =
        pursue_in(first), pursue_in_each(remaining)

      first_stream.interleave_with(remaining_streams).each do |state|
        yielder.yield state
      end
    end
  end
end

This pursues the goal in the first state in the stream, then interleaves the results of that with the results of pursuing the goal in each remaining state.

Pairs

Here’s how a pair should work:

>> pair = Pair.new(5, 9)
=> (5, 9)

>> pair.left
=> 5

>> pair.right
=> 9

We should be able to make a pair of two values, and then later retrieve the left or the right value from the pair.

Fortunately Ruby makes that very easy for us to implement. We can just use a Struct:

Pair = Struct.new(:left, :right) do
  def inspect
    "(#{left.inspect}, #{right.inspect})"
  end
end

The implementation of #inspect lets us see nicely-formatted values in IRB.

Getting our language to “support pairs” means teaching unification to look inside them. For example:

>> goal = Goal.with_variables { |x, y|
     Goal.equal(
       Pair.new(3, x),
       Pair.new(y, Pair.new(5, y))
     )
   }
=> #<Goal @block=#<Proc>>

This goal is trying to make a pair of 3 and x equal to a pair of y and a nested pair of 5 and y. It might not be obvious how to make those things equal, but our unification procedure needs to be able to do it:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> state = states.first
=> #<State @variables=[x, y], @values={y=>3, x=>(5, 3)}>

>> state.values
=> {y=>3, x=>(5, 3)}

The answer is that y has to be 3 and x has to be the pair (5, 3). This can only work if unification knows how to look inside a pair and make it equal to another pair.

That’s actually pretty easy to do. We can take our existing definition of #unify and add an extra clause to it:

class State
  def unify(a, b)
    a, b = value_of(a), value_of(b)

    if a == b
      self
    elsif a.is_a?(Variable)
      assign_values a => b
    elsif b.is_a?(Variable)
      assign_values b => a
    elsif a.is_a?(Pair) && b.is_a?(Pair)
      state = unify(a.left, b.left)
      state.unify(a.right, b.right) if state
    end
  end
end

If #unify finds that it’s trying to make two pairs equal, it just unifies the left elements of the pairs and then unifies the right elements in the resulting state.

We need to teach #value_of to go inside pairs as well: if we ask it for the value of a pair like (x, y), it should be able to extract x and y from the pair, find both their values, and return the pair of them as a result.

It’s easy enough to do that by adding a clause to #value_of:

class State
  def value_of(key)
    if values.has_key?(key)
      value_of values.fetch(key)
    elsif key.is_a?(Pair)
      Pair.new(
        value_of(key.left),
        value_of(key.right)
      )
    else
      key
    end
  end
end

Another little convenience is that the state already keeps track of all the variables that have been declared within it, so instead of looking up variables explicitly by asking “what’s the value of the variable called x?”, we can just ask the state to give us the values of its first few variables:

class State
  def results(n)
    variables.first(n).
      map { |variable| value_of(variable) }
  end

  def result
    results(1).first
  end
end

The #results method finds the first n variables in the state and returns their values, and the shorthand #result method just returns the value of the state’s first variable.

That’s nice because now, whenever we have a state, we can just ask “what’s the value of your first two variables?”, without needing to handle the variables ourselves:

>> state.values
=> {y=>3, x=>(5, 3)}

>> state.variables
=> [x, y]

>> state.results 2
=> [(5, 3), 3]

And it’s even nicer to just be able to ask, “what’s your result?”:

>> state.result
=> (5, 3)

This is just a little convention — when we receive a state containing lots of variables, we can ask it for its result and get the value of its first variable.

Pairs are a little bit boring, but now that we’ve supported them in #unify and #value_of we can build other data structures out of them, and then things start to get interesting.

Lists

For example, as you may know, we can use pairs to encode an array by using a representation called a list.

If we want to represent an array of three values, we can do that by making three nested pairs containing those values along with a magic value that means “empty list”.

Here’s how we could do that in Ruby:

EMPTY_LIST = :empty

def to_list(array)
  if array.empty?
    EMPTY_LIST
  else
    first, *rest = array
    Pair.new(first, to_list(rest))
  end
end

First we pick some special value to represent the empty list — we’re just using the symbol :empty here — and then we write a helper method to recursively convert an array into a list by building nested pairs. If the array is empty then the helper method returns the special empty list value, otherwise it extracts the first element of the array and pairs it up with the result of turning the rest of the array into a list.

If we call #to_list with an array of strings, we get back a list made from nested pairs:

>> to_list ['a', 'b', 'c']
=> ('a', ('b', ('c', :empty)))

We’d like to be able to convert a list back into an array as well. Here’s how to do that:

def from_list(list)
  if list == EMPTY_LIST
    []
  else
    first, rest = list.left, list.right
    [first, *from_list(rest)]
  end
end

If #from_list is called with the empty list then it returns an empty array, otherwise it recursively converts the tail of the list to an array and prepends the head of the list.

So we can turn a list back into an array too:

>> from_list \
     Pair.new('a',
       Pair.new('b',
         Pair.new('c', EMPTY_LIST)
       )
     )
=> ['a', 'b', 'c']

Now that we can turn Ruby’s native arrays into lists, and turn those back into arrays again, we have a way of talking about arrays in our goals. That means we have the power to write goals that make arrays equal. For example:

>> goal = Goal.with_variables { |x, y, z|
     Goal.equal(
       to_list([x, 2, z]),
       to_list([1, y, 3])
     )
   }
=> #<Goal @block=#<Proc>>

This goal tries to make the array [x, 2, z] equal to the array [1, y, 3]. Here’s what happens when we pursue it:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.values
=> {x=>1, y=>2, z=>3}

Pursuing the goal produces a state where x is equal to 1, y is equal to 2 and z is equal to 3. So the goal has been able to compare the two arrays and match up their elements even though we haven’t built explicit support for arrays into the language, because the arrays have been encoded using pairs.

This is particularly interesting because we can also use goals to define operations on the structure of lists, not just individual opaque values inside them.

Here’s a method called #append:

def append(a, b, c)
  Goal.either(
    Goal.both(
      Goal.equal(a, EMPTY_LIST),
      Goal.equal(b, c)
    ),
    Goal.with_variables { |first, rest_of_a, rest_of_c|
      Goal.both(
        Goal.both(
          Goal.equal(a, Pair.new(first, rest_of_a)),
          Goal.equal(c, Pair.new(first, rest_of_c))
        ),
        append(rest_of_a, b, rest_of_c)
      )
    }
  )
end

#append builds a goal which says: the lists a and b joined together are equal to the list c. It’s not worth dwelling on the implementation details, but notice that it’s just built out of our four basic goals. Briefly, it works by saying:

• either a is equal to the empty list, in which case b and c are the same, because appending something to the empty list doesn’t change it;
• or a and c both have the same first element, and if you append the rest of a’s elements with b, you get the rest of c. (There’s a recursive call at the bottom, which talks about appending some smaller lists.)

Don’t get too hung up on the details, but the important thing is that this is essentially a declarative definition of what it means for two lists to be appended to make a third one. It’s written it in a verbose way to make it easier to read, but it’s conceptually very simple.

What’s really interesting about this definition is that there’s no real “input” or “output” — it just constrains a, b and c to have a particular relationship. This definition is really more “relational” than it is “functional”: it defines a specific relation called “append”, and any given values of a, b and c may or may not be related in this specific way.

We can use goals to query this append relation. For example, we can make a goal which says that ['h', 'e'] appended with ['l', 'l', 'o'] is equal to the variable x:

>> goal = Goal.with_variables { |x|
     append(
       to_list(['h', 'e']),
       to_list(['l', 'l', 'o']),
       x
     )
   }
=> #<Goal @block=#<Proc>>

If we pursue that goal in an empty state…

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> state.next.result
=> ("h", ("e", ("l", ("l", ("o", :empty)))))

>> from_list _
=> ["h", "e", "l", "l", "o"]

…we find that the value of x that satisfies this relation is the list encoding of the array ['h', 'e', 'l', 'l', 'o'].

But because our append goal expresses a relation between values instead of a one-way function, we can put that variable in other places. We can ask: if I append x and ['l', 'o'], and the result is ['h', 'e', 'l', 'l', 'o'], what is x?

>> goal = Goal.with_variables { |x|
     append(
       x,
       to_list(['l', 'o']),
       to_list(['h', 'e', 'l', 'l', 'o'])
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> from_list states.next.result
=> ["h", "e", "l"]

The answer is that x is ['h', 'e', 'l']. This is like running a conventional append function backwards, and we get that for free. That’s pretty surprising!

Here’s something even more surprising. We can ask: if appending x and y produces ['h', 'e', 'l', 'l', 'o'], then what are x and y?

>> goal = Goal.with_variables { |x, y|
     append(
       x,
       y,
       to_list(['h', 'e', 'l', 'l', 'o'])
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.results(2)
=> [:empty, ("h", ("e", ("l", ("l", ("o", :empty)))))]

>> _.map { |list| from_list(list) }
=> [[], ["h", "e", "l", "l", "o"]]

The result state says that x is [] and y is ['h', 'e', 'l', 'l', 'o'], so it’s found values of x and y that satisfy the constraint.

But there are more states in the stream! Let’s get the next one:

>> states.next.results(2).map { |list| from_list(list) }
=> [["h"], ["e", "l", "l", "o"]]

It says that x is ['h'], and y is ['e', 'l', 'l', 'o'].

The next state says x is ['h', 'e'] and y is ['l', 'l', 'o']:

>> states.next.results(2).map { |list| from_list(list) }
=> [["h", "e"], ["l", "l", "o"]]

In fact, if we just start the stream again and iterate over it, we get all possible combinations of values that make ['h', 'e', 'l', 'l', 'o'] when appended together:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.each do |state|
     p state.results(2).map { |list| from_list(list) }
   end
[[], ["h", "e", "l", "l", "o"]]
[["h"], ["e", "l", "l", "o"]]
[["h", "e"], ["l", "l", "o"]]
[["h", "e", "l"], ["l", "o"]]
[["h", "e", "l", "l"], ["o"]]
[["h", "e", "l", "l", "o"], []]
=> nil

So not only can we run functions backwards, we can also discover multiple “inputs” that produce the desired “output”. It’s pretty interesting that we can get that behaviour just by expressing what it means to append two lists, and also interesting that this functionality emerges from the simple primitives we built.

Under the hood this is happening through a fairly mundane search strategy encoded in the primitives we built, but the useful thing is the way we’ve expressed the computation we’re interested in and the flexibility of how we’ve been able to interact with it.

Numbers

Let’s briefly try another trick. Instead of encoding arrays as pairs, let’s try encoding numbers. There’s a simple encoding called Peano numbers, where we represent the number 3 as three nested pairs each containing a special increment marker, along with some special zero marker value at the end. It looks like a list of three dummy values:

Here’s how we translate numbers into that encoding. We choose special values to represent zero and increment, and define a method that recursively converts a number into nested pairs:

ZERO, INC = :z, :+

def to_peano(number)
  if number.zero?
    ZERO
  else
    Pair.new(INC, to_peano(number - 1))
  end
end

If we pass in the number 3, it gets turned into three nested pairs:

>> to_peano 3
=> (:+, (:+, (:+, :z)))

We can go the other way too, by starting from zero and recursively incrementing it the appropriate number of times:

def from_peano(peano)
  if peano == ZERO
    0
  else
    from_peano(peano.right) + 1
  end
end

So we can turn three nested pairs back into the Ruby number 3:

>> from_peano \
     Pair.new(INC,
       Pair.new(INC,
         Pair.new(INC, ZERO)
       )
     )
=> 3

Again, this ability to turn numbers into pairs and back again means that we can start talking about them in goals.

For example, we can define a goal like add:

def add(x, y, z)
  Goal.either(
    Goal.both(
      Goal.equal(x, ZERO),
      Goal.equal(y, z)
    ),
    Goal.with_variables { |smaller_x, smaller_z|
      Goal.both(
        Goal.both(
          Goal.equal(x, Pair.new(INC, smaller_x)),
          Goal.equal(z, Pair.new(INC, smaller_z))
        ),
        add(smaller_x, y, smaller_z)
      )
    }
  )
end

This goal says that x added to y is equal to z. It’s similar to append: either x is zero, in which case y and z are the same, or x and z aren’t zero, in which case you can add y to the number one less than x to get the number one less than z. This declaratively specifies what it means for two numbers to add up to a third number.

Once we have #add, we can ask: if 5 added to 3 is x, then what is the value of x?

>> goal = Goal.with_variables { |x|
     add(
       to_peano(5),
       to_peano(3),
       x
     )
   }
=> #<Goal @block=#<Proc>>

When we pursue that goal, we get the answer 8:

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.result
=> (:+, (:+, (:+, (:+,
   (:+, (:+, (:+, (:+, :z))))))))

>> from_peano _
=> 8

But as with append, we can also ask a different kind of question, like: what x added to 3 is equal to 8?

>> goal = Goal.with_variables { |x|
     add(
       x,
       to_peano(3),
       to_peano(8)
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> from_peano states.next.result
=> 5

We get the answer 5. So by defining the notion of addition, we get subtraction for free, just by following the same relation in a different direction.

And we can ask: if x added to y is 8, what are x and y?

>> goal = Goal.with_variables { |x, y|
     add(x, y, to_peano(8))
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.each do |state|
     p state.results(2).map { |peano| from_peano(peano) }
   end
[0, 8]
[1, 7]
[2, 6]
[3, 5]
[4, 4]
[5, 3]
[6, 2]
[7, 1]
[8, 0]
=> nil

We find that x and y can be 0 and 8, or 1 and 7, or 2 and 6, and so on.

One last thing! Here’s another relation on numbers: x multiplied by y equals z.

def multiply(x, y, z)
  Goal.either(
    Goal.both(
      Goal.equal(x, ZERO),
      Goal.equal(z, ZERO)
    ),
    Goal.with_variables { |smaller_x, smaller_z|
      Goal.both(
        Goal.both(
          Goal.equal(x, Pair.new(INC, smaller_x)),
          add(smaller_z, y, z)
        ),
        multiply(smaller_x, y, smaller_z)
      )
    }
  )
end

It’s a similar deal: either x and z are both zero, because zero multiplied by anything is zero, or they’re not zero, and knocking y off z produces the same number as knocking one off x and multiplying by y. That’s confusing but it’s true; it just describes what multiplication is.

But the point of this is that we can ask: what’s 3 multiplied by 8?

>> goal = Goal.with_variables { |x|
     multiply(
       to_peano(3),
       to_peano(8),
       x
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.next.result
=> (:+, (:+, (:+, (:+, (:+, (:+, (:+, (:+,
   (:+, (:+, (:+, (:+, (:+, (:+, (:+, (:+,
   (:+, (:+, (:+, (:+, (:+, (:+, (:+, (:+,
   :z))))))))))))))))))))))))

>> from_peano _
=> 24

The answer is twenty-four.

To finish, let’s ask what x and y can be if their product is 24:

>> goal = Goal.with_variables { |x, y|
     multiply(
       x,
       y,
       to_peano(24)
     )
   }
=> #<Goal @block=#<Proc>>

>> states = goal.pursue_in(State.new)
=> #<Enumerator: #<Enumerator::Generator>:each>

>> states.take(8).each do |state|
     p state.results(2).map { |peano| from_peano(peano) }
   end
[1, 24]
[2, 12]
[3, 8]
[4, 6]
[6, 4]
[8, 3]
[12, 2]
[24, 1]
=> nil

Our system is powerful enough to factorise 24 and tell us that x and y can be 1 and 24, or 2 and 12, or 3 and 8, and so on.

Of course, this is just an illustration of what’s possible. We can make other more complex data structures than lists and Peano numbers, and ask more complex questions about them.