Talk:Fixed-point combinator

This article is rated C-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:

Computer science Mid‑importance This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.Computer scienceWikipedia:WikiProject Computer scienceTemplate:WikiProject Computer scienceComputer science articles Mid This article has been rated as Mid-importance on the project's importance scale. Things you can help WikiProject Computer science with: Here are some tasks awaiting attention: Article requests : Requested articles/Applied arts and sciences/Computer science, computing, and Internet Cleanup : Computer science articles needing attention Computer science articles needing expert attention Copyedit : Computing Expand : Computer science Infobox : Computer science articles without infoboxes Maintain : Timeline of computing 2020–present Photo : Find pictures for the biographies of computer scientists (see List of computer scientists) Computing articles needing images Stubs : Computer science stubs Unreferenced : WikiProject Computer science/Unreferenced BLPs Project-related : Tag all relevant articles in Category:Computer science and sub-categories with {{WikiProject Computer science}} Mathematics Low‑priority This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles Low This article has been rated as Low-priority on the project's priority scale.

To-do list for Fixed-point combinator: edit · history · watch · refresh · Updated 2011-10-26 Here are some tasks awaiting attention: Cleanup : uniform notation Expand : polyvariadic combinators, applications e.g. traced recursion

I saw Y defined in the top portion of the article, but I didn't find FIX defined, at least not by the time it was first used in a calculation. I quickly tried using Y in place of FIX, but it did not seem to be working out. —Preceding unsigned comment added by 71.126.226.201 (talk) 23:15, 26 December 2010 (UTC)[reply]

Did anybody notice that the fixed point combinator by Klop as given here is wrong? Did anybody actually try it? I used it to test my lambda-calculus interpreter and I was thinking of a bug in it, until I found the correct definition somewhere on the web: [1] (look for $). There should be 26 L's, not 28 as given here. The problem is that many web pages directly copy from the Wikipedia text, and give the same (wrong) definition. I don't know whether the page was vandalized long ago, or it was a genuine transcription error. Fixed. --positron 10:14, 7 March 2006 (UTC)[reply]

I don't think anybody did try it. Should've just removed it when I did a big cleanup a while back, I suppose. Thanks for the fix. —donhalcon^╤ 14:52, 7 March 2006 (UTC)[reply]

For those who will be searching for this in the future: the error comes from Klop’s original article, where this combinator has 28 Ls. Kirelagin (talk) 11:29, 16 September 2015 (UTC)[reply]

Could you dumb it down a shade? --Mike Schiraldi 01:53, 27 Jun 2005 (UTC)

• I think the first paragraoh is misleading the reader into thinking about fixpoints as real values, whereas the following paragraph is talking about a fixpoint in function space. It takes a bit of a conceptual leap to understand the latter, and the first paragraph doesn't particularly help...

I've submitted a rewrite that should be a lot easier to understand. --bmills 18:00, 21 October 2005 (UTC)[reply]

I suspect that some of that stuff is graffiti, but I'm not expert enough to say for sure. Will someone please check on it? --unknown

This article certainly doesn't explain things very well except to people who already know the information in the article. I have a bachelor's degree with a double major in computer science and mathematics, one of the courses I took mentioned the Y combinator one day in class, and while I did fairly well in both my majors as well as that class, that particular day in class the material made no sense to anybody and none of the other students understood it either. I still have no idea what on Earth a fixed-point combinator is, as it is described here using very technical language that is so technical you'd probably have to be taking graduate-level courses to understand what any of this means.

Pretty much none of the other programming-related articles on Wikipedia are anywhere near this hard to understand. Somebody really ought to fix this, I still don't have a clue about anything this article is saying and I studied this stuff in college and got good grades in it, at a university that at the time was classified as having one of the top 5 computer science departments in the United States! Could somebody please translate this article from ultra-technical language back into English so that it is readable by people who are not Ph.Ds or in Ph.D programs? I am actually of above average intelligence but even for me this article is way too hard to understand and I agree with the people from 12 years ago back in 2005, it needs to be dumbed down somehow so that people with IQs under 150 and people who did not go to graduate school can understand it. Yes, it's a great article for people who have a Ph.D in computer science and an IQ of 180 but some of us only have IQs in the 140s and only have bachelor's degrees, so please at least dumb it down enough for people like me. --Yetisyny (talk) 11:17, 18 July 2017 (UTC)[reply]

It seems like the Y Combinator should have its own page.

No it doesn't. —Preceding unsigned comment added by 98.108.198.154 (talk) 05:53, 8 March 2011 (UTC)[reply]

excellent argument. "Y combinator" is a term I have run into three times in the past few weeks, and I found better explanations of it elsewhere. Thanks wiki. You suck. More nerds talking to themselves rather than being informative. — Preceding unsigned comment added by 72.92.6.251 (talk) 05:20, 8 September 2012 (UTC)[reply]

