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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
