A look at ECS component approaches

For game implementation, an ECS architecture has a lot of things going for it. This approach puts all the components of a particular type (say, all the Transform components) together in memory by component type instead of by the parent entity. In addition to having the flexibility of a general component architecture, the ECS’s use of contiguous memory to store components and Systems to operate on subsets of those components enables high performance processing.

However, there’s a key challenge that many beginner ECS tutorials don’t address. In these explorations, each example of a System simply iterates along a single array or vector of homogeneous components. What possible kind of interesting behavior can be achieved by examining only one kind of Component at a time? Take even the basic task of movement. In a System processing movement, the calculations would probably go something like this.

  1. Examine the Movement component to get linear and rotational velocities.
  2. Calculate the position and rotation change based on time step size.
  3. Modify the Transform component by the calculated deltas.

This example doesn’t even consider relative position to other entities, which would complicate the matter even more. The issue is that single components alone aren’t enough – we need to be able to easily retrieve and operate on multiple component types that are associated with the same entity. There are several approaches to make this easier, and I consider three of them here.

Assumptions

For context, my interest in these approaches is with respect to usage in a platformer game similar in style to Mario or Megaman. I expect games of this type to have the following characteristics:

  • Players move through levels mostly linearly from beginning to end.
  • Most of the entities exist at the start gameplay.
  • Entities are deleted when destroyed by the player.
  • The player typically destroys enemies from beginning to end, so enemies are destroyed in a somewhat predictable sequence.
  • New enemies are spawned near the player’s location.

Based on the above, a reasonable ordering for the components in a contiguous block of memory is to have the entities encountered first be near the end of the memory block. To see why, let’s assume a vector. When an enemy is destroyed, its associated components get removed from each vector of components: its Movement component get removed from the Movement component vector, its Transform component gets removed from the Transform component vector, etc. Ideally, the removed components would be the very last elements of each vector so that, when removed, there is no shifting of elements to fill the space in memory left by the removed component. By ordering the entities (and by extension, their constituent components) such that the ones encountered by the player first are near the end of the vector, we can greatly reduced the amount of element shifting when entities are removed. Similarly, when entities are added to the game, they are added to the end of the vector to limit element shifting.

Approach 1: Index is entity ID

This is one of the approaches described at t-machine. In each component array, the index of the component corresponds to its associated entity. In other words, Movement[8] and Transform[8] are associated with the same entity. If an entity has no component of a particular type, then the bytes at the index for the component type are null.

I’m only going to touch on this briefly because I don’t like some of the difficulties this method raises.

  • While you save some memory by allowing the position of the component to serve as its identifier, you can lose a lot by having lots of null bytes in the component array to “fill in” the spaces for entities that don’t use components of that particular type.
  • You can’t re-use array positions without some tricks. For instance, let’s say that one of the component types stores a reference to a different entity (say, for a targeted missile). The Targeting component could then store the value 8 to mean that the entity represented by position 8 in each component array is the target. But, before the missile hits its target, entity 8 is destroyed or removed by other means. Can entity 8 be replaced by a new entity 8? Will the missile seek out the new entity 8 automatically, and is this the desired behavior? It requires a lot of bookkeeping to get right, which begins to look a lot like the Handle method (also explored below).
  • Some good things are that entity component lookup is O(1) and the contiguous components keeps the cache full. For a game with a big scope, this might matter, but the scope in which I’m interested is much smaller. Also a big win is that it’s easy to iterate along multiple component arrays simultaneously to do per-entity operations using multiple components.

Approach 2: Handles

Handles are a way to keep track of a resource even if it gets moved around, as explained here. Essentially, a handle works similarly to a component index, but instead of encoding the position of the component directly, it encodes the position of an entry in a lookup table that describes where the component is. This is really useful for a number of reasons.

  • There are no more voids in the component array wasting memory, but we are using additional memory for all the bookkeeping data.
  • It allows us to add, remove, shift, and swap components back and forth in the contiguous memory block without losing track. For example, to remove a component, we can swap it with the end component, pop the new end off, and update the lookup table accordingly.
  • Reusing space for a component is the same as reusing an entry in the lookup table. One advantage of handles is that they not only keep track of the position in the lookup table, but they also keep track of which version of the lookup position was used. This allows outdated handles to automatically become invalidated once the corresponding entry is reused for a different resource.

