Talk:Fixed-point combinator: Difference between revisions

Revision as of 04:40, 13 January 2014

Revision as of 09:08, 13 January 2014

Line 355:

: Why do you want it in normal form? Anyway, {{math|λ''a''.λ''b''.λ''f''.''f''}} might be what you want. [[User:Haklo|Haklo]] ([[User talk:Haklo|talk]]) 04:40, 13 January 2014 (UTC)

:: Starting in mathematics we have a function for which we want a fixed point. The function has a data type and we are expecting a fixed point as a value, of the correct data type. The function is converted to lambda calculus, using an appropriate church encoding. Then we run the lambda expression to find a normal form. The normal form needs to be able to be interpreted as a value of the datatype. The value is mapped back as a mathematical value and is the solution. If the lambda expression does not terminate there are two problems,

:: * The lambda expression does not represent a value of the data type, and does not represent a solution.

:: * There is no proof that the lambda expression represents a single value, and is mathematically sound.

:: So based on this argument only a term in normal form will do.

:: Kind regards [[User:Thepigdog|Thepigdog]] ([[User talk:Thepigdog|talk]]) 09:08, 13 January 2014 (UTC)

==Its not magic==