Category Archives: Software

Reading the TL2 PAK file

Posted on by

I’m gradually continuing to make progress with FNIStash, gradually being the key word.  It’s pretty tough to learn a new language, decode a file format, and plan a wedding at the same time.

Lately, I’ve been working on a Haskell module to decode the Torchlight 2 PAK file.  The PAK file is a single archive file that contains all the configuration and asset files for the game (well, at least most of them).  I’m hoping to read this PAK file and decode its contents so I can, for instance, grab the bitmaps for the various inventory items and use them in the GUI for FNIStash.

In writing the PAK module, I came tried a few different strategies for parsing the binary data, with varying levels of success.  I won’t describe the PAK format here because it is already well described in the readme file included in CUE’s Torchlight II packer.

Objective

The PAK.MAN file associates a file path to a particular part of the PAK file.  What I’d like to do is create a lookup table of all the files archived in the PAK file.  The key would be the file path, and the value would be the right data out of the PAK file.  I call this a PAKEntry.  So the mapping would look something like

type PAKFiles = M.Map FilePath PAKEntry

with PAK entries being parsed with the following Get operation

getPAKEntry :: Get PAKEntry
getPAKEntry = do
    hdr <- getWord32le
    decSize <- getWord32le
    encSize <- getWord32le
    encData <- getLazyByteString $ fromIntegral encSize
    return $ PAKEntry hdr decSize encSize encData

 

Attempt 1 – Using lazy Get

My first attempt used the lazy binary Get monad.  This was also lazy on my part.  My thinking here was that, since I already head a Get monad operation coded up that could parse out a PAKEntry, I could just add a line at the beginning of that operation that skips to the right part of the file.  Something like

(skip . fromIntegral) (offset-4)

with the offset being passed in as a function argument (so the type signature would be Word32 -> Get PAKEntry).  This worked, but was horrendously slow.  What this does is read all the data of the PAK file into memory up to the offset (approximately), and then reads in as much more as it needs to parse out the PAK entry.  For parsing entries near the end of the 800 MB file, this took a long time.  I used this function to construct the table:

readPAKFiles :: FilePath -> FilePath -> IO PAKFiles
readPAKFiles manFile pakFile = do
    man <- readPAKMAN manFile
    pak <- BS.readFile pakFile
    let fileList = pakFileList man
        offsetList = pakFileOffsets man
        fileOffsetList = L.zip fileList offsetList
        f offset = flip runGet pak ((getPAKEntry . fromIntegral) offset)
        mapList = L.zip fileList (L.map f offsetList) :: [(FilePath, PAKEntry)]
    return $ M.fromList mapList

Attempt 2 – Using strict Get

Attempt 2 used the strict Get monad and strict bytestrings.  The code is nearly identical to attempt 1.  Here, the problem was that the BS.readFile function read in the entire contents of the PAK file to memory, then skipped to the right location of the PAK entry (instead of streaming the file into memory as necessary as it did with lazy strings).  This was *much* faster, but required a huge 800 MB of memory to be read in just to parse out a tiny 26k PNG file (the file I was using for testing.).

Attempt 3 – Handle and lazy Get

Check out the type signature of the PAKFiles type.  It maps a FilePath to a PAKEntry.  No where in that definition is IO mentioned.  So PAKFiles cannot do any IO, by definition.  The previous two attempts have PAKFiles defined as a pure result of parsing binary data read through IO.  What I really needed is for PAKFiles to have this type signature:

type PAKFiles = M.Map FilePath (IO PAKEntry)

Now, the result of a lookup operation is an IO action that retrieves a PAKEntry.

Reading the PAK entry lazily is the behavior I wanted to keep because I didn’t know how much data I needed to read in until after I started reading the entry.  But I didn’t want to lazily read in and throw away the data in order to skip to the right part in the file.  My next attempt used handles:

readPAKFiles :: FilePath -> FilePath -> IO PAKFiles
readPAKFiles manFile pakFile = do
    man <- readPAKMAN manFile
    let fileList = pakFileList man
        offsetList = pakFileOffsets man
        fileOffsetList = L.zip fileList offsetList
        f offset = do
            h <- openBinaryFile pakFile ReadMode
            hSeek h AbsoluteSeek (fromIntegral offset - 4)
            pak <- BS.hGetContents h
            let parsedEntry = flip runGet pak getPAKEntry
            hClose h
            return parsedEntry
        mapList = L.zip fileList (L.map f offsetList) :: [(FilePath, IO PAKEntry)]
    return $ M.fromList mapList

