wren romano
  • Member for 11 years, 3 months
  • Last seen more than 4 years ago
Is the Chomsky-hierarchy outdated?
28 votes

In short: yes. More particularly: Chomsky was one of the first to formalize a hierarchy relating languages, grammars, and automata. This insight is still very relevant and is taught in all intro ...

View answer
A category of NP-complete problems?
16 votes

It's possible to categorify lots of things, but that doesn't necessarily mean they're interesting categories. So the answer to "does it make sense" depends on how you mean. As for predicting whether ...

View answer
What should a proof of correctness for a typechecker actually be proving?
5 votes

There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;) One half of this question is proving that your type ...

View answer
What is the difference between proofs and programs (or between propositions and types)?
4 votes

If you accept the Curry–Howard correspondence then the question is mainly a philosophical one. "Are proofs and programs different? Of course. How? Well, we call proofs 'proofs' and we call programs '...

View answer
Reader, Writer monads
4 votes

Consider the adjunction $\langle F,G,\epsilon,\eta \rangle$. For every such adjunction we have a monad $\langle GF, \eta, G\epsilon F\rangle$ and also a comonad $\langle FG, \epsilon, F\eta G\rangle$. ...

View answer
PiSigma: why does 'unfold' bind a variable?
Accepted answer
1 votes

I don't think there's any magic/necessary reason. IMO, it's written that way to make it more straightforwardly obvious that unfold is an analytic/checking elimination rule; just like why split is ...

View answer