There is nothing magic about Wikipedia (except possibly the magic put into it by generous people donating their knowledge and editing skills). There are certainly articles here that are just plain unhelpful to many readers. If you have found better explanations elsewhere, and don't bother to point to them, then you are not being at all helpful in making WP better (which is at the heart of your own criticism). Sorry that I am posting this four years later, when you are no doubt gone, but I share your frustration when reading unhelpful articles. I only wish you had chosen to help us instead of limiting yourself to criticism. David Spector (talk) 01:12, 16 April 2016 (UTC)[reply]

Why does the example mix (a b (c d)) and a(b)(c(d)) notation? It would be a lot clearer, I think, if it stuck to (a b (c d)), and put ( ) on the lambdas as well. It would also be nice to state the final result (fact = (fix ...)). Shinobu 06:57, 8 November 2006 (UTC)[reply]

• The example also appears to be wrong. It uses just part of the church numeral, and confusingly uses f to mean two different things. Can anyone confirm this? (New guy, reluctant to change/break anything) CarpeCerevisi 11:46, 8 February 2007 (UTC)[reply]

Note that the Y combinator is intended for the call-by-name evaluation strategy, since (Y g) diverges (for any g) in call-by-value settings

Can somebody explain this? What does call-by-name versus call-by-value even mean in the context of lambda calculus? Isn't call-by-name always the case in lambda calculus? Why does Y g diverge in call-by-value? What does 'diverge' mean in this context? All these things are totally non-obvious. JulesH 19:12, 11 November 2007 (UTC)[reply]

What call-by-value means is explained at the given evaluation strategy link. The context is evaluation of lambda expressions in real programming languages on real machines. call-by-value requires the evaluation of all of a function's arguments before the function itself is evaluated -- even if evaluation of the function doesn't require some of the arguments. Evaluation of such arguments might not terminate -- it might even diverge if, say, the evaluation creates a lambda expression which in turn becomes the argument to an evaluation ad infinitum, creating larger and larger lambda expressions. -- 98.108.198.154 (talk) 06:43, 8 March 2011 (UTC)[reply]

Also, the "Example" section refers to something described as the "fix" operator, which hasn't been defined. JulesH 19:25, 11 November 2007 (UTC)[reply]

I've read this definition a zillion times and it still makes no sense to me.

A fixed point of a function f is a value x such that f(x) = x.

If you've got an arbitrary function f, why should there be *any* guarantee at all that it will have a fixed point in the first place? If my function is: 'f(x) = x+1', then it's never going to have a value such that f(x) = x for any integer x. If I have a higher-order function 'f(x) = x x', then that's still no guarantee that x x == x for all x's.

It seems like nonsense. What am I misunderstanding here?

I can understand a function which *creates* a higher-order function which is guaranteed to have a known fixed point -- but not one that takes an arbitrary Turing-complete function, somehow analyses it (how do you look inside a lambda abstraction in the first place when the only operation you have is application? And wouldn't working out what value it returns for all arguments involve solving the halting problem?), determines that it has a fixed point, and returns the *fixed point itself*.

Obviously this is a hugely fundamental result in basic computer science, so it must be right, and I thought I vaguely understood lambda calculus, but I can't make head or tail of this definition as written. --Natecull (talk) 23:12, 17 November 2008 (UTC)[reply]

As is explained in the section Fixed point combinator#Existence of fixed point combinators, fixed point combinators need not exist for all settings, and need not be total, i.e. they may diverge for some (even almost all) inputs. However, there are important settings such as CPO, the cartesian closed category of complete partial orders with Scott continuous maps, where fix points always exist. — Tobias Bergemann (talk) 12:25, 18 November 2008 (UTC)[reply]

f is a little too simple, it doesn't have an iterative structure. Let

plus x 0  = x
plus x y  = plus (suc x) (dec y)

where suc(x) is essentially x+1 and dec y is essentially y -1. Your f is just f = (flip plus 1).

OK now the problem is plus is defined recursively. So lets make it a function of 3 variables:

plus' g x 0  = x
plus' g x y  = g (suc x) (dec y)

and if we had a working plus obviously plus' plus x y = plus x y. But we don't. On the other hand we can keep feeding plus' more copies of plus' and actually get a plus:

plus x y = (fix plus') x y

and then you can define your f as

f' x = (fix plus') x 1

jbolden1517^Talk 22:41, 27 March 2009 (UTC)[reply]

Hmmmm. So, if I read you right, you're basically saying what I was figuring at first: that fix (by which I assume you mean Y) can only be defined on functions like plus' which are specially written in such a way as to receive a (fix whatever) function as a first argument? And not on functions like plus which are not?

So how do you prove that all functions in the system are the plus' kind and not the plus kind? Or am I still asking the wrong questions here?

I'm still not seeing what (fix f') should produce here, which was my original question.

If the answer is 'Y can only be defined over recursive functions like plus', don't attempt to take the fixpoint using Y of a non-recursive one like f' then it makes sense to me. But that means it's not actually a generalised fixpoint combinator, is it? It's only the fixpoint for a very small subset of all possible functions which play by the rules.

--Natecull (talk) 06:16, 13 June 2009 (UTC)[reply]

