I used the Y combinator in some school homework!

[d4s_over_dt4]

One of my homework is to write something about the spring festival.

Summary

The Spring Festival is here, and everyone is setting off fireworks. I see a lot of fireworks every night. After the fireworks explode, some sparks will be blown up. Some sparks are red, some green, some blue, some very bright, some not bright, and there are small sparks that explode and will explode again,and look the same as the original big fireworks after exploding again...
Huh, wait, what?
This reminds me of a very important concept:recursion. Recursion is a function that calls its own procedure. Recursion must have state transitions and underlying conditions.
Speaking of functions, I think of function-centric lambda calculus. So, how do you achieve recursion in the lambda calculus? (Because if there is no recursion, some of the functions are uncomputable, such as the Ackermann function.)
In the lambda calculus, there is no operation to define variables (i.e. you cannot define a function, that is, put the function in a defined variable), and variables can only be passed in through parameters. So what to do? I think, think, think.
Huh, yes, then pass the function as a parameter!
But how can this parameter be filled in with this function?
Can you use a function, take the function to be recursive as an argument, and then pass the function as the first parameter of the function? (The reason why only one parameter can be passed is because there is something called curryization, which probably means to simplify multi-parameter functions to the standard form of nested single-parameter functions)
So I gave it a try. The function described in the previous natural paragraph is denoted by the lambda calculus (λx.xx). What if you put this recursive function with no underlying condition (λfλx.f f x) behind it and add a parameter (λx.x)?
（λx.xx）（λfλx.f f x）（λx.x）
=（λfλx.f f x）（λfλx.f f x）（λx.x）
=（λx.（λfλx.f f x）（λfλx.f f x） x）（λx.x）
=（λfλx.f f x）（λfλx.f f x）（λx.x）
Sure enough, there is no standard form! (It means that recursion is never completed, there are no basic conditions, no wonder)
Try this example again:
(λx.xλx0.λx1.λy.yλx0.λy.x0λx0.λy.yλx0.x0λx1.λx2.λy.yλx1.λy.x1λx1.λy.yλx1.xλg.λh.h(gλf.λx2.x0λg0.λh0.h0(g0f)λu.x2λu.u)λu.x1λu.u) (λf.λx.f(fx))
Forget it, hand it over to the calculator:
=λx.λy.y
That's right! I'm so happy.
I learned a lot of new things during the New Year.

(used google translate,some problems with grammar)

Was the description about the Y combinator correct?

[bh]

@d4s_over_dt4

(i.e. you cannot define a function, that is, put the function in a defined variable)

This is a little wrong. It sounds as if there's something special about functions that makes it impossible to put one in a variable (as was the case in actual programming languages until Lisp came along). You can put a function in a variable; what you can't do is give a variable a name, other than by lambda-binding.

@d4s_over_dt4

and then pass the function as the first parameter of the function? (The reason why only one parameter can be passed is because there is something called curryization, which probably means to simplify multi-parameter functions to the standard form of nested single-parameter functions)

You talk about "the first parameter" and then explain that λ-calculus functions have exactly one argument. Also I'd say "pass the function itself as the..." because there are too many functions floating around for it to be clear as it stands.

And the "because" in the parenthesized sentence gets the causation backward. Church defined λ-calculus around single-argument functions because that's all he needed to prove the halting theorem (and therefore the existence of uncomputable functions). Then Curry invented what came to be called "Currying" as a way to represent multi-argument functions in a way that makes them legal.

@d4s_over_dt4

（λx.xx）（λfλx.f f x）（λx.x）
=（λfλx.f f x）（λfλx.f f x）（λx.x）
=（λx.（λfλx.f f x）（λfλx.f f x） x）（λx.x）
=（λfλx.f f x）（λfλx.f f x）（λx.x）

I think this is correct, but I'm guessing that "write something about the spring festival" isn't an assignment from a math teacher, so of course you realize that your teacher will have no idea what you're talking about. You could explain each step by specifying what expression is being substituted for what variable in what body; that would help a little, but if you really want anyone to understand this, you'd have to explain why simplified models of computation are useful to prove things about functions, and by the way you also have to explain the Busy Beaver function, and why you're confusing things by using ideas from λ-calculus to investigate functions grounded in Turing machines. (E.g., it's because of the specifics of Turing machines that BB(6) is so much bigger than BB(5).)