There’s a problem with this, though.  I kept getting errors that the handle was closed before I tried to read it!

Attempt 4 – (Mostly) success with $!

The problem with attempt 3 is that runGet is executed lazily, but hOpen and hClose are not.  When runGet is finally performed, the handle is already closed.  This is easily fixed with the $! operator, which strict evaluates its argument:

readPAKFiles :: FilePath -> FilePath -> IO PAKFiles
readPAKFiles manFile pakFile = do
    man <- readPAKMAN manFile
    let fileList = pakFileList man
        offsetList = pakFileOffsets man
        f offset = do
            withBinaryFile pakFile ReadMode (\h -> do
                hSeek h AbsoluteSeek (fromIntegral offset - 4)
                pak <- BS.hGetContents h
                return $! (flip runGet pak getPAKEntry))
        mapList = L.zip fileList (L.map f offsetList) :: [(FilePath, IO PAKEntry)]
    return $ M.fromList mapList

This version of the operation is fast and uses a low amount of memory.  By “low”, I mean 95 MB to parse out a 26k file.  Something is wrong there, which is my next thing to investigate.  Maybe that will make for another post.

– Update 01/23/2013 –

This post last ended with my creating a lookup table that generated IO actions that returned PAKEntry records.  This turns out to be a horrible idea.  Every time a lookup is made, IO has to be run.  In order to do this, you need to pollute huge parts of your program with the IO monad.  Instead, I reformulated this to be pure and more forward looking – you give the function a clue of what content you want in the table (such as a file path prefix), and it will read all of the necessary files into memory right then and there.  After that, lookups can be done without the IO monad.

Building ATMA for Torchlight 2 (FNIStash)

Posted on by

Back in my old Diablo 2 days, there was an incredible third-party application called ATMA.  ATMA was a muling application for single player.  In Diablo 2, your characters have limited space in your inventory, so you frequently needed to either toss valuable items away or put them on a separate character (called a mule).  ATMA (short for A Tenshi Muling Application) essentially gave you a limitless inventory for your characters.  By modifying the actual Diablo 2 save files, it could “pull” items out of your character’s inventory, store them in a separate and searchable database, and then insert them back into your inventory when you wanted them.

Well, I’ve been playing a little Torchlight 2 recently and found that no similar utility currently exists.  Searching the Torchlight 2 forums reveals a few posts related to the topic, including the scrambling/descrambling algorithm used to obscure the save files, as well as the item format.  Cthon (of clockworkcore.org, I believe) is the furthest along.  He wrote a TL2 character editor that’s quite nice, so I imagine it’s only a matter of time before a nice muling app comes out as well.  The CC website says that the full file specification will be out “hopefully before the end of October.”

Well, I got tired of waiting so I started working on it myself.  Here’s an excerpt of my shared stash data dump after running my code on it:

Full name:  Labarinto Boots
Num Enchants: 1
Item level: 70
Used Sockets: 0/2
Dmg/Armor: 4294967295/51
Num elements: 0
Num mods: 4
Mods: Right [Right

Type: 32833
Name: “OFTHETURTLE ARMOR BONUS”

,Right

Type: 32833
Name: “OFTHEBEAR DAMAGE BONUS”

,Right

Type: 32833
Name: “”

,Right

Type: 33857
Name: “TRINKET_ELECTRICDEFENSE ELECTRICAL DEFENSE”

]
Footer: 0x 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00

The “Right” labels are a Haskell thing indicating something was achieved successfully.  In this case, it’s parsing the mods out of the file correctly.

What I eventually hope to build is a small utility similar to ATMA, which I have tentatively named FNIStash. I want to include basic searchability, and maybe at some point in the future an optimization tool that will automatically select a good set of gear based on certain criteria.  GUI maybe someday, although I’m primarily using this project as a way to learn more Haskell.

I wouldn’t count out clockworkcore.org yet.  I suspect they have something pretty well developed already but are keeping it under wraps until it’s done.

 

Installing Leksah on Windows 7

Posted on by

This past weekend, I convinced myself to give Leksah, the Haskell IDE written in Haskell, a try.  I’m glad I did.  Writing Haskell in it is much more enjoyable than using Notepad++ and WinGHCi side by side.  So much more enjoyable that I actually managed to sit down and write something useful!

