Forem: Vilson Fabricio Juliatto

Understanding the Halting Problem with JavaScript

Vilson Fabricio Juliatto — Thu, 30 Jan 2020 01:35:56 +0000

Understanding the Halting Problem with JavaScript

Sometimes our code has bugs. Well, most of the time. Since our squishy, carbon-based brains are very limited to assess the correctness of our code, it would be nice to get computers to help us. That is what type checkers, linters and other kinds of static analyzers do.

Here I want to focus on one particular problem our programs can have: infinite loops. This might not be the most serious type of bug in the wild. However, if we try to recruit computers to help us with it, we run into a very interesting problem. Understanding this will lead us down a fascinating rabbit hole.

There are programs that always terminate (or halt, thus the name, Halting Problem) and programs that might loop forever, at least for some inputs. We would like to have a program that accepts other programs as input and tells us whether they always terminate. If you have never thought about this, stop for a minute and think about how you would try to implement such a test.

Back yet? Could you do it? It turns out it is impossible to do it. I am not saying it is intractable with our current hardware, or that we haven't figured out how to do it yet. It is logically, mathematically impossible to do it and I will prove that. And, since we seem to live in a world where everything can be done in JavaScript, I will use that to explain the problem.

This is going to be a proof by contradiction. We will start by assuming that we can have a program that tells us whether any given program terminates. That will lead us to a contradiction, implying that our initial assumption is false.

More concretely, imagine we had a function

    function halts(f) {
        // some magic happens here
    }

This should return true if f halts for all inputs and return false if there are any inputs for which f loops forever. For example, consider the following two functions:

    function someRandomFunction(a, b) {
        if (a > b) {
            return 42;
        }
        else {
            return -1;
        }
    }

    function anotherRandomFunction(a, b) {
        if (a > b) {
            return 42;
        } else {
            while(true) {}
        }
    }

someRandomFunction always halts, but anotherRandomFunction will loop forever if the first parameter is not larger than the second. Therefore, halts(someRandomFunction) should be true, while halts(anotherRandomFunction) should be false.

Nothing weird so far, except that I have asked you to accept that the body of that halts function could be filled in some meaningful way. But, if we had halts at our disposal, we could write a function like this:

    function screwy(f) {
        if(halts(f)) {
            while(true) {}
        } else {
            return;
        }
    }

screwy is a higher-order function. It, like halts, accepts a function as input. Then it pulls a switcheroo on us: if the input function halts, screwy loops forever; but if the input function loops forever, screwy terminates. That may be a little mind bending, but it isn't absurd yet.

The absurd, however, is here...

Ready?

What does halts(screwy) return?

In other words, we would like to know whether screwy terminates for all inputs. If we can find any for which it doesn't, we can answer that in the negative. So, does it terminate when given itself as input? That is, does screwy(screwy) ever terminate?

First, let's make sure this makes sense. Looking back at screwy's definition, we see that the only condition on its input is that it's a function — this comes from the same condition being imposed on the inputs to halts. The input can be any function. screwy is a function. There is no reason, then, why it couldn't be given itself as input.

But what happens then? If its input halts, screwy doesn't. Therefore, if screwy acts on itself and it halts, then it doesn't. Similary, if it doesn't halt, then it does.

Say what??? 😲

So, the existence of screwy is absurd. It is logically impossible to have such a function, since that leads to a contradiction. But how can it be impossible? I showed you the definition, it is perfectly valid JavaScript... except for that sneaky call to halts, which I haven't defined and whose existence we just assumed. That is the source of our paradox. If halts existed we would have a contradiction. Therefore, it doesn't exist. It is impossible to have a program that always tells if another given program halts. This is the very famous Halting Problem.

Let me clear up a possible misconception. I'm not saying that if you have a program in front of you it's impossible to say it whether it halts. We have seen examples both of programs that halt and programs that don't. We had no problem figuring out what was the case for each one. What the Halting Problem really says is that you can't have an algorithm that systematically answers this question for every possible program.

