æʃliŋ, ring racers purropawgandist @aescling@cat.family

@vaporeon_ have a good Rest

@packetcat nice

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

do i know type theory? i dunno, but i theorize that you’re my type, babe

the joy of watching introductory videos about dependently typed purrogramming languages like Idris is you will inevitably encounter rather thorough discussions about the succ

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

@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

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

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

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

@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 does vaporeon know about the lambda calculus

mornyawn btw . also @clock, what time is it

@vaporeon_ @amy old enough to drink in the united states

@wallhackio (the short answer is that it’s a template fur writing little ad hoc purrograms that do special cased versions of what your wordle cheating purrogram does)

j was insistent on calling the metal sonic robots in the post-credit scene “mecha sonic”. and, well, if you know, you know lol

@wallhackio (adjust the level of for loop nesting as needed)

@wallhackio if i typed, say, "${i}${j}${k}ed"where the [...]is, this would generate all strings of letters ending in ED, and filter those out to those in the default dictionary used hunspell(1), which in my case is an english language one, because it’s all i installed

in general, i can specify the known constraints of a word (checking letters, known wordle letters, etc, what the pawsible letters in the blanks might be in a game like wordle) and generate a list of valid english words satisfying those constraints