Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.
98

The Matrix Mortality Problem for 2x2 matrices. I.e., given a finite list of 2x2 integer matrices M1,...,Mk, can the Mi's be multiplied in any order (with arbitrarily many repetitions) to produce the all-0 matrix? (The 3x3 case is known to be undecidable. The 1x1 case, of course, is decidable.)


75

Here's my favorite analogy. Suppose I spent a decade publishing books and papers arguing that, contrary to theoretical computer science's dogma, the Church-Turing Thesis fails to capture all of computation, because Turing machines can't toast bread. Therefore, you need my revolutionary new model, the Toaster-Enhanced Turing Machine (TETM), which allows ...


60

UPDATE: The problem I mentioned here is now known to be undecidable! http://arxiv.org/abs/1605.05274 Moreover, the paper was inspired by reading this very answer. :) Programmers in your math-major audience may be surprised to learn that the question "is this type implicitly convertible to that type?" is not known to be decidable in any of Java 5, C# 4 and ...


50

Hilbert's tenth problem over rationals: "Does this polynomial equation have a rational solution?"


45

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 ...


42

The halting theorem, Cantor's theorem (the non-isomorphism of a set and its powerset), and Goedel's incompleteness theorem are all instances of the Lawvere fixed point theorem, which says that for any cartesian closed category, if there is an epimorphic map $e : A \to (A \Rightarrow B)$ then every $f : B \to B$ has a fixed point. Lawvere, F. William. ...


42

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$ ...


38

The extent to which this is possible is actually a major open question in the theory of the lambda calculus. Here's a quick summary of what's known: The simply-typed lambda calculus with unit, products, and function space does have a simple canonical forms property. Two terms are equal if and only if they have the same beta-normal, eta-long form. Computing ...


35

I think the issue is quite simple. All interactive formalisms can be simulated by Turing machines. TMs are inconvenient languages for research on interactive computation (in most cases) because the interesting issues get drowned out in the noise of encodings. Everybody working on the mathematisation of interaction knows this. Let me explain this in more ...


32

It is easy to get confused about what it means to "represent" or "implement" a real number. In fact, we are witnessing a discussion in the comments where the representation is contentious. So let me address this first. How do we know that an implementation is correct? The theory which explains how to represent things in a computer is realizability. The ...


31

The problem of given a linear recurrence along with its initial values, does it take the value 0? Two reference: http://terrytao.wordpress.com/2007/05/25/open-question-effective-skolem-mahler-lech-theorem/ http://www.cs.ox.ac.uk/joel.ouaknine/publications/positivity12.pdf


28

Neither! The best way to see this independence is to read the original papers. Turing's 1936 paper introducing Turing machines does not refer to any simpler type of (abstract) finite automaton. McCulloch and Pitts' 1943 paper introducing "nerve-nets", the precursors of modern-day finite-state machines, proposed them as simplified models of neural activity, ...


26

In terms of number computability (i.e., computing functions from $\mathbb{N} \to \mathbb{N}$), all known models of computation are equivalent. However, it's still true that Turing machines are fairly painful for modelling properties like interactivity. The reason is a little bit subtle, and has to do with the kinds of questions that we want to ask about ...


25

No, it's not. I know two major classes of techniques for avoiding inconsistency/Turing completeness. The first line of attack is to set up the system so that syntax can be arithmetized, but Godel's fixed point theorem doesn't go through. Dan Willard has worked extensively on this and given consistent self-verifying logical systems. The trick is to eliminate ...


25

A simple problem whose decidability is unknown is the following (I think it is still open): Infinite chess: Input: A finite list of chess pieces and their starting positions on a $Z \times Z$ chessboard; Question: Can White force mate? If we add the constraint that White must mate in $n$ moves ($n$ is part of the input), then it becomes decidable: see Dan ...


24

Not necessarily. For instance, the two-dimensional block cellular automaton with two states, in which a cell becomes live only when its four predecessors have exactly two adjacent live cells, can simulate itself with a factor of two slowdown and a factor of two size blowup, but is not known to be Turing complete. See The B36/S125 “2x2” Life-Like Cellular ...


23

In general you cannot determine complexity, even for halting programs: let $T$ be some arbitrary Turing machine and let $p_T$ be the program (that always returns 0): input: n run T for n steps if T is in halting state, output: 0 otherwise, loop for n^2 steps and output: 0 It is clear that it is undecidable in general whether $p_T$ is linear-time or ...


23

Yes, it is. Here's how you do it: You can compile basically any program you like to circuits. See for instance the work of Dan Ghica and his collaborators on the Geometry of Synthesis, which shows how to compile programs into circuits. Dan R. Ghica. Geometry of Synthesis: A structured approach to VLSI design Dan R. Ghica, Alex Smith. Geometry of Synthesis ...


23

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

An extended comment: Collatz-like sequences can be computed by small Turing machines having few symbols and states. In "Small Turing machines and generalized busy beaver competition" by P. Michel (2004), there is a nice table that positions Collatz-like problems between decidable TMs (for which the halting problem is decidable) and Universal TMs. There ...


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 ...


21

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 ...


20

Can such machines be built in practice? Yes. By "machine", Schmidhuber just means "computer program". Are they at least feasible in our Universe? Not in their current form -- the algorithms are too inefficient. From a ten thousand meter perspective, Jürgen Schmidhuber (and former students, like Marcus Hutter) have been investigating the idea of ...


20

Collatz Problem is simple-to-describe problem whose decidability is open. It involves a simple recurrence of elementary arithmetic operations. $f(n)=\mathsf{\{}$ $n/2$ for even integer, $3n+1$ for odd integer The problem is deciding whether iterating this function always return to 1 for a given positive integer $n_0$. Interestingly, a generalization ...


19

It would be better if you specified what you mean exactly by hyper-computation and gave evidence for why you think it has "died down". In any case, assuming that you are talking about computation of functions over natural numbers (and finite strings) (since I think it is clear that models for higher type computation is a very active area, e.g. CCA) and ...


19

No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. $$ \begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array} $$ These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves ...


19

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.)


19

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

Benjamin Werner has proved the mutual interpretability of ZFC with countably many inaccessibles and the Calculus of Inductive Constructions, in his paper Sets in Types, Types in Sets. This means, roughly, that any function which can be shown to be total in ZFC with countably many inaccessibles can be defined in Coq. So unless you are a set theorist ...


18

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.


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