Sedimentkegel! Ich kann euch nicht hören!

Radish
Sun, 08 Jul 2012 00:31:12 GMT

Hollow earth theory views the universe inverted at the center of the earth. To the inside, stuff becomes arbitrarily large. To the outside, stuff becomes arbitrarily small. Digging through the center of the earth means digging through infinity in this model. The same can be done with all ball-shaped objects. So everytime I make myself a radish salad ... I feel mighty.

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Link List 22
Tue, 03 Jul 2012 14:28:35 GMT

Meh. A lot of work to do. And playing Skyward Sword. So: Not many links this time again.

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Lumberjack
Sat, 30 Jun 2012 11:00:00 GMT

only one place I know where I'd want to be now
but this place is impossible to go
so I stay here chopping wood into pieces
thinking about the hypotheses

what if I was a piece of wood
it would be good but I am not
so I stay here chopping wood into pieces
thinking about the hypotheses

breaking wood to continue my dreadful life
feel the shivers shooting in my eyes
I stay here chopping wood into pieces
thinking about the hypotheses

just to burn the stuff away
to enlighten the night and heat up the day
I stay here chopping wood into pieces
thinking about the hypotheses

only one place I know where I'd want to be now
I imagine it being the destination of the smoke
I stay here chopping off my arm
throwing it into the fire and make it warm

my arm shall burn and turn into smoke
going to where I want to go
this part of me is finally released
in my imagination, at least

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

I'll be your aptitude
Wed, 27 Jun 2012 00:30:00 GMT

Bob, you've been waiting much too long
Now it looks like the driver is gone
Bob, you've been compiling all night long
All this time wasted dealing with the blob
If I could get the same attention
I'd give you a lot less dissension

If it doesn't come back ...
If it doesn't come back ...

I'll be your Aptitude, whenever you want me.
Don't you know I'll be your Aptitude, whenever you need me.

Bob, every day you've been tracing stacks
I've been hiding in your tray
Bob, all this time I've been suspended
Showing you on what you depended
I'm gonna wait until i get SIGCONT
Until you need to have a further font

If it doesn't come back ...
If it doesn't come back ...

I'll be your Aptitude, whenever you want me.
Don't you know I'll be your Aptitude, whenever you need me.

Each day by your screen
you sit and sigh
hoping to see windows.
You might as well forget about all
And use me in your terminal

If it doesn't come back ...
If it doesn't come back ...

I'll be your Aptitude, whenever you want me.
Don't you know I'll be your Aptitude, whenever you need me.

(Just a little inspiration. A moralic cake for everyone who finds out on what song this bases.)

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Link List 21
Tue, 26 Jun 2012 14:00:00 GMT

External Content not shown. Further Information. Not many links this time, sorry.

If programming languages were religions
Unity 4 game engine will support Linux natively - finally. However, better support of browsers for HTML 5 would be nicer.
Gigapixel Camera

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Talk on boolean sequences
Mon, 25 Jun 2012 16:00:00 GMT

For the best maths-club of the multiverse I will give a short talk on an already mentioned property of boolean sequences. As the audience consists of a wide range of ages and expierience, I will not do everything as formal as it should be done from a strictly mathematical point of view. My goal is to give young people an idea on what is going on, while providing to older people enough material to complete everything.

Furthermore, there is an easier way of showing the actual result, but I rather want to touch a large variety of topics than doing a short formal proof in detail. I hope to give especially young people an overview on many topics of logic and tcs.

0 Introduction

A boolean sequence is a sequence of boolean values "true" and "false", or 1 and 0. It can be seen as a function $\mathbb{N}_0\rightarrow\mathbb{B}$ from the natural numbers $\mbox{N}_0$ into the boolean values $\mathbb{B}=\{0,1\}$ . There are uncountably many such boolean sequences, as we will show later. Furthermore, in general, it is not decidable whether two such sequences are equal, even if these sequences can be enumerated by a computer program.

We are now interested in functions of the type $(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}$ , that is, functions that assign a boolean value to boolean sequences. In general, their equality is not decidable.

