abou the Godel Numbering for untyped lambda calculus

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

abou the Godel Numbering for untyped lambda calculus

Algebras Math
Hi all,

I am reading the book "The lambda calculus: Its syntax and Semantics" in the
chapter about Godel Numbering but I am confused in some points.

We know for Church Numerals, we have Cn = \fx.f^n(x) for some n>=0,
i.e. C0= \fx.x and C
1 = \fx.fx.

>From the above definition, I could guess the purpose of this kind of
encoding is trying to encode numeral via terms.

How about the Godel Numbering? From definition we know people say #M is the
godel number of M and we also have [M] = C#M to enjoy the second fixed point
theorem : for all F there exists X s.t. F[X] = X.

What the mapping function # is standing for? How could I use it? What the #M
will be? How to make use of the Godel Numbering?

Thank you very much!

alg
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20090331/fb94d606/attachment.htm
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] abou the Godel Numbering for untyped lambda calculus

Dan Weston
I can't tell exactly what you're asking, but I'll give it a try! :)

primes :: [Integer]
primes = [2,3,5,7,11,13,17,19,23,29,31,undefined]

godel :: String -> Integer
godel = product . zipWith (^) primes . map (toInteger . ord)

-- Here is the identity function (note that double backslash is a single
character
godel "\\x -> x"
1629920514342441477851613634029704631135430980107335428017064836156091059806450516131002598452000651374890570022191128551421788559667251656959733380229796871976693176094558797489489057311763922507760911447493016261397754567695234219623056037447490713525815311253273691703346455275115486717580778238094808661626709709766328915159206002675716287759792707200037683200000000000000000000000000000000

-- = 2^92 * 3^120 * 5^32 * 7^45 * 11^62 * 13^32 * 17^120

ungodel :: Integer -> String
   -- ungodel . godel = id

(See http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic for
why this works).

These numbers get large quickly, but are finite for any finite string of
finite alphabet.

godel is a total function (every string has a unique integer), and its
inverse (an exercise to the reader involving prime factor decomposition)
would also be total if the alphabet were infinite (so that ord would be
total).

Frankly, I wouldn't know how to begin encoding the godel numbering in
the type system (shudder!), but being that it is a total primitive
recursive function, I suppose there is no theoretical impediment.

In contrast, Godel's Theorems themselves cannot be so encoded because
the last step involves a general recursive function.

Dan

Algebras Math wrote:

> Hi all,
>
> I am reading the book "The lambda calculus: Its syntax and Semantics" in
> the chapter about Godel Numbering but I am confused in some points.
>
> We know for Church Numerals, we have Cn = \fx.f^n(x) for some n>=0, i.e.
> C0 = \fx.x and C1 = \fx.fx.
>
>  From the above definition, I could guess the purpose of this kind of
> encoding is trying to encode numeral via terms.
>
> How about the Godel Numbering? From definition we know people say #M is
> the godel number of M and we also have [M] = C#M to enjoy the second
> fixed point theorem : for all F there exists X s.t. F[X] = X.
>
> What the mapping function # is standing for? How could I use it? What
> the #M will be? How to make use of the Godel Numbering?
>
> Thank you very much!
>
> alg
>

Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] abou the Godel Numbering for untyped lambda calculus

