14,739 reputation
3578
bio website andrej.com
location Slovenia
age 44
visits member for 5 years
seen 1 hour ago

I am a professional mathematician and theoretical computer scientist (what is the difference?) . My area of work is a mix of logic, semantics, programming languages, category theory, constructive mathematics and computability.


2d
comment Is `sort` typeable on elementary afine logic?
Maybe these comments can be turned into an answer?
Aug
29
comment Is `sort` typeable on elementary afine logic?
And another question (the term is too big for me to stare at it): does any bound variable ever get mentioned more than once? Hmm, b is like that is it not?
Aug
29
comment Is `sort` typeable on elementary afine logic?
Does it have an "ordinary" type? What happens if you plug it into Haskell?
Aug
28
awarded  Yearling
Aug
25
comment Problem with the Inductive Types and recursors in LEAN
This is not the appropriate forum to ask basic questions about a theorem prover. They don't seem to have a mailing list for Lean, but surely you can open issues on Github. They'll quickly figure out they have a community and will create a mailing list.
Aug
15
awarded  Nice Answer
Aug
5
comment Rendering of type-level computation
I simply understood @MartinBerger 's rule to implicitly require that $\alpha \equiv_{\mathrm{type}} \beta$ implies that $\alpha$ and $\beta$ are types. In general, I would always expect that we impose whatever conditions are necessary to avoid bringing in garbage.
Aug
5
comment Rendering of type-level computation
Should the top left $N$ in the first rule be $M$?
Aug
5
comment Rendering of type-level computation
Interesting, but would this work for arbitrary $\Gamma$ and $\Delta$? Can we write down reasonable rules for $\equiv_{\mathrm{type}}$ with such double sided contexts? (Transitivity looks tricky as it would bring in three contexts.) Isn't there some sort of a chat system around here?
Aug
4
comment Rendering of type-level computation
Now that I look at it more closely, you need to have $M \equiv_{\mathrm{Type}} N$ in a context. But which context, $\Gamma$ or $\Delta$? Same goes for $\alpha \equiv \beta$. That might be the reason for aversion to the rule: it forces you to break symmetry in an arbitrary fashion.
Aug
4
comment Rendering of type-level computation
Probably nothing, since it looks admissible :-)
Aug
3
comment Rendering of type-level computation
Well, I wouldn't try to put your general rule in. Instead I would try to prove that it is admissible.
Aug
3
comment Rendering of type-level computation
Are we doing "theory" here or are we actually thinking about how compilers work? Can you explain a bit what you're after? None of the rules you wrote would actually be used directly in a compiler.
Jul
29
comment Why does Coq have Prop?
As far as I know nobody can really tell how to extract anything from $(-1)$-types. It's clear that they contain some computational content, but not what this might be.
Jul
29
revised Why does Coq have Prop?
added 1063 characters in body
Jul
29
comment Why does Coq have Prop?
You do not have the information "I want $k$". That is an extra assumption, and obviously once they tell you which particular result they want, you can just optimize away dead code. Actually, I thought of a better answer: it is a design question which things to put in $\mathsf{Prop}$. You need to know what the user wants, and he tells you what he wants by using $\mathsf{Prop}$. It is easy to come up with examples where there are several options. I will add one to my answer.
Jul
28
comment Why does Coq have Prop?
Yes, the sorting example presented in my answer. How can you tell that verify is useless?
Jul
26
comment Why does Coq have Prop?
The extracted code produces higher-order functions. A code optimizer cannot tell whether these will be used in a useful way. So yes, unless there is some mechanism to indicate which parts of code are "useless", you can't tell.
Jul
26
awarded  Nice Answer
Jul
19
comment Computation of reals: floating point vs TTE vs domain theory vs etc
An alternative is to use intervals of some sort as an approximation and a Reader monad for the output (or input) precision. You can then start your computation on and desired output (or input) precision without waiting for the stream to get there. iRRAM does something like this, for instance.