However, if two such functions can be calculated by a computer program, it is decidable whether they are equal. We will show this in a rather complicated way, as our goal is not to give a prove of this, but to touch many fields of logic and computer science.

1 Crashcourse Infinite Sets

While for finite sets it is rather easy to talk about "numbers" of elements, for infinite sets we need a more sophisticated notion. We may assign every set its "cardinality", however, for our purposes it is sufficient to be able to compare the size of sets.

Definition: Two sets $A$ and $B$ have the same cardinality, iff there is a bijection $f:A\rightarrow B$ .

Simple examples of infinite sets of the same cardinality are $\mathbb{N}_0$ and $\mathbb{Z}$ through the bijection $z\mapsto |2z|+\frac{1}{2}|\mbox{sgn}(z)|(\mbox{sgn}(z)-1)$ . Furthermore, $\mathbb{N}_0^2$ and $\mathbb{N}_0$ are of the same cardinality, one bijection is the cantor pairing $(x,y)\mapsto\frac{1}{2}(x+y)(x+y+1)+y$ .

Definition: Sets of the same cardinality as $\mathbb{N}_0$ are called countable.

That is, $\mathbb{Z}$ and $\mathbb{N}_0^2$ are countable. Furthermore, $\mathbb{Q}$ is countable.

Theorem: The set $\mathbb{N}_0\rightarrow\mathbb{B}$ of boolean sequences is not countable.
Proof: Assume there was a bijection $f:\mathbb{N}_0\rightarrow(\mathbb{N}_0\rightarrow\mathbb{B})$ from the natural numbers into the boolean sequences. But then $x\mapsto 1 - f(x)(x)$ cannot be in the image of $f$ . Contradiction. --

Furthermore, $\mathbb{R}$ and $\mathbb{C}$ are not countable.

2 Crashcourse Computation Theory

There are several equivalent formal definitions of computability. However, they are rather technical, and outside the scope of this talk.

Improper Definition: A function is called computable, if it can be computed by a computer with inexhaustible memory in a finite amount of time.

Most functions you will usually have to deal with are computable. A simple example of a non-computable function is the following function $nc:(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}$