So at first glance, it looks like our problems with Approach 1 are solved! We actually lost something important, though. With Approach 1, a common index in each respective component array both identifies the location of the component’s data and associates the different components together to form an entity implicitly. Handles, however, have no relationship to each other, so while they can be used to find an individual component quickly, they don’t associate different components together.

We have to do the component association on our own. For simple cases, we might get away with one component directly holding the handle for another, but we’ll quickly get handle spaghetti with that approach. Instead, we could have a component reference a container object that holds handles to all components belonging to an entity. If one component needs the data from another, it first references the container, then it finds the handle of the needed component, and then it can get the needed data.

This approach isn’t terrible, but it doesn’t seem very clean to me. Take the Transform and Movement system mentioned earlier. For each Movement component, you must get the association object, then check that a handle to a Transform component exists, then get and modify that data accordingly. It’s very possible that all these lookups and bouncing around in memory might blow the cache performance. It also subtly introduces a pseudo-singleton pattern by requiring a single, almost-global set of component association objects.

Approach 3: Flat map

This approach returns to the simplicity of Approach 1. Instead of association of components implicitly through their position in the array, it is done explicitly using a matching array of IDs. Thus, each collection of components is a vector of IDs and a vector of components of matching length. I like this approach a lot.

  • Deletion of components for existing entities or adding new components to existing entities could happen anywhere in vector and cause elements shifts, but the linear progression of the levels means it will mostly be happening near the end and be rare compared to other calculations.
  • When looking for an individual component, we search in reverse from the end linearly for the matching ID. We can abort the search early if the iteration encounters IDs lower than the desired one. As a future enhancement, we could even save the position of the previous lookup and then start the next linear search from that position, with the expectation of increasing average lookup speed.
  • Iterating across two component lists is easy because it’s essentially performing an operation on the intersection of two sorted arrays. We can iterate across each linearly in an alternating pattern to find the common elements and then apply the desired operation.
  • There’s no external object associating components together. It’s just an ID.
  • One downside is that the onus of generating unique IDs for each entity is now on the programmer. Typically, we want each new entity to have an ID higher than any other entity so that the new components get appended near the end of the vector. This is easily handled with a counter as long as possible rollover is taken into account.

It’s lightweight and flexible. The real downsides are the linear time complexity for searching as well as the shifting of elements when deleting, but I think the expected access pattern will cause those negatives to be negligible.

Comparison of handles and flat map

I implemented Approach 2 and Approach 3 and timed how long it took each to do the same operation. These aren’t scientifically controlled tests by any stretch. I simply implemented the two approaches in a straightforward, obvious way, and did the same for the tests. I call each collection of components an object_manager. Each implementation was used independently of the other in different git branches, so I don’t think there was any coupling between the tests.

Test 1: Add/remove components

In this test, the object manager was populated with 4000 simple components (which were just ints). Then I timed the amount of time it took to:

  1. Add new component 1 at the end.
  2. Add new component 2 at the end.
  3. Remove the previous end component (now third to end).
  4. Remove new component 1.
  5. Remove new component 2.
  6. Repeat this test until component collection is empty.

This insertion and access pattern is supposed to simulate an action platformer. New components 1 and 2 might belong to two new projectiles launched by the player. The first hits an enemy, so the enemy and projectile are removed. The second projectile misses and is removed once out of bounds.

When using the handles methods, my machine did this test in about 0.0002 seconds for 4k elements. Using the flat map method, the time was a greater 0.0002 to 0.0003 seconds.

Test 2: Dual iteration

In this test, two object managers were used. One had 4000 components (doubles) for IDs 0 to 3999, and another had 2000 components (ints) for every odd ID. For the handle case, the components also had the requisite handle pointing to a game object, which was just a struct with handles to both component types. The test was to update the double of C1 with 1.5 times the value of C2’s int for all entities that had both components (i.e., every odd numbered entity) and skip those that did not meet this criterion.

Using the handles method, my machine completed this in about 4e-5 seconds. The flat map method, however, did it in only 1e-5 seconds! The discrepancy is likely caused by all the checking and auxiliary structures needed in the handles method. Each iteration requires following the handle to the game object container, checking whether the matching component exists, then following the handle to the matching component. The flat map just iterates along two sorted ID vectors looking for common elements.

So which one is best?

