You can use Internet to talk to a Vaporeon. You probably don't want to, though.

@wallhackio Vaporeon systems are at 5% capacity. Despite that, they are requesting mathematics infodump from Clodsire.

@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

Follow

@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

worse re: sorry 

@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) :blobfacepalm:

The repeated function application does look familiar!

Sign in to participate in the conversation
📟🐱 GlitchCat

A small, community‐oriented Mastodon‐compatible Fediverse (GlitchSoc) instance managed as a joint venture between the cat and KIBI families.