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

John Tromp john.tromp at gmail.com
Tue Mar 31 09:57:39 EDT 2009

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


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.


More information about the Haskell-Cafe mailing list