If I have a higher-order function 'f(x) = x x', then that's still no guarantee that x x == x for all x's. -- But that's not the requirement. All we have to do is find some x for which x x = f(x) = f(f(x)) = f(f(f(x))) etc. -- 98.108.198.154 (talk) 07:04, 8 March 2011 (UTC)[reply]

Both examples for the Y combinator use functional languages, which support Currying. This means that the given examples can not simply be translated to other languages which support first-class functions, but no currying/partial exaluation.

Here is an example in Ruby of the y combinator and its use with factorial. It explicitly uses an additional function which takes the arguments for our original function, apart from that, it is a direct translation of the y combinator's definition. Maybe we could try to improve it a little / make it more readable (at least add proper indendation) and then incorporate it into the article.

y = lambda { |f| (lambda { |x| lambda { |*args| (f.call(x.call(x))).call(*args) }}).call(lambda { |x| lambda { |*args| (f.call(x.call(x))).call(*args) }})}
b = y.call(lambda { |f| lambda {|i| if i == 0 then 1 else i * (f.call(i-1)) end }})
puts(b.call 5) # 120

Subwy (talk) 10:58, 10 December 2008 (UTC)[reply]

One really good demonstration of how the Y combinator works (it has enough hand waving to make the general principles accessible to the layman), is this:

      let Y = (lambda (f)
                ((lambda (g) (f (g g)))
                 (lambda (g) (f (g g)))))
      let H = (lambda (g) (f (g g))) for convenience
  
      let fact = (Y fact-h)  
  
         fact 
      => (Y fact-h)
      => (H H)      ; with f = fact-h
      => (fact-h (g g))
      => (fact-h (H H))
      =  (fact-h (Y fact-h))
      =  (fact-h fact)
  
      ;; => indicates a substitution step, while = indicates an equivalence
      ;; which is not actually a substitution

Unfortunately, this uses a lispy syntax, which most people are not familiar with. We should work this into something that could go into the article. — Edward Z. Yang^(Talk) 06:23, 29 January 2009 (UTC)[reply]

Technically the Haskell definition is the equation that defines any fixed point combinator no? So why is it Y? Pcap ping 04:51, 21 August 2009 (UTC)[reply]

Well, that was incorrect, so I've fixed it. Pcap ping 21:33, 21 August 2009 (UTC)[reply]

Functions in lambda calculus don't have a name, so that statement is nonsensical in the context of lambda calculus. To make some sense you need to specify some formal language where you can/must have names for some functions. But the example that is supposed to clarify the meaning of "anonymous" (as opposed to named) is in lambda calculus, where all functions are anonymous! The anonymous (like all other!) function returned by Y (i.e. factorial) is indeed a primitive recursive function, but all μ-recursive functions are lambda definable (see a theory book for proof, e.g. [2]), so what are you trying to say here? Pcap ping 05:38, 21 August 2009 (UTC)[reply]

I think I've clarified the matter. Pcap ping 07:22, 21 August 2009 (UTC)[reply]

It is true that the only form of recursion in lambda calculus is anonymous recursion (since there are no functions names). But for most people in other languages, they are only familiar with recursion by explicitly using the function name. The very concept of anonymous recursion is surprising to many people. It is therefore informative to tell them that fixed point combinators is the mechanism by which anonymous recursion is done (and specifically "anonymous" recursion, to distinguish it from the recursion that they are familiar with). Fixed point combinators are not just for lambda calculus, but also other languages too. --76.173.203.32 (talk) 04:31, 22 August 2009 (UTC)[reply]

This was mentioned in the lead, with references, and I now added another paragraph that delves on the matter in the "how it works" section. There's also a (short, because it's somewhat off-topic) section describing alternative solutions to the problem of anonymous recursion. Pcap ping 08:37, 22 August 2009 (UTC)[reply]

The opening sentence of this article is: "A fixed-point combinator (or fixpoint combinator) is a higher-order function that computes a fixed point of other functions."

I think it would be better preceded with a couple of words specifying which academic field this subject falls under. Eg "In computer science, a fixed-point combinator..." Or perhaps "In mathematics..." or "In logic theory..." (I don't know which is most appropriate, or I'd add it myself.)

Without any context, the opening sentence seems a bit obscure and esoteric, if you're unfamiliar with the subject (like me). Denbosch (talk) 11:31, 10 November 2011 (UTC)[reply]

Done. —Ruud 15:14, 10 November 2011 (UTC)[reply]

There are two fix point combinators in Haskell, one is code-replicating, another is through sharing:

fix f = f (fix f)

fix f = x where x = f x

The second one lends itself naturally to corecursive definitions, like

fibs = fix ((0:) . (1:) . next) 
  where 
    next (a:t@(b:_)) = (a+b):next t

Used w/ the first fix, it still works though runs in quadratic time.

Can/should/how can this be incorporated into the article? – WillNess (talk) 21:54, 11 November 2011 (UTC)[reply]