It’s hard to say which one of the two methods I tested is best. The flat map method is much faster when iterating along component arrays, which is what most of the work is in the game loop. The handle method is a bit faster when creating and deleting components, but that’s a relatively rare occurrence in the game loop. In games, though, the speed of processing doesn’t really matter as long as it’s being done fast enough to render the game at a smooth 60 fps in both normal and exceptional circumstances. In terms of easy of programming use and decoupling, the flat map is my clear favorite.

Converting continuous filters to discrete implementation

Here’s a trick to quickly convert a continuous, strictly proper transfer function into pseudocode for a discrete time implementation.  Let’s start with a first order low pass filter:

$$\frac{Y(s)}{U(s)} = \frac{1}{\tau s + 1}$$

The first step is to cross multiply the terms (for simplicity I’ll omit the Y(s) and U(s) for the rest of this post).

$$\tau sY + Y = U \rightarrow \tau \dot{Y} + Y = U $$

Then solve the transfer function for the highest ordered derivative of $Y$ (meaning the $Y$ term with the most $\cdot$ above it), then integrate both sides of the equation until $Y$ (with no dots) becomes the left hand side.  The integration is with respect to time, but I’ve omitted that for clarity in the expression.

$$ \dot{Y} = \frac{U-Y}{\tau} \rightarrow \int{\dot{Y}} = \int{\frac{U-Y}{\tau}} \rightarrow Y = \int{\frac{U-Y}{\tau}} $$

Now replace the $=\int\left(\right)$ with a $+= dt\left(\right)$ to achieve the following pseudocode

$$ Y += dt\left( \frac{U-Y}{\tau} \right)$$

Here, $dt$ is the time between filter updates, and $Y$ is a static variable whose value persists between filter updates.  What we did is solve for the derivative of the filter output ($\dot{Y}$) and then integrated the derivative using Euler’s method to get the filter’s software implementation.

We can do the same thing with a second order filter:

$$ \frac{Y}{U} = \frac{\omega_n^2}{s^2 + 2\zeta\omega_ns + \omega_n^2} $$

$$\ddot{Y} + 2\zeta\omega_n \dot{Y} + \omega_n^2 Y = \omega_n^2 U \rightarrow \ddot{Y} = -2\zeta\omega_n \dot{Y} + \omega_n^2(U-Y) $$

Here we’ve again solved for the highest ordered derivative of $Y$.  Now what we’ll do is integrate both sides of the equation until we are again left with only $Y$ on the left hand side.

$$ \int{\ddot{Y}} = \int{-2\zeta\omega_n \dot{Y} + \omega_n^2(U-Y)} \rightarrow \dot{Y} = -2\zeta\omega_n Y + \int{\omega_n^2(U-Y)} $$

$$\int{\dot{Y}} = \int{\left(-2\zeta\omega_n Y + \int{\omega_n^2(U-Y)}\right)} \rightarrow Y = \int{\left(-2\zeta\omega_n Y + \int{\omega_n^2(U-Y)}\right)} $$

Let’s break the previous expression into two parts so only one $\int()$ appears on the right hand of any equals sign.

$$ k = \int{\omega_n^2(U-Y)} $$

$$ Y = \int{\left(-2\zeta\omega_n Y + k\right)}$$

Now we pull the same trick we did before by replacing each $=\int()$ with $+= dt()$ to arrive at the software pseudocode.

$$ k += dt\left(\omega_n^2(U-Y) \right)$$

$$ Y += dt\left(-2\zeta\omega_n Y + k \right)$$

Now we have two static variables, $k$ and $Y$, that each represent a separate state variable of the second order filter.

As an exercise for the reader (oh man, did I really just say that?), show that the second order band pass filter

$$ \frac{Y}{U} = \frac{2\zeta\omega_n s}{s^2 + 2\zeta\omega_ns + \omega_n^2} $$

has the following pseudocode implementation

$$ k += dt(-\omega_n^2Y) $$

$$ Y += dt\left(k + 2\zeta\omega_n(U – Y)\right) $$

Natural numbers and the infinite search monad

My previous post explored the usage of infinite search techniques to exhaustively search the natural numbers to find a witness satisfying a total predicate, or decide when no such witness exists.  Turns out, these “searchable” spaces form a monad, available in the infinite search package on hackage.

