Show newer

call/cc? i have anxiety, i prefer texting/cc

I never want to see a wojak again in my lifespan. I would give so much to see wojaks exterminated from the timeline

wolf bit my laptop on the top right corner and i had to remove her before she broke the screen

that was terrifying

"The two most common ways of proving statements in data structure analysis are proof by induction and proof by contradiction (and occasionally proof by intimidation, used by professors only)."

reminder not to do axiom of choice or you'll get hit by a car on 3rd

Exercise 1.7.

Let A and B be m by n and n by m matrices, respectively. Tell me why my wife left me

re: "abstract" ""interpretation"" 

so basically, rather than directly saying "terminate here", we actually get our full program state space, and then use that as the evaluator? I guess.

and finally we are decidable.

Show thread

re: "abstract" ""interpretation"" 

the problem with this is that while we now have a finite state space, the interpreter isn't aware of that, and it'll just keep looping when it reaches the same state. so like, in a conventional setting, we'd make a hash-set or something of seen states and terminate when we get in a loop

here, we define configurations as a triple <exp, env, store>, and then we introduce a cache from configurations to <value, store> pairs. we also store evaluation results in a cache, which is "more defined" than the input cache

then, the least fixed point of an evaluator transforming our in-cache to our out-cache is a sound approximation. of our approximation.

yea.

Show thread

re: "abstract" ""interpretation"" 

so in order to get a first step towards decidability, we finitize closures by finitizing the set of addresses. we modify stores similarly to the AAM recipe, where we implement stores with a join and a nondeterministic choice.

if we implement with the variable name as the address, we can get a 0CFA-like abstraction. so, if we have the code:

(let ([f (lambda (x) x)])
(f 1)
(f 2))

we get '(1 2) as our result, since the fs aren't distinguished.

Show thread

re: "abstract" ""interpretation"" 

so the reason this was defined so weird (it requires Y or an equivalent fix-point to be run) is so you can do deep introspection. here, they're using that fact to implement a tracing semantics. in addition, this involves "dead" subexpressions, too.

so now you can collect "other stuff" with your result. this is probably really similar to what I want.

Show thread

re: "abstract" ""interpretation"" 

back to this.

so they start off with the stack ReaderT FailT StateT Identity. then they have a regular interpreter. for now, they're always returning fresh addresses, with no real abstraction behind it.

the entrypoint is just running the monad transformer stack. voila.

Show thread

i wonder how my life would be different if i majored in computational linguistics instead

fucking decidability. how does it work

hazel :ms_asleep: boosted

if i was a supreme court justice i would simply make good rulings instead of bad ones

i am currently discussing the viability of "pineapple sweats" as well as discussing a math professor who uses arch linux while watching a carpet cleaning video in my living room

Show thread

does everyone else not have the roof of their mouth burn for a full hour after you eat a pineapple? is this just me?

Show thread

just had an agonizing conversation with my roommates [and betty] in which i have discovered that the "pineapple sweats" are not a thing and in fact i am just allergic to pineapples

Show older

hazel :ms_asleep:'s choices:

types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.