Content deleted Content added
MalnadachBot (talk | contribs) m Fixed Lint errors. (Task 12) |
→Article is unintelligible: new section |
||
| (3 intermediate revisions by 2 users not shown) | |||
Line 1:
{{summary in|Lambda calculus}}
{{WikiProject
{{WikiProject Computer science|importance=Mid}}
{{WikiProject Mathematics|priority=low}}
}}
{{To do}}
Line 605 ⟶ 607:
Cheers.—[[User:InternetArchiveBot|'''<span style="color:darkgrey;font-family:monospace">InternetArchiveBot</span>''']] <span style="color:green;font-family:Rockwell">([[User talk:InternetArchiveBot|Report bug]])</span> 23:08, 21 January 2018 (UTC)
== Confusing/contradictory claims about lambda calculus semantics ==
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.
[[User:Nathanielvirgo|Nathaniel Virgo]] ([[User talk:Nathanielvirgo|talk]]) 04:28, 17 October 2023 (UTC)
== Article is unintelligible ==
The article, as currently written, is unintelligible to anybody who isn't already an expert in the field.
The article needs to be rewritten from the beginning, in such a way as to answer the question "What is a fixed-point combinator?" '''in terms that can be understood by somebody who does not already know the answer.'''
[[User:Geoffrey.landis|Geoffrey.landis]] ([[User talk:Geoffrey.landis|talk]]) 20:05, 21 May 2025 (UTC)
| |||