In the introduction, the statement that there is an infinity of fixed-point combinator in the simply-typed lambda calculus is flagged with "citation needed" (July 2011). However, this statement is expanded upon and sourced in section 2.2 "Other fixed-point combinators" (the Goldberg, 2005 reference). Shouldn't "citation needed" be replaced with "see below" or some such?

Ixache (talk) 17:59, 7 December 2011 (UTC)[reply]

Reading recursively enumerable set it seems it's not necessarily infinite. I added same tag in that section you mention. -- WillNess (talk) 11:21, 8 December 2011 (UTC)[reply]

Huh? Why do we need a citation for such a trivial fact? If we have one fixed-point combinator, say f, then e.g. I f, B I f, B f I, K f f and many others are fixed-point combinators (with B=λfgx.f(g x), I=λx.x, K=λxy.x). What Mayer Goldberg shows is a different fact, namely that the set of fixed-point combinators is c.e.

And last, but not least: in simply typed lambda calculus there is no fixed-point combinator, as the article correctly states.

--Daniel5Ko (talk) 14:34, 9 December 2011 (UTC)[reply]

I was merely acting on an observation that c.e. (or r.e.) is not necessarily infinite. I think your explanation should be added into the page, maybe as ref remark, replacing the "cn" tag. WillNess (talk) 17:20, 9 December 2011 (UTC)[reply]

Here's a tested PHP 5.4 implementation for the Y Combinator function:

function Y(callable $f)
{
	$funcA = function ($x) use ($f)
	{
		return $f(function ($v) use ($x)
		{
			$funcB = ($x($x));
			return $funcB($v);
		}); 
	};
    return $funcA($funcA);
}

And the factorial example applied to it:

$factorial = Y(
	function ($fac)
	{
		return function ($n) use ($fac)
		{
			if ($n === 0) {
				return 1;
			} else { 
				return $n * $fac($n - 1);
			}
		};
	}
);

$result = $factorial(5); // 120

Jazzer7 (talk) 06:51, 6 June 2012 (UTC)[reply]

Something that has bothered me about many of the articles regarding lambda calculus. There is a tendency to make examples a massive cludge from lots of different program languages that do not add any encyclopedic value to the content of the article. Everyone looks at an article, and says, "My favorite language isn't represented here!" and then adds it.

In the last few weeks, I noticed two additions to this article list of examples (C-sharp and Javascript). These are useless examples. I'm always a little weary getting rid of content, but this every growing list of examples has to stop. It violates WP:NOT on indiscriminate lists; in particular, it is a list of information which was gathered in a thoughtless manner not consistent with expanding the encyclopedic value of the article.

