@vaporeon_ would you accept a vaporeon on a roomba

@wallhackio OK, especially since we're going to sleep soon

But I do want to listen to Clodsire talk about maths and improve my maths knowledge

@vaporeon_ https://youtube.com/clip/UgkxcIYmOUG36XxOaxf2Su0lE28kkk3weIAV?si=Kh1Ds7uYKtCuVECR

@wallhackio Amazing

@vaporeon_ @wallhackio does vaporeon know about the lambda calculus

@aescling @wallhackio Vaguely... It was some way of writing down function, I think... Someone of y'all has talked to me about it before, but unfortunately, my memory is very bad.

@vaporeon_ @wallhackio the most impurrtant rule of the lambda calculus is the beta substitution rule, which is a fancy way of saying that when applying a function to an argument, you substitute all instances of the parameterized value with the argument. you know, like in a function

so, say, if you had the function λx.x + 2 (more or less equivalent to f(x) = x + 2, then if you applied the function to, say, 3 (which you might write like (λx.x + 2) 3, basically the same as writing f(3)), then you can beta-substitute and simplify the string to 3 + 2

there are, like, two other rules in the lambda calculus (one, eta-equivalence is just that λx.x + 2 is definitionally exactly equivalent to λy.y + 2)

i realize this is almost condescendingly simple when i explain it like this, but the absol-utely mindbending thing about the lambda calculus is that it’s already turing-complete. the expurressivity is way higher than you would ever expect; it’s thoroughly pawsible to define numbers and arithmetic opurrations in pure lambda calculus, fur example

hell, it’s pawsible to cheat your way into introducing something almost like general recursion into the language, using some rather clever hacking, without needing any change to the fundamental syntax at all

just about all functional purrogramming languages can be accurately described as having the semantics of a (typed) lambda calculus (which requires some extra rules, but purrevents all sorts of logical inconsistencies from being expurressible) with extra bells and whistles

@vaporeon_ @wallhackio i hope this was an at least somewhat adequate replacement fur Clodsire Math

@aescling @wallhackio Yeah... Currently looking at the Wikipedia for the Church encoding, but unable to process it due to sleep deprivation...

We did a perhaps somewhat similar exercise in our functional programming course years ago, when we defined a natural number to be either 0, or the successor of another natural number. So 1 would be Succ Zero, and 2 would be Succ Succ Zero, and so on

@vaporeon_ @wallhackio ah, yes, i love peano arithmetic

@aescling @wallhackio Piano arithmetic 🎹

@vaporeon_ @wallhackio mathematicians be like: “i’m gonna Succ this Peano”

@aescling @wallhackio So the lambda calculus does it differently? I will look at it after I have gotten sleep

@vaporeon_ @wallhackio no, the typical church encoded natural number is deliberately isometric to peano arithmetic. if you’re vaguely familiar with peano numbers then you should at least be able to get what the idea it’s going fur is

@aescling @wallhackio

I'm stupid and was looking at the wrong chapter of the Wikipedia page (the chapter with the booleans)

The repeated function application does look familiar!

@vaporeon_ @wallhackio i didn’t say “substitution” smh smh smh

@vaporeon_ anyway if you would like some mathematical blabbery I did blather on quite a bit of math on lady's forum like a year ago. Let me know if you are able to access the following link:
https://forum.ladys.computer/viewtopic.php?t=47

@wallhackio Can't:

The board requires you to be registered and logged in to view this forum.

What is the forum about?

@vaporeon_ it's a little forum one of my friends made where like 10 of us talk about our hyperfixations

@wallhackio @vaporeon_ you could surely get an invite if you’d like one

@vaporeon_ this specific topic is a thread where I infodumped mathematics I had made to analyze Battlefield 1, a first person shooter i get obsessed with once ever three or so years