50

System $F$ is quite expressive. As proved by Girard here, the functions of type $\mathbb{N}\rightarrow\mathbb{N}$ (where $\mathbb{N}$ is defined to be $\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$) are exactly the definable functions ($\mathbb{N}\rightarrow\mathbb{N}$) in second order Heyting Arithmetic $\mathrm{HA}_2$. Note that this is the same ...


46

This is a badly phrased question, so let's first make sense of it. I am going to do it the style of computability theory. Thus I will use numbers instead of strings: a piece of source code is a number, rather than a string of symbols. It does not really matter, you may replace $\mathbb{N}$ with $\mathtt{string}$ throughout below. Let $\langle m, n\rangle$ ...


25

As Steven notes, the canonical example is $\mathsf{IP} = \mathsf{PSPACE}$. This collapse does not relativize, in the sense that there is an oracle $A$, subject to which $\mathsf{IP}^A \ne \mathsf{PSPACE}^A$. The intuition why the known proof of this result avoids the relativization barrier is that it uses arithmetization (Yonatan alluded to this in a comment)...


22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...


22

You're in good company. Kurt Gödel criticized $\lambda$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it is not intuitive, or that it does not sufficiently explain what is going on. In contrast, he found Turing's analysis of computability and the ensuing notion of ...


21

It is unknown whether or not it is decidable to determine if a given shape can tile the plane, even for polyomino tiles.                     (Image from Wikipedia.)


21

Any language which is not Turing complete can not write an interpreter for it self. This statement is incorrect. Consider the programming language in which the semantics of every string is "Ignore your input and halt immediately". This programming language is not Turing complete but every program is an interpreter for the language.


21

The question displays a fundamental misunderstanding about the nature of what can be done with computers. To correct this misunderstanding, I suggest getting a copy of the computer algebra software Maple and trying the commands expand((1+sqrt(2))^5); sin(Pi/4); If computers can only deal with rational numbers, how do you explain the results?


18

Check out the Computability and Complexity in Analysis network. Quote: The topics of interest include foundational work on various models and approaches for describing computability and complexity over the real numbers. They also include complexity-theoretic investigations, both foundational and with respect to concrete problems, and new implementations of ...


18

You're assuming that numbers can only be represented as fractions (either literally, by having a datatype storing integer numerator and denominator, or implicitly by using some kind of floating point representation) but this isn't true. For example, you can easily represent rational complex numbers by storing the rational real and imaginary parts. Similarly,...


18

First, the name of the conjecture is "Hartmanis-Stearns", not "Hartmanis-Stearn". Second, the Hartmanis-Stearns conjecture concerns those real numbers computable by a multi-tape Turing machine in real time; in other words, the TM must compute the n'th digit in n time. Third, the result of Adamczewski et al. is only about finite automata and deterministic ...


17

Yes. First, since it took me a minute to figure this out myself, let me formalize the difference between your question and $\mathsf{AlmostP}$; it's the order of quantifiers. $\mathsf{AlmostP} := \{L : Pr_R(L \in \mathsf{P}^R) = 1\}$, and the result you allude to is $\forall L\, L \in \mathsf{BPP} \iff Pr_R(L \in \mathsf{P}^R) = 1$. If I've understood ...


17

Hmm, turns out there's actually an matching upper bound that isn't too hard: To produce the truth table $HALT_n$ in a finite amount of time, the only information that is needed is the number of machines of description length at most $n$ which halt. This number is not more than $2^{n}$, so it can be represented with about $n$ bits, and say the number is $m$. ...


17

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 answered negatively by Turing in his famous 1936 paper "On Computable Numbers, with an application to the Entscheidungsproblem". The word literally means ...


16

The real numbers may be characterized in a couple of ways, let us work with the Cauchy-complete archimedean ordered field. (We need to be a bit careful how exactly we say this, see Definition 11.2.7 and Defintion 11.2.10 of the HoTT book.) The following theorem is valid in any topos (a model of higher-order intuitionistic logic): Theorem: There is a ...


16

