Stack Overflow
Stack Overflow

Questions tagged [decidable]

Decidable languages are languages such that the problem of whether a given word belongs to it or not is decidable. A decision problem, i.e., a question with a yes/no answer, is called decidable if there exists an algorithm (a Turing machine) that can and will return a Boolean true or false value (instead of looping indefinitely).

92 questions
26
votes
2 answers

Haskell/GHC UndecidableInstances - example for non-terminating type check?

I've written some Haskell code which needs -XUndecidableInstances to compile. I do understand why that happens, that there is a certain condition which is violated and therefore GHC yells. However, I've never come across a situation where the type…
scravy
  • 11,904
  • 14
  • 72
  • 127
20
votes
2 answers

Why knowing whether some piece of memory is needed is undecidable?

I was reading the Javascript tutorial of Mozilla and I come through this piece of information. High-level languages embed a piece of software called "garbage collector" whose job is to track memory allocation and use in order to find when a piece…
ralzaul
  • 4,280
  • 6
  • 32
  • 51
19
votes
3 answers

Relationship between NP-hard and undecidable problems

Am a bit confused about the relationship between undecidable problems and NP hard problems. Whether NP hard problems are a subset of undecidable problems, or are they just the same and equal, or is it that they are not comparable? For me, I have…
akaHuman
  • 1,332
  • 1
  • 14
  • 33
8
votes
4 answers

Why is OWL Full undecidable?

I've been looking all around on why OWL Full is undecidable, but I haven't found an easy to understand example that would lead me to comprehend it. I've found statements that explain that it is due to "Entailment Closure" and that is also correlated…
Juan Andrade
  • 81
  • 2
8
votes
1 answer

Does Provable == Decidable?

In computation theory are the terms Provable and Decidable interchangable? Do they mean the same thing? For example you often see the question whether something is provable referred to as a decision problem (Das Entscheidungsproblem).
Robben_Ford_Fan_boy
  • 8,494
  • 11
  • 64
  • 85
8
votes
1 answer

Generating run time proofs with type predicates in Idris

I am using this type to reason about strings on which decidable parsing can be performed: data Every : (a -> Type) -> List a -> Type where Nil : {P : a -> Type} -> Every P [] (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x::xs) For…
Vic Smith
  • 3,477
  • 1
  • 18
  • 29
6
votes
2 answers

haskell : making a superclass of Num

I want to make a superclass of Num, called Linear class Linear a where add :: a -> a -> a instance (Num a) => Linear a where add = (+) I get the error : Illegal instance declaration for `Linear a' (All instance types must be of the form (T…
Karan
  • 559
  • 5
  • 12
6
votes
1 answer

Why is E(dfa) a decidable language?

I don't understand why the Turing Machine T, ACCEPTS when no accept state is marked and rejects when an accept state is marked: E(dfa) = {| A is a DFA and L(A) = the empty set(don't have the symbol)} E(dfa) is a decidable language. Proof: A DFA…
h4x0rjax
  • 359
  • 1
  • 6
  • 15
5
votes
2 answers

Exactly what quantifiers is SMT complete for?

I've been looking at various SMT solvers, mainly Z3, CVC4, and VeriT. They all have vague descriptions of their ability to solve SMT problems with quantifiers. Their documentation is primarily example based (Z3), or consists of academic papers,…
jmite
  • 8,171
  • 6
  • 40
  • 81
5
votes
1 answer

Prove whether this language is decidable and recognizable

If L1 and L2 are languages we have a new language INTERLACE(L1, L2) = {w1v1w2v2 . . . wnvn | w1w2 . . . wn ∈ L1, v1v2 . . . vn ∈ L2}. For example, if abc ∈ L1 and 123 ∈ L2, then a1b2c3 ∈ INTERLACE(L1, L2) How can I prove that the INTERLACE is:…
theodor
  • 53
  • 5
5
votes
1 answer

Is equality decidable on any coinductive type?

this is my first post, apologies if it I have made mistakes. I suspect that, in Coq, coinductive types like Stream do not have decidable equality. That is, given two streams s and t, it is not possible identify whether s=t or ~(s=t). I suspect that…
Mitchell Buckley
  • 118
  • 6
3
votes
1 answer

Is this language decidable?

I'm struggling with whether or not this is decidable: A = {x is an element of the set of Natural Numbers | for every y greater than x, 2y is the sum of two primes} I'm inclined to think that this is decidable given the fact that when fed into a…
user1171851
  • 31
  • 1
  • 2
3
votes
1 answer

Is "less than" for rational numbers decideable in Coq?

In the Coq standard library, the "less than" relation is decidable for the natural numbers (lt_dec) and for the integers (Z_lt_dec). When I search however (Search ({ _ _ _ } + {~ _ _ _ })) I can't find a Q_le_dec or Qle_dec for the rationals, only…
LogicChains
  • 4,332
  • 2
  • 18
  • 27
3
votes
1 answer

Does pointwise decidability imply total decidability?

Does it hold that if I can decide a proposition P n for each specific n, then I can also decide whether or not forall n, P n ? It feels like it should be doable by some induction over n, but how can I prove that in Coq? Lemma dec_forall: forall…
larsr
  • 5,447
  • 19
  • 38
3
votes
1 answer

Does the order of prenex quantification matter in EPR fragment?

Effectively Propositional (EPR) fragment of the first-order logic is often defined as the set of prenex-quantified formulas of the form ∃X.∀Y.Φ(X,Y), where X and Y are (possibly empty) variable sequences. Does the order of quantification, i.e. ∃*∀*,…
Gowtham Kaki
  • 357
  • 1
  • 10
1
2 3 4 5 6 7