Aranfoolcaytar - ar•an•fool•cay•tar, n: a programmer perennially comporting himself like a fool

Extensible BBCode for Drupal 7

Arancaytar — Tue, 26 Oct 2010 21:43:48 +0000

I'm happy to announce that my extensible BBCode module XBBCode is now ported to Drupal 7. I last worked on (and wrote about) this module in April while writing a new parsing engine for it.

Although the filter was working well, there were many small flaws in the surrounding management code that dealt with storing and editing custom tags and settings, interfaced with Drupal's filter API and handled the installation.

A recent core update to the filter module changed the numerical format IDs to textual names, which makes things lots more easier for automatically created text formats (namespaces, etc), so the required compatibility fix left the installation process far cleaner than it had been before.

Also, the actual tag packages, xbbcode_basic, xbbcode_list and xbbcode_table have been ported, so the module can actually be used beyond custom tags.

Unfortunately, while the Syntax Highlighter tie-in has been ported to Drupal 7, it is useless until the Highlighter module itself is ported. I cleaned it up for Drupal's CVS a few months ago, but it is still only compatible with Drupal 6.

Note that while the module can be installed and used without causing immediate major errors on a clean Drupal 7 install, it has not been exhaustively tested, and small bugs can still remain. It should not be used in production yet.

The release is available at http://ermarian.net/downloads/software/drupal/xbbcode/xbbcode-7.x-2.0.4-....

It can be checked out from SVN at http://svn.ermarian.net/drupal/modules/xbbcode/trunk/xbbcode.

Paper-based computing

Arancaytar — Sat, 23 Oct 2010 19:24:29 +0000

While traveling to a workshop with a friend and family this morning, I had the rare occasion to be not only awed by a piece of technology, but completely flabbergasted at its existence. This friend has a liking for cool gadgets, and what he showed me today had me first suspecting some sleight of hand, then shortly later positively drooling. The best part? It's a fraction of the price of a netbook.

He took out a pen that looked like a fairly ordinary if slightly bulky fountain pen at first glance, but obviously had some technomancy inside as shown by the LED display on the side and some kind of metal charger contacts. He then opened an even more ordinary notebook of plain paper and thumbed through it to some lecture notes he had taken earlier.

Then he uncapped the pen, activated it and tapped a word on the page with the tip.

Instantly, the sounds of the lecture came from the pen's built-in speakers, apparently exactly at the point in the recording that matched the place in the notes.

What the fuck?

Okay, so putting a voice recorder and flash memory in a pen is simplicity itself. Putting sensors into the tip that can record what you write is less easy, though possible when you think about it. But how the hell did the pen know exactly where on the page you tapped it, and what to play from the recording? Looking more closely at the page, I now saw it had some unusual stuff at the bottom - buttons (printed on) that were labeled "Play", "Stop", etc. However, no barcode or anything was visible that would have allowed the pen to pinpoint even its page, leave alone its location.

So how does it work? There has to be something special in the paper. I asked if it was some expensive "smart" paper with electronic gadgetry, but it turned out to be quite as normal as it looked: Some microscopic dots of ink were printed on it (printable with any laser or offset printer), and the camera built into the tip scanned and recognized the unique dot pattern to be able to identify its location.

I had one of those "Holy crap, we're living in the twenty-first century" moments.

And then one of those "WANNA" moments.

Pity the thing is made by only a single producer unwilling to support Linux. While the pen itself is a closed system that works well with loudspeakers or earphones, archiving the notes to a computer requires some kind of proprietary Windows application that is reportedly impossible to run on Wine. Maybe if the market were a bit larger, a reliable open-source driver would be developed, but as this thing has been around since 2008, it probably won't happen so soon. Still, the technology used to accomplish this is awesome.

Server moved, PHP rebuilt

Arancaytar — Mon, 23 Aug 2010 14:28:46 +0000

