Questions that ask for or about correctness proofs of algorithms.

learn more… | top users | synonyms

0
votes
0answers
36 views

How does the induction proof work in this example?

Refer to answer 1.1 of this file: http://www.dei.unipd.it/~geppo/AA/DOCS/NPC.pdf From my understanding and this thread, http://math.stackexchange.com/a/928412, we need 3 steps for that proof. ...
4
votes
1answer
24 views

Is the inverse of MST cycle property always true? Why?

I am trying to find an algorithm which would check for each edge in a given weighted undirected graph whether it belongs to any of the graph's Minimum Spanning Trees. I have found many potential ...
0
votes
1answer
85 views

Algorithm for length of longest common subsequence

The case of multiple strings. A slight modification of the dynamic programming algorithm for two strings is used as a subroutine. Here is the pseudo code: ...
4
votes
2answers
39 views

Is bounded waiting ensured in given version of Dekker's solution for critical section problem?

William Stallings discuss various step by step process in developing Dekker's algorithm in his Operating Systems book. In process, he reaches to following version of algorithm (which is incomplete as ...
0
votes
0answers
17 views

Greedy algorithm correctness proof (UVA 10716)

Given an input string, not necessarily a palindrome, compute the number of swaps necessary to transform the string into a palindrome. By swap we mean reversing the order of two adjacent symbols (UVA ...
9
votes
2answers
176 views

How to prove greedy algorithm is correct

I have a greedy algorithm that I suspect might be correct, but I'm not sure. How do I check whether it is correct? What are the techniques to use for proving a greedy algorithm correct? Are there ...
0
votes
0answers
48 views

Checking for 4-cycles in a graph

I was reviewing some selected problems on algorithms and time complexity and the notes had the following exercise (ex. 4.3 from book Algorithms by Dasgupta, Vazirani, Papadimitriou): Design and ...
0
votes
0answers
17 views

Is there a minimum spanning tree including $e$ after removing at most $k$ edges?

Let an undirected, connected graph $G=(V,E)$ with the weight funciton $w:E\to \mathbb{R}$, an edge $e$, and $0<k\in\mathbb{N}$. Describe an algorithm determines if there are at most $k$ edges could ...
2
votes
1answer
64 views

Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
1
vote
2answers
32 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
24 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
33 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
82 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
70 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
207 views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
2
votes
0answers
57 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
1answer
141 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
35 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
187 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
41 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
36 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
79 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] = S[...
1
vote
2answers
92 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 finite-...
1
vote
1answer
105 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
206 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
74 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
72 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 languages,...
2
votes
1answer
76 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
91 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$ n-...
-2
votes
1answer
74 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
79 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
86 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 $h^{-1}(...
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
155 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
80 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
401 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
26 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
126 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
0
votes
0answers
95 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) = \begin{...
0
votes
1answer
36 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
47 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
90 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
191 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
2k 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
318 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 ...