Sacchini uses it but doesn't define it

how do I define WHNF in words. who has done it before that I can copy from

I'll do it during office hours if no one arrives, although I'm p sure ppl will arrive seeing as the assignment is due next week

I have the sudden urge to write a post about Girard's paradox instead of doing any actual work

I give up. I give up! I'm not doing this

In this way, one finds a term of type ⊥ in λU- that uses modus ponens 12 times. It is of the form [P Q], where P is a normal term of type "Ω is not well-founded" and Q is a normal term of type "Ω is well-founded".

please just tell me what the term is. I can't figure it out

I am once again trying to decipher Girard's paradox

Yeah that sounds right: if you have strong impredicative pairs, you can stick a bigger thing and pretend it's a Prop, and then later on pop the thing out, which is the same as being able to eliminate things in Prop to arbitrary universes, which is the same as Type in Type

Thinking about this again. Type: Type gives you Girard's paradox, and so does arbitrary large elimination of something in an impredicative universe, since that lets you squish something from a bigger universe to a smaller universe, which is basically the effect of Type: Type
You can't have negative datatypes because you can prove false pretty easily, and you can't have non-strictly-positive datatypes with impredicativity because... why? I did it once in Coq but I don't understand what it is I did
And finally I don't know you can't have strong impredicative pairs but I suspect it's along the same lines as large elimination of impredicative universes

You can't have two impredicative universes. You can't have Type: Type. You can't have impredicative strong pairs. You can't have large elimination of an impredicative universe. You can't have positive datatypes when you have an impredicative universe. You can't this, you can't that. When will it end?

I'm sure I looked it up in Luo's paper last time, or maybe it was Coquand's, but I don't have anything written down anywhere

Every now and then I wonder why I can't have impredicative pairs and then I wonder why I didn't figure it out the last time I wondered it

Absolutely unfair. If I were me doing work wouldn't make me tired. Completely ridiculous

unfortunately I've gotten work done which means I'm tired now

Trying to find the correct LaTeX file to compile like

re: shop talk

I've had enough of this. This is the final straw. I cannot keep forgetting what breaks subject reduction and why I am going to write ALL of it down

shop talk

My figures have straight up disappeared

What if I went into the lab just to play Minecraft

I didn't think I'd get much done at home today anyway so might as well get nothing done with everyone else

Show older

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