[Haskell-cafe] abou the Godel Numbering for untyped lambda
calculus
Dan Weston
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
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
>
More information about the Haskell-Cafe
mailing list