To use the monad for search across the naturals, we have to first define the set of naturals.  Defining the set is all that is required to start performing infinite searches.  Here is one of my failed attempts at defining the naturals:

natural :: Set Nat
natural = foldr1 union $ map (singleton) $ iterate S Z

What’s wrong with this definition?  It defines the set {Z, S Z, SS Z, …}, which represents the entire space of naturals.  Let’s try to do a search:

> search natural (\x -> x+2 == 1)
Nothing

> search natural (\x -> x*2 == 1)
(infinite loop)

Why does the second predicate above, which works just fine using search’ and lyingSearch from the previous post, fail on this predicate?  The issue is that the search’ function searches across the one-point compactification of the naturals (i.e. including infinity).  Our definition of natural above doesn’t include infinity because every element of the set ends in Z due to the iterate function.  Without infinity, the set is not compact, and hence not searchable.  Thanks goes out to Luke Palmer for providing the correct (and prettier!) definition:

natural :: Set Nat
natural = union (singleton Z) (S <$> natural)

This recursive set definition defines infinity as part of the set, so now…

> search natural (\x -> x*2 == 1)
Nothing

 

 

Infinite search explained

The Haskell subreddit recently had a post about the cleverest piece of Haskell code you know, and the comments ignited a discussion of Martin Escardo’s exhaustive search of the Cantor set, which can be thought of as the set of all infinite chains of 1’s and 0’s.  The techniques are exciting, but initially confounding for many, including me.  I set out to fully understand the processes involved and devoured as many of the sparse resources as I could find.  I didn’t really start to get a mental grip on it until I started playing with code – specifically Luke Palmer’s infinite search code.  This code doesn’t search the Cantor set but instead exhaustively searches the natural numbers, and it’s just a little easier to dissect mentally as a precursor to the Cantor set.  I think I now know how it works, what its limitations are, and how to break it.  My goal is that by reading this post, you’ll come away with the same feeling.

Disclaimer: I am very much a Haskell newbie and not a computer scientist by training.  I just think this stuff is cool.

Representation of natural numbers

First, let’s cover the representation of the domain, the natural numbers.  The representation of natural numbers is defined recursively from Zero:

data Nat = Zero | Succ Nat

That is, a natural number is either Zero, or it is the Succ (successor) of another natural number.  So for instance 0 = Zero, 1  = Succ (Zero), 2 = Succ (Succ (Zero)) etc.  While this may seem cumbersome at first, the key advantage to representing the domain this way is that it makes comparison operations much more powerful.  Consider the comparison

Succ (Zero) /= Zero

which represents that 1 is not equal to 0, which is true.  Now consider what happens if we reformulate the expression as

Succ (?) /= Zero

where ? can be Zero, Succ (Zero), etc.  By examining only the heads of each side of the expression, we are no longer comparing 1 with 0; we are comparing every number greater than or equal to 1 with 0, and like before, the expression is still true.  If we compare

Succ (?) /= Succ (?)

then by examining just the head, we can only claim that the two values being compared are possibly equal.  We cannot even claim to know which values are being compared, except to say that neither is Zero.  So in this case, we have to examine more than just the heads of each expression to determine equivalency.  We in fact have to examine as much of the expression as necessary to find a Zero on either the left side, the right side, or both.  If a Zero does not exist, such as in

infinity = Succ infinity

infinity == infinity

then equivalency can never be determined.  If you try to execute this in GHCi, you’ll get an infinite loop.

These comparison advantages are the reason why Palmer says that in order to use these infinite search techniques, the domain must be representable as a recursive polynomial type, and why Escardo says that the predicate must be computable.  These conditions allow us to construct seemingly infinite comparisons as long as one side of the comparison reduces to something finite eventually.

Testing equivalence

I implemented by own instance of Eq for Nat instead of using Haskell’s derived implementation.  You can see it in the full code listing at the bottom if you’re curious.  Let’s test out some comparisons:

*Main> Succ (Succ (Succ (Zero))) == Succ (Zero)
-- Comparing Succ == Succ --> Possibly equal
-- Comparing Succ == Zero --> Not equal
False

Here we are comparing 3 and 1.  The salient point here is that we can determine that the two values are not equal by only comparing the first two elements of each representation.  The same is true when comparing to infinity:

*Main> infinity == Succ (Zero)
-- Comparing Succ == Succ --> Possibly equal
-- Comparing Succ == Zero --> Not equal
False

