Talk:Fixed-point combinator: Difference between revisions

Revision as of 13:26, 25 April 2017

Revision as of 23:33, 25 April 2017

Line 528:

In lambda calculus nor combinator logic, one can't write recursive definitions like fact x = if x=0 then 1 else x*fact (x-1)

that is the reason for a fixed point combinator. <!-- Template:Unsigned IP --><small class="autosigned">—&nbsp;Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/201.124.239.99|201.124.239.99]] ([[User talk:201.124.239.99#top|talk]]) 13:25, 25 April 2017 (UTC)</small> <!--Autosigned by SineBot-->

== Values and domains section is obscure ==

I can not understand what is this section about, it has some misconceptions repeated along all the article, let's see what I mean.

:Every expression has one value. This is true in general mathematics and it must be true in lambda calculus. This means that in lambda calculus, applying a fixed point combinator to a function gives you an expression whose value is the fixed point of the function.

Lambda calculus is a theory of computable functions, a function is a relation between to sets, i.e. it has one input and one output.

Higher order functions, may have functions in their ___domain and codomain. Fixed point combinators are higher order functions.

# fac : (Int -> Int) -> (Int -> Int)

# fix : (t -> t) -> t with [t := (Int -> Int)]

--------

:3. fix fac :: Int -> Int

:However this is a value in the [[Deductive lambda calculus#Domain of lambda calculus|lambda calculus ___domain]], it may not correspond to any value in the ___domain of the function, so in a practical sense it is not necessarily a fixed point of the function, and only in the lambda calculus ___domain is it a fixed point of the equation.

What does it mean? Should I have to read the whole lambda calculus ___domain to know what is going on?

:For example, consider,

:: <math> x^2 = -1 \Rightarrow x = \frac{-1}{x} \Rightarrow f\ x = \frac{-1}{x} \and \textsf{Y}\ f = x</math>

:[[Church encoding#Division|Division]] of [[Church encoding#Signed numbers|Signed numbers]] may be implemented in the Church encoding, so ''f'' may be represented by a lambda term. This equation has no solution in the real numbers. But in the ___domain of the [[complex number]]s ''i'' and ''-i'' are solutions. This demonstrates that there may be solutions to an equation in another ___domain. However the lambda term for the solution for the above equation is weirder than that. The lambda term <math>Y\ f</math> represents the state where x could be either ''i'' or ''-i'', as one value. The information distinguishing these two values has been lost, in the change of ___domain.

What does this mean? What does the formulas refer to?

Church numerals are a representation for natural numbers with lambda expressions to establish a correspondence with primitive recursive functions can be represented in lambda calculus.

There are not divisions between naturals, 1/2 = 0.5, a rational.

there are no subtractions among naturals 1-2=-1, a negative integer number. There are quotient and reminder of natural numbers, and a monus, not minus operator 1 monus 2 = 0. One can build representations for integers and rationals within lambda calculus, but those are not Church numerals.

:For the lambda calculus mathematician, this is a consequence of the definition of lambda calculus. For the programmer, it means that the beta reduction of the lambda term will loop forever, never reaching a normal form.

The reduction order depends on the profession of the reader?

For this reasons this section should be deleted!