Questions tagged [proofs]
Used for questions about existing or possible proofs of a specific theorem or conjecture
84
questions
3
votes
0
answers
60
views
What's the difference between "modular" and "compositional"?
When talking about reducing complexity in a software system, we often talk about making it "modular" by breaking it up into multiple modules that are all linked together to form the overall ...
29
votes
4
answers
5k
views
Implications of unprovability of $P\neq NP$
I was reading "Is P Versus NP Formally Independent?" but I got puzzled.
It is widely believed in complexity theory that $\mathsf{P} \neq \mathsf{NP}$. My question is about what if this is ...
- 332
4
votes
1
answer
185
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 ...
- 22.5k
0
votes
1
answer
119
views
Sources that prove solving 2-SAT with DP takes linear time
Would anyone have any sources that describe/an explanation of how solving 2-SAT using dynamic programming takes a linear amount of time? Can't seem to find a text that proves it in detail/formality. ...
- 2,723
0
votes
0
answers
20
views
Proof that Sufficiency and Caliberation by group are equivalent notions
I am currently reading through the Fairness and Machine Learning book and I have a problem understanding the proof of Proposition 1 in Chapter 3 (titled Classification) (https://fairmlbook.org/...
1
vote
1
answer
198
views
Uniqueness of the distribution maximizing the channel capacity
Setting: We look at a discrete memoryless channel which takes an input probability distribution acting over symbols in $\mathcal{X}$ to an output probability distribution over symbols in $\mathcal{Y}$....
- 23.9k
0
votes
1
answer
104
views
On the proof of $PP = P \iff \#P = FP$ in Arora & Barak (Lemma 17.7)
Introduction
I am currently studying chapter 17 (of the famous textbook by Arora & Barak [1]) on the complexity of counting and got stuck on the proof of Lemma 17.7, which states $\mathrm{PP} = \...
- 173
0
votes
0
answers
27
views
How can I show that {a,b}∗ & {a,b,c}∗ are in an equivalence relation using the CBS theorem?
I am perplexed about how can I use the CBS theorem to prove that $\{a,b\}^* \cong \{a,b,c\}^*$. I know that for an injection $h : \{a,b,c\}^* \rightarrow \{a,b\}^*$ we can use two-letter codes for a,...
5
votes
1
answer
164
views
Establishing competing memory limits for pushdown automata
Let $L$ be the language of all even-length strings whose first half is a palindrome.
Let $L$ be the language of all even length strings whose first half is imbalanced—with an unequal number of $\...
- 8,234
0
votes
0
answers
61
views
A fundamental question about the proof by induction in session types
I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma:
$$
\text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X.
Q ~~\text{then}~~ \...
- 109
8
votes
1
answer
136
views
Construction of arbitrary functions with exponential-size $MODp \circ MODq$ circuits
It is mentioned in multiple papers [1], [2] that $MODp \circ MODq$ circuits for two distinct primes $p, q$ can compute arbitrary functions in exponential size. However, [1] provides no citation for ...
- 15.6k
4
votes
0
answers
179
views
Any problems for which we know the complexity, but no algorithms with the same time?
I suddenly found myself wondering if there are any problems for which the complexity (time or space or anything else) is proven, say to be O(n^2), but for which the best known algorithms are worse ...
- 59
4
votes
2
answers
100
views
Proving that a given formula in LTL is the smallest way to express it
I am looking for a way to prove that a given LTL formula is expressed with the fewest number of temporal operators possible.
I would like to do this to compare the expressive length with other ...
- 1,165
3
votes
1
answer
358
views
How hard is this combinatorial optimisation problem?
Suppose we have multiple intervals $R_1,R_2,...,R_i$ of non-negative integers. These intervals may overlap and we use $R_h(\mathrm{median})$ to denote the median integer in the $h$-th interval $R_h$, ...
- 2,758
4
votes
3
answers
404
views
Proving proof system properties within the proof system itself?
While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas:
$$\begin{...
- 15.6k
57
votes
18
answers
2k
views
Where and how did computers help prove a theorem?
The purposes of this question is to collect examples from theoretical computer science where the systematic use of computers was helpful
in building a conjecture that lead to a theorem,
falsifying a ...
- 5,624
12
votes
4
answers
4k
views
Proof of Levenshtein distance
In the article Levenshtein distance Wikipedia says about the proof of invariant that:
This proof fails to validate that the number placed in d[i,j] is in
fact minimal; this is more difficult to ...
- 7,175
94
votes
9
answers
19k
views
What would it mean to disprove Church-Turing thesis?
Sorry for the catchy title. I want to understand, what should one have to do to disprove the Church-Turing thesis? Somewhere I read it's mathematically impossible to do it! Why?
Turing, Rosser etc ...
19
votes
3
answers
927
views
Examples of the value of proofs for algorithms
In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to prove things about algorithms. (For many students, at least in many US ...
- 5,624
7
votes
1
answer
193
views
Document references describing weaknesses for cutting planes and algebraic proof system?
Here, Fortnow says (section 4.3):
Since then complexity theorists have shown similar weaknesses in a number of other proof systems including cutting planes, algebraic proof systems based on ...
- 196
16
votes
2
answers
989
views
Complexity of counting the number of edge covers of a graph
An edge cover is a subset of edges of a graph such that every vertex of the graph is adjacent to at least one edge of the cover. The following two papers say that counting edge covers is #P-complete: ...
- 8,234
7
votes
1
answer
399
views
Where is the quote "Informal proofs are algorithms, formal proofs are code" from?
Does anyone know the origin of the quote,
Informal proofs are algorithms; formal proofs are code.
Its made in Benjamin C. Pierce et al.'s Software Foundations.
- 594
29
votes
1
answer
4k
views
What's the status of Babai's Graph isomorphism result?
It's been over a year since his January 2017 retraction and correction.
Is there news?
If not is this normal for validation to take this long? I would expect it would get plenty of attention.
Has ...
- 15.6k
13
votes
2
answers
1k
views
An Interactive Proof of God's Number?
I've been learning about interactive proofs lately and I've been wondering if the whole thing was nothing more than a theoretical curiosity, or if it had any practical applications. I thought I'd ...
- 957
-1
votes
1
answer
69
views
Formally prove that the loops of this sorting algorithm will terminate [closed]
Given is the sorting algorithm Bubblesort
...
1
vote
0
answers
324
views
EXPSPACE proof and its implications
I'm dealing with the min-max regret 0-1 Integer Linear Programming problem (MMR-ILP, for short), which is formulated as below.
\begin{equation} \label{eq:nip_obj}
\min_{x \in \Phi} \sum_{i = 1}^n ...
- 185
3
votes
1
answer
682
views
Possible to do Complexity theory with only counting and Pigeonhole
Most of the proofs in the book Computational complexity by Barak and Arora seem to be Pigeonhole in disguise. What are some places in Complexity theory where counting and Pigeonhole was insufficient ...
- 12.6k
10
votes
0
answers
256
views
How would proof of the Lindelöf hypothesis improve our understanding of computational complexity classes?
A recent press release from the Viterbi School of Engineering at USC discussed the proof of the Lindelöf hypothesis by Athanassios Fokas, a visiting professor from the Department of Applied ...
- 233
1
vote
0
answers
137
views
Proof of Sipser-Lautmann Theorem
I have written the following answer as an attempt to prove a variation of Sispser-Lautmann theorem, but it was rejected without any comments. I would appreciate if anyone can find the flaws in this ...
- 21
15
votes
1
answer
1k
views
Examples of algorithms and proofs that seem correct, but aren't
In my intro to programming course, we're learning about the Initialization-Maintenance-Termination method of proving an algorithm does what we expect it to. But we've only had to prove that an ...
- 9,545
23
votes
4
answers
6k
views
Proof of the pumping lemma for context-free languages using pushdown automata
The pumping lemma for regular languages can be proved by considering a finite state automaton which recognizes the language studied, picking a string with a length greater than its number of states, ...
- 1,141
2
votes
1
answer
447
views
Paxos made simple, invariant P2c
I am reading
Leslie Lamport's Paxos Made Simple paper.
Can someone explain why $P2^c$ implies $P2^b$?
$P2^b$ If a proposal with value $v$ is chosen,
then every higher-numbered proposal issued ...
- 101
3
votes
2
answers
667
views
Formally proving no algorithm exists [closed]
Are there standard techniques to show that no algorithms exist for given complexity constraints?
For example, consider the following problem. The input is a list of items with exactly one duplicate, ...
- 2,758
2
votes
0
answers
216
views
Graph optimization problem with multiple objectives/constraints
Let's assume that we have a directed acyclic graph $G = (V, E)$, non-negative vertex weight functions $w_a(v)$ and $w_b(v)$, and a non-negative edge weight function $t(u,v)$. We can divide vertices in ...
CommunityBot
- 1
4
votes
1
answer
481
views
Proof that the graph optimization problem is NP-hard
I'm trying to prove that the following optimization problem is NP-hard:
Given a graph $G=(V,E)$, non-negative vertex weight functions $w(v)$ and $s(v)$, and a non-negative edge weight function $t(u,v)...
- 126
8
votes
1
answer
141
views
How to prove relations between "classes" of types?
After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System.
In ...
- 10.6k
25
votes
4
answers
2k
views
Proofs, Barriers and P vs NP
It is well known that any proof resolving the P vs NP question must overcome relativization, natural proofs and algebrization barriers. The following diagram partitions the "proof space" into ...
- 21.4k
1
vote
2
answers
217
views
Are equalizers of regular functions always regular languages? (My guess is no because PCP, but...)
Edit: I originally defined a regular function as a function computable by a Mealy machine, but Denis pointed out that that was a weaker model than what I was thinking of.
So to be more precise, by a "...
- 420
3
votes
0
answers
233
views
New proofs from "The Book" [closed]
The book "Proofs from The Book", referencing Erdős' notion of God's book, which contains the most beautiful proofs, was published in 1998.
Are there any new proofs that should be considered for "...
- 5,511
14
votes
1
answer
637
views
How is the MA version of SETH proven to be false?
According to this paper, which discusses a nondeterministic extension of the Strong Exponential Time Hypothesis (SETH), "[…] Williams has recently shown related hypotheses about Merlin-Arthur ...
- 26.7k
11
votes
2
answers
2k
views
On the provability of P versus NP
First of all, my understanding on Gödel's incompleteness theorem (and formal logic in general) is very naive, also is my knowledge on theoretical computer science (meaning only one graduate course ...
CommunityBot
- 1
1
vote
0
answers
69
views
Looking for reference proving polynomial-time bounds for A* search under specific conditions
In the textbook "Artificial Intelligence - A Modern Approach" (Russel, Norvig), it mentions that a sufficient criteria for the A* search algorithm to complete in polynomial time is for the heuristic ...
- 415
8
votes
3
answers
561
views
Would a proof assuming a physical law be considered sufficient?
I've always wondered if proofs in computer science would be considered sufficient proofs of the proposition if they needed to assume physical laws?
For example, I'm wondering what would happen if ...
- 10.9k
8
votes
1
answer
605
views
Humanifying computer-generated or computer assisted proofs
I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post ...
- 10.6k
-1
votes
1
answer
166
views
Undecidable Single Programs [closed]
So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate.
But suppose I start listing out ...
- 1,082
1
vote
0
answers
117
views
Minimum size counter-example in a 2-machine scheduling problem proof
I'm confused about something in the main proof in this paper (sorry that it's behind a paywall, but I assume many people on here have access to such things through their university and my posting the ...
- 111
13
votes
1
answer
1k
views
Correctness proofs of classic Paxos and Fast Paxos
I am reading the "Fast Paxos" paper by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos.
For consistency, the value $v$ picked by the coordinator in phase ...
- 2,329
0
votes
0
answers
210
views
Correctness proof of recursive-descent recognizer
Let G be a grammar that contains no left-recursive rules, and we use a recursive-descent recognizer that uses full backtracking, using list of results for example, to recognize strings of G.
How ...
- 376
1
vote
0
answers
70
views
Proof of convergence of alternative minimization/maximization [duplicate]
Given a problem
\begin{equation}
\max_{x\in X} \min_{y \in Y} f(x,y)
\end{equation}
where $f$ is strongly convex in $Y$ and strongly concave in $X$
How to show that the following iterative ...
CommunityBot
- 1
6
votes
1
answer
395
views
Would an optimal sorting network ever have to swap two numbers the "wrong" way
Intuitively it seems like an optimal (either minimum depth or minimum gates) sorting network should never have to compare-swap two numbers the "wrong" way (such that the larger one goes into the ...
- 23.9k