Questions that ask for or about correctness proofs of algorithms.

learn more… | top users | synonyms

0
votes
0answers
30 views

Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
1
vote
1answer
27 views

What is the point of the “respect” requirement in cut property of minimum spanning tree?

The cut property stated in terms of Theorem 23.1 in Section 23.1 of CLRS (2nd edition) is as follows. Theorem 23.1 Let $G = (V, E)$ be a connected, undirected graph with a real-valued weight ...
1
vote
1answer
18 views

Proof of 0/1 knapsack optimal substructure

I'm trying to understand why exactly the 0/1 knapsack problem actually has the optimal substructure property. Let $E$ be the set of items to consider and $v$ and $w$ the value and weight functions ...
1
vote
0answers
32 views

I need help understanding how to prove partial correctness

Please help me understand how I would prove the partial correctness of the below pseudocode with respect to the following predicates: Pre: {n>=0} Post: ...
1
vote
1answer
81 views

How to use the concept of loop invariant to reduce errors in loops?

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example ...
2
votes
1answer
62 views

How to find loop invariant from weakest precondition?

Consider this code: Precondition: Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key ...
4
votes
3answers
206 views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
1
vote
0answers
49 views

Modal logic axiom S4, transitive and reflexive frame, tableaux solver

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful: S4 axiom is a class of transitive ...
3
votes
0answers
72 views

Proof of correctness of A star search algorithm

I've been looking for the proof of correctness for the A star (A*) algorithm but none of the texts and websites offer it. Mostly they are talking about the proof of optimality of the A* algorithm. I'm ...
0
votes
0answers
33 views

simple iterate algorithm proof by induction

Suppose I have a function where it calculates which bit is larger called LargerBinary. Let's say I have an input 110111;101001, the output will be 110111 and if the input is 110110:110110, the output ...
1
vote
1answer
47 views

Validate that a threaded binary tree works as intended

I am attempting to validate that my threaded binary tree’s insertion and deletion works as intended. Would it be safe to assume that the following procedure would have tested all corner cases at ...
1
vote
1answer
132 views

Proof by Reduction: From Empty Language to Halting Problem on Empty Input

Question: Let language $E$ = {$\langle M \rangle$ | $M$ accepts no inputs whatsoever} Let language $H$ = { $\langle M \rangle$ | $M$ halts on an empty string input}. Is it possible to show that $H$ ...
0
votes
0answers
37 views

Longest double increasing subsequence (LIS variant)

I'll start with the definitions:Let $S = s_1s_2...s_n$ be a sequence of $n$ integers. A double increasing subsequence of $S$ is a sequence $P=p_1p_2...p_k$ (not necessarily continuous) where for each ...
3
votes
2answers
16 views

Can I use the set of “used arguments values” as a memoization key for a deterministic function?

I have a deterministic function $f(x_1, x_2, ..., x_n)$ that takes $n$ arguments. Given a set of arguments $X = (x_i)$, I can compute $U_X = \{ i \in [1, n] : x_i \text{ was read during the ...
2
votes
1answer
30 views

Quicksort $T(n)_{best}=\Omega(n\log n) $ proof

About the proof that quicksort has $T(n)_{best}=\Omega(n\log n)$. I can't find this specific aspect anywhere online which is strange. I'm going through a proof for this in a book and I don't ...
1
vote
2answers
53 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
3
votes
1answer
61 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
88 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
94 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
200 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
22 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
2answers
69 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
70 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 ...
0
votes
1answer
63 views

CLRS Rod Cutting Inductive proof

I'd like to preface this question by saying that it is not a homework question. However, it is a question regarding the course material. In the rod-cutting example an equation is presented to ...
6
votes
2answers
87 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
71 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
73 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
85 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
52 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
150 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
70 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
335 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
25 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
120 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
0
votes
0answers
89 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
35 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
46 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
82 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
166 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
1k 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
264 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
40 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
220 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
507 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
303 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
49 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
186 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
41 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
405 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 ...