Yesterday, the entire Ermarian Network was migrated to a different server. After spending the past four years on millhouse, an AMD Opteron machine with two 2GHz cores and 2GB RAM, it is now hosted on carvin a brand new Intel Xeon with four 2.5GHz cores (hyperthreaded to eight virtual cores) and 16GB RAM. These impressive numbers are of course slightly misleading, since I'm one of a great number of users sharing the server.

Naturally, the very first thing that happened after the server move was that all my sites stopped functioning. This was to be expected and warned about, since I was using a PHP interpreter I had compiled myself, dynamically linking against multiple system libraries. With a new system and different version numbers, there was bound to be a mismatch (in this case, libssl.so.0.9.7 being replaced by a newer version). I had to recompile PHP. While doing so, I also decided to switch to the new PHP 5.3.x release (I had been using 5.2.x before).

If you have ever installed software without a package manager, using only ./configure --prefix=$HOME && make && make install, you know what a royal pain this can be. But if you have never done this with PHP, you have no idea. Compiling only the barest essential extensions, those that are packaged with the PHP source, is not that bad. Even linking to mysql is easy. But I use a fairly wide mix of extensions that include cURL, libtidy, mcrypt and PEAR.

Installing this software and then linking with it is an intricate arcane ritual. For example, mcrypt requires both libmcrypt and mhash to be installed, but its installer offers no easy way of looking for those libraries in a custom folder. Since I have to do everything in my $HOME, and no access to /usr/local, that's tricky.

I solved this using the following command:

env LD_LIBRARY_PATH=$HOME/lib LD_FLAGS="-L$HOME/lib -I$HOME/include" ./configure --prefix=$HOME

The -L and -I linking flags tell the compiler to look for libraries and header files in these custom directories.

The second issue was far harder to identify: While running the PHP ./configure script, it cancelled mysteriously and warned that there was an error with the mysql library. Confusingly, it found the mysql library (changing to another path resulted in a different error), but the sample C++ code it tried to use to test the library failed.

Eventually, I found out this was not because of MySQL at all, but because the libltdl library it was trying to include was missing. This was an extra component of libmcrypt, and I had to install it separately using

cd ~/files/installs/libmcrypt/
./configure --prefix=$HOME --enable-ltdl-install && make && make install

After doing this, the configure script ran through, as did the compilation and installation.

I then had to update a few symbolic links, rename the php-cgi file to php.cgi (to this day I have no idea why this is required), and add the old php.ini, and the Ermarian Network was once again functioning, now on PHP 5.3.3!

Note that Drupal 5 uses many deprecated functions, and its error handler does not recognize the new DEPRECATED bitmasks (8192 and 16384) of PHP 5.3.3, leading to a lot of "undefined offset" notices. That was also easy enough to fix, however.

Code Jam 2010

Arancaytar — Sat, 08 May 2010 23:27:22 +0000

The first qualification round of the Google Code Jam just ended, and I managed to scrape through with two of the three problems solved in time. On the third, unfortunately, I failed to take into account the orders of magnitude of complexity, and my algorithm was not fast enough to solve the larger input case.

Since the round is now closed, I can publish the solutions I used without unfairly influencing the competition. (Don't read on if you want to figure it out for yourself, though. It's really fun to solve on your own.)

Problem 1: Snappers

The Snapper is a clever little device that, on one side, plugs its input plug into an output socket, and, on the other side, exposes an output socket for plugging in a light or other device.

When a Snapper is in the ON state and is receiving power from its input plug, then the device connected to its output socket is receiving power as well. When you snap your fingers -- making a clicking sound -- any Snapper receiving power at the time of the snap toggles between the ON and OFF states. [read on]

The beautiful simplicity of this problem is obvious as soon as you consider the pattern of switches on each clap:

Having established that the switches follow the progression of binary numbers, it is also clear what property the binary number must have for the light to be on: All switches must be switched on; the binary number (from the nth digit to the right) has to completely consist of ones. That means if you add one to the number, that pattern must consist of zeros.

It is possible to do all this using modulo arithmetic, but I thought using actual bitwise operators might be somewhat faster.