Now you may be asking: so what? We can't have a static analyzers that always detects infinite loops. What's the big deal? The big deal is that this reveals a deep and surprising truth about the nature of computation. There are problems that can't ever be solved algorithmically. Not now, not tomorrow, not if we spend the next billion years trying to implement them. We say that they are undecidable. The halting problem is the most famous, but not the only example of an undecidable problem. In fact, the standard way of proving other problems undecidable is by showing them to be equivalent to the Halting Problem. The ever useful Wikipedia has a list such problems.

That's what I had for you today folks. I hope you found it enlightening (or maybe even entertaining?)!

PEDANTIC DISCLAIMER - One could argue that this is not really a fully rigorous, mathematical proof, since that would require us to first define precisely the semantics of JavaScript. I don't know if this has been done rigorously so OK, fair enough. But the essential idea of the proof is what I showed and what remains is "just" to formalize it, with Turing Machines or something else.

Advent of Code 2019 in PureScript - Day 1, part 1

Vilson Fabricio Juliatto — Wed, 04 Dec 2019 01:12:26 +0000

What's this about?

Hi, folks! The Advent of Code 2020 is underway! That is an annual series of small programming puzzles, released daily during Advent. You can find more details about it here.

Since I'm now learning PureScript, I decided to use it to solve the AoC puzzles. I intend to share my solutions here as I write them. Even though my goal is not to teach PureScript now, I hope the code will be more or less understandable even to people who are not familiar with it. If you don't understand anything, don't shy away from asking! Any suggestions of improvements will be highly appreciated too.

The puzzle

The first part of the day 1 puzzle is quite straightforward. There is a rocket, which is composed of several modules. Each module has a certain fuel requirement, according to its mass. The precise statement is:

To find the fuel required for a module, take its mass, divide by three, round down, and subtract 2.

In the examples and in the input given the masses are always integers, so I assumed that to always be the case. Changing the code to work with floats would be easy though, so that's not a big deal.

Computing the fuel for a single module

The implementation is quite simple:

fuelFromMass :: Int -> Int
fuelFromMass mass = mass `div` 3 - 2

For those not familiar with PureScript, however, there are three things that can cause confusion here.

First, the fuelFromMass :: Int -> Int line. That is a type annotation, which means that fuelFromMass is a function that takes as input an Int (a 32 bit integer) and returns another Int. PureScript has type inference, what means that, for simple enough code, the compiler can figure out the types for itself, so that we don't always have to write types explicitly. However, it is a good practice to provide annotations for top level bindings.
Notice that PureScript functions don't require parentheses for their parameters. So, mass is the parameter being passed to fuelFromMass.
What is that weird div in backquotes? div is just the integer division operator. The code above could also be written as haskell fuelFromMass mass = (div mass 3) - 2 However, Purescript allows functions that take two or more parameters to be used in infix position if they are enclosed in backquotes.

Computing the total fuel

Suppose now that we have an array containing the masses of all the modules. We need to do two things: first, compute that the fuel for each one and then sum all of the results to get the total. For someone coming from an imperative background, this sounds like it call for a loop. In functional programming we reach for a map instead. The map function takes two arguments, a function and an array and returns a new array consisting of applying the function to all elements of the input array ¹.

So, if we have an array moduleMasses the corresponding fuel array is simply map fuelFromMass moduleMasses. Then we use the sum function to get the total value:

totalFuel :: Array Int -> Int
totalFuel moduleMasses = sum (map fuelFromMass moduleMass)

Actually, I wrote this as totalFuel = sum <<< (map fuelFromMass). I will not explain here why this is equivalent to what I showed before, because that would require me to explain currying and point-free syntax. But, if you're curious about this, ask me in the comments and I'll be glad to give more details.

Input and Output

This is all the business logic we need. Now it's just plumbing to get the input to the totalFuel function and then print the result to the console. I have the input saved as a text file, where each module's mass is contained in a line. We have to:

Read the file into memory, generating a big string.
Break this string on newlines, generating an array of strings.
Parse each string into a number, generating an array of Ints.
Pass this array to totalFuel.
Print the return value to the console.

