Questions that ask for or about correctness proofs of algorithms.

learn more… | top users | synonyms

3
votes
1answer
39 views

Proof for Minimum number of insertions to convert a string to a palindrome

For the problem "Find the minimum number of insertions to convert a string $S$ to a palindrome", a recurrence relation usually given is: $$ c[i,j] = \begin{cases} c[i+1,j-1] & \text{if } S[i] = ...
1
vote
2answers
80 views

Can we enumerate provably non-terminating functions?

In trying to understand the Halting Problem better, I am trying to come up with classes of provably non-terminating programs. For example, any program (including input) which leads to a ...
1
vote
1answer
73 views

Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
1
vote
5answers
163 views

Correctness of the greedy algorithm

I am trying to solve the following problem: Given a matrix which consists of only 0's and 1's. Considering the matrix as a metal sheet, we need to "cut-out" square blocks of sizes 2x2 consisting of ...
0
votes
0answers
21 views

Method of inductive statements for proving partial correctness of block-schemes

I'm trying to find an explanation and more information on a method and some example problems with solutions using that method. The method doesn't seem to translate well in english (I'm from a ...
0
votes
1answer
40 views

Trouble finding loop invariant for this while loop

I'm having trouble coming up with an invariant for proving partial correctness of this function. ...
2
votes
0answers
61 views

Proof Carrying LLVM?

I am intrigued by and understand the very basics of Proof Carrying Code (PCC) and I recognize that LLVM is a machine-independent intermediate language. LLVM is the intermediate form of many ...
6
votes
2answers
71 views

Correctness of Freivald algorithm for checking matrix multiplication, why is the probability of checking $AB \neq C$ at least 1/2?

I am going to consider Freivald's algorithm in the field mod 2. So in this algorithm we want to check wether $$AB = C$$ and be correct with high probability. The algorithm choose a random $r$ ...
-2
votes
1answer
66 views

An algorithm for vertex cover

Let $G = (V,E) $ and let be $T \subseteq V$ . $T$ is called vertex cover if each edge of the graph is incident to at least one vertex of $T$ . Let be the following decisional problem : $PROBLEM$ ...
3
votes
1answer
57 views

If we sort a table column-wise and then row-wise why the table is still sorted column-wise?

Say we have a $n \times n$ table which elements are sorted column-wise, for example: $$ \left( \begin{array}{ccc} 2 & 4 & 1 \\ 3 & 5 & 6 \\ 7 & 9 & 8 \end{array} \right) $$ ...
1
vote
1answer
71 views

Homomorphism Languages

Let $h$ be a homomorphism and let $L$ be a language. Writing ${}^*$ for Kleene star, I want to show that $(h^{-1}(L))^* \neq h^{-1}(L^*)$. Can I prove this just by showing that we can have ...
3
votes
1answer
51 views

Inference rule with two conclusions or rather inverse function application

I want to express a simple correctness theorem for a term-desugaring function $\Delta$. The goal is to express that if the evaluation of a desugared term yields a value, this value is the desugared ...
3
votes
1answer
133 views

Minimizing inversions in an array with a single swap

This was asked in the (very) recently concluded Hackerrank Worldcup. Paraphrased: Given a permutation $a$ of integers from $1$ to $N$, how can I minimize the number of inversions by a single ...
1
vote
2answers
62 views

How to prove if an algorithm is reentrant?

I think, maybe some formalism could exist for the task which makes it significantly easier. My problem to solve is that I invented a reentrant algorithm for a task. It is relative simple (its pure ...
0
votes
1answer
184 views

Algorithm for constructing BST from post-order traversal

Given a post-order traversal of Binary Search tree with $k$ nodes, find an algorithm that constructs the BST. My Algortihm Let $n$ represent the next element to be inserted. Let $P(y)$ ...
0
votes
1answer
21 views

Proving equality between foldl recursive and iterative fold

Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative. I am looking for an algebraic proof that the two definitions are equal ideally ...
2
votes
2answers
90 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
0
votes
0answers
65 views

Proving a dynamic programming recurrence for coin exchange correct

Suppose I have $n$ kinds of coins $c_1, c_2, \dots, c_n$. I'm given: $S$, an amount of money I should construct with minimum number of coins. I came into the following formula: $$ T(n,S) = ...
0
votes
1answer
32 views

prove sufficient number of comparisons for the merge problem

It is given two subsequences. Their length are following: $2$ and $5$. I can show that lower bound of comparisons is $5$. My problem is that I can't show that $5$ is sufficient number of comparisons ...
3
votes
3answers
1k views

Why does this sort algorithm work?

The following O(n^2) sorting algorithm works but I can't figure out why. ...
-1
votes
1answer
39 views

Proving correctness of a recursive algorithm using induction

For the program mean(A,n) if n = 1 then return A[n] else return A[n]/n+mean(A,n-1)*(n-1)/n end Show that if the recursive call to ...
-2
votes
1answer
71 views

Using dynamic programming to find the number ofl increasing subsequences [closed]

I got this question today and I'm nowhere near the solution, Given a sequence of real numbers (X1, X2, ..,Xn). write an algorithm as efficient there is, that finds the number of strictly increasing ...
4
votes
1answer
142 views

Greedy algorithm correctness proof for “Elegant Permuted Sum” (UVa 11158)

Given a sequence of $2 \leq n \leq 50$ numbers $s = (s_1,s_2,...,s_n)$, find a permutation $a = (a_1,a_2,...,a_n)$ of $s$ such that $$\sum_{i=1}^{n-1} |a_i - a_{i+1}|$$ is maximized. I found many ...
0
votes
2answers
523 views

How does this Turing machine accept $a^n b^n$?

I'm reading this tutorial from the University of Illinois about Turing Machines, and I don't understand something. They give a pseudocode algorithm for an machine that accepts strings from the ...
1
vote
1answer
168 views

Complete examples of program correctness proofs

Does anyone have any complete example of a proof of program correctness? I'm talking about something that includes the usual predicate, base case, inductive hypothesis, and inductive step. But also ...
0
votes
1answer
36 views

Which element is at its final position after the partitioning step in Quicksort?

In Algorithms, 4th Edition, I read that after the partitioning step one element is in its final position. The entry a[j] is in its final place in the array, for some j. No entry in a[lo] ...
2
votes
1answer
202 views

Finding a good loop invariant

I want to prove that the following program is correct. The code takes an array i of length N and a number ...
2
votes
1answer
272 views

Updating an MST $T$ when the weight of an edge not in $T$ is decreased

Given an undirected, connected, weighted graph $G = (V,E,w)$ where $w$ is the weight function $w: E \to \mathbb{R}$ and a minimum spanning tree (MST) $T$ of $G$. Now we decrease the weight by $k$ ...
-1
votes
1answer
206 views

Prove that Ford-Fulkerson can decide if there is more than one min cuts

Probelm: Deciding whether a network flow graph has more than one min cut. Optimal running time: O(V^2*E). I trying to prove the correctness of the next algorithm: run Dinitz to find max-flow and ...
3
votes
0answers
44 views

How is Chinese Remainder Theorem used in the proof of correctness for RSA

Question At the very end of (most) proofs of RSA's correctness we have something like $$m^{ed}\equiv m\pmod p$$ $$m^{ed}\equiv m\pmod q$$ Therefore by the Chinese Remainder Theorem (CRT) ...
0
votes
2answers
146 views

Counter example to graph coloring heuristic using BFS

I am considering the following heuristic for the graph coloring problem (i.e. to color a graph $G$ using a minimal number of colors so that no two adjacent vertices have the same color): Explore ...
3
votes
1answer
37 views

Seemingly non sequitur in proof

I'm trying to understand a small proof in an article about computing lumpability on Markov chains. There is a small detail that I cannot understand, i.e. I don't think it follows from the argument. ...
0
votes
1answer
223 views

People crossing a bridge (a proof for a greedy algorithm)

The problem Some people are crossing a bridge. Each one takes a different time to pass. Assume the people are sorted by their passing time increasingly. These are the conditions of crossing the ...
0
votes
2answers
327 views

Why do these recurrences determine the number of ways of tiling a 3xN rectangle with 2x1 dominoes?

http://www.algorithmist.com/index.php/UVa_10918 The above link is a solution to UVa 10918 Problem. The problem is based on Dynamic Programming. I am not able to understand this approach to the ...
0
votes
0answers
100 views

Proving the correctness of the CKMS algorithm for biased quantiles

I'm trying to prove the correctness of my implementation of the CKMS algorithm from "Effective Computation of Biased Quantiles over Data Streams" and I'm having trouble showing that my implementation ...
1
vote
1answer
365 views

provability of while loop vs for loop [closed]

I'm abit afraid to ask this question here seeing as I asked it on programmers SE already, the thing is I think the question is more about the underlying theory than the use in practice (or call it ...
1
vote
2answers
67 views

Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
4
votes
0answers
248 views

Suurballe's Algorithm: Proof of Correctness

I was reading about Suurballe's algorithm on Wikipedia, for the shortest edge-disjoint paths problem, i.e. given nodes $s$ and $t$ finding a pair of paths between these nodes, whose accumulated weight ...
18
votes
2answers
1k views

Are there programs that never halt and have no non-termination proof?

Like black holes in computer science. We can only know they exist but when we have one of them we will never know it's one of them.
4
votes
1answer
434 views

Is there a flaw in this Wikipedia proof of cycle property of Minimum Spanning Tree?

On wikipedia, there is a proof for the cycle property of the Minimum Spanning Tree as follows: Cycle Property: For any cycle C in the graph, if the weight of an edge e of C is larger than the ...
1
vote
0answers
79 views

Proof of Randomized Self-Adjusting Binary Search Tree

I developed a randomized self-adjusting binary search tree years ago, which I called a shuffle tree, but was unable to ever have it published because my proofs were rejected (with little explanation). ...
2
votes
2answers
147 views

How to go about proving an algorithm correct?

The algorithm (called as rmax(1,n)) finds the maximum of a list of numbers contained in an array S[1..n]. ...
3
votes
2answers
429 views

Binary Indexed Trees: Why does i & -i work?

I already read this related question on the intuition behind binary indexed trees, and while the answer explains how the tree structure works, it does not really explain how this correlates back to ...
0
votes
1answer
133 views

Understanding a proof in the sweep line algorithm when finding all line segment intersections

You have a set of line segments and you want to find all intersections. First sweep line approach: Use a priority queue Q for the events as they come, where each ...
3
votes
3answers
697 views

Rigorous Proof of Insertion Sort

Currently I self study CLRS book (Outside of any course, so I got no access to an instructor) And I am stuck proving Insertion Sort, The proof in CLRS book is not so formal. Here's the algorithm: ...
0
votes
0answers
108 views

stuck on proving the optimality of a greedy algorithm [closed]

I'm Ph.D. student doing research in wireless networks. My past projects are more oriented to systems than theory. For my current project, I devised a greedy algorithm for an optimization problem. ...
1
vote
1answer
113 views

Proving correctness of an AVL-Tree colouring algorithm

I came up with the following recursive algorithm to colour the nodes of an AVL tree so that the resulting tree is red-black. The logic is that the algorithm first colours the root and, recursively, ...
5
votes
1answer
487 views

Proving optimality of a dynamic programming algorithm

We have a string $s$ containing $n \leq 100$ bits. The move we can make on it is erasing from $s$ some substring $x$, but only if $x$ is directly preceded by $x^R$, where $x^R$ means string $x$ ...
0
votes
2answers
111 views

How to show that this algorithm for evaluating polynomials works?

I'm having trouble showing how to solve this problem in particular the part where it asks "To Show that the following pseudo-code fragment finds the value of the polynomial..." How do I exactly show ...
0
votes
2answers
118 views

Hoare Calculus Incorrect Assignment Axiom

I'm currently preparing for an exam and recently came across the following exercise and would like to know whether my solution would be correct. Exercise: Prove that the following axiom is not ...