12,533 reputation
3066
bio website andrej.com
location Slovenia
age 43
visits member for 4 years, 3 months
seen 3 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.


2d
comment Can typed lambda calculi express *all* algorithms below a given complexity?
The Ackermann function can be expressed in the calculus of constructions, so it can't be right that that one is just doubly exponential.
2d
comment Is there a purely functional vector with O(1) access to the front and back but O(log n) concatenation?
I am just scrtaching the back of my skull, but where do finger trees stand on this issue?
2d
comment Equality of decidable proofs?
By the way, just one more comment: you should look for an inhabited propostion $P$ such that its equality is not decidable. For if $P$ is decidable and has non-decidable equality, then $P$ holds, since $\lnot P$ implies that $P$ has decidable equality.
Dec
13
comment Equality of decidable proofs?
What's your point?
Dec
13
awarded  Enlightened
Dec
13
awarded  Nice Answer
Dec
12
comment Equality of decidable proofs?
The product rules are weird if we do that because they cause $\mathsf{Set}$ to be impredicative (but fortunately that is consistent). Let's ignore the inductive stuff, that'll be complicated and there is the pesky "singleton elimination". Hmm. Maybe there is a simpler way to see that there are elements in Prop for which we cannot establish decidability of equality.
Dec
12
comment Equality of decidable proofs?
Actually, since we're doing this for Coq, we should probably consider $\mathsf{Prop} = \mathsf{Set}$. If you look at the rules (coq.inria.fr/doc/Reference-Manual006.html) and change $\mathsf{Prop}$ to $\mathsf{Set}$ everything, does anything strange happen, or do you just get Coq without $\mathsf{Prop}$?
Dec
12
comment Where can I find the proof of the theorem and what is the computational complexity of the computably isomorphic map?
I am not sure. You could have a silly representation of reals. Pick an arbitrary computable subset $S \subseteq \mathbb{Q}$ of rationals. I could define that a real $x$ is encoded by a sequence $(q_n, b_n)_n$ where $(q_n)_n$ is a sequence of rationals which converge fast to $x$, and $b_n \in \{0,1\}$ is 1 iff $q_n \in S$. Now to convert from the usual representation of reals to this one, you need to calculate whether $q_n \in S$, and the complexity of that can be arbitrarily high. So I very much doubt you get just polytime.
Dec
12
comment Equality of decidable proofs?
Still not quite right, because in Coq we cannot show that functional equivalence is undecidable. The statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is what Martin Escardo calls a constructive taboo: it can be neither proved nor disproved in Coq. So the correct argument is: if $\mathtt{Prop} = \mathtt{Type}_1$ then $\mathbb{N} \to \mathbb{N}$ is a proposition, and the statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is not provable. (Whereas you said: and the statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is false).
Dec
12
comment Expressive enough to talk about Turing machines / Peano arithmetic?
You said "when we build a TM that decides PA sentences". I just pointed out there is no such TM, so what you are saying sounds very odd. You should react by explicitly addressing the fact that there is no TM which decides PA sentences: why did you say "when we build one"? Did you think there was one? Or what?
Dec
12
comment Expressive enough to talk about Turing machines / Peano arithmetic?
There is no TM that decides PA sentences.
Dec
11
comment Expressive enough to talk about Turing machines / Peano arithmetic?
Which two notions?
Dec
11
comment Equality of decidable proofs?
Sure, we have to tack an index onto $\mathtt{Type}$. The point for @AdamBarak to understand is this: because $\mathtt{Prop} = \mathtt{Type}_1$ does not lead to any contradiction in Coq, we can show that something cannot be done in Coq by showing that it would lead to a contradiction if we also had $\mathtt{Prop} = \mathtt{Type}_1$.
Dec
11
answered Where can I find the proof of the theorem and what is the computational complexity of the computably isomorphic map?
Dec
11
comment Expressive enough to talk about Turing machines / Peano arithmetic?
I do not really understand the question, and if I did, I would probably think it's not research-level. Are you just asking about Gödel encoding of Turing machines, i.e., how to encode Turing machines and their workings using numbers and arithmetical operations?
Dec
11
comment Equality of decidable proofs?
There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there?
Dec
11
answered Equality of decidable proofs?
Dec
11
comment Equality of decidable proofs?
What you wrote does not make sense. If $P$ is a proposition then $p : P$ is a proof, and you cannot form $p \lor \lnot p$. Did you mean your hypothesis to be $P \lor \lnot P$ instead of $p \lor \lnot p$, i.e., "$P$ is decidable"?
Dec
7
comment Decidability of sets of free variables in Lambda Calculus
It is blatantly obvious that $\mathcal{F}_1$ is computable (decidable). As for $\mathcal{F}_2$, it is certainly computably enumerable, and I would bet it is not computable.