__NOTOC__
[[Category:Checkup]]
[[Category:Abstract Data Structure]]
[[Category:Sequence]]

== General information ==
'''Representation invariant:'''
# This abstract data structure is [[Genericity|generic]] and parameterized by a fixed '''key type''' <math>\mathcal{K}</math> and a fixed [[comparison]] <math>c</math> defined on <math>\mathcal{K}</math>.
# An object with key type <math>\mathcal{K}</math> represents a finite, dynamically changing [[multiset]], of elements of type <math>\mathcal{K}</math> (the multiset may be empty).
# An object has two additional attributes, which are natural numbers:
## Attribute <math>n</math> stores the current number of elements (in particular, <math>n</math> is dynamically changing).
## Attribute <math>N_\text{max}\in\mathrm{N}</math> is the maximum number of elements that can be stored in the queue (<math>N_\text{max}</math> is constant throughout the object's life time).
# Therefore, at any moment, it is <math>n\le N_\text{max}</math>.
'''Constructor:''' Gets a [[comparison]] <math>c</math> and a natural number <math>N_\text{max}</math>, and initializes the queue so as to be empty with a maximum capacity of <math>N_\text{max}</math> items.

== Method ==
'''Name:''' insert

'''Input:''' A key <math>K\in N_\text{max}</math>

'''Output:''' A unique ID (natural number), which is permanently associated with the inserted key, until the key is extracted from the queue.

'''Precondition:''' It is <math>n<N_\text{max}</math>.

'''Postcondition:''' The input key <math>K</math> is inserted into the queue (a.k.a. ''enqueued'').

== Method ==
'''Name:''' extract minimum

'''Input:''' -

'''Output:''' Returns the minimum key <math>K</math> that is currently stored in the queue.

'''Precondition:''' It is <math>n>0</math>.

'''Postcondition:''' For the minimum key currently stored in the queue, one occurrence is removed (a.k.a. ''dequeued'').

== Method ==
'''Name:''' find minimum

'''Input:''' -

'''Output:''' Returns the minimum key <math>K</math> currently stored in the queue.

'''Precondition:''' It is <math>n>0</math>.

'''Postcondition:''' -

== Method ==
'''Name:''' decrease key

'''Input:''' A natural number <math>ID</math> and a real number <math>x</math>.

'''Output:''' -

'''Precondition:'''
# The input is the ID of some queue element (returned on insertion).
# The value of <math>x</math> is not larger than the current value of the key to which ID refers.

'''Postcondition:''' The key to which ID refers is now <math>x</math> (the old value of that key is lost).

== Method ==
'''Name:''' number

'''Input:''' -

'''Output:''' The value of attribute <math>n</math>, that is, the number of keys currently stored in the queue.

'''Precondition:''' -

'''Postcondition:''' -

== Known implementations ==
[[Heap as array]]

== Remark ==

== Reference ==

Binary search tree: find

2014-10-02T22:07:26Z

Jhohmann: /* General Information */

[[Category:Binary_Search_Tree]]
[[Category:Algorithm]]
<div class="plainlinks" style="float:right;margin:0 0 5px 5px; border:1px solid #AAAAAA; width:auto; padding:1em; margin: 0px 0px 1em 1em;">
<div style="font-size: 1.8em;font-weight:bold;text-align: center;margin:0.2em 0 1em 0">Binary Search Tree<br>Find</div>

<div style="font-size: 1.2em; margin:.5em 0 1em 0; text-align:center">[[Sorted sequence]]</div>

