Re: [Haskell-cafe] about the Godel Numbering for untyped lambda calculus
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
John Tromp wrote:
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.
Also don't forget Jot[1] [1] http://barker.linguistics.fas.nyu.edu/Stuff/Iota/ -- Live well, ~wren
participants (2)
-
John Tromp -
wren ng thornton