Installing Leksah on Windows is not hard, but it is easy to mess up, as I found out.  Here is what I hope is a step-by-step guide to doing it on Windows 7.  Note that this walkthrough assumes you already have GHC installed, probably by installing the Haskell Platform.

  1. Determine your ghc version by typing “ghc –version” at a command prompt.  In my case, it was 7.0.4.
  2. Download the Leksah binary installer that matches your ghc version.  Matching of versions is not optional!
  3. Run the installer and accept the default installation location.  Mine was C:\Program Files (x86)\Leksah\
  4. Start up Leksah (you can search for it in the Start menu).  When you first start up Leksah, you will be asked to provide the path to your cabal packages.  This is so Leksah can process your packages into an explorable database.
  5. Add the packages path into the text field, then click the Add button.  You should see the path listed in the path list as confirmation of your selection.  My path was C:\Users\MyUserName\AppData\Roaming\cabal\packages.  Then click OK.
  6. Leksah will process your installed packages.  This takes a few minutes.  If it looks like Leksah performed this processing really quickly/nearly instantly, then double-check that your Leksah installer matches your ghc version.  (This was my problem for quite a while.)
  7. Leksah saves your package data in a .leksah folder in the top level of your user directory.  If you delete this folder, Leksah will revert its behavior as if it were freshly installed.  This is useful if the guide above doesn’t work for you and you need to debug some stuff but don’t want to endlessly uninstall then reinstall.

And that’s it!  If you need help on using Leksah, try this series of youtube videos.

Converting continuous filters to discrete implementation

Posted on by

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) $$

Testing equivalence of rationals using natural encodings

Posted on by

I’ve recently been spending a decent amount of my free time in self-study of Ulrich Kohlenbach’s Applied Proof Theory: Proof Interpretations and their Use in Mathematics.  As someone who has no experience with Constructivism, it is definitely challenging, but there is no better way to learn than hands-on.  Here I explore one of the topics the book mentions – encoding rational numbers into the naturals – using Haskell.

The idea is simple – take operations on $\mathbb{Q}$ and transform them into operations on $\mathbb{N}$.  We’ll use a special encoding to assign a unique $n \in \mathbb{N}$ for each $q \in \mathbb{Q}$ (yes, there are just as many natural numbers as there are rationals!).  We can then perform operations (in this exercise, equivalence tests) in the encoded set ($\mathbb{N}$) and have the results be valid in the set we care about ($\mathbb{Q}$).  Some of the steps below will seem silly, but this is just an exercise in theory.

The gist is available here.

Before we jump in, we’ll establish some prerequisite machinery for our exploration.  First, we’ll take the Nat instance from the exploration on infinite search and expand it a bit using the nomenclature in Kohlenbach.  Next, we’ll borrow the least function from Seemingly Impossible Functional Programs, slightly modified:

least p = if p 0 then 0 else 1 + least(\n -> p (1 + n))

Lastly, we’ll build the one-point compactification of $\mathbb{N}$ for use in the infinite search monad.  The premise of this monad is that by defining an infinite set, an algorithm for exhaustively searching that set is automatically generated.

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

Now we’re ready for math.

Rationals can be thought of as pairs of integers, one being the numerator $num$ and the other the denominator $den$.  There are two challenges in trying to encode this information into $\mathbb{N}$.

  1. The encoding has two inputs and one output.
  2. Rationals have sign, but the naturals have no sign.

We’ll tackle 2 first.  If $q$ is positive, then its numerator $num$ is mapped to the even natural $2|num|$ and the odd natural $2|num|-1$ otherwise.  In this way, we can encode the sign information in $q$ into the parity of a natural $n_{num}$.  The denominator $den$, on the other hand, maps to separate natural $n_{den}$ through $|den| – 1$.

Now that we have $num$ and $den$ mapping to two naturals, we’ll map the pair of naturals $(n_{num}, n_{den})$ to a single natural $q_c \in \mathbb{N}$, with $q_c$ meaning an encoded rational.  Using the Cantor pairing function

