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 ...
- 28.3k
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 $|$, $+$...
- 16.9k
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,598
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,631
14
votes
Accepted
Logical Reations for an Impredicative System in a Predicative MetaTheory
In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...
- 13.7k
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 ...
- 9,595
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 ...
- 28.3k
13
votes
Accepted
Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?
First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....
- 5,273
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, ...
- 4,431
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 ...
- 13.7k
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 ...
- 28.3k
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 ...
- 28.3k
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 ...
- 32.4k
13
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 ...
- 16.9k
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 ...
- 648
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,431
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 ...
- 16.9k
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,431
12
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,273
11
votes
Can you explain an intuition behind Coherent Spaces?
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 ...
- 32.4k
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 ...
- 28.3k
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 ...
- 13.7k
11
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.4k
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,616
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
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
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 ...
- 921
Only top scored, non community-wiki answers of a minimum length are eligible