Expanding the Num instance

Palmer’s Num instance includes the operations (+), (*), and fromInteger.  The purpose of the first two is clear.  fromInteger takes an integer literal and transforms it into our Nat representation so we can compare it with another Nat representation:

*Main> fromInteger 2::Nat
-- Transforming 2 into Nat form.
---- Returning Succ as element of the transformation
---- Returning Succ as element of the transformation
---- Returning Zero as element of the transformation
Succ (Succ Zero)
*Main> Succ (Zero) == fromInteger 2
-- Transforming 2 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Zero == Succ --> Not equal
False

The operation (-), however, is not defined.  We can define it by adding the following to the Num instance:

Zero   - y = Zero
Succ x - Zero = Succ x
Succ x - Succ y = (x - y)

This definition of (-) carries two caveats.  First, Zero minus anything is Zero.  Consistently, any n – (n + k), where k >= 0 is Zero.  This can lead to unexpected behaviors like

Zero - 130 == Zero
-- Comparing Zero == Zero --> Equal
True

so we need to ensure we are using it appropriately given the properties we have defined for it.

The second caveat is that, unlike addition, subtraction between two Nats cannot be done lazily.  With addition, we know that for any x and y

Succ x + y = Succ (x + y)

so we don’t need to know what x and y are in order to start returning the result because we know it begins with Succ.  However, with subtraction we have

Succ x - Succ y = (x - y)

so we have no idea whether the result will start with Succ or Zero until we traverse x and y and find a Zero in one of them.  Indeed, something like

infinity - infinity

will never return a result.

The search’ function

With the background out of the way, let’s examine the algorithm itself, starting with the search’ function.  You’ll notice that my code throughout this post is slightly different than the Palmer code and littered with trace calls.  These will be useful later when we start exploring examples.

search' fTop    | trace "Starting search.  Starting top level predicate call (TLPC)" fTop $ bestGuess = Just bestGuess
                | otherwise       = Nothing
        where
        bestGuess = trace "The TLPC has no defined x yet, so start building the best guess with lyingSearch" lyingSearch $ fTop

The important thing to note about search’ is that all it does is apply the predicate fTop to a single natural number, bestGuess.  That’s all.  In fact, the entire infinite search algorithm begins when this single application of fTop begins to be evaluated, and ends when fTop finishes its evaluation (the Maybe wrapping notwithstanding).  I changed the name of the predicate in the search’ function to fTop to try to capture this special significance.

The lyingSearch function

The bestGuess that search’ applies fTop to is merely the result of the lyingSearch call made above.  So what does lyingSearch do?  It recursively builds the best-guess solution for satisfying fTop while fTop is being evaluated. Let’s examine the code.

lyingSearch :: (Nat -> Bool) -> Nat
lyingSearch fRec = if trace "Can we finish the best guess with a Zero and succeed?  Let's try it" (fRec Zero)
                    then trace "Yes, so end best guess search with Zero.  Next, complete TLPC" Zero
                    else trace "No, so continue best guess with Succ and do lyingSearch again" (Succ (lyingSearch (fRec . Succ)))

The input argument to lyingSearch, fRec, does two things:

  1. Includes the predicate we are trying to satisfy
  2. Records the progress of the best-guess solution

The record keeping is achieved by composing fRec with an additional Succ each time lyingSearch decides that the next element of the best-guess solution is Succ.  Thus, when search’ first calls lyingSearch with fTop, the best-guess is empty because no Succ’s have yet to be tacked on the end.

Let’s go through lyingSearch step by step. Assume that fRec is fTop composed with zero or more Succ’s that represent the current state of the best guess.  By applying fRec to Zero, we are testing whether or not the next element of the best guess should be Zero.  If true, then the next element should indeed be zero because the predicate fTop will be satisfied.  If false, then we just assume that the rest of the best guess must be Succ plus whatever is produced by another call to lyingSearch.  Assuming this about the best guess does not guarantee that the predicate will be satisfied; we just know that it won’t be satisfied with Zero.  In this way, lyingSearch could eventually return a result that does not satisfy the predicate (a lie).

Example: finding a solution

Let’s go through a few search examples and examine the traces that are produced step by step.  I’ve included some additional annotations to the trace output in parentheses to add a little specificity where needed.