Let's tackle each point in order. First, how do we read a file? One important thing which I haven't mentioned so far is that, by default, PureScript compiles down to JavaScript. Therefore, is natural to use the functionality provided by NodeJS (more precisely, its fs module) to interact with the filesystem. One can import JavaScript into PureScript but, fortunately, that will not be necessary here. There is already the purescript-node-fs library which wraps the fs API into a nice, type safe set of PureScript functions. All we are going to need is the readTextFile function. There are some subtleties here regarding how to deal with impure stuff in a pure functional language, involving the dreaded m word, but that is a discussion for another day.

Once we read our text file into a string, we need to split it on newlines. The purescript-strings library has the split function which helps us write things like:

splitOnNewlines :: String -> Array String
splitOnNewlines someString = split (Pattern "\n") someString.

The next step is a bit subtle. We need to turn a String into an Int. There is a function that does it for us: fromString (it can be found on the Data.Int module). However, its type signature, fromString :: String -> Maybe Int, tells us that something more is going on. Why is it not simply String -> Int? The problem is that not every string can be parsed into an integer. For strings like "3", "58649" or "-9503" there is no problem. But something like "34.53" cannot result in an integer. And something like "aRandomString" cannot be parsed into a number at all. Therefore, fromString has to be able to handle failure somehow and the most basic way to do that in strongly typed functional languages is with Maybe.

A type like Maybe Int contains a special value, Nothing, which denotes the absence of a valid value. Then, for example, fromString "34.53" returns Nothing, which signals that it couldn't parse its input. But what does fromString "3" return? It cannot be 3 because that is an Int and we need to return a Maybe Int. The way to wrap an Int into a Maybe Int is with a Just constructor. In other words, fromString 3 returns Just 3.

At the end of the day, we need to work with Int and not with Maybe Int. So, we need to unwrap the Just values and decide what to do with Nothing. For the solution of this puzzle the last point doesn't really make a difference, since the given input contains only valid integers and no Nothing ins generated. However, PureScript doesn't know that and it forces us to be consistent and handle failure appropriately. We do that with the maybe function, which allows us to unwrap a Maybe ², while providing a default value

I wrote this step and the last as a single function

readNumbers :: String -> Array Int
readNumbers = map (maybe 0 identity <<< fromString) <<< (split (Pattern "\n"))

Don't worry if you don't fully understand this. It uses some notation and ideas that I haven't explained, but nothing that will affect what comes later.

We can finally put everything together and write the complete solution:

module Main where

import Data.Int (fromString)
import Data.String.Common (split)
import Data.String.Pattern (Pattern(..))
import Effect (Effect)
import Effect.Console (log)
import Node.Encoding (Encoding(..))
import Node.FS.Sync (readTextFile)
import Prelude (Unit, bind, div, identity, map, show, (-), ($), (<>), (<<<))

main :: Effect Unit
main = do
  text <- readTextFile ASCII "./input.txt"
  log $ "Part 1: " <> (show $ totalFuel <<< readNumbers $ text)

readNumbers :: String -> Array Int
readNumbers = map (maybe 0 identity <<< fromString) <<< (split (Pattern "\n"))

fuelFromMass :: Int -> Int
fuelFromMass mass = mass `div` 3 - 2

totalFuel :: Array Int -> Int
totalFuel = sum <<< (map fuelFromMass)

Hopefully, even folks who are not used to PureScript can at least get the gist of this. Once again, I will be happy to (try to) answer any questions you may have. In the next post I will tackle the part 2 of this puzzle. Thanks for reading!

In reality, map is more general than this. The second argument doesn't have to be just an array, but can be any of a class of things called functors. That's why I avoided writing map's type signature, which, in it's full glory, is map :: forall a b f. Functor f => (a -> b) -> f a -> f b. ↩
You may find it confusing that there are two things called maybe/Maybe, one being a function and another being a type, differing only by capitalization. That is fine because, basically, PureScript, has two namespaces, one for names at the value-level and another for names at the type-level and it distinguishes (this is forced by the compiler) between them with capitalization. In other words, you can't write a type with a lowercase name, nor can you write a function with an capital initial. So, it's easy to know which is which when see pairs like maybe/Maybe. ↩