31
votes
Accepted
Is it provably true/false that for a program, there exists a proof whether it halts or not?
Actually this is no different from the halting problem unsolvability. If you have any formal system T with a proof verifier program V that can reason about programs (as you desire in your question), ...
- 707
5
votes
Combinational logic check if bits is prime
There is no known regularity in the primes, and for small numbers (such as 8 bits naturals), the best is to implement them as a table.
If you want an instant answer, one comparator per prime can do. ...
- 8,777
5
votes
Is it provably true/false that for a program, there exists a proof whether it halts or not?
Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it ...
- 201
5
votes
Accepted
How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?
Algorithm design is known to be an art. There is no magical recipe. It all depends on the mathematical properties of the problems addressed.
In the case of sorting, the designers were helped by a few ...
- 8,777
4
votes
Using hypercomputation for "impossible" problems?
Nope.
Russell's paradox and the liar's paradox aren't undecidable. They aren't even decision problems.
As far as we know, hypercomputers don't exist. They are an imaginary idea that don't appear ...
D.W.♦
- 152k
4
votes
Can we accept that all axioms are equivalent?
What you have discovered is that any two true propositions are logically equivalent (you do not need them to be axioms in your argument, only that they hold).
What may be confusing is that the truth ...
- 29.4k
4
votes
Accepted
Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$
What prevents me from treating the bottom part as if it was "$-\varphi \land \Gamma \implies \Delta$"?
Nothing prevents you! In fact, this is exactly the right idea. You can think of the ...
- 6,757
3
votes
Accepted
Is finding a Polytime reduction from $L_1$ to $L_2$ equivalent to proving $L_2 \in P \Rightarrow L_1 \in P$
No, this only works one way.
If there is a polynomial time reduction from $A$ to $B$, then $B \in P \implies A \in P$. This works irrespective of the what kind of languages $A$ and $B$ are.
The ...
- 111
3
votes
Accepted
What is the difference in heap configurations? Separation logic with CVC5 SMT solver
Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.
3
votes
Accepted
What defines a byte?
A "byte", as defined by the C and C++ standard, is the accessible unit of memory, and exactly large enough to hold one char, signed char, or unsigned char. It must be at least 8 bits, but ...
- 27.4k
3
votes
Accepted
3
votes
Accepted
Is any 2-CNF has 2-DNF representation?
How about $\phi = (x_1 \vee x_2) \wedge (x_1 \vee x_3) \wedge (x_1 \vee x_4)$? This formula is satisfied iff $x_1$ is true, or $x_2$, $x_3$, and $x_4$ are all true.
Suppose that $\phi$ had a $2$-DNF ...
- 26.4k
2
votes
Is it possible to write an AND gate using XOR gates?
No
Consider W the set of the functions that maps {0, 1}×{0, 1} to {0, 1}. For example, the AND gate (denoted by ^) and the XOR gate (denoted by ⊕) are elements of W.
Now, for f ∈ W, define Val(f) in ...
2
votes
If computers only work with intuitionistic/constructivist logic, so how it works with binary code?
If I were to attempt to make a computing analogue of this question, it would be this: instead of relating 0 and 1 with 'false' and 'true', suppose we called them 'diverge' and 'halt'. Now by encoding ...
- 2,319
2
votes
Accepted
Formal language rewrite rules: strange notation
Yes, I think that's basically the intent. I guess the book is trying to write grammars without grammatical symbols. For me, it's abuse of notation, but that's pretty common.
Because there is no formal ...
- 11.7k
2
votes
Accepted
substitution of same variable in context-free grammars
As you suspect probably, theorem 6.1 still holds even if $A$ and $B$ are the same variable. This can be seen by following the proof of the theorem, assuming $B$ is $A$.
So, it is not correct to say &...
- 38.2k
2
votes
How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?
Bubblesort to Quicksort requires some cleverness, but is a quite natural progression.
First, you implement Bubblesort, and you find that for 100,000 random items it is indeed very slow. 100,000^2 ...
- 27.4k
2
votes
How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?
No matter how much one optimizes its code, a bad algorithm will always be bad.
The key to great software is starting with a great algorithm.
What distinguishes an algorithm is something that makes it ...
- 297
2
votes
Accepted
What is the proper way to write logic formula, say concerning graph theory?
The standard logical notation I have seen among computer scientists for saying there exists $x \in X$ such that $\varphi(x)$ holds is to write
$$\exists x \in X . \varphi(x).$$
In other words, we use ...
D.W.♦
- 152k
2
votes
Combinational logic check if bits is prime
Of course, the circuit will just grow rapidly. For 8 bits there is no problem.
You check whether bit 0 is 0 or 1. If it is 0, then you check whether the input is 2.
If it is 1, then you check bit 7. ...
- 27.4k
2
votes
Accepted
Why do simple Logical Gates have an Irrational amount of Bits?
An amount of information does not need to be an integer, just like the weight of an object does not need to be an integer number of grams.
One might see as a source of confusion to give the same name ...
- 8,777
1
vote
How do you write a logic function to determine if one 2s complement binary number is less than another?
This page shows you the formula for a one-bit subtractor with borrows in and out. You can use this as a building block for a three-bits subtractor:
https://www.geeksforgeeks.org/full-subtractor-in-...
- 8,777
1
vote
What is the Kripke semantic for a linear temporal logic?
tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind.
Details:
Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
- 479
1
vote
Accepted
Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$
Since you are asking to find any inhabitant, how about $\lambda (x : A). \lambda y : B(x). A$?
In other words, we take $P := \lambda (u : A) . \lambda (v : B u) . A$. It looks like part of your ...
- 29.4k
1
vote
K in SKI combinator calculus: why doesn't it take one parameter since it ignores its second?
Maybe it would help to think about it comparing to functions:
$K$ can be interpreted as the function with two arguments that returns the first. In Python, it would be
...
- 12k
1
vote
Accepted
Proof that propositional resolution is refutation complete
There is an error in the example: $S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$ is actually satisfiable. Every interpretation $I$ that sends $p_1$ to $true$ actually works.
With this in mind, notice ...
- 300
1
vote
Does quantum computing imply LPO?
No, this is not possible. It is known that Turing machines can simulate quantum machines (albeit very inefficiently). If there were a quantum machine that realized LPO then we could simulate it on a ...
- 29.4k
1
vote
"Largest set" in coinductive definitions
I think the precise definition of a final coalgebra might help.
Fix a set of symbols $\Sigma$. For any set $X$ define $F(X) = \Sigma \times X$, and for any $f : X \to Y$ let $F(f) : F(X) \to F(Y)$ be ...
- 29.4k
1
vote
"Largest set" in coinductive definitions
Here is a tentative self-answer.
I think it must just be that there is an additional requirement that wasn't mentioned in the tutorials I read, namely that one of the destructors must apply to each ...
- 936
1
vote
Boolean Logic when one component switches from 0 to 1
Designing pure functions (i.e. output depends only on input) is called combinational logic, and designing stateful logic (i.e. a finite state machine) is called sequential logic. If you're working ...
- 20.2k
Only top scored, non community-wiki answers of a minimum length are eligible