Goedelization of first-order logic

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.


0 and 1 remain 0 and 1.
2 becomes (1+1)
3 becomes ((1+1)+1)
4 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

IEEE-754 encoding of floating-point numbers

Here is a taste of the kind of stuff we're doing in my Python class. These two functions generate a string representation of the binary IEEE-754 encoding of floating point values, in semi-precision (16 bit), single (32), double (64) and quadruple (128) precision.

In IEEE-754, the first bit carries the sign. The following number of bits allocated to the exponent are 5 (-15 to +16), 8 (-127 to +128), 11 (-1023 to +1024) and 15 (-16383 to +16384) respectively. The remaining bits are the fraction, of which the first bit stands for 0.5 * 2^exp. The fraction starts out at an implicit value of 1, since it is normalized to the range between 1 and 2. (0 is actually represented as 2 raised to the smallest exponent, eg. 2^-127 for single precision).

def ieee(f, word=32):
    """Generate the binary string representing a floating-point value in IEEE754 code."""
    f = float(f)
    if word not in (16, 32, 64, 128):
        raise ValueError("IEEE754 is defined for 16, 32, 64 and 128 bit words.")
    exp_bin = range({16:5, 32:8, 64:11, 128:15}[word])
    frac_bin = range(word - len(exp_bin) - 1)
 
    # Sign.
    sign_bin = [int(f < 0)]
    f = abs(f)
 
    # Find exponent (adding the bias).
    bias = 2**(len(exp_bin)-1) -1
    exponent = bias
    while f >= 2:
            exponent += 1
            f /= 2
    while f < 1 and exponent > 0:
        exponent -= 1
        f *= 2
    if not 0 <= exponent < 2*(bias+1):
        raise ValueError("Exponent overflow: Absolute exponent must be smaller than %d." % (bias + 1))
 
    # Encode exponent in binary.
    for i in exp_bin[::-1]:
        exp_bin[i-1-] = int(exponent % 2)
        exponent /= 2
 
    # Remove the leading 1 bit.
    f -= 1
    for i in frac_bin:
        f *= 2
        frac_bin[i-2-] = int(f >= 1)
        f -= frac_bin[i-3-]
 
    # Join the binary string components together.
    return "".join(map(str, sign_bin + exp_bin + frac_bin))
    
def ieee_decode(binary):
    """Decode a binary string representing a floating-point value in IEEE754 code."""
 
    # Determine the word size of the binary.
    word = len(binary)
    if word not in (16, 32, 64, 128):
        raise ValueError("IEEE754 is defined for 16, 32, 64 and 128 bit words.")
 
    # Determine the length of the exponent.
    e = {16:5, 32:8, 64:11, 128:15}[word]
 
    # Turn the binary string into a bit-list.
    binary = [int(c) for c in binary]
 
    # Split the components.
    sign = -2 * binary[0] + 1
    exp_bin = binary[1:1+e]
    frac_bin = binary[1+e:]
 
    # Decode the exponent.
    bias = 2**(e-1) - 1
    exponent = -bias
    c = 1
    for i in exp_bin[::-1]:
        exponent += i * c
        c *= 2
 
    # Decode the fraction.
    f = float(2**exponent)
    power = f
    for i in frac_bin:
        power *= 0.5
        f += i * power
 
    return sign * f

Some sample encodings:


0: 00000000000000000000000000000000
2^128: 01111111100000000000000000000000
15/7: 11000000000010010010010010010010
0.2: 00111110010011001100110011001100

Lost in translation

I just came across this little gem on the German version of the Mozilla Firefox website.

The English version of the page says:

See How We Stack Up

We’ve told you about what makes Firefox great, but how do we compare against Internet Explorer? Check out our handy browser comparison chart to see for yourself.

The German one is entitled:

Sehen Sie sich an, wie hoch wir stapeln

Okay, so literally this means "look at how high we stack" which comes pretty close. Idiomatically however, a "Hochstapler" (High-stacker) is one who brags or embellishes, a charlatan or con man. In other words, the effective meaning of the title is this:

Look At Us Posturing

Since the page is essentially a parody of the hilariously named "GetTheFacts" campaign by Microsoft, I actually thought that was purposefully tongue-in-cheek until I saw the English version.

Making Google Earth run fast in Linux

I have just found out why Google Earth runs so awfully slow on my Ubuntu system: It cannot access the graphics drivers directly, and is probably forced into a very slow software-based mode. I am using an Nvidia graphics chipset, and Earth runs significantly faster after doing the following:


sudo chmod 666 /dev/nvidia0
sudo chmod 666 /dev/nvidiactl

