[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
>