def snapper(n, k):
    # Add one to the number, AND it with the number "2^n-1", check for 0.
    return (k+1) & ((1<<n) - 1) == 0
 
def main():
    labels = ["OFF", "ON"]
    try:
        cases = xrange(1, int(raw_input())+1)
        for case in cases:
            n, k = map(int, raw_input().split())
            print "Case #%d: %s" % (case, labels[snapper(n, k)])
    except ValueError:
        print "INVALID INPUT"
 
main()

Problem 2: Doomsday

On our planet, Jamcode IX, three Great Events occurred. They happened 26000, 11000 and 6000 slarboseconds ago. In 4000 slarboseconds, the amount of time since all of those events will be multiples of 5000 slarboseconds, the largest possible amount... and the apocalypse will come.

This one was a bit trickier. Obviously, you will immediately be thinking along the right lines of what is required here: Modulo arithmetic and greatest common divisors. Hope you have the Euclidean algorithm fresh in your mind (gcd a b = b ? (gcd b a%b) : a). However, it is not immediately clear what you need to do with those numbers. Clearly, 26000, 11000 and 6000 have nothing in common, divisor-wise, with 5000.

Naturally, the differences between these numbers do. You will find that regardless of the order of the numbers, the intervals between them have the same greatest common divisor - 5000. Even more, it can be shown that any group of numbers shares a remainder class for the greatest common divisor of their differences - 1000 in this case. The complement of this remainder class (4000) is the doomsday time we are looking for.

So the algorithm looks like this:

def doomsday(events):
    T = gcd_n(intervals(events))
    return -events[0] % T
 
# Absolute values of the intervals between N numbers.
def intervals(z):
    return [abs(a-b) for a, b in zip(z, z[1:])]
 
# Greatest Common Divisor of N numbers.
def gcd_n(z):
    # gcd(a, b, c) = gcd(gcd(a,b), c)
    return reduce(gcd_2, z)
 
# Greatest Common Divisor of 2 numbers.
def gcd_2(a, b):
    while b:
        a, b = b, a % b
    return a
 
def main():
    try:
        cases = xrange(1, int(raw_input())+1)
        for case in cases:
            line = map(int, raw_input().split())
            n, events = line[0], line[1:]
            assert n == len(events)
            print "Case #%d: %d" % (case, doomsday(events))
    except:
        print "INVALID INPUT"
            
main()

Problem 3: Theme Park

The roller coaster can hold k people at once. People queue for it in groups. Groups board the roller coaster, one at a time, until there are no more groups left or there is no room for the next group; then the roller coaster goes, whether it's full or not. Once the ride is over, all of its passengers re-queue in the same order. The roller coaster will run R times in a day.

This is the problem I didn't manage to solve in time. I had two implementations using the same approach, one in Haskell and one in Python. Both did not scale well, as the algorithm ran in linear time and the final input differed by orders of magnitude from what I had tested it with.

-- Does the next group fit aboard?
  if (length queue > 0) && (head queue <= size - sum aboard)
  -- Then let them pay, leave the queue and step aboard.
  then advance rides size (tail queue) (aboard++[head queue]) (profit + (head queue))
  else
    -- Otherwise, are there rides left?
    if rides > 1
    -- Then let everyone disembark and requeue for the next ride.
    then advance (rides - 1) size (queue++aboard) [] profit
    else profit
    
-- Start out with an empty ride and no profit.
start rides size queue = advance rides size queue [] 0

def rollercoaster(rides, size, queue):
    profit, aboard = 0, 0
    while rides > 0:
        i, aboard = 0, 0
        for x in queue:
            if aboard + x > size:
                break
            i, aboard = i + 1, aboard + x
        profit += aboard
        queue = queue[i:] + queue[:i]
        rides -= 1
    return profit
 
def main():
    cases = xrange(1, int(raw_input())+1)
    for case in cases:
        rides, size, queue_len = map(int, raw_input().split())
        queue = map(int, raw_input().split())
        assert queue_len == len(queue)
        print "Case #%d: %d" % (case, rollercoaster(rides, size, queue))