@d4s_over_dt4

(λx.xλx0.λx1.λy.yλx0.λy.x0λx0.λy.yλx0.x0λx1.λx2.λy.yλx1.λy.x1λx1.λy.yλx1.xλg.λh.h(gλf.λx2.x0λg0.λh0.h0(g0f)λu.x2λu.u)λu.x1λu.u) (λf.λx.f(fx))

I have no idea where this came from! And neither will your teacher.

P.S. The actual Y combinator is a little more complicated than this. You have one that works on functions that already take themself as input; what you want is one that takes the standard one-argument math function, turns it into a two-arg function, and then calls it with itself.

[d4s_over_dt4]

@bh

This is a little wrong. It sounds as if there's something special about functions that makes it impossible to put one in a variable (as was the case in actual programming languages until Lisp came along). You can put a function in a variable; what you can't do is give a variable a name, other than by lambda-binding.

yeah the original file says

which means "so" not "i.e",its a problem on google translate

@bh

@d4s_over_dt4

and then pass the function as the first parameter of the function? (The reason why only one parameter can be passed is because there is something called currying(not curryization dumb translator), which probably means to simplify multi-parameter functions to the standard form of nested single-parameter functions)

You talk about "the first parameter" and then explain that λ-calculus functions have exactly one argument. Also I'd say "pass the function itself as the..." because there are too many functions floating around for it to be clear as it stands.

translates to "How about putting the function as a parameter?But,how can I put the function itsself into its own parameter?"

@bh

I think this is correct, but I'm guessing that "write something about the spring festival" isn't an assignment from a math teacher, so of course you realize that your teacher will have no idea what you're talking about. You could explain each step by specifying what expression is being substituted for what variable in what body; that would help a little, but if you really want anyone to understand this, you'd have to explain why simplified models of computation are useful to prove things about functions,

I'm very,very,very bad at writing essays.
Because of that,my teachers expect bad essays from me.
Last time,I wrote about a long and very hard math problem(including arccosines,complex exponentiation,arcsine logarithmic formulation,hard equations and a lot more) and my teacher said "Very good!" meaning "Finally you learned to write long enough to satisfy the constraints listed on the homework description!"
So yeah I was just using this stuff to stuff up word count.But I don't want to write false stuff even if no one looks at it,so I am asking this.

@bh

and why you're confusing things by using ideas from λ-calculus to investigate functions grounded in Turing machines. (E.g., it's because of the specifics of Turing machines that BB(6) is so much bigger than BB(5).)

Whaaa?
Did you mispost this here instead of that BB thread?

@bh

I have no idea where this came from! And neither will your teacher.

well,I can tell you its from
(λf.f f)(λf.λx.pair ⊥(f(pred x))(isZero(x)))(succ(succ ⊥))
meaning

((x)=>{
if x==0:
return false;
else:
return this script(x-1)
})(2)

@bh

P.S. The actual Y combinator is a little more complicated than this. You have one that works on functions that already take themself as input; what you want is one that takes the standard one-argument math function, turns it into a two-arg function, and then calls it with itself.