<div style="font-size: 1.2em; margin:.5em 0 .5em 0;text-align:center">[[File:olw_logo1.png|20px]][https://openlearnware.tu-darmstadt.de/#!/resource/binary-search-tree-1938 Openlearnware]<br>See Chapter 2,3</div>
</div>
== General Information ==

'''Algorithmic Problem:''' [[Sorted sequence#Find|Sorted Sequence:find]]

'''Type of algorithm:''' loop

'''Auxiliary data:''' A pointer '''''p''''' of type "pointer to binary search tree node of type <math>\kappa</math>".

== Abstract view ==
'''Invariant:''' After <math>i\geq 0</math> Iterations.
# The pointer '''''p''''' points to a tree node '''''v''''' on height level '''''i''''' (or is void).
# The key '''''K''''' is in the range of '''''v'''''.
'''Variant:''' '''''i''''' is increased by 1.

'''Break condition:''' Either it is <math>p = void</math> or, otherwise, <math>p.key = K</math>.
== Induction basis ==
'''Abstract view:''' Set '''''p''''':= '''''root'''''.

'''Implementation:''' Obvious

'''Proof:''' Nothing to show

== Induction step ==
'''Abstract view:''' If '''''p''''' points to a node but not with key '''''K''''', '''''p''''' descends in the appropriate direction, left or right.

'''Implementation:'''
# If <math>p = void</math>, terminate the algorithm and return '''''false'''''.
# Otherwise, if <math>p.key = K</math>, terminate the algorithm and return '''''true'''''.
# Otherwise:
## If <math>K < p.key</math>, set <math>p := left</math>.
## If <math>K > p.key</math>, set <math>p := right</math>.

'''Correctnes:''' Obvious.

== Complexity ==
'''Statement:''' Linear in the length of the sequence in the worst case (more precisely, linear in the height of the tree).
[[File:wcbst.png|300px|thumb|right|Worst case binary search tree]]
'''Proof:''' Obvious.

== Pseudocode ==
TREE-SEARCH (x, k)
:if x= NIL or k = key[x]
::then return x
:if k < key[x]
::then return TREE-SEARCH(left[x], k)
:else return TREE-SEARCH(right[x], k)

Bucketsort

2014-10-02T22:04:39Z

2014-10-02T11:28:07Z

Jhohmann: /* Induction Basis */

[[Category:B-Tree]]
[[Category:Algorithm]]
== General Information ==
'''Algorithmic problem:''' See B-Tree

'''Prerequisites:'''
# A node <math>p</math> with a key at position <math>k</math> that is not void
# The number of keys in <math>p.children[k-1]=p.children[k]=M-1</math>

'''Type of algorithm:''' loop

'''Auxiliary data:'''
# Three pointers <math>p, p_1, p_2 </math> of type "pointer to B-tree node".

== Abstract View ==
'''Invariant:''' After <math> i \ge 0</math> iterations:
# <math> p_1</math> points to the left children of the key of <math>p</math> at position <math>k</math> and <math>p_2</math> points to the right children of the key of <math>p</math> at position <math>k</math>.
# <math>p_1.n = M+i</math>.
# <math>i</math> shows on the index of the copied key in <math>p_2</math>.

'''Variant:''' <math>i</math> increases by <math>1</math>.

'''Break condition:''' <math>i=M-1</math>

== Induction Basis ==
=== Abstract view: ===
# Assign <math>p_1</math> the left children of <math>p</math> at position <math>k</math> and <math>p_2</math> the right children of <math>p</math> at position <math>k</math>.
# Move the key from <math>p</math> at position <math>k</math> to <math>p_1</math> at position <math>M</math>.
# Copy the left children of <math>p_2</math> to the new key in <math>p1</math> at position <math>M</math>
# Change the number of keys in <math>p_1</math> and <math>p</math>.

=== Implementation: ===
# Set <math>p_1 := p.children[k-1]</math> and <math>p_2 := p.children[k]</math> and <math>p.children[k] := void</math>.
# Set <math>p_1.keys[M] := p.keys[k]</math> and for <math>j \in k+1, \dots , p.n</math> (in this order), set <math>p.keys[j-1] := p.keys[j]</math>
# Set <math>p_1.children[M] := p_2.children[0]</math>
# Set <math>p_1.n := p_1.n+1</math> and set <math>p.n := p.n-1</math>

=== Proof: ===
In the induction basic <math>p_1</math> and <math>p_2</math> are assigned to the left and the right children of the key of <math>p</math> at position <math>k</math> (Invariant 1). The key of <math>p</math> at position <math>k</math> is shifted to <math>p_1</math> at position <math>M</math>. So the elements <math>1 \dots , M</math> are filled (B-Tree #5). The number of elements in <math>p_1</math> is increased by one and <math>p</math> is decreased by one (B-Tree #3). So are in <math>p_1 M</math> keys (Invariant 2). We removed a key of <math>p</math>, but because of the invariant of remove (<math>minM</math> keys in <math></math>), now we have <math>minM - 1</math> keys in <math>p</math> (B-Tree #4). We added the key from <math>p</math> to the left children (all keys in this children are smaller) on the right side, so the sorting order is correct again (B-Tree #6). The copied children comes from the right children, so all keys in this children are bigger again (B-Tree #7). The copied children come from the same level (<math>p_1</math> and <math>p_2</math> are both children of <math>p</math>), so all leaves are on the same level again (B-Tree #8). In the induction basic is no key copied from <math>p_2</math> (Invariant 3).

== Induction Step ==
'''Abstract view:'''
# If not all keys (and children) of <math>p_2</math> are copied, copy the key and children from position <math>i</math> of <math>p_2</math> to position <math>M+i</math> of <math>p_1</math>.
# Otherwise, terminate the algorithm.

'''Implementation:'''
# if <math>i \le M-1</math> (that is, not all keys of <math>p_2</math> are copied):
## <math>p_1.keys[M+i] := p_2.keys[i].</math>
## <math>p_1.children[M+i] := p_2.children[i].</math>
## <math>p_1.n := p_1.n+1</math>
# Otherwise, terminate the algorithm.

'''Correctness:''' In the induction step we copy a key and a children from <math>p_2</math> to <math>p_1</math>. The copy is in the same order as the elements and on the same level. Implementation invariants #1, #2, #4, #6, #7 and #8 are trivially fulfilled. In step 1.3 we increase <math>p_1.n</math> by one for each copied element (B-Tree #3).

== Complexity ==

'''Statement:''' Linear in <math>M-1</math> steps in the best and worst case

'''Proof:''' Obvious.

2014-10-01T06:18:23Z

Jhohmann:

[[Category:Checkup]]

[[Category:B-Tree]]
[[Category:Algorithm]]
== General Information ==
'''Algorithmic problem:''' [[Sorted sequence#Remove|Sorted sequence: remove]]

'''Type of algorithm:''' loop

'''Auxiliary data:'''
## Pointers, <math>p</math>, <math>p'</math>, <math>p_1</math> and <math>p_2</math> of type "pointer to B-tree node".
## A Boolean variable '''''found''''', which is '''''false''''', in the beginning and set '''''true''''' once the key <math>K</math> to be removed is seen.

== Abstract View ==

'''Invariant:'''
# <math>p</math> points to a node of the B-tree.
# If <math>found = false</math>, <math>K</math> is in the [[Directed Tree#Ranges of Search Tree Nodes|range]] of the node to which <math>p</math> points.
# It is <math>found = true</math> if, and only if, <math>K</math> is contained at least once in one of the current nodes of previous iterations.
# If <math>found = true</math>
## <math>p'</math> points to a node where <math>K</math> is currently stored.
## The [[Directed Tree#Order of Tree Nodes|immediate predecessor]] of <math>K</math> is in the [[Directed Tree#Ranges of Search Tree Nodes|range]] of the node to which <math>p</math> points.
# If <math>p</math> points to the root, at least two keys are currently stored in the root; otherwise, at least <math>M</math> keys are currently stored in the node to which <math>p</math> points.

'''Variant:''' <math>p</math> is redirected to a node one level deeper.

'''Break condition:''' <math>p</math> points to a leaf.

== Induction Basis ==

=== Abstract view: ===

# If the tree is empty, terminate the algorithm and return '''''false'''''
# The pointer <math>p</math> is initialized so as to point to the root <math>N</math>
# If <math>N</math> is a leaf:
## Remove <math>K</math> if contained in <math>N</math>.
## If <math>N</math> is empty now, make the tree empty.
## Terminate the algorithm and return '''''true''''' if <math>K</math> was contained in <math>N</math>, '''''false''''' otherwise.
# Otherwise, if <math>N</math> contains exactly one key and is not a leaf: rearrange the root and its two children appropriately.

=== Implementation: ===

# If the tree is empty, terminate the algorithm and return '''''false'''''.
# Let <math>p</math> point to the root.
# If <math>p.children[0] = void</math> (that is, the root is a leaf):
## If <math>K</math> is contained in the root, say at position <math>k</math>:
### Remove the occurrence of <math>K</math> at position <math>k</math>.
### If the root is empty now, make the tree an empty tree.
### Otherwise (that is, the root is still non-empty):
#### For <math>j \in \{k+1,\dots,p.n\}</math> (in this order), set <math>p.keys[j-1] := p.keys[j]</math>.
#### Set <math>p.n := p.n - 1</math>.
### Terminate the algorithm and return '''''true'''''
## Otherwise, terminate the algorithm and return '''''false'''''.
# If <math>p.n = 1</math>:
## If <math>p.children[0].n = p.children[1].n = M - 1</math>:
### Set <math>p.key[M] := p.key[1]</math>.
### Set <math>p_1 := p.children[0]</math> and </math>p_2 := p.children[1]</math>.
### Set <math>p.children[0] := p_1.children[0]</math> and <math>p.children[M] := p_2.children[0]</math>.
### For <math> j = 1,\dots,M-1</math> set <math>p.keys[j] := p_1.keys[j]</math>, <math>p.children[j] := p_1.children[j]</math>, <math>p.keys[M + j] := p_2.keys[j]</math>, and <math>p.children[M + j] := p_2.children[j]</math>.
### Set <math>p.n := 2M - 1</math>.
## Otherwise:
### If <math>K \leq p.keys[1]</math>:
#### If <math>p.children[0].n = M - 1</math>, call [[B-Tree:Shift_Key_to_Sibling]] with pointer <math>p</math>, index <math>1</math>, and <math>shiftRight = false</math>.
#### If <math>p.keys[1] = K<math>, set <math>p' := p</math> and <math>found := true</math>.
#### Set <math>p := p.children[0]</math>.
### Otherwise (that is, <math>K > p.key[1]</math>):
#### If <math>p.children[1].n = M - 1</math>, call [[B-Tree:Shift_Key_to_Sibling]] with pointer <math>p</math>, index <math>1</math>, and <math>shiftRight = true</math>.
#### If <math>p.keys[1] = K</math>, set <math>p' := p</math> and <math>found = true</math>.
#### Set <math>p := p.children[1]</math>.

=== Proof: ===

Basically, we have to verify that the [[B-Trees|implementation invariants of the B-tree data structure]] and the above-mentioned loop invariants of the removal procedure are fulfilled after the preprocessing.

If the tree is empty (Step 1), the proof is trivial, so consider the case that the tree is non-empty.

Implementation invariants #1, #2, and #8 are trivially fulfilled. Implementation invariants #3, #5, #6, and #7 are guaranteed by Steps 3.1.3 and 4.1.3-5 and by the postconditions of the subroutines called in Step 4.2, respectively. Implementation invariant #4 is guaranteed by Step 3.1.2 and the postconditions of the subroutines called in Step 4, respectively.

The loop invariants of the removal procedure are only affected if Step 4 is executed. Loop invariants #1, #2, and #3 are obvious, #4 does not apply, and #5 is guaranteed by the subroutines called in Step 4.

Obviously, the case distinction in Step 4 covers all possible cases.

== Induction Step ==

=== Abstract view: ===

# If a leaf is reached:
## If <math>K</math> is in that leaf, remove it.
## Otherwise, if <math>K</math> has already been seen, overwrite the found occurrence of <math>K</math> with its immediate predecessor (which is <math>p.keys[p.n]</math>).
## Terminate the algorithm
# Otherwise:
## Let <math>k \in \{0,\dots,p.n\}</math> such that <math>p.children[k]</math> is the next node where to descend.
## If <math>p.children[k].n = M - 1</math>, rearrange the current node at its children appropriately.
## Check whether <math>K</math> is in the current node.

=== Implementation: ===

# If <math>p.children[0] = void</math> (that is, <math>p</math> points to aleaf):
## If <math>K</math> is contained in that leaf:
### Let <math>k \in \{1,\dots,p.n\}</math> such that <math>p.keys[j-1] := p.keys[j]</math>.
### For <math>j \in \{k + 1,\dots,p.n\}</math> (in this order), set <math>p.keys[j-1] := p.keys[j]</math>.
### Remove the key at position <math>p.n</math> in the node pointed by <math>p</math>.
### Set <math>p.n := p.n - 1</math>.
### Terminate the algorithm and return '''''true'''''
## Otherwise, if <math>found</math>:
### Let <math>k \in \{1,\dots,p'.n\}</math> such that <math>p'.keys[k] = K</math>.
### Set <math>p'.keys[k] := p.keys[p.n]</math>.
### Remove the key at position <math>p.n</math> in the node pointed by <math>p</math>
### Set <math>p.n := p.n - 1</math>
### Terminate the algorithm and return '''''true'''''
## Otherwise terminate the algorithm and return '''''false'''''
# Otherwise (that is, <math>p</math> does not point to a leaf):
## If <math>K \leq p.keys[1]</math>, set <math>k := 0</math>; otherwise, let <math>k \in \{1,\dots,p.n\}</math> be maximal such that <math>K > p.keys[k]</math>
## If <math>p.children[k].n = M - 1</math>:
### If <math>k = p.n</math> (that is, no sibling to the right):
#### If <math>p.children[k-1].n = M - 1</math>: call [[B-Trees|B-tree: merge two siblings]] with pointer <math>p</math> and index <math>k</math>.
#### Otherwise (that is, <math>p.children[k-1].n > M -1</math>): call [[B-Tree:Shift_Key_to_Sibling]] with pointer <math>p</math> index <math>k</math> and <math>shiftRight = true</math>.
### Otherwise (that is, <math>k < p.n</math>):
#### If <math>p.children[k+1].n = M - 1</math>: call [[B-Trees|B-tree: merge two siblings]] with pointer <math>p</math> and index <math>k + 1</math>.
#### Otherwise (that is, <math>p.children[k+1].n > M = 1)</math>: call [[B-Tree:Shift_Key_to_Sibling]] with pointer <math>p</math> index <math>k + 1</math> and <math>shiftRight = false</math>.
## If <math>K</math> is contained in the node to which <math>p</math> points:
### Set <math>found = true</math>
### Set <math>p' := p</math>
## If <math>K \leq p.keys[1]</math>, set <math>k := 0</math>; otherwise, let <math>k \in \{1,\dots,p.n\}</math> be maximal such that <math>K > p.keys[k]</math>.
## Set <math>p := p.children[k]</math>

=== Correctness: ===

Analogously to the induction basis, we have to verify that the [[B-Trees|implementation invariants of the B-tree data structure]] and the above-mentioned loop invariants of the removal procedure are maintained by an iteration of the main loop.

Again, implementation invariants #1 and #2 are trivially fulfilled. In case points to a leaf, implementation invariants #4, #7, and #8 are trivially maintained as well. In this case, Steps 1.1.3 and 1.2.3 guarantee #3, Step 1.1.2 guarantees #5, and Steps 1.1.2 and 4 guarantee #6. In case does not point to a leaf, implementation invariants #3-8 are guaranteed by the subroutines called in Step 2.

Finally, consider the loop invariants of the removal procedure. #1 is trivial; #2 is guaranteed by Step 2.4; #3 and #4.1 by Step 2.3; #4.2 by Step 4, and #5 by the subroutines called in Step 2.

== Complexity ==

'''Statement:''' The asymptotic complexity is in <math>\Theta(\log n)</math> in the best and worst case.

'''Proof:''' Follows immediately from the facts that
# <math>M</math> is assumed to be fixed, and
# the height of a B-tree with <math>n</math> nodes is in <math>\Theta(\log n)</math> (cf. the remark clause of the [[B-Trees]] page).

== Further Information ==
In the above specification, each node with exactly <math>M - 1</math> keys is modified when visited. This is done for precautionary reasons only. With a slight modification, this can be avoided: when the leaf is reached, go back along the traversed path and modify each nodes with <math>M - 1</math> keys until the first node with more than <math>M - 1</math> keys is visited. Evidently, this reduces the number of modifications. However, chances are high that these nodes have to be modified sooner or later, so the true benefit is not clear. The version of the removal procedure presented here has primarily been selected because its loop invariant is simpler and more intuitive.