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

[John Tromp]

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

My Wikipedia page on Binary Lambda Calculus.

  http://en.wikipedia.org/wiki/Binary_lambda_calculus

shows a simple encoding of lc terms as bitstrings, which in
turn are in 1-1 correspondence with the natural numbers.

It also shows how to represent bitstrings as lambda terms,
and gives an interpreter that extracts any closed term M
from its encoding #M.

It also give several examples of how all that is applicable
to program size complexity.

regards,
-John