$$j(x^0, y^0) := \left\{ \begin{array}{lr} \mbox{min }u \le (x+y)^2 + 3x + y [2u = (x+y)^2 +3x + y] \mbox{ if it exists} \\ 0\mbox{ otherwise} \end{array} \right. $$

The function numden2QCode below performs this encoding, returning a natural number of type QCode representing a rational from the rational’s numerator and denominator.

numden2QCode :: Integer -> Integer -> QCode
numden2QCode num den  | (num >= 0 && den > 0) || (num <= 0 && den < 0)  = j (fromInteger $ 2*abs(num)) (fromInteger $ abs(den)-1)
                      | otherwise                                       = j (fromInteger $ 2*abs(num)-1) (fromInteger $ abs(den)-1)

j :: Nat -> Nat -> QCode
j x y = if k <= t then QCode k else QCode 0
        where   k = least (\u -> 2*u == t)
                t = (x+y)*(x+y) + 3*x + y

Testing for equivalency of rationals using QCodes might seem like a straightforward process of comparing the QCodes themselves, but one characteristic of the numden2QCode encoding we’ve developed is that $(num, den)$ (1, 2) has a different QCode than (2,4), even though these rationals are equivalent.  To test for equivalence, we’ll project the QCode back into the $n_{num}$ and $n_{den}$ pairs .

$$ j_1(z) := \mbox{min }x \le z[\exists y \le z (j(x, y) = z)] $$

$$ j_2(z) := \mbox{min }y \le z[\exists x \le z (j(x, y) = z)] $$

Here, $z$ is our rational encoding $q_c$, $j_1$ returns $n_{num}$ and $j_2$ returns $n_{den}$.  For example,

>j1 $ j 2 3
S (S Z)

>j2 $ j 3 4
S (S (S (S Z)))

Lastly, to test equivalence, we’ll extend QCode to be an instance of the Eq typeclass.  The trick here is that we need to handle odd and even $n_{num}$ cases separately, since that indicates the rational is positive or negative.  Once we back out the $n_{num}$ and $n_{den}$, we convert back to rational num/den form and equate using cross multiplication.

instance Eq QCode where
(==) n1 n2 | evenNat j1n1 && evenNat j1n2 = (j1n1/2)*(j2n2 + 1) == (j1n2/2)*(j2n1 + 1)
           | oddNat  j1n1 && oddNat  j1n2 = ((j1n1+1)/2)*(j2n2 + 1) == ((j1n2+1)/2)*(j2n1 + 1)
           | otherwise                    = False
           where j1n1 = j1 n1
                 j1n2 = j1 n2
                 j2n1 = j2 n1
                 j2n2 = j2 n2

Finally, we can equate some rationals!

print $ numden2QCode (-1) 1 == numden2QCode (-2) 2 -- True
print $ numden2QCode (-1) 1 == numden2QCode (-3) 3 -- True
print $ numden2QCode (-1) 2 == numden2QCode 2 (-4) -- True
print $ numden2QCode 1 2    == numden2QCode 2 4    -- True
print $ numden2QCode 1 2    == numden2QCode 1 3    -- False

Note that you’ll probably want to compile these into an executable like I did because they are slow otherwise.  In executable form, they are done in about 1.5 seconds.  In a future post, I’ll explore why a few changes to the Num instance for Nat reduced execution time from 88 seconds down to 1.5.

 

Natural numbers and the infinite search monad

Posted on by

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

Posted on by

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)

Problems with Matlab parfor data disappearing

Posted on by

I work a lot in Matlab at work, and Matlab’s object-oriented capabilities in particular.  I encountered a problem that took me a couple hours to debug, and hopefully I can help someone else avoid the experience.

I had my code set up to use a regular for loop when processing serially and a parfor loop when processing with a Matlab pool.  The code worked fine in the serial case, but when using parfor, some of my objects’ properties seemed to be vanishing into empty matrices.  Very literally, one line before the parfor, the object had correctly populated data, and one line within the parfor that data was gone.  No errors from Matlab except errors later on down the road caused from the property being empty.  No indication of what was going on.  No luck finding solutions online.

If you find this happening, the problem is likely with the saving and loading of your object.  Matlab communicates data to each matlab pool worker by serializing the objects, which essentially means saving them in the client thread and having each worker load it back up.  If your object doesn’t save and load correctly, then it won’t get into the parfor loop correctly.

To test the saving and loading, construct an object of the class that’s giving you problems, save it, clear your workspace, then load it.  Inspect the object for missing or incorrect properties.  If you see a problem with a property, check to see if it has a custom set method defined, comment it out, save the updates (and remember to clear classes), and try again.  You should see the data is no longer corrupted.