Dan Weston
DISCLAIMER: The last I studied this was over 20 years ago, so my brain
is seriously rusty. You are warned...

 > you mean the godel function (denoted by # and generally will be in type,
 > #:term -> number ?) is a kind of functions instead of a particular
 > function?

No. The Godel mirror function (as defined by Godel) is a single
function, the product of primes (whose ordering gives the position in
the string) with exponents (giving the symbol at that position).
However, I think any total injective function with partial injective
inverse will do. Don't get hung up on the details of the mirroring
(Godel doesn't). Once you accept that it can be done, there is no need
to actually do it.

There is nothing magic about integers, beyond the fact that elementary
arithmetic is "well understood" by humans and should not have
inconsistencies (it probably doesn't, but we can't prove it within any
language more intuitive than arithmetic, so why should be believe the
proof in that language?). Importantly, all but the last step of the
proof can be encoded as primitive recursive functions, meaning that they
always halt within a predetermined number of steps (satisfying the
Finitists). Only the last step cannot be so limited. This is a clear
example where non-finite mathematics has demonstrably more power in a
fundamentally important way.

Why bother going through this encoding? The main reason for the encoding
is to overcome the fundamental limitation of structural induction
whereby there is no "this" smaller than this. I.e. quoting a sentence
only makes it longer. With functions on integers, this limitation is
removed, so that although there is no string saying "This statement is
not true", (since "This statement" != "\"This statement is not true\""),
there *is* some function taking the Godel number of the unquoted This to
the Godel number of the string to which it refers. Doing so takes some
bit of cleverness, but the original proof in German is only about 8
pages long, as I recall.

If we don't go with mirroring and just use strings, we need to introduce
some equivalent trick, namely named functions. In a language without
pointers and only lambda expressions, there is no way to refer to
oneself without repeating the quote in infinite regression. For instance
"\x -> 3333333" is longer than "333333". You cannot talk about a string
without embedding it as a substring. However, once you add named
functions to your metalanguage (Haskell):

f 3 = 33333333

Then the string "f 3" is shorter than the string "xxxxxxx". Suppose f 4
= "~xxxxxxx". Now one can talk about the other with the shorter string
on the left:   length "f 3" < length "~xxxxxxx" but also length "f 4" <
length "xxxxxxx". A longer string can talk about a shorter string (but
not vice versa), so this mapping is critical to overcoming the
limitation about talking about oneself.

After that, the rest is easy: encode the Liar's Paradox and voila. once
we have the encoding of a language, and construct functions to encode
proof transformations, we can reduce derivability to a simple predicate
derivable :: String -> Bool and look for some formula f such that
derivable (f) == False and derivable("~" ++ f) == False.

Godel's First Incompleteness Theorem merely says that there is some
integer (which mirrors some well-formed formula) not in the set of
integers that mirror "derivable theorems", making your system
incomplete. Moreover, if you remedy this situation by adding this
integer to the set as an axiom, you immediately can derive another
integer which mirrors its negated formula, making your system inconsistent.

The metasystem (with symbols for derivable, transformation rules like
modus ponens, and the like), are not part of the formal system, but in
the metalanguage. By encoding this metalanguage as well and redoing the
above, you get Godel's Second Incompleteness Theorem, which says that no
system can prove its own consistency, and if an axion is added to assert
  consistency, you can immediately also prove its negation, making it
unsound.

Don't look for a hat trick. Encoding the meta-meta-system buys you
nothing extra.

That's about all I can remember without hypnosis, and I'm afraid of what
I might say under hypnosis... :)

Dan

Algebras Math wrote:

> you mean the godel function (denoted by # and generally will be in type,
> #:term -> number ?) is a kind of functions instead of a particular
> function? If so, what kind of property this kinds of functions have? any
> limitation? how capable they will be?
>
> Thanks
>
> alg
>
> On Tue, Mar 31, 2009 at 4:01 AM, Dan Weston <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     I can't tell exactly what you're asking, but I'll give it a try! :)
>
>     primes :: [Integer]
>     primes = [2,3,5,7,11,13,17,19,23,29,31,undefined]
>
>     godel :: String -> Integer
>     godel = product . zipWith (^) primes . map (toInteger . ord)
>
>     -- Here is the identity function (note that double backslash is a
>     single character
>     godel "\\x -> x"
>     1629920514342441477851613634029704631135430980107335428017064836156091059806450516131002598452000651374890570022191128551421788559667251656959733380229796871976693176094558797489489057311763922507760911447493016261397754567695234219623056037447490713525815311253273691703346455275115486717580778238094808661626709709766328915159206002675716287759792707200037683200000000000000000000000000000000
>
>     -- = 2^92 * 3^120 * 5^32 * 7^45 * 11^62 * 13^32 * 17^120
>
>     ungodel :: Integer -> String
>      -- ungodel . godel = id
>
>     (See http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic
>     for why this works).
>
>     These numbers get large quickly, but are finite for any finite
>     string of finite alphabet.
>
>     godel is a total function (every string has a unique integer), and
>     its inverse (an exercise to the reader involving prime factor
>     decomposition) would also be total if the alphabet were infinite (so
>     that ord would be total).
>
>     Frankly, I wouldn't know how to begin encoding the godel numbering
>     in the type system (shudder!), but being that it is a total
>     primitive recursive function, I suppose there is no theoretical
>     impediment.
>
>     In contrast, Godel's Theorems themselves cannot be so encoded
>     because the last step involves a general recursive function.
>
>     Dan
>
>
>     Algebras Math wrote:
>
>         Hi all,
>
>         I am reading the book "The lambda calculus: Its syntax and
>         Semantics" in the chapter about Godel Numbering but I am
>         confused in some points.
>
>         We know for Church Numerals, we have Cn = \fx.f^n(x) for some
>         n>=0, i.e. C0 = \fx.x and C1 = \fx.fx.
>
>          From the above definition, I could guess the purpose of this
>         kind of encoding is trying to encode numeral via terms.
>
>         How about the Godel Numbering? From definition we know people
>         say #M is the godel number of M and we also have [M] = C#M to
>         enjoy the second fixed point theorem : for all F there exists X
>         s.t. F[X] = X.
>
>         What the mapping function # is standing for? How could I use it?
>         What the #M will be? How to make use of the Godel Numbering?
>
>         Thank you very much!
>
>         alg
>
>
>