Category Archives: Languages

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.

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.

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)

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.

Understanding Monads in Haskell

Posted on by

Update: I started reading up on monads again recently, and here is the best explanation I’ve found.  Also, the update caused my Beckman links to vanish unfortunately…

I’ve been digging through the Haskell resources I posted earlier (and some other ones ), and I must say that treatment of  monads has been pretty poor.  There are all kinds of cognitive metaphors out there, the least clear and most ridiculous of which has to be the space station analogy.  However, I think after seeing a few key resources the picture is starting to come together.

First is a great pair of videos from Microsoft’s Brian Beckman.  It’s geared toward concurrency, but he talks about Haskell’s State monad as a way of automatically mutating an explicit (vs implicit) state.  Doing this non-monadically would mean passing in the current state into each function, but with monads, you can construct larger operations by composing the monads together, and the monads will handle all the work of passing around and updating the state.

The videos are pretty long, but quite interesting and really help to introduce the way a particular monad (the State monad) handles compositing.

The next resource is Monads as a computation. This page generalizes the concepts introduced in the videos. Essentially, monads a way of describing how computations are chained together to form more complex computations. The logic of what happens between computations (such as pre- and post-processing) before moving on to the next step is built into the monad (specifically the return and >>= functions).

Lastly, Learn You a Haskell (which, incidentally, I’m beginning to like more than RWH as the concepts get more sophisticated) has a chapter on monads, which goes in to how Maybe and List monads handle their own processing between steps. For instance, if at any point in a Maybe monad chain Nothing is the result, then that Nothing is propagated to the end of the chain (canceling later computations on the way).

From my understanding of monads (so far), they are a convenient way to automatically handle any book keeping that needs to be done between successive operations (Writer monad, which can be used to log all operations performed) or for controlling the flow of operations in a standardized way (aborting operations with Maybe, handling list flattening with List).

Resources for learning about Haskell

Posted on by

As my last post alluded, I’ve started to dive into the world of functional languages.  I chose to go with Haskell over Scala since Haskell is allegedly the most “pure” of the functional languages in use, and I am of the mindset that I should go big or go home.

I’ve started to read a lot about Haskell lately, and do a few toy examples to try to solidify the concepts more.  In my reading, I have come across some good resources.

The first and I think best resource I have found is Real World Haskell.  It goes through Haskell concept quickly with an appropriate amount of dumbing down.

Similar to RWH is Learn You a Haskell for Great Good.  If you find the style of RWH a little too formal, then Learn You a Haskell is for you.  I thought Learn You a Haskell’s style a little charming at first but then rather annoying, so I recommend RWH.

I am still learning about monads, but I think this resource is decent What the hell are monads?.

And then, if you want to know more of the pros and cons of using functional languages (Haskell in particular) I would direct you to a slashdot discussion on the topic as well as this rather recent blog post.