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


1h
comment Commutativity of addition in polymorphic lambda calculus
It wouldn't, and that's what they are saying, as you write yourself: "does not follow from the Church-Rosser argument". Other things do follow, for example the fact that $\mathsf{Add}\,u\,z = u$ where $z = \Lambda t \lambda f x . x$ is "zero" is obtained by reducing all $\beta$-redexes on the left-hand side.
1h
comment Commutativity of addition in polymorphic lambda calculus
I would imagine they are talking about the fact that the polymorphic $\lambda$-calculus is strongly normalizing.
1h
revised Is it decidable that a computable analytic function over $\mathbb{R,C} ,$ equals $0$
added 144 characters in body
4h
answered Is it decidable that a computable analytic function over $\mathbb{R,C} ,$ equals $0$
Nov
20
awarded  Nice Answer
Nov
20
answered How to judge the definition of computational complexity of reals is natural or suitable?
Nov
20
comment How to judge the definition of computational complexity of reals is natural or suitable?
But it's not true that the complexity does not depend on the representation. By switching to a stupid representation you can always ruin the complexity of an algorithm. The question to ask is: "What is a good representation of the input?" For discrete problems this is much easier to answer than for real numbers, because one has a good feel for what it means to "don't waste bits".
Nov
20
awarded  Nice Answer
Nov
19
comment How to judge the definition of computational complexity of reals is natural or suitable?
You seem to think there is a complexity notion for real number computation which is independent of the representation of reals. What makes you think so? This is not the case in classical complexity either. It matters whether you have a tape or a RAM machine, it matters whether you represent graphs by adjancency lists or 01-matrices, etc.
Nov
13
comment Is there an algorithm to find whether 2 combinators form a Turing-complete system?
As we say in Slovenia, I probably got up on my left leg.
Nov
13
comment Is there an algorithm to find whether 2 combinators form a Turing-complete system?
Your question is ill-posed, and once it gets fixed it is not research-level. How are the combinators specified, by equations? If so, then there won't be an algorithm because a special case of what you're asking for will be the undecidable semigroup word problem.
Nov
10
answered Minimal specification of Martin-Löf type theory
Nov
7
comment What is a term of the type $\bot\rightarrow A$?
Well, whenever you add a new type or a new constructor to type theory, you should not be surprised by the addition of new terms, namely those that correspond to the introduction and elimination rules on the logic side of things. You make it sounds like this is a bad thing, but it is completely expected. You wouldn't be suprised to get wet when you go swimming, either.
Nov
7
awarded  Enlightened
Nov
7
awarded  Nice Answer
Nov
6
comment Type variables and parametric polymorphism
They do not assume that all substitution instances are well typed. Rather, it is a theorem that this is the case for ML and Haskell.
Nov
2
answered What is a term of the type $\bot\rightarrow A$?
Nov
2
revised Relating univalence for a theory of cateogries to the skeleton concept
added 906 characters in body
Nov
2
answered Relating univalence for a theory of cateogries to the skeleton concept
Nov
2
comment Relating univalence for a theory of cateogries to the skeleton concept
Have you read Chapter 9 of the HoTT book? It's about category theory.