Questions tagged [decidability]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
-6 votes
2 answers
199 views

Does the Linz Halting Problem proof contain a fatal flaw?

It is the case that the input to the embedded Linz H would never reach its final state and halt when the Linz H is a simulating halt decider. (see below). computation that halts… the Turing machine ...
  • 65
6 votes
0 answers
93 views

Algorithmically determining proof complexity for Frege systems?

I apologize if this falls wildly short of research level - I am just learning the very basics of proof complexity and lack any real logic background. Let $F$ be a Frege proof system (a finite complete ...
  • 161
-7 votes
1 answer
340 views

Does the Linz Ĥ applied to ⟨Ĥ⟩ correctly transition to its final reject state? [closed]

By making a slight refinement to the halt status criterion measure that remains consistent with the original a halt decider may be defined that correctly determines the halt status of the conventional ...
  • 65
2 votes
0 answers
90 views

Tenth Hilbert problem on interval arithmetic

What is the decidability status of Hilbert's Tenth problem interpreted over interval arithmetic? In details, let $p\in\mathbb{Q}[x_1,\ldots,x_n]$ be a Diophantine polynomial. The problem is that of ...
  • 1,122
3 votes
1 answer
147 views

How to solve an unification problem on $\mathbb{N}$?

Usually, the unification problem for two given terms $t$ and $s$ is to find a substitution $\theta$ such that $\theta t = \theta s$, which is equal to finding the certain $\langle x_1 , \cdots , x_n \...
21 votes
2 answers
1k views

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

It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, ...
  • 842
15 votes
1 answer
679 views

Computability and continuity

Say $L_1$ and $L_2$ are computable languages. Let $f$ be a function $L_1 \rightarrow L_2$. Let $C$ be the statement, "if $l \subseteq L_2$ and $l$ is a computable language, the preimage $f^{-1}(...
  • 253
1 vote
0 answers
29 views

Decidability of regular partition construction given its existence

Let $G = (N,T,P,S)$ be a context-free grammar where $T,N$ are sets of terminals and nonterminals respectively, $P$ contains all the productions of the grammar, and $S \in N$. If we know that $G$ is LL(...
  • 111
3 votes
1 answer
361 views

Can the halting problem be solved probabilistically? [closed]

Let $H$ be the halting oracle, meaning that $H$ is a function on pairs of strings such that $H(P,X) = 1$ iff $P$ halts on $X$. A probabilistic program is a program that has (oracle) access to a random ...
  • 137
3 votes
0 answers
105 views

Deciding whether an arbitrary context-free grammar generates a deterministic push-down automata?

I know that it's undecidable whether an arbitrary context-free grammar is ambiguous, but is it decidable whether that grammar is deterministic? I can't find the answer to this question anywhere on the ...
3 votes
2 answers
253 views

Dependence of decidability on the encoding of Turing machines

Let $f : \{0, 1\}^* \to \{0, 1\}^*$ be a computable function. Given any encoding $\left<M\right>$ of Turing machines over binary (i.e., a function from the set of Turing machines to the set of ...
4 votes
1 answer
145 views

Deciding whether a 2nfa halts on every input on every branch

A 2nfa is a nondeterministic finite automaton that can move its head left or right on the input tape, or not. Is the following language known to be decidable? $$ \textit{H}_{\mathsf{2nfa}} = \{ \...
0 votes
0 answers
40 views

Is this a proof that diophantine equation solutions can't be bounded by power towers?

From this 2017 paper on upper bounds for solutions to diophantine equations: Conjecture 1. If a system of equations S ⊆ Bn has exactly one solution in positive integers x1, . . . , xn , then x1, ....
6 votes
1 answer
157 views

Decidability of rank-k polymorphism vs. System F

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
  • 325
0 votes
2 answers
207 views

Is the decidability of a language decidable? [closed]

Is there a Turing machine that takes a language as input and decides/semi-decides if it is a decidable language? Comments + answer say trivially the answer is yes; however, I'm wondering here would ...
  • 291
-1 votes
2 answers
202 views

Turing meta-oracle

Let H(P) be some program that given P('s source code) computes whether or not P terminates, i.e. solves the halting problem. H only needs to terminate if P terminates. (This disallows solutions like ...
-1 votes
1 answer
134 views

Gödel-Numbering of the Context-Sensitive Languages

I would like to have a Gödel-numbering of the context-sensitive languages. Because there is no obvious syntactic distinction between LBAs and TMs, I cannot number the former in an immediate way. So I ...
7 votes
1 answer
368 views

Uniform mortality problem for Turing Machines

Consider the following generalisation of the mortality problem for Turing Machines. Given a Turing Machine $M$. Is there a bound $k_M$ such that starting from any configuration $c$ machine $M$ ...
9 votes
1 answer
454 views

Is there an algorithm that finds the forbidden minors?

The Robertson–Seymour theorem says that any minor-closed family $\mathcal G$ of graphs can be characterized by finitely many forbidden minors. Is there an algorithm that for an input $\mathcal G$ ...
  • 13.6k
5 votes
1 answer
207 views

Post correspondence problem for finite monoids

The Post correspondence problem has the following version for finite monoids: Input: a finite monoid $M$ and a finite list $(m_1,m_1'),\ldots, (m_n,m_n')$ of pairs of elements of $M$ Question: is ...
2 votes
1 answer
200 views

Petri net termination

Termination is the following problem. Input: a Petri Net with initial marking Output: "yes" iff there exists an infinite firing sequence. The naive algorithm in the case of bounded nets for example ...
  • 91
2 votes
2 answers
197 views

How can you state how abstract interpretation gets around Rice's Theorem succinctly?

At this question, abstract interpretation has a nice in-depth look. However, I'd like someone to clearly and very precisely state how abstract interpretation takes the result of Rice's Theorem over ...
  • 309
4 votes
2 answers
1k views

Enumerating decidable languages

[The assumption in this question is wrong. It is possible to enumerate exactly the decidable languages with semideciders.] Lets say we have a TM $M_E$ enumerator that writes out codes of TM's on a ...
6 votes
1 answer
1k views

Show that minimal CFG is undecidable via mapping reduction

Actually the problem below is an exercise in Sipser's textbook (Problem 5.36). However, from my perspective, it is not so trivial so that I post this question on this site instead of CS.SE. The ...
  • 395
1 vote
0 answers
98 views

Deciding reachability under iterated independent polynomial mapping

For any $1\leq i\leq m$, $f_i: \mathbb{Q}\rightarrow \mathbb{Q}$ is a polynomial mapping over $x_i$, where $\mathbb{Q}$ is the set of rationals. For $\vec{a}_0=(a_1, \cdots, a_m)\in \mathbb{Q}^m$, we ...
0 votes
1 answer
185 views

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem? In other words, could the Tarski–Seidenberg theorem subsume Buchberger's algorithm and Wu's ...
19 votes
1 answer
1k views

Is equivalence of unambiguous context-free languages decidable?

It is well known that the equivalence problem is undecidable for general context-free languages. However, all proofs of this fact that I am aware of seem to involve some ambiguous context-free ...
5 votes
0 answers
95 views

Which computational models support bigotous programs?

A bigotous program is a program which decides if its input is semantically equivalent to itself. Of course, this is impossible in a Turing complete language due to Rice's theorem. In fact, its pretty ...
  • 471
4 votes
2 answers
583 views

About the decidability of sets enumerated in non decreasing order

It is well known that a set of numbers enumerable in nondecreasing order is decidable. However, the typical proof, by cases on the finiteness of the enumerated set, is not constructive. In general, it ...
5 votes
1 answer
491 views

Proof that the theory of rationals is convex

In Example 10.12 of the book The calculus of computation by Bradley and Manna, it is said The theory of rationals is convex, as it is convex in a geometric sense. How does the geometric sense of ...
  • 153
6 votes
1 answer
282 views

Proof of decidability of type checking of calculus of (co)inductive constructions?

I often see it asserted that type checking is decidable for CIC, but I haven't seen it proven. Is there a good paper (or simple demonstration) of this?
  • 213
18 votes
2 answers
775 views

Deciding whether a unary context-sensitive language is regular

It is a well-known result that the question Does a context-free grammar generate a regular language? is undecidable. However, it becomes decidable on a unary alphabet, simply because in this case,...
  • 4,721
35 votes
3 answers
3k views

Turing Machine restrictions that render halting decidable

If one restricts Turing Machines to a finite tape (i.e., to use bounded space $S$), then the halting problem is decidable, essentially because after a number of steps (which can be calculated from the ...
8 votes
0 answers
374 views

Decidability of existential first-order theory of reals with exponential

The first-order theory over the reals as an ordered field with polynomials is decidable with doubly exponential complexity. However, if we additionally allow the exponential function, that is $e^x$ ...
-1 votes
1 answer
135 views

Global satisfiability in LTL

In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0. Is it known to be un/decidable to check the ...
0 votes
2 answers
299 views

Are there any open problems concerning decidability? [duplicate]

I am learning computability theory. I am just interested to know some famous problems (Formally languages) whose decidability is in question.
  • 119
9 votes
1 answer
152 views

Oracle-Decidability of Algebraic Independence

Consider numbers $x_1,...,x_n\in \mathbb{R}$ given by TMs $M_1,...,M_n$ such that $M_i$ approximates $x_i$ to an arbitrary precision (by allowing it to run longer and longer). I am interested in the ...
  • 5,271
6 votes
2 answers
264 views

FSM transducer sequential composition decidability

this is a followup/ sequel to this recent question which was answered, this one presumably significantly harder. consider a deterministic FSM transducer $F$ and its mapping $F(x)$ of an input word $x$....
  • 10.9k
25 votes
2 answers
2k views

Is it decidable to determine if a given shape can tile the plane?

I know that it is undecidable to determine if a set of tiles can tile the plane, a result of Berger using Wang tiles. My question is whether it is also known to be undecidable to determine if a single ...
5 votes
1 answer
218 views

Is algebraic dependency decidable?

A set of numbers $S=\{x_1,...,x_n\}$ is said to be algebraically dependent if there exists a (multivariate) polynomial $p$ with coefficients in $\mathbb Q$ whose roots contain $x_1,...,x_n$ (or a ...
  • 5,271
2 votes
1 answer
4k views

Deciding whether a context-free language is regular [closed]

Does anyone know whether the following decision problem is decidable: Given a context-free language $L$, is $L$ regular? Here $L$ can be expressed, e.g., using a context-free grammar. Does anyone ...
2 votes
0 answers
741 views

Decidability of CFG ambiguity

I have been trying to show the following language is undecidable. $L = \{ (\langle G \rangle , n ): G$ is a context-free grammar with an ambiguous string of length $\le n \}$. I think it is ...
  • 233
11 votes
2 answers
262 views

Vector Addition Systems with finite "obstacles"

A Vector Addition System (VAS) is a finite set of actions $A \subset \mathbb{Z}^d$. $\mathbb{N}^d$ is the set of markings. A run is a non-empty word of markings $m_0 m_1\dots m_n$ s.t. $\forall i \in \...
9 votes
1 answer
362 views

Membership problem for certain class of unrestricted grammars

Consider an arbitrary context-free grammar $G$ over the alphabet $\lbrace 0,1,\overline{0} ,\overline{1} \rbrace$. To the productions of this grammar, add two fixed non-context-free productions $P$: $...
  • 113
-1 votes
1 answer
132 views

Consistency and completeness of any arbitrary 3-valued logic? [closed]

Based on the explanations here [1] I know that 3-valued first order logic has many different versions, which differ in the definition of their operations (e.g. implication). All of these (as far as I ...
  • 739
3 votes
1 answer
232 views

Decidability of first-order theory of real closed fields with functions

By a famous theorem of Tarski, the first-order theory of real closed fields is decidable, as it admits quantifier elimination. Can this result be extended so that propositions can be quantified over ...
  • 11.1k
5 votes
1 answer
174 views

What language $L \in NCM$ has $\overline{L} \not \in NCM$?

$NCM$, the class of non-deterministic reversal-bounded counter machines, has a lot of interesting dependability and closure properties. It's known that, unlike the deterministic version, NCM is not ...
6 votes
3 answers
240 views

Solving problems by deciding a logic

I am curious to know when open problems have been solved by expressing them in a specific logic, and then showing that this logic is decidable. I have two distinct cases in mind: The problem is ...
  • 7,747
20 votes
5 answers
802 views

What notable automaton models have polynomially-decidable containment?

I'm trying to solve a particular problem, and I thought I might be able to solve it using automata theory. I'm wondering, what models of automata have containment decidable in polynomial time? i.e. if ...
8 votes
1 answer
200 views

Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...