[Haskell-cafe] abou the Godel Numbering for untyped lambda
westondan at imageworks.com
Mon Mar 30 23:01:33 EDT 2009
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
godel "\\x -> x"
-- = 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
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
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.
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!
More information about the Haskell-Cafe