Skip to main content
Share Your Experience: Take the 2024 Developer Survey
25 votes

Theoretical Computer Science vs other Sciences?

As a theoretical computer scientist I am proud of the following achievements of the field. Logicians figured out that all logical connectives can be build from a single one, paving the road for ...
Andrej Bauer's user avatar
  • 29.1k
21 votes
Accepted

Decidability of diophantine equations over {=, +, gcd}

($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$...
Emil Jeřábek's user avatar
18 votes

Theoretical Computer Science vs other Sciences?

As a TCS researcher, I understand the feeling and feel it too sometimes. I think it is healthy to be able to appreciate the wonder that other sciences have to offer. We must also keep in mind that it ...
Denis's user avatar
  • 8,893
17 votes
Accepted

Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The two words do not refer to the same thing. Hilbert's Entscheidungsproblem was the question whether there is an algorithm that decides the universal truth of first-order logical sentences, which was ...
Jan Johannsen's user avatar
14 votes

Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's. Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ...
Neal Young's user avatar
  • 10.8k
14 votes
Accepted

What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

Note that formulas using $\land$ and $\lor$ gates (and possibly the constants $0$ and $1$) are known as monotone. The complexity of monotone formula equivalence depends on how complex formulas are ...
Emil Jeřábek's user avatar
14 votes

Where is the model theory in programming language theory?

Let me amend Damiano's answer with more specific comments. Terms of type bool are not logical statements. Expressions like ...
Andrej Bauer's user avatar
  • 29.1k
13 votes

What is the difference between unification and anti-unification?

The following category theory inspired analysis (adapted from Plotkin's A Note on Inductive Generalization) explains a sense in which unification and anti-unification are dual concepts. As notation, ...
Noam Zeilberger's user avatar
13 votes

How to think about coherent spaces intuitively?

The intuition behind coherence spaces is that the elements of a coherence space represent observations of some underlying data, and the coherence relation tells you whether two observations could have ...
Neel Krishnaswami's user avatar
13 votes
Accepted

Is there a good notion of non-termination and halting proofs in type theory?

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ...
cody's user avatar
  • 13.9k
13 votes
Accepted

Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

Yes, LEM implies K. See HoTT book Theorem 7.2.5, known as Hedberg's theorem, which shows that any type with decidable equality satisfies axiom $K$. If we assume excluded middle, all types have ...
Andrej Bauer's user avatar
  • 29.1k
13 votes

Why/when do we ever need transfinite loop variants?

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid ...
Andrej Bauer's user avatar
  • 29.1k
13 votes
Accepted

What logic correponds via Curry-Howard to a Monad?

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan ...
Neel Krishnaswami's user avatar
13 votes
Accepted

Is there a language of first-order logic such that every r.e. set is Turing-equivalent to some finitely axiomatizable theory in that language?

The answer is yes. This was proved by Hanf (Model-theoretic methods in the study of elementary logic, in the Theory of models volume). A "uniform" version of this result was conjectured by ...
Noah Schweber's user avatar
13 votes
Accepted

Where is the model theory in programming language theory?

The model theory of programming languages is called denotational semantics. You can google the term to find out more about it, I'll give an extreme synthesis of it. Denotational semantics is a ...
Damiano Mazza's user avatar
12 votes

Incomplete basis of combinators

[Expanding the comment into an answer.] First, just a clarification about counting bound variables in a combinator (= closed term) $t$. I interpret the question as asking about $$ \text{the total ...
Noam Zeilberger's user avatar
12 votes
Accepted

What is the intuition behind linear logic?

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...
Martin Berger's user avatar
12 votes
Accepted

Does the first order theory of a finite structure have bounded quantifier rank?

The theory of any finite structure is model complete. In fact, it is easy to see that any formula is equivalent to an existential formula with one quantifier per each element of the structure, after ...
Emil Jeřábek's user avatar
12 votes

Representing bound variables with a function from uses to binders

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments. To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, ...
Noam Zeilberger's user avatar
11 votes
Accepted

Standard reference for basic model theory definitions

Here is one possibility, but other people might use different words. I will use first-order logic as a running example. Language The language is a collection of expressions, which are syntactic ...
Andrej Bauer's user avatar
  • 29.1k
11 votes
Accepted

Typo in the calculus of constructions paper?

You are correct, there is an error in that paper, and the rule should indeed read: $$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$ the use of jugements of this style for equality (sometimes ...
cody's user avatar
  • 13.9k
11 votes
Accepted

Equilibrium in a Halting Game

Even if you have a one-player game there is no computable equilibrium. Consider nature putting probability $1/2^i$ on program $i$. Any computable strategy will achieve some value strictly less than ...
Lance Fortnow's user avatar
11 votes

Philosophy behind monotonicity requirement for inductive types

When you write an inductive, you are defining a type by an equation. For example, if we write $F_1(X)=X^X=X\to X$, bad should satisfy $F_1($...
xavierm02's user avatar
  • 556
11 votes
Accepted

How do continuations represent negations (under the Curry–Howard correspondence)?

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type ...
Dan Doel's user avatar
  • 1,021
11 votes
Accepted

Stronger "induction" principles than induction-recursion

Anton Setzer has work on type theories that are stronger than standard induction-recursion. In some ways, though, it's still in terms of simultaneous inductive and recursive definitions. The ...
Dan Doel's user avatar
  • 1,021
11 votes

Theoretical Computer Science vs other Sciences?

I run a small software business producing XML processing tools, so I'm very much a practical engineer rather than a theoretician. It's 50 years since I did my CS degree. And you know, I'm constantly ...
Michael Kay's user avatar
10 votes

What's the expressive power of Simply Typed Lambda calculus?

As explained by Damiano Mazza here on MathOverflow (see also this TCS.SE question), for a very natural choice of encodings of input strings and output booleans, one gets exactly the regular languages! ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
10 votes

How to think about coherent spaces intuitively?

I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". ...
Arthur Azevedo De Amorim's user avatar
10 votes
Accepted

Conclusions from reverse mathematical strength of graph minor theorem

I am not sure I understood your question, but if you are asking how difficult it is to compute the set of obstructions, you may be interested in the following http://www.jucs.org/doi?doi=10.3217/jucs-...
M. kanté's user avatar
  • 1,046
10 votes
Accepted

Sparsification Lemma for k-SAT and Exponential Time Hypothesis

I think your confusion might come from misquoting the statement of ETH. $3$-SAT instances (with $n$ variables and $m$ clauses) cannot be solved in time $poly(n)\cdot 2^{o(n)}$. This statement is ...
Alex Golovnev's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible