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