Examples are good however. So I propose that we leave two examples. One from a procedural language and one from a functional language. I think the best ones to leave are Python (because it's very human-readable) and ML, which for some reason isn't even on the article despite being of the greatest theoretical importance (probably because you need to use let rec...). I would be bold, but I'm a little hesitant to alter so many people's edits without giving a chance for people to tell me why they believe this isn't a indiscriminate list of information. So without other suggestions, I will make my proposed changes soon. Wgunther (talk) 14:32, 25 November 2012 (UTC)[reply]

This is a problem across many computer science articles, I like to call it "language creep". The only solution it to prune mercylessly, preferably leaving only a single example in a non-real language like PCF or psuedo-ML. Also, the section should under not be called "Example in <language X>", this is too big of an invitiation to add an additional section "Example in <language Y>", and so on. Occasionally it might be useful to add a link to Wikibooks or Rosetta Code with more examples. —Ruud 16:07, 25 November 2012 (UTC)[reply]

I agree: prune heavily to just the one or two best examples. No need for a gallery of languages. — Carl (CBM · talk) 19:31, 25 November 2012 (UTC)[reply]

Seconded. Especially glad to see the C-sharp version amended/removed, since it uses named recursion (the Y function calls the Y function) which defeats the point. Plus it's type annotations make it look a mess ;) 87.194.139.125 (talk) 20:55, 30 November 2012 (UTC)[reply]

I took out all the examples written in the form of a code repository, citing MOS:CODE a month ago. Now I'm getting some undos, with no edit summary and no discussion, and no attempt to reformat and pick examples that actually increase the encyclopedic nature of the article. I'm not willing to do this, because I don't think any of the example eliminated have encyclopedic nature, and believe a consensus was reached about these examples as well. I'm assuming good faith, but I will enforce my elimination without new talk or at least an edit summary on the undo. Wgunther (talk) 23:25, 11 January 2013 (UTC)[reply]

I think we should return most of the code examples (excl. wrong ones, as C#). While it's the case that they do not add any encyclopedic value, I find them really useful when one tries to grasp anonymous recursion. They may provide better background for understanding somewhat more abstract way of implementing recursion with y-combinator serving as quick how-it's-done reference than more theoretically-inclined lambda calculus or ML/Haskell - imo most people comfort with these languages already have sound theoretical foundations and concrete code example adds little or no benefit. I suggest keeping at least Python/Javascript and Scheme/Lisp. БръмБръм (talk) 13:40, 14 February 2013 (UTC)[reply]

Under "Explanation for imperative programmers", it is stated that "It is difficult and confusing to try to write fixed_point() in imperative terms, so we will not attempt it."

However, the example there can be fixed to address this (if I am not mistaken), without the explicit introduction of a general fixed-point combinator for that language, i.e., it can be changed to show how a non-iterative, non-recursive solution can be programmed. How about this rewrite (changes in bold):

How is a recursive function written in these languages? It is done by breaking the function into two parts. The first part looks very similar to the recursive version of the function. The difference is that it takes a function as a parameter and calls that parameter instead of calling itself recursively. (Remember, functions are values so they can be passed as arguments to functions. This isn't often done in imperative programming.)

factorial_helper(function foo, integer n) {    --- added function as a parameter
  if n=0 then
    return 1;
  else
    return n * foo(foo, n-1);   --- recursive call replaced with call to parameter
}

Now, if that function parameter was "factorial", then this helper function would calculate the factorial. So, the second part of building the recursive function is to create a function "factorial" and set it equal to "factorial_helper" with "factorial_helper" as the first parameter.

factorial(integer n) { 
  factorial_helper(factorial_helper, n)   --- "factorial_helper" is passed as the function parameter to itself
}

Now, the subsequent paragraph can be deleted:

This doesn't quite work because we've run into the same problem as before: the function "factorial" is using its value before we get to the end of its definition. The fixed-point function solves this for us. Due to its special structure, it is able to call "factorial_helper" recursively without using a value before it is defined. The fixed point function takes the helper as an argument and returns the recursive function. (Remember functions are values - they can be passed as arguments and returned by functions.)

factorial = fixed_point(factorial_helper)

It is difficult and confusing to try to write fixed_point() in imperative terms, so we will not attempt it.

Instead, it can be pointed out that this specific solution could be obtained via a general fixed-point combinator, which can also be used for other recursive definitions, rather than relying on ad hoc solutions (for the fixed point).

Wstomv (talk) 20:34, 26 August 2013 (UTC)[reply]

What you've given is a (correct) way to define a fixed point (for factorial), but it is still "difficult and confusing" to try to write "the" fixed_point (i.e. the function). Haklo (talk) 23:50, 9 January 2014 (UTC)[reply]

Does this work? It doesn't involve a fixpoint combinator (or does it?).

factorial_helper(function foo, integer n) {
  if n=0 then
    return 1;
  else
    return n * foo(foo, n - 1);
}

factorial(n) {
  return factorial_helper(factorial_helper, n)
}

If this is a valid way to do anonymous recursion, why do we need fixpoint combinators to do this? — Preceding unsigned comment added by 18.111.28.55 (talk) 17:57, 14 November 2013 (UTC)[reply]

The Y combinator is not the only way to do recursion. Recursion in lambda calculus always involved passing in the function to be called as a parameter. Kind regards Thepigdog (talk) 09:14, 13 January 2014 (UTC)[reply]

"every function has at least one fixed point"

What about not.

${\displaystyle x=\neg x}$

Thepigdog (talk) 10:03, 9 January 2014 (UTC)[reply]

Every function has at least one fixed point in (untyped) lambda calculus. The example you have given implies something like a boolean algebra, which will not have fixed points for all functions. If you give some lambda expressions instead the fixed point will be obvious (more or less). Haklo (talk) 23:38, 9 January 2014 (UTC)[reply]

Boolean logic may be implemented in lambda calculus. See Church encoding. You can give an expression for Y F in this case, but the calculation would never terminate (beta reduce to normal form). So no fixed point.

${\displaystyle \operatorname {not} _{1}=\lambda p.\lambda a.\lambda b.p\ b\ a}$

${\displaystyle (\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))(\lambda p.\lambda a.\lambda b.p\ b\ a)}$

And the re-cursion is,

${\displaystyle (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))}$

${\displaystyle (\lambda p.\lambda a.\lambda b.p\ b\ a)\ ((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))}$

${\displaystyle \lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a}$

...

${\displaystyle \lambda a.\lambda b.(\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a)\ b\ a}$

... (beta and then eta reduction)

${\displaystyle (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))}$

Which is the first line and will re-curse indefinitely.

Thepigdog (talk) 01:10, 10 January 2014 (UTC)[reply]

I have taken out,

"In these formalizations, the existence of a fixed-point combinator means that every function has at least one fixed point; a function may have more than one distinct fixed point."

I don't believe this statement, but will happily eat crow if someone can show me a fixed point term in normal form for the function,

${\displaystyle \lambda p.\lambda a.\lambda b.p\ b\ a}$

The basis of learning is finding out you are wrong so please prove me wrong, and I will put the statement back.

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

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 Thepigdog (talk) 09:08, 13 January 2014 (UTC)[reply]

