11,663 reputation
2861
bio website andrej.com
location Slovenia
age 43
visits member for 4 years, 2 months
seen 7 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.


Oct
27
comment Categorical semantics for non-monotonic logics?
Are you asking whether someone has done it, or whether it can be done? Surely it can be done, but I do not know whether it has been done. (You just shouldn't model the consequence relation as the subobject relation, but pass to a fancier fibration.)
Oct
27
comment Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?
This question is ill posed and it is not clear what is being asked. Furthermore, the accepted answer is misleading at best.
Oct
27
comment Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?
It is false that $\mathbb{N}$ corresponds to $\top$. You are making the mistake of ignoring proofs and you are just looking at inhabitation. (That roughly corresponds to making everything proof irrelevant). Just because two types are both inhabited, that does not make them equal, nor does it mean they correspond to the same proposition. They may have the same extension (truth value), but they have different meaning.
Oct
27
comment Are there presentations of set theory in terms of lambda-calculus?
You are looking for Church's type theory, and what you're planning sounds like a toy version of the HOL proof assistant, which is based on Church's type theory. And this isn't research-level.
Oct
19
comment Can we design our own `if` clause in Normal Order evaluation
That would be Haskell.
Oct
19
revised Can we design our own `if` clause in Normal Order evaluation
added 1035 characters in body
Oct
19
answered Can we design our own `if` clause in Normal Order evaluation
Oct
19
comment Can we design our own `if` clause in Normal Order evaluation
Not everyone on this planet knows what "SICP" refers to.
Oct
13
comment Representing boolean function by a polynomial
Related: cstheory.stackexchange.com/questions/25291/…
Oct
10
comment Scott's stochastic lambda calculi
As I said, as soon as you choose a countable base $(B_n)_n$ on a $T_0$-space that gives you an encoding of the space: a point $x$ is encoded as the set $\{n \in \mathbb{N} \mid x \in B_n\}$.
Oct
10
comment Scott's stochastic lambda calculi
Every countably based $T_0$-space embeds in the graph model. Via this embedding we can then happily marry $\lambda$-calculus with topology and compute with, say, real numbers. The embedding is quite natural: a point is represented by the filter of its basic neighborhoods.
Oct
8
comment How is IO a monad?
Monads in functional programming are not too advanced for cs.stackexchange. That's like saying objects are too advanced for anyone who has never seen an object-oriented langauge. And this question is not research-level.
Oct
7
comment Which formalism is best suited for automated theorem proving in set theory?
@dezakin: $S(x)$ means "$x$ is a set" (as opposed to its being a class). It can be defined as $\exists y . x \in y$, so it is largely a matter of choice how we set things up.
Sep
30
awarded  Explainer
Sep
29
comment Purely functional uniquely-represented deques
Doubly-linked lists are only uniquely represented if one cannot compare pointers.
Sep
24
revised Dependent Sums and Products
deleted 2 characters in body
Sep
24
answered Dependent Sums and Products
Sep
17
answered Explaining monad transformers in categorical terms
Sep
16
comment Do Genetic Algorithms Expect a Independent Search Space
You definitely do not mean "separable", see en.wikipedia.org/wiki/Separable_space
Sep
10
revised Computability of infinite-dimensional vector space
added 37 characters in body