14,030 reputation
3472
bio website andrej.com
location Slovenia
age 44
visits member for 4 years, 9 months
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.


May
20
comment Categorical way of factoring out points
It's not clear to me at all why you need categories, and in any case your definition of the category is not clear, how does composition work, where do identity morphisms come from? Also, I think I do not understand the terminology. If the objects of your category are literals, then how can an implication $a_i \leftarrow L_i$ be a morhism when $L_i$ is a conjunction of several literals? At best this could be a multicategory, or there's something basic I misunderstand here.
May
20
comment Is there a lambda function that evaluates any other lambda function with any input expression?
Or $\lambda f . f$ for that matter...
May
18
comment Actual practical example of a prefix-free Turing-complete language
@EmilJeřábek: you're right about adding digits in an arbitrary way. But we can save the day and require that every computable way of adding more digits to a string eventually produces a valid program (because König's lemma fails by Tarski's unbouded computable tree that has no computable infinite path).
May
15
comment Categorical way of factoring out points
Could you say a bit more about how your categorical semantics works so far. What is $\Pi$ in the semantics, an object? Why do you need categories anyway? Can't you just do everything with sets?
May
15
comment Categorical way of factoring out points
Rather than asking for something in category theory, it might be better to explain what sort of semantics you're looking for.
May
15
comment Categorical way of factoring out points
Given a category $\mathcal{C}$ and an object $X$ in it, you can always "take out" the object $X$ by forming the full subcategory on all the objects except $X$. You could also throw out all isomorphic copies of $X$. But I am guessing this is not what you want.
May
15
comment Categorical way of factoring out points
Voting to close in order to motivate the author of the question to ask his question in such a way that we will understand him.
May
15
comment Is there any research on approximation of reals with computable numbers
There's definitely research in "how computable" a real number is (for instance, maybe we can only approximate it computably from below), and there is definitely a notion of computational complexity for real numbers. But your complexity looks more like Kolmogorov complexity, and I have not really heard of anything like that (but it's not my area either).
May
14
comment Is there any research on approximation of reals with computable numbers
It's not clear to me what preciely you're asking here. Is there any reseearch? Well, did you check the usual places, like MathSciNet? If you can prove these results, you could present them to the relevant communities and see what they say (for instance Computability in Europe and Computability and Complexity in Analysis would be two conferences where the topic would be deemed relevant).
May
6
awarded  Nice Answer
May
3
awarded  Necromancer
May
3
awarded  Excavator
May
3
comment Are runtime bounds in P decidable? (answer: no)
In view of @DavidG link the title of the question is misleading. It is possible to decide linear running time.
May
3
answered Are runtime bounds in P decidable? (answer: no)
May
3
revised To what extent can an algorithm predict the time complexity an arbitrary input program?
Continuing the crusade to erradicate useless or improper uses of "provably" in computer science.
Apr
28
comment Is there a typed lambda calculus which is consistent and Turing complete?
It's hard to be more precise here because the question is not precise.
Apr
27
comment Is there a typed lambda calculus which is consistent and Turing complete?
Well, it doesn't exactly follow. There are probably situations in which you could inhabit every type by fiat, without having any diverging terms (in $\lambda$-calculus we should probably say "normalizing" instead of "divirging"). But in nature the typical reason that all types are inhabited is existence of a fixed-point operator, which leads to divergent terms.
Apr
27
awarded  lambda-calculus
Apr
26
comment Is there a typed lambda calculus which is consistent and Turing complete?
In my proof you can read "programming language" as "some sort of $\lambda$-calculus". Your "consistency" requirement translates to "the programming language is total" (for if you have diverging terms then the calculus is "inconsistent" in the sense that all types are inhabited). The theorem says that such a language cannot simulate itself, but "simulate itself" is a computable map, therefore no such language can be Turing-complete.
Apr
26
comment Is there a typed lambda calculus which is consistent and Turing complete?
This answer has a theorem which says you can't have any sort of calculus that is both Turing-complete and total.