14,639 reputation
3477
bio website andrej.com
location Slovenia
age 44
visits member for 4 years, 11 months
seen 16 hours 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.


17h
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.
22h
revised Why does Coq have Prop?
added 1063 characters in body
22h
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.
1d
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.
Jul
16
comment Computation of reals: floating point vs TTE vs domain theory vs etc
Any implementation which uses streams of digits, or anything else that has a fixed rate of convergence, is handicapped from the outset in that it will converge too slowly. Also, stream-based implementations tend to force you to calculate all the previous approxmations to get the next one, which is also a design mistake as well.
Jul
16
awarded  Nice Answer
Jul
16
comment Computation of reals: floating point vs TTE vs domain theory vs etc
Good point. In fact, it's difficult to change the floating point format for the same reason: hardware manufacturers see no point in it so they don't do it. But recently there's been new motivation: by improving FP format they can save electricity. Let's hope for the best.
Jul
16
comment Computation of reals: floating point vs TTE vs domain theory vs etc
Hmm, I don't think so. Think of exact real arithmetic as interval arithmetic that self-adjusts intermediate precision to achieve the desired output precision.
Jul
16
revised Computation of reals: floating point vs TTE vs domain theory vs etc
added 110 characters in body
Jul
16
answered Computation of reals: floating point vs TTE vs domain theory vs etc
Jul
12
awarded  Nice Answer
Jul
8
comment Can all linear lambda calculi be linearity checked syntactically?
Are you asking whether the linear $\lambda$-calculus can be checked by checking the intuitionistic $\lambda$-calculus types and then checking syntactically the linearity condition?
Jul
8
comment Can all linear lambda calculi be linearity checked syntactically?
I do not understand the question.
Jul
8
revised Can all linear lambda calculi be linearity checked syntactically?
added 10 characters in body
Jul
4
revised Information-theoretic Diffie-Hellman
Fix the world's worst abuse of LaTeX ever.
Jul
2
comment Smallest possible universal combinator
Maybe this is of interest: wolframscience.com/nksonline/page-1123a-text?firstview=1
Jun
12
comment Why do non-proper types have no terms?
Type operators are clearly not types, unless you stretch the meaning of "type" beyond anything reasonable. They are functions from types to types. Why you call them improper types in your class I do not know.