predFxn1 x = let lhs = x*x
                 rhs  = 4
             in trace ("-- Comparing LHS with RHS") (==) lhs rhs
*Main> search' predFxn1
Starting search. Starting top level predicate call (TLPC)
-- Comparing LHS with RHS (This is part of the TLPC)
The TLPC has no defined x yet, so start building the best guess with lyingSearch
Can we finish the best guess with a Zero and succeed? Let's try it
-- Comparing LHS with RHS (This begins the application of fRec to Zero)
-- Transforming 4 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Zero == Succ --> Not equal (This ends the application of fTop to Zero)
No, so continue best guess with Succ and do lyingSearch again
-- Transforming 4 into Nat form. (This is part of the TLPC)
---- Returning Succ as element of the transformation (The first element of the best guess is Succ!)
-- Comparing Succ == Succ --> Possibly equal (4 begins to be compared to (best guess)^2. Best guess so far is just Succ)
Can we finish the best guess with a Zero and succeed? Let's try it
-- Comparing LHS with RHS (This begins the application of fTop . Succ to Zero)
-- Transforming 4 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Zero == Succ --> Not equal (This ends the application of fTop . Succ to Zero)
No, so continue best guess with Succ and do lyingSearch again
---- Returning Succ as element of the transformation (The second element of the best guess is Succ!)
-- Comparing Succ == Succ --> Possibly equal (Continues the comparison of (best guess)^2 to 4 in TLPC)
Can we finish the best guess with a Zero and succeed? Let's try it
-- Comparing LHS with RHS (This begins the application of fTop . Succ . Succ to Zero)
-- Transforming 4 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Zero as element of the transformation
-- Comparing Zero == Zero --> Equal (This ends the application of fTop . Succ . Succ to Zero)
Yes, so end best guess search with Zero. Next, complete TLPC
---- Returning Succ as element of the transformation (Continue and complete comparison of (best guess)^2 to 4)
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Zero as element of the transformation
-- Comparing Zero == Zero --> Equal
Just (Succ (Succ Zero))

This is all well and good, but how does infinite search determine that there is no solution?

Example: finding no solution

No solution exists when we try to satisfy an impossible predicate.  We saw in the last example that whenever we try to end the best guess with Zero but fail, we assume the right path forward is to use a Succ instead.  If the predicate always returns false, then our best guess becomes an infinite chain of Succ’s.  So then how does the algorithm know to give up the search?

predFxn2 x = let lhs = x*x
                 rhs  = 3
             in trace ("-- Comparing LHS with RHS") (==) lhs rhs
*Main> search' predFxn2
Starting search.  Starting top level predicate call (TLPC)
... Uninteresting sections of trace omitted here.  Best guess is now Succ (Succ (Zero)) ...
Can we finish the best guess with a Zero and succeed?  Let's try it
-- Comparing LHS with RHS
-- Transforming 3 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Zero as element of the transformation
-- Comparing Succ == Zero --> Not equal (This is the first time (best guess)^2 overshoots 3)
No, so continue best guess with Succ and do lyingSearch again (Best guess is now Succ (Succ (Succ (Zero))))
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal (This is part of the TLPC)
Can we finish the best guess with a Zero and succeed?  Let's try it
-- Comparing LHS with RHS
-- Transforming 3 into Nat form.
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Succ as element of the transformation
-- Comparing Succ == Succ --> Possibly equal
---- Returning Zero as element of the transformation
-- Comparing Succ == Zero --> Not equal
No, so continue best guess with Succ and do lyingSearch again (Best guess is now Succ (Succ (Succ (Succ (Zero)))))
---- Returning Zero as element of the transformation (We've reached the end of 3's Nat representation in the TLPC)
-- Comparing Succ == Zero --> Not equal (This is the conclusion of the TLPC)
Nothing

What’s interesting here begins on line 14.  The right hand side of the comparison, 3, is not changing, and we know the operation x*x results in a longer and longer series of Succs.  With this information, you and I could conclude that this predicate will never be satisfied.  The algorithm, however, doesn’t conclude that no solution can be found until the same comparison fails in the TLPC (line 31).

To summarize, the infinite search algorithm uses the predicate in two ways:

  1. Deciding what the next element of the best guess should be
  2. Deciding whether or not the best guess succeeds or fails

