[Haskell-cafe] abou the Godel Numbering for untyped lambda calculus

[Algebras Math]

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 C
1 = \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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090331/fb94d606/attachment.htm