main()

Hard drives and stupidity do not mix

Arancaytar — Thu, 29 Apr 2010 07:39:15 +0000

At 0400 on Wednesday (yesterday), my home partition suddenly disappeared. I didn't have a clue what had happened, but the problem persisted on reboot.

Now, Enki has two hard drives - one contains /home, and one contains my backups. I was able to mount the backup drive manually, but the one containing /home appeared to be unresponsive.

So I took out what I assumed to be the defective drive. I then connected it to a different computer and was instantly smelling magic smoke.

After buying a new drive, I built it in and launched Puppy Linux to partition it and set up a new /home. My first priority, though, was to copy all files off the backup partition in case that failed too. It's amazing how diligently you make backups on the day after losing data (... and a dollar short.)

So I mounted what I presumed to be the backup drive, and saw... /HOME.

First thought: Oh wow. It's all still here. I'm saved. There's some stuff on the backup drive too that I'll miss, but not really a lot.
Second thought: This means I not only built out the wrong drive, it also means I killed it through mishandling (since it was working a moment earlier).
Third thought: Actually, I killed it for absolutely no reason, because even what seemed broken was in fact okay.

Final thought, just now: Actually, the last one makes it hurt most, but is also the best. Imagine if my /home had died, and in trying to fix it I'd destroyed the only backup of it. Now THAT would suck.

Building a better Tag-Parser, part 2

Arancaytar — Fri, 16 Apr 2010 12:11:34 +0000

As I concluded in the first part, one problem remains with the strict "inner-tag-first" evaluation of code (which roughly equates to a Left-Right-Root traversal of the code tree). Namely, some tags, like [nocode], require that further code inside them is not parsed.

At first glance, this looks easy: Just determine if the currently open tag allows any code inside it, and ignore any opening tags otherwise until it closes (other closing tags must still be examined in case the nocode tag is dangling). There are multiple conditions where this fails:

The [nocode] tag is not closed. Even though it is ultimately discarded, all tags following it will remain unrendered. "Discarded" tags should not influence the rendering.
The tag is discarded because its parent tag is closed before it itself is. This causes the same problem as condition 1, up to the closing parent tag.
Even with valid code, if the nocode tag contains a valid pair of tags, and the opening one is ignored, then the closing one may be misinterpreted as closing a parent tag above nocode, resulting in condition 2.

From number 3 it is clear that even without rendering them, tags still have to be tracked inside the nocode block. But how to ensure that they will be retroactively rendered in case the nocode tag ends up discarded?

In this case, it is possible to recursively reapply the filter to the text block that hasn't yet been rendered. In pseudocode (some context added in parentheses; refer to the code of the first part), the additions and changes are:

1.  Let `nocode` be 0.

2.  (Inside the iteration over `tags`:)
        (If `T` is an opening tag:)

            If `T` is a nocode tag:
                Increment `nocode` by 1.

        (If `T` is a closing tag:)
            (While popping dangling tags off `open_tags`:)

                If `Current` is a nocode tag:
                    Decrement `nocode` by 1.
                    If `nocode` is 0:
                        Run myself on the input `Current.content` and store it in `Current.content`

            
            (Instead of always rendering the tag when it is closed)
            If `nocode` is greater than 0:
                Append `Current.element` to `Parent.content`
                Append `Current.content` to `Parent.content`
                Append [/`Current.name`] to `Parent.content`
            Else:
                Append the rendered form of `Current` to `Parent.content`

I am not yet sure whether the recursion/backtracking can be maliciously exploited, in the sense that certain crafted input might take a lot of server resources to process. Even if that is the case though, it would be simple to put in some safeguards.

The upside of this change is that the "weight" of tags becomes completely obsolete. Instead of having a specified order for every single tag, every single tag merely specifies whether it wants to be rendered before its content is, or after.

Building a better Tag-Parser

Arancaytar — Thu, 15 Apr 2010 22:15:02 +0000

The Problem

