92 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
8
votes
1
answer
347
views
A type with `Eq a` but not `Ord a`
In (an idealized version of) Haskell, is there a concrete type a such that we can implement Eq a lawfully, but it is impossible to implement Ord a? The order doesn't need to be meaningful, and any ...
1
vote
0
answers
62
views
I have two types that should be semantically identical. Why is one resulting in an error while the other one gets accepted?
Take the following TypeScript code (you can see it live at https://tsplay.dev/w1GYAm):
type Graph<T=any> = {
A?: T,
B?: T,
C?: T,
};
type X<T extends Graph> = T['B'] | T['C'] |...
1
vote
1
answer
208
views
Applying Reflexivity of String Equivalence in Agda Proofs
In my Agda program, I have a small function that checks for string equality (simplified for example):
open import Data.String.Base using (String)
open import Date.String.Properties using (_≈?_)
open ...
0
votes
2
answers
256
views
Are linear problems on rational numbers decidable in Z3?
I'm working with linear problems on rationals in Z3. To use Z3 I take SBV.
An example of a problem I pose is:
import Data.SBV
solution1 = do
x <- sRational "x"
w <- sRational &...
2
votes
1
answer
557
views
Z3: is Nonlinear integer arithmetic undecidable or semi-decidable
In Z3 (Python), I solved the following:
y1,y2,x = Ints('y1 y2 x')
univ = ForAll([x], (y1<y2+x*x))
phi = Exists([y1,y2], univ)
solve(phi)
Note that the encoding does not make sense, just playing.
...
3
votes
1
answer
240
views
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 ({ _ _ _ } + {~ _ _ _ })) ...
1
vote
2
answers
2k
views
Prove that we can decide whether a Turing machine takes at least 100 steps on some input
We know that the problem "Does this Turing machine take at least this finite number of steps on that input?" is decidable, because it will always answer yes or no, where it will say yes if the machine ...
0
votes
1
answer
422
views
Recognizabilty of a set in regards to their size bounds
Trying to teach myself Computational Theory, and stumbled upon this question:
Suppose we have two sets:
{T | T is a turing machine and L(T) contains at least 1001 string}
{T | T is a turing machine ...
0
votes
1
answer
1k
views
Recursive vs recursively enumerable language in Turing Machines?
We say language L is recursive if it is decided by a TM.
L is recursively enumerable (r.e.) if it's recognized by a TM.
Suppose, enumerator (en-r) is a deterministic Turing Machine with a printer that ...
0
votes
1
answer
186
views
Undecidable if TM overwrites its input?
I came across a statement postulating that it's undecidable whether a TM overwrites any of its own input.
What would be intuition as well as an actual proof for that?
0
votes
1
answer
105
views
Looking for the Agda module that contains decidable equality for lists
Given two lists xs and ys, I would like to obtain a value of Dec(xs ≡ ys).
Does any one know the name of the standard library module which contains such an operator?
1
vote
1
answer
918
views
"Reduction" from the complement of the universal language (L_u) to the language of nonempty-language Turing machines (L_ne)
I have a question from the domain of theoretical computer science.
The so-called universal language, L_u, is composed of pairs (M, w) such that w \in L(M). The language L_ne consists of machines M (...
1
vote
1
answer
607
views
Is a given TM having finite states is decidable or not?
first of all is above question is correct?
i think decidability is property of particular problem
like 1. whether given string belong to particular language
2. whether TM will reach particular state ...
0
votes
0
answers
808
views
reduction from ALLtm to Etm
I am trying to understand why this "proof" of Etm undecidability is wrong.
ALLtm={ < M >|M is a TM, L(M)=∑*}
ETM={< M >|M is a TM, L(M)=∅}
We know that ALLTM is undecidable, lets ...
1
vote
1
answer
101
views
How to define a subformula of an inductively defined type in Agda?
I'm trying to define a simple predicate to determine if a formula is a subformula of a given formal over a simple inductively defined syntax. I'm running into a few, presumably simple, problems.
(i) ...
user avatar
user5775230