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 ...
- 29.4k
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 $|$, $+$...
- 18.2k
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 ...
- 8,923
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 ...
- 4,640
15
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 ...
- 32.8k
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 ...
- 10.9k
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 ...
- 18.2k
14
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 ...
- 5,598
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 ...
- 29.4k
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 ...
- 29.4k
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 ...
- 29.4k
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 ...
- 541
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 ...
- 4,561
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 ...
- 11.5k
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 ...
- 18.2k
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, ...
- 4,561
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 ...
- 14k
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 ...
- 8,741
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($...
- 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 ...
- 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 ...
- 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 ...
- 211
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! ...
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". ...
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-...
- 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 ...
- 2,247
10
votes
Accepted
Is Church-pentation implementable in Agda?
According to the paper you linked, I think the answer to the question you want to ask is, "no." Pentation is not definable in a stratified version of system F.
The paper says that their system can ...
- 1,021
10
votes
Representing bound variables with a function from uses to binders
I'm not sure how your variable-to-binder-function would be represented and for what purpose you'd like to use it. If you are using back-pointers then as Andrej noted the computational complexity of ...
- 1,187
10
votes
Theoretical Computer Science vs other Sciences?
My impression from your comments is that perhaps you have just not seen enough theoretical CS to get to some of the kind of content you are excited about in, say, physics.
I'll also point out that you ...
- 37.8k
10
votes
Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic
I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement
$$
(\forall x .\, \exists y .\, R(...
- 29.4k
Only top scored, non community-wiki answers of a minimum length are eligible