Questions tagged [decidability]
The decidability tag has no usage guidance.
74
questions
0
votes
0
answers
166
views
Decidability of the complexity of decision problems
This might be a question that is related to some of the existent questions on the topic in the title, but I still find some answers either not full, or the topic still slightly different (maybe due to ...
-7
votes
2
answers
357
views
Self Referential Undecidability Construed as Incorrect Questions
Please see my answer before you read any of this. The answer says the same thing much much more clearly
PhD computer science professor Rick Hehner and I independently derived what we mutually agree ...
7
votes
1
answer
293
views
Is there a well-defined notion of an “R/poly” complexity class?
This would be the complexity class of all problems that are decidable in finite time with a polynomial length advice string that can be arbitrarily hard to compute. But potentially undecidable without ...
0
votes
0
answers
30
views
Decidability of Mixed-Integer Semidefinite Programs
Semidefinite programs (SDP) have an "efficient" solution, as a convex problem, by e.g. the ellipsoid method; but this comes with standard caveats as the output can be exponentially long (...
4
votes
1
answer
216
views
Halting problem proofs that do not utilise self-reference or diagonalization
Are there any proofs of the Halting problem that do not involve any self-reference, and diagonalization (or any diagonal argument) whatsoever?
All the duplicate questions I have come across end up ...
-13
votes
2
answers
1k
views
Can you see that the Linz Halting Problem proof contains a fatal flaw?
Applying a Simulating Halt Decider to the Linz Halting Problem Proof
When a simulating halt decider correctly simulates N steps of its input it derives the exact same N steps that a pure UTM would ...
7
votes
0
answers
100
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 ...
-8
votes
1
answer
381
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 ...
2
votes
0
answers
92
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 ...
3
votes
1
answer
153
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, ...
15
votes
1
answer
695
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}(...
1
vote
0
answers
30
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(...
3
votes
1
answer
425
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 ...
3
votes
0
answers
146
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 ...
4
votes
2
answers
268
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
163
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
45
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
229
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 ...
0
votes
2
answers
235
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 ...
-1
votes
2
answers
217
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
135
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
415
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
503
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$ ...
5
votes
1
answer
230
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
309
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 ...
2
votes
2
answers
208
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 ...
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
2k
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 ...
1
vote
0
answers
100
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
195
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
96
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 ...
4
votes
2
answers
613
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
524
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 ...
6
votes
1
answer
309
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?
18
votes
2
answers
845
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,...
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
403
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
145
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
328
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.
9
votes
1
answer
167
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 ...
6
votes
2
answers
276
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$....
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
231
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 ...
3
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
844
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 ...
12
votes
2
answers
279
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
383
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$: $...
-1
votes
1
answer
158
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 ...