Talk:Fixed-point combinator: Difference between revisions

Revision as of 04:28, 17 October 2023

Revision as of 04:30, 17 October 2023

Line 610:

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 haltsbeta 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

Line 618:

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