This is coincidentally also the command necessary to let Picasa run on Linux systems. I thought it might be a useful trick.

Install Drupal 7 with a script

The seventh version of Drupal has greatly improved the installation process once more. Among other changes, the installer has become more user-friendly, but the best part is under the hood, and somewhat less obvious. It is now much easier than ever to install Drupal using a PHP script that runs in the console, rather than the interactive web installer.

Since I have not yet seen a detailed documentation of this feature, here is a guide.

1. Build an install script

The central function you need to call (after including install.php in your installation script) is, oddly enough, install_drupal(). The argument you need to pass to this function is less obvious, and here it is, line by line:

<?php
 
$settings = array(
  # First, tell Drupal you are not using the interactive installer.
  'interactive' => FALSE,
 
  # This part is required for multisite support. The keys
  # you put here overwrite the $_SERVER array, allowing Drupal
  # to find a site path (in this case, localhost.my.site, my.site etc.
  'server' => array(
    'HTTP_HOST' => 'localhost',
    'SCRIPT_NAME' => '/my/site',
  ),
 
  # Next, choose the profile and locale Drupal should use.
  # The profile must be in a ./profiles/$profile/ folder.
  'parameters' => array(
    'profile' => 'expert',
    'locale' => 'en',
  ),
 
  # This is the data that will be submitted to the various 
  # forms in the installation wizard.
  'forms' => array(
    # Database configuration.
    'install_settings_form' => array(
      'driver' => 'mysql',
      'database' => 'db_name',
      'username' => 'db_user',
      'password' => 'db_pass',
      'host' => 'localhost',
      'port' => '',
      'db_prefix' => 'drupalsite_',
    ),
    # Site information, and the data of the root user.
    'install_configure_form' => array(
      'site_name' => 'Drupal Test Site',
      'site_mail' => 'drupal@localhost',
      'account' => array(
        'name' => 'root',
        'mail' => 'drupal@localhost',
        'pass' => array(
          # This is a bit of a WTF, but that's the way it works.
          # Even non-interactively, password fields require two identical values.
          'pass1' => 'hunter2',
          'pass2' => 'hunter2',
        ),
      ),
 
      # This is the timezone of the Drupal site. You can find the
      # PHP timezone strings at http://php.net/timezones
      'site_default_country' => 'DE',
      'date_default_timezone' => 'Europe/Berlin',
 
      'clean_url' => TRUE,
 
      # Check for updates: 
      #   array() = off, 
      #   array(1) = on, 
      #   array(1, 2) = on, and notify by email
      'update_status_module' => array(),
    ),
  ),
);
 
 
# Finally, fire it off.
require_once './install.php';
install_drupal($settings);

2. Set up/clean the environment

Note that this script will not clear or prime the site folder, so your installation will only work if a pristine "settings.php" file is in the site folder you want to install to.

The standard procedure to delete and clear a site is, in pseudocode:


if dir "sites/SITE/" exists:
database = parse file "sites/SITE/settings.php"
delete database tables
else
make dir "sites/SITE/"
done

copy file "sites/default/default.settings.php" "sites/SITE/settings.php"

run installation script

3. Useful modifications in install.php

One disadvantage I've found is the, well, non-interactiveness of the non-interactive installer. If the installer runs through correctly, running the above PHP code will print no output at all. Since installation can take between 30 and 60 seconds on slow PCs, it would be nice to know the installer's progress. To this end, I put the following lines into the install.php file:

@@ -406,6 +406,7 @@ function install_run_task($task, &$insta
       return;
     }
     else {
+      print "Submitting information to task $function... ";
       // For non-interactive forms, submit the form programmatically with the
       // values taken from the installation state. Throw an exception if any
       // errors were encountered.
@@ -415,6 +416,7 @@ function install_run_task($task, &$insta
       if (!empty($errors)) {
         throw new Exception(implode("n", $errors));
       }
+      print "done.n";
     }
   }
 
@@ -437,6 +439,7 @@ function install_run_task($task, &$insta
         variable_set('install_current_batch', $function);
       }
       else {
+        print "Running batch process $function... n";
         $batch =& batch_get();
         $batch['progressive'] = FALSE;
       }