Type theories in which every type is inhabited are far from being useless. True enough, through the eyes of logic they are inconsistent, but there are other things in life apart from logic. A general purpose programming language has general recursion. This allows it to populate every type, but we would not conclude from this fact that programming is a ...


16

This is not a research-level question, but since the general level of interest seems high, here is an answer. I cannot guess from your question whether you're shooting for something that will result in the usual computable numbers, or you're trying to surpass that. First we have Turing's definition of computable real number, and it is the one others have ...


15

I'm not sure whether this is what you're looking, but the phase transition in random SAT is an example. Let $\rho$ be the ratio of number of clauses to number of variables. Then a random SAT instance with parameter $\rho$ is very likely to be satisfiable if $\rho$ is less than a fixed constant (near 4.2) and is very likely to be unsatisfiable if $\rho$ is a ...


15

Probably you already got these in your bag :-) Two way one counter machine over unary alphabet (Minsky61). Two way weak counter machines (the counter has no effect on the computation but the machine halts if counter reaches zero) [1]. Quantum one counter automata [2]. With binary alphabets, the emptiness remains undecidable for: One way machines with one ...


15

I can see why the question is being downvoted, but this is too good not to post. Suppose you have a coin with bias $p\in[0,1]$, which might be rational or irrational. Question: using only finite memory, can you devise a test for determining whether $p$ is rational or not from a sequence of independent $p$-coin flips? Incredibly, as Hirschler and Cover showed ...


14

Here are two results cited in Charles E. Hughes "Undecidability of finite convergence for concatenation, insertion and bounded shuffle operators": Theorem 3: The class of mortal Turing machines is exactly the class of the constant running time Turing machines. $ConstT = \{ M \mid \exists s $ s.t. for all initial configurations $C$, $M$ halts in no more ...


14

No, the bombe was very specific. It consisted of a bunch of enigma machines hooked together. It was very limited in its use. A more interesting question is whether the Colossus computer, also used in Bletchely Park, was Turing-complete. When asking such a question, it should be understood that no physical computer is Turing-complete, since it cannot handle ...


14

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 theorem. (See comment section below for further discussion.) Let $K(x)$ be the Kolmogorov complexity of string $x$. lemma. $K$ is not computable. Proof. ...


13

I am not exactly sure what the question is here, but I can try to say a bit to clean up possible misunderstandings. First of all, if we are talking about complexity of a map $f : \mathbb{R} \to \mathbb{R}$, it makes no sense to ask "What is a good representation for $\sqrt{2}$?" Instead, you have to ask "What is a good representation for all inputs of $f$?"....


13

Higman's Embedding Theorem: The finitely generated computably presented groups are precisely the finitely generated subgroups of finitely presented groups. Furthermore, every computably presented group (even ones countably generated) is a subgroup of a finitely presented group. Note that this statement could relativize to: "The $O$-computably presented ...


13

This question is not research-level, but since it is receiving answers, I would like to offer an answer that may actually clear things up a bit, and provide references. There is an entire area of theoretical computer science which studies computability in analysis, algebra and topology. Of central importance is the notion of computability for real numbers. ...


13

Let $L_1 = L_2 = \mathbb{N}$ and let $M \subseteq \mathbb{N}$ be a maximal set and let $L = \mathbb{N} \setminus M$ be its complement. Recall that $L$ is infinite, and that every computably enumerable (c.e.) subset $S \subseteq \mathbb{N}$ contains either finitely many elements of $L$ or all but finitely many elements of $L$. Let $f : \mathbb{N} \to \mathbb{...


12

The semantics of computer programs can be understood geometrically in three distinct (and apparently incompatible) ways. The oldest approach is via domain theory. The intuition behind domain theory arises from the asymmetry behind termination and nontermination. When treating programs extensionally (ie, only looking at their I/O behavior, and not their ...


12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...


12

The most natural ways to represent knots are either to embed them piecewise linearly in $\mathbb{R}^3$ (just store the coordinates of the vertices and where you want to put segments) (any tame knot can be embedded piecewise linearly) or with a knot diagram, i.e. storing a projection on $\mathbb{R}^2$ as a graph where at every crossing you specify which ...


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