So what’s happening here?  When Matlab loads objects (either from a mat file or through serialization), it invokes the set method for all properties being loaded.  If an error occurs in a set method during this process, Matlab gives up on setting that property, provides no notice that an error occurred, and just leaves it as the default specified for that property.  Unless your properties block in the classdef says otherwise, the default value for the property will be an empty matrix.

(I have also had problems with handle objects getting into and out of parfor loops, but that wasn’t the problem here.)

In my case, the error I was getting was due to a self-consistency check in my set method.  Before setting the property A, I check to make sure that it is consistent with some other property B.  However, property A was being loaded before property B, so the consistency check always failed on load.  I worked around this by checking to make sure property B was non-empty before doing the consistency check.  This didn’t pose any problems for my class because in normal usage, my property B must always be defined before property A.  Unfortunately, this wasn’t the case when loading or serializing.

An Aside on Set Methods and Loading

In my experience with Matlab OOP, the automatic invoking of set methods on load or serialization has been a significant headache.  As far as I know, the main reason for doing this is so the class version can be checked, and the loaded property modified if necessary to maintain backwards compatibility.  In my experience, I use set methods almost exclusively for type checking and consistency checks on inputs, so any object that doesn’t throw an error has an allowable state, is saved in that allowable state, and should be loaded in that allowable state.  Checking the state again when loading by invoking the set methods is not needed for my uses, and has caused me headaches such as the one outlined above on more than one occasion.

Admittedly, Matlab’s mlint says that you shouldn’t reference one property from another property’s set method.  While I usually follow mlint’s suggestions, this is one I ignore outright as it significantly reduces the utility of set methods in my opinion.  Having users set properties in a natural way, and having the set methods automatically check the correctness of those properties, is by far the best use of set methods I can think of.  If anyone knows of a better way to achieve the same functionality, or a better reason to use set methods, I would love to hear it and learn more.

Sprite Clipper v0.91.1 released

Posted on by

A new version of Sprite Clipper has been released!  This version incorporates some user suggestions from the good people at the Push Button Engine forums, and one user especially.

The updates include

  • Select All now selects in an up/down, left/right order.  Before the order was based on sprite area, and users were frustrated that the sprite ordering on the sheet was not preserved.
  • A new packing method, Grid, has been added.  This puts the sprites in a uniformly spaced grid, which is a format that many game frameworks expect.
  • Fixes to small 1 or 2 pixel positioning bugs.
  • The default connected criterion is now 8 connectivity with a 3 px half edge.  This is probably a better choice for most situations than straight 8 connectivity.

As always, comments, bug reports, complaints, etc. all welcome.

Quick update – Games, Reality, and Haskell

Posted on by

It had been a little while since my last post, so I wanted to just jot down some stuff I’ve been doing lately.

First, in order to learn Haskell, I started working though Haskell’s 99 Questions, which is a series of short functions of increasing difficulty.  I have my solutions hosted on my github repo.

The other thing I have going on is I’m reading Jane McGonigal’s Reality Is Broken.  The book leverages a lot of research in positive psychology to argue that games (the book takes the slant of video games, but really any kind of unnecessary obstacle activity such as rock climbing) are “better” than reality.  The basic argument of the book so far is this: if modern psychological research shows us that people are in their happiest and most activated state when playing games, then why must we endure our normal lives?  Why can we not use the best aspects of games in igniting human happiness and incorporate them into our societies to improve the quality of life of everyone?

I’m less than 100 pages in so far, and I have mixed feelings.  The book does a pretty good job of highlighting interesting findings in positive psychology, and the points made in that regard I feel are spot on.  I would read a short paragraph and think to myself, “You know…you’re right.  That *does* make my happy.”  On the other hand, I think the book really stretches to apply the research findings to the field of video games.  The author, being a game designer, clearly has a bias in this sense, but that also drives her passionate prose style.  She spends a lot of time explaining the mechanics of certain video games like SMB 2 and Tetris, but then fails to really drive home her point that video games are the ideal medium in which to engineer human happiness.  It’s almost like she thinks it is self-evident that games and positive psychology go hand in hand.

Again, I’m only a little ways in, so maybe I’m trying to jump ahead to points she makes (or doesn’t make) later.  I just learned recently that my good friend Seth read this book and wrote a paper on it for a class, so I’m eager to chat with him about it.