@@ -469,6 +472,7 @@ function install_run_task($task, &$insta
 
   else {
     // For normal tasks, just return the function result, whatever it is.
+    if (!$install_state['interactive']) print "Running task $function... n";
     return $function($install_state);
   }

I'll admit that this is a far cry from an actual installation tool that can be packaged, but it should make setting up test environments or deployment a whole lot easier.

XBBCode 7.x-0.9 released

I've spent a few more days improving and cleaning up the new version.

One thing I have managed to make loads better is the handler settings form: Instead of a table with simple checkboxes and weight selection elements, the form now uses tablesort and tabledrag. The extra space is used to display the tag description,

(Note: Due to a bug in core most of the cool stuff will not work without applying a core patch.)

http://ermarian.net/downloads/software/drupal/xbbcode/xbbcode-7.x-0.9-r4...

Porting XBBCode to Drupal 7

Well, as you can see, the NaNoWriMo didn't really work out. Astonishingly, it turns out that a day has only twenty-four hours.

However, I have managed to devote an afternoon this weekend to porting my XBBCode module. This is particularly interesting if you are from Spiderweb, because XBBCode for Drupal 7 is one of the steps on the roadmap to the new Pied Piper Project and the new Blades Forge.

I've managed to achieve a few milestones in short time:

- Creating, editing and deleting custom tags works.
- The basic tag package has been ported.
- The actual filter works, including basic, custom and dynamic tags.

Other than cleanup, the only part that remains of the actual XBBCode port are the other two sub-modules, list and table. The far bigger task ahead is the porting of the Highlighter module. Highlighter unfortunately contains some nasty file juggling and PEAR voodoo, which will be hard to modernize.

Trying something new

The first few words of what may turn out to be a story are at Twitter. My inspiration for this came from Max Barry's latest stunts - after already publishing a story via email newsletter, he recently sat down and wrote for a live audience at a convention.

Twitter fulfills the criteria of making it all but impossible to go back to edit, and adding a bit of public pressure. Also, instant persistence. I could write from anywhere. And I need to think in sentences below 140 letters, which eliminates the Kafka syndrome.

Well. Back to actually writing, now.

NaNo, after two years hiatus

Who knows?

All I know is that out of six years I have known about NaNoWriMo, I have written only in the four years where stress and insomnia have all but killed me. In the two past years, where I had mostly nothing to do, I didn't write a word.

Now that my life has picked up a bit again, I might give it another shot.

In which case this would be the shortest time before day 0 I've ever decided to do it. I haven't even got an idea yet, just a vague jumble of rambles.

What I know is that this year, I won't type-set at all, nor use backspace or even the cursor. Text will flow straight from the keyboard, via cat, to the hard drive.

We shall see.

OpenDNS - a disappointment

Last week I decided to give OpenDNS a shot. It seemed like a good alternative to the DNS server of my ISP (not that my service provider has proved itself untrustworthy on that score, but I decided to be rather safe than sorry).

Specifically, what I wanted to avoid was a scenario that has played out far too often among ISPs, called DNS Hijacking.

Particularly the more infamous providers (including Comcast and Verizon) have made bad headlines in the past few years for doing this. It goes like this:

When your computer looks up a domain like "invalid.asdfghjklomnbv.tld", the DNS server is supposed to return a clear signal that the lookup failed, which is called "NXDOMAIN". That lets the client decide what to do next - maybe try another nameserver, maybe redirect to Google, maybe display an error message or log a failed connection attempt. The beauty of this is that the NXDOMAIN is part of the DNS protocol and therefore independent of what kind of computer you actually connect with. It might be a server for IRC, SMTP, a web or a news server. The client will know what to do in case of a failed lookup.

The DNS server doesn't actually have to do that, of course. As in all other matters, you have to trust it to give you accurate information.

What some ISPs have realized is that they can drive massive traffic to advertisers by hijacking their customers' failed domain lookups. In effect, that means you never get a normal "domain does not exist" message. Instead, the DNS server lies to you and says the domain resolves to its very own ad-server. You connect to the server, get some vaguely related search results. It's annoying, it's a violation of the DNS protocol, it breaks non-web clients, and is one of the things I hoped to avoid with an alternative DNS service.

Imagine my chagrin when I entered a non-existent domain while using OpenDNS, and saw this.

IMAGE(<a href="http://stuff.ermarian.net/aranca" title="http://stuff.ermarian.net/aranca">http://stuff.ermarian.net/aranca</a>...)

What is worse, if I connect to a bad mail or IRC server, I'm stuck waiting while my client tries to connect to port 6667 or 25 on the OpenDNS server, which times out.

Long story short, I'm using OpenNIC instead now, and it works like a charm. Amazingly, they have also managed to restrain themselves from trying to hijack my domain lookups. Moral: Not everything that has "Open" in the name is actually useful or reliable (though that was probably clear since the farce Microsoft made of the International Standards Organization with Office Open XML).

Syndicate content Syndicate content