Subscribe to LambdaLand        RSS Feed
-----

Infinite streams and Exact real arithmetic

Icon Leave Comment
I've been gone for a while but have been learning lots. School has taken up too much time for me to do my own programming; I'm too busy doing school work and work for my job. I don't even feel like programming when I get done with the day. I have turned to reading about things in theoretical computer science instead. Most of all I have become interested in higher type computability, mostly thanks to this artical. It simply blew my mind. I'd now like to pass on some of that fascination to you.

I'd love to go over everything in that blog but that would be very redundant. Instead I'd like to go over some related topics concerning exact real arithmetic. Exact real arithmetic is NOT arbitrary precession arithmetic. Arbitrary precession arithmetic lets you select the precession but it is fixed at that point, or perhaps it vary's from operation to operation but the precession is always finite nevertheless. With exact real arithmetic we want to always have infinite precession. This might sound impossible and if it does I suggest you read the article above before making any conclusion; it is after all called "seemingly impossible functional programs".

The first thing we are going to want to talk about is infinite streams. Infinite streams are infinitely long lists of values. This of course begs the question "how does one fit an infinite amount of information onto a finitely sized computer". Well we don't because that is impossible. What we can do is fit a finite description of how to generate an infinite stream on a computer. A handy encoding of such a description is the all familiar function.

In C we might say something like this
bool generate(int x) {
   ...
}


in haskell something more like this
generate :: Int -> Bool
generate = ...


acutely haskell has lazy lists so we could even do something like this
generate :: [Bool]
generate = ...



Such a function describes how to create an infinite sequence because it tells us what should go at each position. For instance plugging in zero gives us the first item in the sequence and plugging in 2 gives us the 3rd item in the sequence and so on. Now because this function has a finite representation in memory we have seemingly represented an infinite amount of information in a finite amount of space. As you might expect we have to give something up here because you simply can't fit an infinite amount of information in a finite amount of space. But what exactly did we give up? This turns on the halting problem.

If you are not familiar with Godel numberings then I will give a brief explanation. Specifically for this I want to talk about Godel numberings of programs and not logical statements. Consider the bytes in memory that encode a function like those above. A list of bytes together form an integer. 1 is a byte, 2 is a short, 4 is an int, and 8 is a long and when there are an arbitrary number of bytes we call it a big int. The point is that a sequence of bytes trivially forms an integer. This integer is what we will call the Godel number of a function in some language. Other encodings can be chosen and often are for more theoretical purposes but for the sake of leveraging the more piratical knowledge of this community I thought this was a good enough for the purposes of this thought experiment.

Now consider the sequence of 1s and 0s (bits) such that the Nth bit is 1 if and only if N is the Godel number of a well formed program and that program halts. Let's call this sequence the turing sequence. If we could write a function that described this sequence like so
bool turing(int n) {
   ...
}


Then I could solve the halting problem quite simply by just plugging the Godel number of the given program into this function (note that we would have to go away from int and use something like a big int instead) and it would spit out exactly the thing we wanted.

So clearly not all sequences are describable in this fashion. In fact we can use totally different reasoning to conclude that we can't even describe infinite sequences in a finite amount of space. If we realize that strings are just sequences of bytes then they too have trivial Godel numbers to them as well. Now any string in mathematics corresponds to some Godel number and thus there are countably many mathematical strings. However a simple diagonal argument will show that there are uncountably many infinite streams of bits (they are called the Cantor space in fact after Gregor cantor). So there exists (classically anyhow, I prefer intuitionism anyway) infinite streams of bits that mathematics cannot describe because there are simply more streams than descriptions. I could have skipped right to this but I so much more enjoy the halting problem version that I thought I would expound apon it.

Now that I have showed you the two dirty little secretes of infinite streams (they must have finite descriptions and some can't be computed) I can show you a basic encoding of exact real numbers. Real numbers have an infinite number of digits and a dot somewhere in their a finite distance away from the first digit. We can also choose the base that we want. I have decided that we will use binary. So a real number for our purposes is an infinite stream of binary digits and an integer to tell us where the dot should go. So now one can imagine a real number that solves the halting problem. The turing sequence now corresponds to a real number. This real number is called Chatin's constant. In fact there is not just 1 such constant but rather an infinite number of them. Each of them would allow us to solve the halting problem as we could compile any turing complete language/system down to another and check the result in the new system.

This is all I have for you today but if we want to acutely get into the algorithms I recommend this page

Have fun!

0 Comments On This Entry

 

Trackbacks for this entry [ Trackback URL ]

There are no Trackbacks for this entry

February 2020

S M T W T F S
      1
2345678
9101112131415
16171819202122
23 242526272829

Tags

    Recent Entries

    Search My Blog

    0 user(s) viewing

    0 Guests
    0 member(s)
    0 anonymous member(s)

    Categories