If you read the code of my Extensible BBCode module for Drupal, you'll notice that my tag parsing algorithm is kind of complex. In two steps, the tags are first "paired" (inserting a matching ID into the opening and closing tag) and then "rendered", all by an evaluated regular expression that calls another function. The process certainly ensures that all tags are balanced - and it even allows some tags to be rendered before others are, regardless of nesting.

But for all its voodoo magic and messing about, it is vulnerable to the same bug as most primitive BBCode parsers. Namely, allowing input that will result in this output:

<strong>This sentence is <em>not</strong> valid HTML code.</em>

Now, the quirks mode of all layout engines are very good at dealing with simple cases like that. Inline markup will be rendered correctly even with overlapping elements.

But what if it includes block elements? In phpBB, I recently noticed that it is extremely easy to disrupt the page layout using just two simple tags; [spoiler] and [quote].

The following overlapping input will be accepted:

[quote]
  [spoiler]
[/quote]
  [/spoiler]

The following output will (roughly) be generated:

<blockquote>
  <div><div><div>
</blockquote>
  </div></div></div>

Unlike the inline markup, several major layout engines (Gecko (layout engine)|, WebKit and Presto (layout engine)| are the ones tested) take issue with this. The quirk mode behavior in all three drops the three unmatched div tags inside the blockquote element, and then applies the three closing div tags to parent div elements higher up in the tree. This naturally wreaks havoc on the page. (I'd almost consider this a mild denial-of-service vulnerability because any malicious user can break the page layout.)

XBBCode is vulnerable to the same, because in spite of all its careful "pair matching", it never actually checks that the tag tree is nested correctly.

The Algorithm

So now I'm working on a much simpler and in my opinion more stable approach. I can only suppose it hadn't occurred to me earlier because I was thinking that BBCode had to be rendered "in-place", replacing each tag in the string where it was found. It seems that a better approach is to first find all tags, and then gradually build the output from substrings of the original text.

In Pseudocode (the actual PHP code is not as clean, alas):

1. Let `tags` be a list of the opening and closing tags in the input.
        Every element has the properties .name, .is-opening, .args, .index, .length
            .index is the string offset of the first character of the tag - "[".
            .element is the whole tag's string, from "[" to "]".
   Let `open_tags` be a stack of tags.
        Every element has the properties .name, .args, .content, .element and .offset
   Let `open_tags_by_name` be a dictionary of String -> Int.

2. For every tag `T` in `tags`:
       Is `T.is-opening` true?

       Then:
           Let `Parent` be the top element of `open_tags` (leave it on the stack).
           Append the substring between `Parent.offset` and `T.index` to `Parent.content`.
           Let `Parent.offset` be `T.index`.
           Let T2 be:
               .name : `T.name`, 
               .args : `T.args`, 
               .content : "", 
               .index : `T.index` + `T.length`
               .element : `T.element`
           Push T2 onto `open_tags`.
           Increment `open_tags_by_name[T.name]` by 1.

       Else:
           If `open_tags_by_name[T.name] greater than 0?
           Then:
               Pop an element off `open_tags` and call it `Current`.
               While `T.name` is not equal to `Current.name`:
                   Decrement `open_tags[Current.name]` by 1.
                   Let `content` be `Current.element` concatenated with `Current.content`
                   Let `offset` be `Current.offset`
                   Pop an element off `open_tags` and call it `Current`.
                   Append `content` to `Current.content`
                   Let `Current.offset` be `offset`

               Let `Parent` be the top element of `open_tags` (leave it on the stack).
               Append the substring between `Current.offset` and `T.index` to `Current.content`
               Let `output` be the output of rendering `Current`
               Append `output` to `Parent.content`
               Decrement `open_tags[Current.name]` by 1.

3. Let `Current` be the top element of `open_tags` (leave it on the stack).
   Append the substring between `Current.offset` and the end of input to `Current.content`

4. While `open_tags` has more than 1 element:
       Pop an element off `open_tags` and call it `Current`
       Let `Parent` be the top element of `open_tags` (leave it on the stack).
       Append `Current.element` to `Parent.content`
       Append `Current.content` to `Parent.content`

5. Let `Root` be the only element of `open_tags`.
   Return `Root.content`

You can see that even though the algorithm and the data it operates on is iterative, the text is rendered recursively from the inside out: Whenever a tag is closed, it is rendered and the output appended to the parent element's content.

If the tag being closed lies further down the stack, then all intermediate unclosed tags are discarded (though any complete tags inside them are kept). In the end, the same is considered to happen to the virtual "root" tag, that encloses the entire input - unclosed tags are discarded. (Note that "discarded" means "displayed in the output as unrendered BBCode", as is customary.)

The Costs

The first and greatest downside to this method is that tags cannot be weighted anymore. Every tag renderer will receive its content with all nested BBCode tags already rendered. Deferring the rendering of a tag is just not feasible in this algorithm.

However, this can be trivially circumvented by using a feature that is a lot easier to implement. Tags can be given a "nocode" property, which will tell this algorithm to ignore any tags nested inside it. The tag renderer could then independently run the BBCode filter on its content to render the tags that were left unrendered earlier.

(I'm not yet at the point where a dangling nocode tag will not stop enclosed tags from being rendered. It's not trivial, alas.)

I am crazy

Arancaytar — Thu, 15 Apr 2010 21:03:39 +0000

During my first semester here in Frankfurt, I took five subjects and was unable to sleep more than six nights per week (that's one too few, if you want to keep count). Surprisingly, I was still able to score a 1.0 in three and a 1.7 in one of the courses (deferred testing for the fifth, Logic).

So naturally, after barely surviving that, this semester I am taking six subjects. Since two of these courses will be tested both with a written and an oral exam, and I'm planning to take the test for Logic this semester, that means that I'll be facing nine tests instead of just four this time.

There's no way that is going to work.

(Sounds like a challenge.)

Factorizing a large set of numbers fast

Arancaytar — Wed, 03 Mar 2010 09:32:48 +0000

Factorizing a number can be done by several methods. The first is a naive way, which iterates over every natural number between 2 and the square root of n, then dividing by it as long as the number is divisible by it.

def factor(n):
    factors = []
    i = 2
    while i*i <= n:   # Iterate up to the square root of n.
        exp = 0       # Start with exponent 0
        while n % i is 0:  # Increment exponent and divide while divisible.
            exp += 1
            n /= i
        if exp > 0:
            # Note: All prime factors of n that are less than i are
            # already gone, therefore i itself is definitely prime if we're here.
            factors.append((i, exp)) # Append the prime factor.
            i += 1
    # If n is not yet 1, then it is now prime.
    if n > 1:
        factors.append((n, 1))
return factors

This requires us to iterate over n^0.5 numbers in the worst case (which is when n is prime). An upper bound for factorizing all numbers 1<x<n is O(n^1.5) (though admittedly that is a loose upper bound since 1<n<10^⁴ contains 12.3% prime numbers, 1<n<10^⁵ has 9.6% and 1<n<10^⁶ has only 7.8%. Still, the ratio changes slowly enough to be considered constant.

A slight performance improvement can be had by pre-calculating the set of prime numbers between i and n (which can be done in O(n*log(n*log(n)*loglog(n)) time with the Sieve of Erastothenes) and then reusing it for every number to be factored. After incurring an initial linear-logarithmic cost, we then do the following:

def factor(n):
    global primes
    factors = []
    for p in primes:
        exp = 0
        while n % p is 0:
            exp += 1
            n /= p
        if exp > 0:
            factors.append((p, exp))
        if p*p > n:
            break
    if n > 1:
        factors.append((n, 1))
    return factors

It is apparent, however, that this produces merely the practically constant improvement of only checking prime numbers instead of all numbers. It's down by a factor 10 if n is small (up to maybe 20 when n is 10^8), but it's still in the O(n^1.5) upper bound.

Can we improve on this?

Yes.

The Sieve of Erastothenes can be slightly modified without changing its O(n*log(n)*loglog(n)) complexity, and the modified sieve will let us factor primes in constant and any number in logarithmic time.

First, the modified sieve:

def sieve(n):
    # We need to fill the first 2 spots with 0's to cleanly ignore the case i < 2.
    table = [0]*2 + [1] * (n-2) # A list filled with 2 0's and n-1 1's.
    for i in xrange(n):
        if table[i-7-] is 1:
            for j in xrange(2*i, n, i): # Iterate over all multiples of i
                table[j] = i # This is where we'd normally mark j as not prime.
    return table

The output of this algorithm is a list that assigns each non-prime number its largest prime factor, and each prime number the number 1.

For example, the output for 0<=n<=10 is:

[0, 0, 1, 1, 2, 1, 3, 1, 2, 3, 5]

When factorizing now, we just need to look into this table to find the next prime factor, instead of finding it by iteration:

def factor(n):
    global sieve
    if sieve[n] > 1:
        # Divide n by the prime factor and recurse.
        return [sieve[n]] + factor(n / sieve[n])
    # n is prime, stop recursion.
    return [n]

(Note that the output of this algorithm is not identical to the previous. Instead of [(2, 5), (5, 5)] for 10^5, it will produce [5, 5, 5, 5, 5, 2, 2, 2, 2, 2].)

What was our worst case earlier is now the best: If a number is prime, the algorithm will immediately halt. The best case from earlier (a small prime to a high power, like 2^20) is now the worst case - but it will still be done in logarithmic time. 2^20 needs 20 recursions and so on. (If the recursion depth bothers you, the algorithm can also be formulated iteratively.)

Since our worst case for a single number is now logarithmic, the whole problem has gone from O(n^1.5) to O(n*log(n)), which is about the complexity we spent building the sieve in the first place. From linear-root to linear-logarithmic is quite an improvement for big numbers.

Goedelization of first-order logic

Arancaytar — Tue, 26 Jan 2010 04:53:42 +0000

In our Logic class, we just started on Goedelization of logical formulae - that is, the encoding of the language of first-order (arithmetic) logic into numbers, such that every formula gets a unique natural number. (For an analogy, take the English language and consider every word as a number in base 27, where "a" is 1 and "z" is 26. Something similar works for logic.)

Needless to say, these numbers are unbelievably large for even very short formulae.

For example, the first four natural numbers themselves are (of course) terms in arithmetical logic. However, the language does not actually allow writing these numbers out in their literal form: Rather, a term must be constructed only of the basic operators ("+" and "*") and the basic constants ("0" and "1"), and every term must be enclosed in parentheses.

and 1 remain 0 and 1.
becomes (1+1)
becomes ((1+1)+1)
becomes (((1+1)+1)+1)
...

Our encoding specifies 0xd for 0, 0xe for 1, 0x7 and 0x8 for parentheses, and 0xc for +.

So the hexadecimal code for the term equivalent to 3 would read:

0x77ece8ce8

The decimal form of this number is 32191187944. That's our Goedel number of the natural number 3.

(You don't want to know what the Goedel number for 32191187944 is. I did, but my inefficient recursive function crapped out.)

Here's an algorithm for generating the representation and then converting it to decimal:

def basic_num(n):
    if n < 0:
        raise ValueError()
    elif n <= 1:
        return str(n)
    else:
        return "(" + basic_num(n-1) + "+1)"
 
def goedel(s):
    if type(s) is int:
        s = basic_num(s)
    code = {
        # Logical operators
        "~":0x2, # NOT
        "&":0x3, # AND
        "|":0x4, # OR
        "E":0x5, # EXISTS
        "A":0x6, # ALL
        "(":0x7,
        ")":0x8,
        "=":0x9,
 
        # Arithmetic operators
        "<":0xa, # <=
        "+":0xb, # ADD
        "*":0xc, # MULT
        "0":0xd, # 0
        "1":0xe, # 1
    }
 
    g = 0
    for char in str(s):
        g = g * 16 + code[char]
    return g