Thanks for chasing this down!

]]>The error and fix are discussed here: https://math.stackexchange.com/a/4331329/833760 Special thanks to Taroccoesbrocco.

]]>If Todd isn’t reading the forum right now, there may not be anyone here who can check your work. I probably could in principle, but my brain isn’t currently formatted for combinatory logic and I don’t have the time to reformat it for the foreseeable future. If you and the others at math.se are confident in your fixes, please go ahead and edit the pages. Thanks!

]]>Please disregard comments #19 and #20. I was mistaken - that is not the error in pointer to a proof. The step from the first line to the second line is correct. On the other hand there’s an error in the third step. If possible, delete those comments.

On the other hand, I did find the error in pointer to a proof. The error is in the third line and I describe it in detail in this other math.se post. Please double check my work. Thanks.

]]>If you see a way to fix the entry (or entries), it would be much appreciated.

]]>Re: comment #18. I think there might be an error in:

$\array{ Y &= & \lambda y. (s I I)(s(k y)(s I I)) \\ &= & s(\lambda y. s I I)(\lambda y. s(k y)(s I I)) }$I think the second line, $s(\lambda y. s I I)(\lambda y. s(k y)(s I I))$, is actually equal to $\lambda y. ((s I I)y)(s(k y)(s I I))$ which is slightly different than the first line.

]]>Re: comment #18. I think there might be an error in:

$\array{ Y &= & \lambda y. (s I I)(s(k y)(s I I)) \\ &= & s(\lambda y. s I I)(\lambda y. s(k y)(s I I)) }$I think the second line, $s(\lambda y. s I I)(\lambda y. s(k y)(s I I))$ is actually equal to $\lambda y. ((s I I)y)(s(k y)(s I I))$ which is slightly different than the first line.

]]>Just to highlight that the expression in question in comment #17 (the one here) was added in rev 1, Aug 2012 by Todd Trimble (who may no longer be reading the forum here). Later in rev 6 Todd added what seems to be meant as a pointer to a proof.

]]>The SKI fixed-point combinator mentioned in the **Combinatory logic** section:

does not seem to actually be a fixed-point combinator upon closer inspection. Maybe a typo was made. See my math.se post. I’m waiting on confirmation either from math.se or from this forum before editing. Thanks.

]]>In general, can $Y_K$ be constructed to have any number of $L$s (as long as we modify $L$ accordingly)? Is the $Y$-combinator a special case of $Y_K$ with $K = 2$? If so, let me know and I’ll elaborate on this in the **Untyped $\lambda$-calculus** section.

What’s the value in constructing new fixed point combinators from old ones?

]]>Thanks! I haven’t looked at the paper, but the brief description you added to the entry looks a bit weird. Can you say anything about what the purpose of this example is? Is it that one can make lots of fixed-point combinators by adding lots of stuff that gets ignored?

]]>Thanks!! (I already said this in another thread, but I should say it here :-)

I have just added a few more links back and forth, here and there.

]]>Okay, done!

]]>Surely in a (multi)typed context, the fact that we are applying Y to something means automatically that it must be of function type?

Let’s just add some link behind which the user can find an explanation of what it means to “apply a term to another term”.

]]>I did mean to write and link to “unityped”. Thanks for making the redirect; I added a comment to lambda calculus.

On the other hand, I don’t really like the parenthetical “(of function type)” *because* of the unityped case (and also because it makes an already long and involved sentence more long and involved). Surely in a (multi)typed context, the fact that we are applying $Y$ to something means automatically that it must be of function type?

I understand that non-typed means that there is precisely one type. But I am still wondering if the author of those lines did indeed mean to write and link to “unityped”.

We did have a redirect for “untyped lambda-calculus”. Google knows no “unityped lambda-calculus”. My impression is that – whatever the logic of terminology might be – the conventional term is “untyped” and that it would be clearer to use that.

But anyway, both terms now redirect to “lambda-calculus”. I suggest that whoever is fond of “unityped” should there add a corresponding comment.

]]>They really mean the same thing; an untyped whatever doesn’t really have zero types; it has one type, which you then don’t bother to mention.

]]>You really mean to write “unityped $\lambda$-calculus” instead of “untyped $\lambda$-calculus”?

In any case, I made that term, too, redirect to *lambda-calculus*.

Some trivial edits, check if you like them:

In the Idea-section after

term $Y$

I included

term $Y$ (of function type)

to make clear what kind of term we are talking about (necessary, since the line above says we can do this generally in type theory).

Then the word “applied” just a little bit further down I gave a hyperlink to evaluation map. Maybe there should be a more dedicated entry for this, but I think in any case “function application” is a technical term that should be hyperlinked to its explanation.

I also made “recursive function” and “programming language” into hyperlinks, even though the entries do not exist yet.

]]>Very cool additions, Mike!

]]>Lovely! I added some remarks on general recursion and typed $\lambda$-calculus.

]]>