Lambda terms are mathematical objects in their own right, just like sets (for example), and lambda calculus is its own mathematical theory. The "data types" and "conversions" you are talking about are further considerations, and not relevant to what is true or false in lambda calculus. In this particular discussion, when we talk about finding the fixed point to a function, the function we mean is a lambda term; it is not a function in a different theory which has been "converted" to a lambda term. Such a "converted function" question is a very different question, more along the lines of lambda definability. Finally, because the "fixed point question" is a question about lambda terms (and nothing else), normal form is not relevant. Haklo (talk) 22:50, 14 January 2014 (UTC)[reply]

Hmmm interesting perspective. I dont disagree very much. But we start by defining the y combinator in mathematics, so we must give a mathematical value for the fixed point. From the readers point of view this is what they expect. If you were only talking about a lambda calculus fixed point function only then things would be different. But then you could not talk about "value" or "exists" or "solving". I dont think the Y combinator gives a solution in any sense that I can think of. It is a function that satisfies the properties of the equation, but it is not a solution, because it is not a value. You are saying a normal form is not necessarily a value, which I agree with. Do you have a reference for this? We desperately need references. I would love to have a reference that says any of,

* The value of two expressions is the same iff the two expressions are equal.

* A normal form is not necessarily a value.

* A value in mathematics is a canonical form

Or any other reference that gives a coherent picture of this. I dont think you can say that LC is just it's own theory and has no relationship to mathematics. That doesn't seem useful to me. Better to explain the relationship, it least for the readers benefit. Regards Thepigdog (talk) 00:15, 15 January 2014 (UTC)[reply]

"Mathematics" is the thing which is not a theory. ZFC set theory is a (mathematical) theory. Euclidean geometry is a (mathematical) theory. First order arithmetic is a (mathematical) theory. Lambda calculus is a (mathematical) theory. I'm not sure of the best way to interpret "value" in the context of this discussion, but "equals" is easy; it's whatever the axioms of the theory say, and the axioms of lambda calculus say it's convertibility (see Barendregt for example; I don't have my copy handy just at the moment). With regard to a fixed point combinator in "mathematics", i.e. the (informal) meta-theoretic question, I'm less sure what to say. The meta-theoretic concept of a fixed point is reasonably clear, because the meta-theoretic concept of a (first order) function is reasonably clear, but I don't think a combinator is, because higher-order functions aren't (at least to me). Haklo (talk) 00:50, 15 January 2014 (UTC)[reply]

By mathematics I loosely mean ZFC based stuff. My only problem is saying that the Y combinator gives a solution of the fixed point equation. But then the fixed point equation is expressed in "mathematics", not LC. Anyway for me a value is a property of an expression (wff) that is the same iff the two expressions are equal. And a solution is a value that satisfies the equation. But maybe this not the standard definition for mathematician (only for other humans). My objection before was you referring to Y f as a solution of x = f x. I will re-read what you wrote in light of this discussion later. Regards Thepigdog (talk) 02:22, 15 January 2014 (UTC)[reply]

I think an intuitive (informal) notion of "value" that might work for you is that lambda terms are their own values so long as "equals" is expanded to convertibility as per the usual axioms of LC. This is a bit like providing semantics for lambda calculus using a term algebra generated by the usual formation rules for lambda terms. A better notion of value is a Bohm tree, which makes explicit the value of a non-normalising term (it still has a value). Haklo (talk) 04:40, 15 January 2014 (UTC)[reply]

I think a Bohm tree is OK for me as a value for LC. As I understand it, a bohm tree allows you to access parts of the value (like a record where some fields are given but not others). Does that help you in giving me a value for x = not x? Regards Thepigdog (talk) 06:42, 15 January 2014 (UTC)[reply]

I've revised the Bohm tree page, although I haven't put references in yet and the phrasing is awkward because I've tried to keep it non-mathematical (and so I didn't quote Barendregt). It may help giving "values" for terms that do not have normal forms, but I don't think you need it for the "not" example; I think the fixed point I gave for that earlier should serve? Haklo (talk) 12:45, 16 January 2014 (UTC)[reply]

The point is; your right and I was wrong. The Y combinator applied to a function must represent a single value in the LC domain. Its a definitional thing. The domain of LC is not necessarily the same as the domain of the function. Crow must be eaten. I have added a section Values and domains, but of course feel to rewrite or modify. Your changes to the Bohm tree are good and make it more understandable. I get the motivation but I dont fully understand yet. Thepigdog (talk) 14:09, 16 January 2014 (UTC)[reply]

"That is, we can ask the question in reverse: does there exist a lambda abstraction that satisfies the equation of FACT? The answer is yes, and we have a "mechanical" procedure for producing such an abstraction: simply define F as above, and then use any fixed point combinator FIX to obtain FACT as FIX F."

This sounds like the Y combinator is an equation solver. The Y combinator only implements recursion. If in c++ language,

 double SquareRoot(double x) { return x/SquareRoot(x); }

Is equivalent to,

${\displaystyle {\operatorname {SquareRoot} (x)}^{2}=x}$

${\displaystyle \operatorname {SquareRoot} (x)={\sqrt {x}}}$

But we cant claim that the SquareRoot calculates the square root. It doesn't even converge to it.

Thepigdog (talk) 13:30, 9 January 2014 (UTC)[reply]