Usage 2 imposes a constraint on the structure of the predicates we can look to satisfy.  Specifically, the algorithm can only declare that no solution exists if the predicate evaluates to False when given an infinite chain of Succs (i.e. infinity).

Breaking infinite search

With the constraint on the predicate in mind, let’s try to break infinite search.  Here are a couple of simple predicates that work just fine, one with a solution and one without.

predFxn3 x = x*x == 6 - x
predFxn4 x = x*x == 7 - x
*Main> predFxn3 infinity
False
*Main> predFxn4 infinity
False

Now we know that for either of these predicates, search’ will give up the search if no solution exists.

*Main> search' predFxn3
Just (Succ (Succ Zero))
*Main> search' predFxn4
Nothing

Great.  What about these modified predicates, again one with and one without a solution?

predFxn5 x = x*x == 6 + x
predFxn6 x = x*x == 7 + x

When evaluated with infinity, both of these predicates generate an infinite loop because, at the end of the day, we’re evaluating infinity == infinity.  However, predFxn5

*Main> search' predFxn5
Just (Succ (Succ (Succ Zero)))

returns its solution, while search’ predFxn6 looks for one forever and never gives up.  We can try to be clever and reformulate the predicate like this

predFxn7 x = x*x - x == 7

to eliminate infinity from one side, but all we’ve done is replace the non-terminating operator (==) with the non-terminating operator (-).  Alas, predFxn7 will not work, either.

Other explorations

Hopefully I’ve been able to make infinite search a little less confounding, or at least this particular application of it.  Here are some other questions to ponder for the curious mind.  I’ll be pondering these myself.

  • Can Nat infinite search be modified to handle predFxn6 or predFxn7?
  • Can these techniques be used to perform epsilon-delta proofs on compact subsets of the reals?
  • Must all lists contain at least three items?

Code listing

{-- Playing with Haskell infinite search --}

import Debug.Trace

data Nat = Zero | Succ Nat
    deriving (Ord, Show)
infinity = Succ infinity   -- This line is interesting but not necessary

fromInteger' 0 = trace "---- Returning Zero as element of the transformation" Zero
fromInteger' n = trace "---- Returning Succ as element of the transformation" Succ (fromInteger' (n-1))

instance Num Nat where
    Zero   + y = y
    Succ x + y = Succ (x + y)

    Zero   - y = Zero
    Succ x - Zero = Succ x
    Succ x - Succ y = (x - y)

    Zero   * y = Zero
    Succ x * y = y + (x * y)
    fromInteger n = trace ("-- Transforming " ++ show n ++ " into Nat form.") $ x
                    where x = fromInteger' n

instance Eq Nat where
    Succ x == Zero = trace ("-- Comparing Succ == Zero --> Not equal") False
    Zero == Succ x = trace ("-- Comparing Zero == Succ --> Not equal") False
    Zero == Zero = trace ("-- Comparing Zero == Zero --> Equal") True
    Succ x == Succ y = trace ("-- Comparing Succ == Succ --> Possibly equal") (x == y)

-- lyingSearch f returns a Nat n such that f n, but if there is none, then
-- it returns a Nat anyway.
lyingSearch :: (Nat -> Bool) -> Nat
lyingSearch fRec = if trace "Can we finish the best guess with a Zero and succeed?  Let's try it" (fRec Zero)
                    then trace "Yes, so end best guess search with Zero.  Next, complete TLPC" Zero
                    else trace "No, so continue best guess with Succ and do lyingSearch again" (Succ (lyingSearch (fRec . Succ)))

search' fTop    | trace "Starting search.  Starting top level predicate call (TLPC)" fTop $ bestGuess = Just bestGuess
                | otherwise       = Nothing
        where
        bestGuess = trace "The TLPC has no defined x yet, so start building the best guess with lyingSearch" lyingSearch $ fTop

predFxn1 x = let lhs = x*x
                 rhs  = 4
             in trace ("-- Comparing LHS with RHS") (==) lhs rhs

predFxn2 x = let lhs = x*x
                 rhs  = 3
             in trace ("-- Comparing LHS with RHS") (==) lhs rhs

predFxn3 x = x*x == 6 - x
predFxn4 x = x*x == 7 - x
predFxn5 x = x*x == 6 + x
predFxn6 x = x*x == 7 + x
predFxn7 x = x*x - x == 7

 

 

(Continues the comparison of (best guess)^2 to 4 in TLPC)