13,841 reputation
3369
bio website andrej.com
location Slovenia
age 43
visits member for 4 years, 8 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.


2d
answered How can I formalize key value stores with set theory?
Apr
18
comment Applicative functors in categorical terms
This is not a research-level question, it should be asked on cs.stackexchange.com.
Apr
11
comment A 2-state Turing machine complete catalog?
My instict tells me that a very simple heuristic will eliminate a lot of the machines. Have you tried anything yet? And 28.561 doesn't sound like a big number, actually.
Apr
11
comment A 2-state Turing machine complete catalog?
Have you checked Wolfram's "A New Kind of Science"? For instance this bit?
Apr
11
comment Calculating least fixed points in equations
Your question is unclear. Wht are $P$ and $S$? What is $X$? It looks like $P$ must be a logical statement and a set at the same time. Please be more specific and describe what is what.
Apr
6
answered Why do constructivists not seem to care too much about call/cc
Mar
30
awarded  Enlightened
Mar
30
awarded  Nice Answer
Mar
27
comment Why it's impossible to declare an induction principle for Church numerals
I am not too strong on references in this area, thanks @cody!
Mar
25
revised Why it's impossible to declare an induction principle for Church numerals
edited body
Mar
25
answered Why it's impossible to declare an induction principle for Church numerals
Mar
24
comment How can I prove that Hamming distance is upper bound for Levenshtein distance?
I added an example to the answer.
Mar
24
revised How can I prove that Hamming distance is upper bound for Levenshtein distance?
added 33 characters in body
Mar
24
comment How can I prove that Hamming distance is upper bound for Levenshtein distance?
Oh, you answered your own question above. Excellent. You could also just edit my answer, it would then be easier to spot your explanation.
Mar
24
comment Ramification of An Impredicative Type Theory
It's not just logically frightening but also set-theoretically frightening. You'll have to ask the Coq developers why it's off be default.
Mar
23
comment Ramification of An Impredicative Type Theory
Ha! There is an -impredicative-set command-line option in Coq... Keep trying.
Mar
23
comment Ramification of An Impredicative Type Theory
I suppose Coq is not "most theorem provers" to you, because it accepts the above definition.
Mar
23
comment Ramification of An Impredicative Type Theory
Are type theorists predicative, or their theories?
Mar
23
comment Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains
I do not understand what you are asking. I was giving set theory as an example, and it is definitely not special.
Mar
14
comment Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains
I would put it differently: the set-theoretic semantics of $\lambda$-calculus maps syntax directly into sets. To each type corresponds a set, not a symbol which denotes a set. But when you write this on paper you will use symbols to explain what you mean. The "countable model" problem is irrelevant because it confuses internal and external points of view. Inside the model (which is where we are when we give semantics) uncountable sets are uncountable setes, no magic. Stop thinking in terms of "everything is a model" because then you keep switching to a meta-level at the wrong moment.