$nc(f) = \left\{\begin{array}{cl} 0 & \mbox{if } f(x)=0 \mbox{ for all } x\in\mathbb{N}_0 \\ 1 & \mbox{otherwise} \end{array}\right.$

It takes as an argument a boolean sequence, and decides whether this boolean sequence contains a $1$ .

If you do not believe me that this function is not computable, go on, try to implement it in the programming language of your choice! In fact, trying this is probably a good exercise.

Let $b:X\rightarrow\mathbb{B}$ be a boolean function on some set $X$ . If we have a given set $X$ and such a function, we can build the set $\{x\in X|f(x)=1\}$ . This way, boolean functions can be seen as functions which "decide" what elements belong to a set. This yields the following definition:

Definition: $\mathbb{N}_0$ is decidable, and for every decidable set $X$ , if there is a computable function $f:X\rightarrow\mathbb{B}$ , the set $\{x\in X|f(x)=1\}$ is called decidable.

The intuition behind this definition is that a set is called decidable, if a computer can decide whether it contains a given element.

As with computable functions, also most sets one has to explicitly deal with is decidable. An exception can be derived directly by the above example $nc$ : The set of (computable) boolean sequences which have at least one $1$ in their image is not decidable. In fact, quite a lot of sets one uses implicitly are not decidable.

3 Crashcourse Logic

Definition: Formulae that only quantify over objects, but not over relations or functions of objects, are called first-order formulae. A first-order theory is a set of such formulae.

An example for such a theory is group theory

$\{ \forall_xx=x+0, \forall_x\exists_y x+y=0, \forall_x\forall_y\forall_z (x+y)+z=x+(y+z)\}$

Every structure satisfying a theory is called a model of this theory. For example, every group is a model of group theory.

Notice that theories need not be finite.

If a formula holds in all models of a theory, the theory implies this formula, and it can be shown that there exists a formal proof of this formula from the theory. This is called Completeness Theorem and the proof requires a lot of theory.

If a formula holds for a theory, then it holds for a finite subset of this theory: By the Completeness Theorem, it must be provable, and a formal proof is a finite object and can only use finitely many axioms.

4 The Proof

We will now show that in fact the equality of computable functions $(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}$ from boolean sequences into booleans is decidable.

If two functions $f,f'$ are not equal, we can find a boolean sequence $g$ such that $fg\neq f'g$ . Therefore, in this case we can prove the inequality. The more interesting part is that we can prove equality if it holds.

Firstly we notice that such a function $f$ can, as it only runs for a finite amount of time, only access finitely many elements of its argument. That is, when calculating $f(g)$ for some $g:\mathbb{N}_0\rightarrow\mathbb{B}$ , there is a maximal $m_g\in\mathbb{N}_0$ such that the calculation depends on $g(m_g)$ , but not on $g(m'), m'>m_g$ . For a given sequence $g$ we can find this $m_g$ by tracking which image values of $g$ the calculation of $f$ uses.

Our strategy is now to use this property to encode functions into a first-order theory. Denote by $PA$ the theory of peano arithmetic (usual elementary number theory). We define an additional relation $A_i$ on natural numbers $i$ .

Let $f:(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}$ and $a:\mathbb{N}_0\rightarrow\mathbb{B}$ . Then we encode the information that $f(a)=k$ by

$M_{c,f,a}:=(\bigwedge_{a(i)=1,i\le m_f} A_i \wedge \bigwedge_{a(i)=0,i\le m_f} \lnot A_i)\rightarrow c=k$

That is, we postulate that if $A_i$ is true for $a(i)=1$ and false for $a(i)=0$ for all $i\le m_f$ , then $c=k$ . This is a straightforward encoding. To encode $f$ completely, we define the theory

$T_{c,f}:=\{M_{c,f,a}|a\in\mbox{dom}(f)\}$

Now assume a second function $g$ is given, with $f = g$ . Then, $PA\cup T_{c,f}\cup T_{d,g}\cup\{c\neq d\}$ implies a contradiction. By the Completeness Theorem, there is therefore a formal proof of a contradiction. We can use an exhaustive proof search (a "blast") to find a contradiction proof in that case, as we know it exists.

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Virtual Linux with NFS-Root under QEMU
Wed, 20 Jun 2012 15:40:25 GMT

Probably, there will be a bright future for Linux Containers. However, so far, I miss a network configuration which is comparably easy to the default networks of Qemu and VirtualBox. I do not know whether the situation is better in OpenVZ, but I somehow do not like OpenVZ much. The main advantage of OpenVZ and Lxc for me is that they use the host filesystem as root filesystem. For incremental backups with rsync, this is vital, but it also makes quick changes to the configuration a lot easier.

So the idea was to actually use Qemu with a small image that boots into an nfsroot. I will try to give a little howto on how to do this with Xubuntu. However, I cannot guarantee that this will work for everyone else. Especially, the command line arguments are constantly changing, so in a few months, this might not work anymore at all. So better take it as a starting point for your own research rather than the final truth.

The packages needed (I hope I did not forget one) are nfs-kernel-server, qemu, qemu-kvm, kvm, debootstrap.

To build an initramfs, I first create a chroot, which I built with debootstrap. I want Debian Wheezy.

# mkdir /qemuChroot
# debootstrap wheezy /qemuChroot http://ftp.de.debian.org/debian/

This does a lot of stuff and takes a while. While it clatters, we can already begin to do our NFS configuration. We need to put the following lines into the /etc/exports file:

/qemuChroot 127.0.0.1(rw,sync,no_subtree_check,no_root_squash,insecure)

"insecure" is necessary, since we want to run the Qemu usermode network stack. Then we have to restart the nfs-kernel-server, to get the new configuration (or use exportfs -a, but I prefer restarting when possible).

Now, hopefully debootstrap ended correctly. Time to chroot into the system:

# chroot /qemuChroot/

In this chroot environment, install a linux-image, and initramfs-tools, and change BOOT=local to BOOT=nfs in your /etc/initramfs-tools/initramfs.conf and run

# update-initramfs -uk all

inside your chroot (please, check twice that you are in the chroot!!!). It will drop a few warnings (we could prevent them by mounting /proc and /sys and /dev) but should work.
To be able to access the machine later, we need to set a root password, using

# passwd

Exit the chroot again. The initramfs and kernel image we need is now in /qemuChroot/boot. For the kernel I use, they are called initrd.img-3.2.0-2-amd64 and vmlinuz-3.2.0-2-amd64.

We now have everything to start Qemu. Firstly, make sure that the kvm-modules are loaded, and that your user has apropriate access to these devices - for me, he needs to belong to the libvirtd-group. To use kvm, we add the argument -enable-kvm to our Qemu-commandline - leave it out if you do not want kvm acceleration, but be aware that this will be slow.
Qemu can directly boot into a linux kernel and initramfs, without the need of an extra image. Just add -initrd /qemuChroot/boot/initrd.img-3.2.0-2-amd64 -kernel /qemuChroot/boot/vmlinuz-3.2.0-2-amd64, or the appropriate paths for you, to the commandline.
We need to inform the kernel of our nfsroot. This is done by kernel arguments, which can be passed by -append "root=/dev/nfs nfsroot=10.0.2.2:/qemuChroot".
Finally, we want virtio-net (to make it faster).

The commandline to start the VM becomes

$ qemu-system-x86_64 -enable-kvm -initrd /qemuChroot/boot/initrd.img-3.2.0-2-amd64 -kernel /qemuChroot/boot/vmlinuz-3.2.0-2-amd64 -append "root=/dev/nfs nfsroot=10.0.2.2:/qemuChroot" -netdev type=user,id=usernet -device netdev=usernet,driver=virtio-net

This should correctly boot you into a virtual machine with the given root. However, for some reason resolvconf does not work properly, so make sure it is not installed on the virtual machine, and change the contents of /etc/resolv.conf into

nameserver 10.0.2.3

It is important to use the internal nameserver, udp packages are not transmitted for some reason.

You may want to export some services from your virtual machine to your host. For me, these are ssh and http. The -netdev argument must be changed into type=user,id=usernet,hostfwd=tcp::2200-:22,hostfwd=tcp::8800-:80 and I leave it to the reader to find out how other ports are forwarded.

Here is a documentation on Qemu-Networking, and here is some information about diskless booting with an Arch Linux rather than Debian. Both sites were very helpful for creating this howto.

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)

Silverlight for broken toilets
Tue, 19 Jun 2012 13:08:09 GMT

It is natural that stuff gets broken, especially during a refurbishment, as it currently appears in my university. So I was only a little angry when the leaking toilet drenched my pants while flushing.

Well, I thought, let us try to find out the number of the janitor, and tell him. The department's page has a list with employees, but their function is not mentioned explicitly. So I called the head office, and they gave me a name. Unfortunately, this name did not appear on that list, so I googled it.

I found his mail address hidden in the deep forests of my universitie's website, and mailed him immediately.

I got a reply that there is a web interface for notifications about broken things, and he gave me a link to this web interface. So I followed this link.

A site showed up, telling me that plugins are missing. Well, I thought maybe it needs Java, and clicked on automatic installation.

It turned out that it requires Silverlight. Or Moonlight, in my case. And of course, after Moonlight was installed, it showed a shiny progress wheel around a percentage which did not get beyond 0%.

The university has a Windows Terminal Server, and I could get an account there, but ... only for noticing the janitors about a broken toilet? Well, our friendly admin sent me to a person who got that stuff work with his computer and usually does these notifications.

Silverlight... seriously? I mean, what could be the content of such a site? A textarea for the problem. Maybe something that searches for already filed damages. Maybe something to choose the room, and some address-field for correspondence. Why the heck would such an interface use Silverlight? I wonder how much they had to pay for this interface.

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)