The Y combinator solves the lambda calculus equation Y F = F (Y F). If you switch to a different theory or domain it's an entirely different story. Haklo (talk) 23:41, 9 January 2014 (UTC)[reply]

${\displaystyle FX={\frac {1}{X}}}$

Y combinator does not solve this. It does not terminate. So in general the Y combinator does not solve the equation. In face ${\displaystyle FX=X\implies \operatorname {false} }$ is Curry's paradox. This is why it is called the paradoxical combinator. Given an extra parameter the calculation may terminate, but for most functions the Y combinator does not terminate. In reality the Y combinator only implements simple recursion.

"=" does not mean "compute" (and it certainly doesn't mean anything number-algebraic) in the lambda calculus; it means "is convertible". The kinds of computations to which you refer are ways in which convertibility may be established, but they are not the same as convertibility. The lambda calculus itself is not a computation. Haklo (talk) 03:16, 10 January 2014 (UTC)[reply]

Lambda calculus is a model for computation, and numbers (and anything else computable (see Church–Turing thesis)) may be represented by Church encoding. Your statements imply that Y combinator can compute the solution to fixed point equation in all cases. But all it does is simple recursion. For the case given for the definition of factorial, it terminates, but for most cases it does not. This is what I am not understanding.

Thepigdog (talk) 03:49, 10 January 2014 (UTC)[reply]

The problem is only how you are trying to interpret "=". For example, the following statement (identity) is true in the lambda calculus: (λf.f)X = X. And this is true regardless of what X is; it may be Ω, which is an expression that does not have a normal form, and so does not "correspond" to a computation that terminates. There is a relationship between computations and lambda expressions, but they are not the same thing. Haklo (talk) 05:41, 10 January 2014 (UTC)[reply]

I am not understanding the relevance of your response.

Do you agree that for most (or at least many) functions F the Y F will not reduce to a normal form by beta and eta reductions? (even using applicative order).

Do you agree that there are functions F (in mathematics) for which the cardinality { Y F | Y F = F Y F} is 0, 1 or > 1.

Do you agree that if the cardinality is zero there does not exist a fix point of F?

Do you agree that numbers and any other data type may be represented (as higher order functions) in Lambda calculus?

I am really struggling to make sense of your responses. If you could confine your self to

answering these specific points we may uncover the critical point I am not understanding here.

Is there a link to some article that explains your viewpoint?

Since you say all functions have at least one fixed point, what is the fixed point of ${\displaystyle \operatorname {not} _{1}=\lambda p.\lambda a.\lambda b.p\ b\ a}$?

Thepigdog (talk) 07:26, 10 January 2014 (UTC)[reply]

I have done a little bit of editorial work mainly moving stuff around and trying to organize things. If something important to you has been lost add a note here. I hope the changes are acceptable for everybody.

Thepigdog (talk) 05:06, 16 January 2014 (UTC)[reply]

A somewhat clumsy introduction section, but I wanted to cover the misunderstandings I have seen in the past.

Thepigdog (talk) 04:58, 20 January 2014 (UTC)[reply]

 fix :: (a -> a) -> a
 fix f = f (fix f)            -- non-sharing fixed-point, for recursive definitions
 -- alternative:
 -- fix f = let x = f x in x   -- sharing fixed-point, for corecursive definitions

Are the comments correct??? From my reading, the two forms have nothing to do with recursion and corecursion. Both are recursive definitions; one is the lifted form of the other.

Thepigdog (talk) 03:41, 4 February 2014 (UTC)[reply]

I don't see enough merit in having yet another C++ example. This is not a collection of different implementations of the Y combinator. See rosettacode.org for that. So I have taken it out.

If I was to be picky I would say.

• Y combinator should be templated (not int -> int).
• Dont need main (so remove iostream, cassert)

But you do all that and it still adds nothing to the understanding of the Y combinator. Sorry.

#include <functional>
#include <iostream>
#include <cassert>
 
using std::function;
// Y-combinator compatible factorial
int fact(function<int(int)> f,int v)
{
  if(v == 0)
    return 1;
  else
    return v * f(v -1);
}
 
// Y-combinator for the int type
function<int(int)>
    y(function<int(function<int(int)>,int)> f)
{
  return [=](int x) {
    return f(y(f), x);  
  };
}
 
int main(void)
{
  function<int(int)> factorial = y(fact);
  assert(y(fact)(5) == fact(y(fact), 5));
  std::cout << factorial(5) << std::endl;
  return 0;
}

Thepigdog (talk) 05:39, 30 October 2014 (UTC)[reply]

I think this example does not add anything. Perhaps you would like to add it to,

• http://rosettacode.org/wiki/Y_combinator

For example, a Y-combinator implementation of factorial in the Wolfram Language would be

Y = Function[f, #[#]&[Function[g, f[g[g][##]&]]]];
factorial = Y[Function[f, If[# < 1, 1, # f[# - 1]] &]];
factorial[6] (*Yields 120*)

Thepigdog (talk) 02:20, 26 May 2015 (UTC)[reply]

Hello fellow Wikipedians,

I have just modified 2 external links on Fixed-point combinator. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20110822202348/http://mvanier.livejournal.com/2897.html to http://mvanier.livejournal.com/2897.html
• Added archive https://web.archive.org/web/20110822202348/http://mvanier.livejournal.com/2897.html to http://mvanier.livejournal.com/2897.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 19:07, 5 April 2017 (UTC)[reply]

I fixed some parts, later I saw here, some comments proposing similar fixes.

I think that the main problem of this article is that it seems to be based in some notes about scheme. Scheme is based on lambda calculus, it is not lambda calculus. 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. — Preceding unsigned comment added by 201.124.239.99 (talk) 13:25, 25 April 2017 (UTC)[reply]

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.

1. fac : (Int -> Int) -> (Int -> Int)
2. fix : (t -> t) -> t with [t := (Int -> Int)]

3. fix fac :: Int -> Int

However this is a value in the 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,

${\displaystyle x^{2}=-1\Rightarrow x={\frac {-1}{x}}\Rightarrow f\ x={\frac {-1}{x}}\land {\textsf {Y}}\ f=x}$

Division of 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 numbers 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 ${\displaystyle Y\ f}$ 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! — Preceding unsigned comment added by 201.124.239.99 (talk) 23:33, 25 April 2017 (UTC)[reply]

See the wiki page on Church encoding. In fact negative numbers may be represented in lambda calculus. Also division may be implemented.

In fact any data type can be.

Pure mathematicians are interested in lambda calculus as a system with it's own domain. Computer programmers just want to use lambda expressions.

Thepigdog (talk) 01:08, 19 May 2017 (UTC)[reply]

Hello fellow Wikipedians,

I have just modified 4 external links on Fixed-point combinator. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20140408014716/http://cs.anu.edu.au/courses/COMP3610/lectures/Lambda.pdf to http://cs.anu.edu.au/courses/COMP3610/lectures/Lambda.pdf
• Added archive https://web.archive.org/web/20090113202334/http://www.latrobe.edu.au/philosophy/phimvt/joy/j05cmp.html to http://www.latrobe.edu.au/philosophy/phimvt/joy/j05cmp.html
• Added archive https://web.archive.org/web/20061110043130/http://use.perl.org/~Aristotle/journal/30896 to http://use.perl.org/~Aristotle/journal/30896
• Added archive https://web.archive.org/web/20090314203740/http://bc.tech.coop/blog/070611.html to http://bc.tech.coop/blog/070611.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 22:11, 1 October 2017 (UTC)[reply]

Hello fellow Wikipedians,

I have just modified one external link on Fixed-point combinator. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20160304101809/http://osdir.com/ml/lang.haskell.cafe/2003-10/msg00211.html to http://osdir.com/ml/lang.haskell.cafe/2003-10/msg00211.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 23:08, 21 January 2018 (UTC)[reply]

This is mostly about the "values and domains" section, but there are also various other comments scattered throughout the article that I think need clearing up.

I'm not an expert, but it seems to me that there are at least two ways to think about the semantics of untyped lambda calculus. One is the "domain" approach, explained (though not very clearly) in the linked Deductive lambda calculus article. In this interpretation every lambda expression has a value, even the non-halting ones. But there is also the more obvious semantics where each lambda expression is a partial function. It has a value if it beta reduces to a normal form, but otherwise it doesn't have a value. I believe that both of these are consistent and it's really a matter of choice which one to use.

The issue is that the article sometimes talks in terms of one and sometimes in terms of the other. For example, in the lede it states

a fixed-point combinator (or fixpoint combinator) is a higher-order function that returns some fixed point of its argument function, if one exists.

This sounds like it's taking the partial function view: the argument function might not have a fixed point, and in that case the fixed-point combinator doesn't return a value.

(Though now I come to think of it, this statement is not actually correct. Consider the Y combinator applied to the identity function. It's easy to see that no value is returned in this case, even though any lambda term at all is a fixed point of the identity function. I guess the correct statement would be that it returns some fixed point of its argument function if it halts.)

On the other hand the article also makes statements like

In the classical untyped lambda calculus, every function has a fixed point

which seems to me to be true in the domain interpretation but not in the partial function interpretation. (Although I could be wrong about that.) It also makes statements like

Every expression has one value. This is true in general mathematics and it must be true in lambda calculus.

Which seems like it's trying to justify the domain semantics as the only true semantics of the lambda calculus. But really it's just a false statement, since there's nothing to stop you defining a system where an expression might have many or no values, and the partial function semantics is such a system (I think).

So it seems to me that the article has sort of mixed up two different views about the semantics of the lambda calculus and also tried to present one of them as the only semantics, without flagging up that this is a choice. I would try to fix this myself but I don't feel I have the expertise to be sure I'm getting it right - I'm just mentioning this because I think it needs attention from someone who knows what they're doing.

Nathaniel Virgo (talk) 04:28, 17 October 2023 (UTC)[reply]