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

[wren ng thornton]

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