12,933 reputation
3267
bio website andrej.com
location Slovenia
age 43
visits member for 4 years, 5 months
seen 19 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
answered Simple example of halting-unprovable Turing machine
Jan
11
comment What is the formalism behind ?- (query) in Prolog?
Ah, sorry about that. A query is a goal that Prolog tries to solve. It is the equivalent of a program to be executed in Java, or a query in SQL. If you want queries in Java you'll have to implement something: a database, a search engine. There are languages which combine proof search with other aspects of computation, for instance $\lambda$-prolog.
Jan
10
comment Type theoretic equivalent of isomorphism class
Yeah, what's wrong with @cody's suggestion?
Jan
10
answered What is the formalism behind ?- (query) in Prolog?
Jan
7
awarded  Enlightened
Jan
3
awarded  Good Answer
Jan
3
awarded  Nice Answer
Jan
2
comment Representation as sum of unit fractions: primitive recursive?
It is worth mentioning that these are Egyptian fractions: en.wikipedia.org/wiki/Egyptian_fraction
Dec
29
comment How Univalence can be used for proofs about algorithm correctness
It's always good to have some hopes.
Dec
28
comment Formalizing Homotopy Type theory in Idris
Idris is oriented more heavily towards programming. One thing that would worry me is whether it has the equivalent of Agda postulate or Coq Axiom. If it does, how does it manage to compute with it (it's a compiled language)? The point is that the univalence axiom needs to be postulateded.
Dec
27
comment Law of excluded middle in MLTT
I mean the computational interpretation of classical logic whereby we interpret Perice's law using callcc.
Dec
27
comment Why has hypercomputation research died down?
There weren't any black holes nearby to send a Turing machine into.
Dec
26
comment Law of excluded middle in MLTT
MLTT can be interpreted in classical set theory, therefore it is consistent to add excluded middle to it.
Dec
26
comment Law of excluded middle in MLTT
Classical logic can have proof objects.
Dec
23
revised How Univalence can be used for proofs about algorithm correctness
added 1 character in body
Dec
23
answered How Univalence can be used for proofs about algorithm correctness
Dec
23
comment Uses of $\infty$-categories in TCS
Have a look at Michael Shulmans section "Expository notes and talks" at the bottom of his page home.sandiego.edu/~shulman/papers/index.html. Mike is a homotopy-theorist by training, so you might find his stuff more easily understandable.
Dec
23
answered Uses of $\infty$-categories in TCS
Dec
23
comment Uses of $\infty$-categories in TCS
You should ask this question five years from now. We don't know yet exactly how we're going to use $\infty$-categories in computer science. At the moment we have a pretty good idea about $\infty$-groupoids: they improved greatly our understanding of type theory.
Dec
15
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.