(Yeah that's what I was looking for by posting this on the forum.)
Ok...lemme see if I can try making it...
(\f.(\x.xx)(\x.f(xx))?

[bh]

@d4s_over_dt4

I'm very,very,very bad at writing essays.

If you worked at it, you could learn to write essays about mathematics that laypeople could actually understand. You should read some good math-for-normal-people books, starting with Gödel, Escher, Bach.

@d4s_over_dt4

which means "so" not "i.e",its a problem on google translate

?? That doesn't change the issue, which is that it's wrong to say you can't put a function in a variable. What you can't do is give a variable a name other than by lambda-binding it.

@d4s_over_dt4

(\f.(\x.xx)(\x.f(xx))?

I dunno, ask Wikipedia.

@d4s_over_dt4

Did you mispost this here instead of that BB thread?

Oops!

[d4s_over_dt4]

@bh

If you worked at it, you could learn to write essays about mathematics that laypeople could actually understand. You should read some good math-for-normal-people books, starting with Gödel, Escher, Bach.

Oh ok.
(my perception of "laypeople" is people like me,but i had a lot of communication problems doing so,so its weird)

@bh

?? That doesn't change the issue, which is that it's wrong to say you can't put a function in a variable. What you can't do is give a variable a name other than by lambda-binding it.

Oh right.I did not quote exactly the mistranslated paragraph.

"In lambda calculus,there is no operation of defining variables(that means you cannot define functions in a sense of putting a function into a defined variable)variables are only definable by parameter passing."
I was thinking about the

button when writing that.
Maybe "defining variables" isn't the correct term for giving variables names/memory pointers.

@bh

Oops!

(was that a sarcasm or a joke?(i wanted to mean "do you want to mean 'hey you no picking problems on teachers' or 'oops i did post at wrong place,lol'?" in the preceding sentence))

@bh

I dunno, ask Wikipedia.

ok

not helpful
maybe ill try another source instead of bing

[d4s_over_dt4]

@bh

I dunno, ask Wikipedia.

it means "the y combinator outputs a bird that its input is fond of" if you have read the mocking bird book
Still no definite answer and i dont think that my combinator looks like that

\t (\f.ff)(\f.t(\x.ffx))

[bh]

@d4s_over_dt4

my perception of "laypeople" is people like me

You won't know until grad school whether you're a real mathematician (I'm not one), but you're hardly a layperson!

Are you autistic? I mean, officially, not just in your own opinion. And if so, are you getting good therapy for it?

@d4s_over_dt4

"In lambda calculus,there is no operation of defining variables(that means you cannot define functions in a sense of putting a function into a defined variable)variables are only definable by parameter passing."

Yeah, around 50 years ago I got yelled at by a real computer scientist (I'm not one of those either) for saying something in Computer Science Logo Style suggesting that variables are defined in environments. The Official Right Thing is that there are two separate operations regarding variables:

name ———➞ variable ———➞ value

So variables don't have names; names are bound to variables in environments, whether by global binding or by λ binding. Independently, variables have values, which they get by assignment, which can happen simultaneously with λ binding or with a conventional assignment statement.

If you have to say something like var v or int v before you can say v ← 5 in your programming language, then it is exposing to you this distinction. If you can assign a value to the variable without declaring it first, your language is doing you the favor of automatic declaration.

So I stopped talking about binding names to values, but I never really understood why it mattered until we wanted to let users implement the FOR block, which lets you change the name of the loop variable in the context in which FOR is used without changing its name inside the body of FOR itself, i.e., until we implemented upvars. An upvar is bound to two different names in two different environments, but it's the same variable: giving it a new value in one environment also changes the value in the other environment.

@d4s_over_dt4

(was that a sarcasm or a joke?(i wanted to mean "do you want to mean 'hey you no picking problems on teachers' or 'oops i did post at wrong place,lol'?" in the preceding sentence))

oops i did post in the wrong place.

@d4s_over_dt4

If you click on that link instead of the one the browser suggests for you, you'll get to a page on which you can disambiguate the computer science meaning from the company.

[d4s_over_dt4]

@bh

but you're hardly a layperson!

No wonder the school people don't know what I'm saying when I chat about lambda calculus!

@bh

Are you autistic? I mean, officially

nope

@bh

I'm not one of those either

I think you are

@bh

The Official Right Thing is that there are two separate operations regarding variables:

name ———➞ variable ———➞ value

Okay,I'll change that in my essay

@bh

An upvar is bound to two different names in two different environments, but it's the same variable: giving it a new value in one environment also changes the value in the other environment.

Never thought it in that way!Nice!

@bh

If you click on that link instead of the one the browser suggests for you, you'll get to a page on which you can disambiguate the computer science meaning from the company.

Maybe my admin blocks wikipedia too

[bh]

@d4s_over_dt4

I think you are

Well, thank you, but I'm really not. I'm a decent CS student, but I've never done any original CS. My work has been in CS education; that's really my field.

[d4s_over_dt4]

@bh

CS education

Oh.
I thought that teachers were all mathematicians.

[bh]

@d4s_over_dt4

I thought that teachers were all mathematicians.

C'mon, you're joking, right? Is your history teacher a mathematician?

[d4s_over_dt4]

@bh

right

...yeah