10,879 reputation
2456
bio website andrej.com
location Slovenia
age 43
visits member for 3 years, 11 months
seen yesterday

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.


Jul
19
comment Does hyper-computational power of infinite time Turing machines also require infinite memory?
It's an order-theoretic problem, not one of cardinality. Both $\omega$ and $\omega + \omega$ have the same size, namely $\aleph_0$, but one has a limit point in the middle. Presumably you can't get rid of it with physics. To compute for $\omega + \omega$ steps you'd have to somehow fly into a black hole, emerge from it, and then fly into it again. Or something like that.
Jul
18
comment Does hyper-computational power of infinite time Turing machines also require infinite memory?
Only if you can get black holes to let you compute beyond $\omega$ steps. I am aware of theories that show how you get infinite time, but infinitely many infinite times? That would require some serious black hole engineering.
Jul
18
answered Does hyper-computational power of infinite time Turing machines also require infinite memory?
Jul
8
comment How are these statements about CTT reconcilable?
Judgments are not about being true or false. They are basic "constructors" from which we build derivations. For instance, you can have a judgment which tells you how to build an ordered pair. What's "true" about that?
Jul
8
comment How are these statements about CTT reconcilable?
It is also very important to note that a judgment is "top level", it is a basic building block of the formal system, whereas a proposition is something that lives "inside" type theory. It is an object in the theory.
Jul
7
comment How are these statements about CTT reconcilable?
Before answering this, do you understand the difference between a judgment and a proposition in the sense of type theory? That may be the first stumbling block.
Jul
3
comment What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?
In that case you should understand the text and then do it in whatever proof assistant and/or theorem prover seems to best fit your purpose.
Jul
3
comment What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?
Is there historic interest in exactly following the book, or could you just extract the gist of it (the basic setup and the axioms) and formalize the theory in an available modern system?
Jul
2
comment Categories a computer scientist should know about
I dunno. There are CS students our there who learnt algebraic topology from a computational point of view in one semester. Look up things like "persistent homology".
Jul
2
comment Categories a computer scientist should know about
You could try something completely different to get some feel for the other 90% of category theory. For instance, you could have a look at the basic setup of algebraic topology. That would give you some perspective.
Jun
29
comment What is known about reduction by “$P_1$ interprets $P_2$” for generalized programming languages?
For starters, $P$ should be a computable enumerable set, not computable one. I am also highly tempted to state that all primitive recursive functions should be implemented, so the lowest level should be the primitive recursive functions. If not, then at least we should include conditional statements.
Jun
29
comment What is known about reduction by “$P_1$ interprets $P_2$” for generalized programming languages?
Also, I think my definition of "inteprets" is ad hoc and not very good.
Jun
29
comment What is known about reduction by “$P_1$ interprets $P_2$” for generalized programming languages?
I'd look at John Longley's theory of applicative morphisms.
Jun
29
revised Isomorphism between algebraic data-types
added 78 characters in body
Jun
29
revised Isomorphism between algebraic data-types
deleted 69 characters in body
Jun
29
comment Isomorphism between algebraic data-types
Ah, I see. You're right, it suffices to find one counter-examples for $A$'s.
Jun
29
answered Isomorphism between algebraic data-types
Jun
29
comment Isomorphism between algebraic data-types
This reasoning is flawed, you're applying it to the type constructors instead of the fixed points of those type constructors. By your reasoning: let $T_1(X) = 1 + X$ and $T_2(X) = 1 + 1 + X$. Then $T_1(\mathtt{empty}) = 1 \not\cong 1 + 1 = T_2(\mathtt{empty})$, whereas the inductive types $N_1 = T_1(N_1)$ and $N_2 = T_2(N_2)$ are isomorphic because they are both the natural numbers.
Jun
29
comment Isomorphism between algebraic data-types
Do you mean inductive types, or are infinite trees allowed (like in Haskell, which does not have inductive types)? Also, what do you mean by "isomorphic"? If you mean "isomorphic as sets of values" then the answer is obviously "yes, since they have the same cardinalitity". Do you mean something else?
Jun
27
revised A total language that only a Turing complete language can interpret
added 193 characters in body