

In [ ]:

    
%%HTML
<style>
.container { width:100% } 
</style>

Insertion Sort

The function sort is specified via two equations:

$\mathtt{sort}([]) = []$
$\mathtt{sort}\bigl([x] + R\bigr) = \mathtt{insert}\bigl(x, \mathtt{sort}(R)\bigr)$

This is most easily implemented in a recursive fashion.



In [ ]:

    
def sort(L):
    if L == []:
        return []
    x, R = L[0], L[1:]
    return insert(x, sort(R))

The auxiliary function insert is specified as follows:

$\mathtt{insert}(x,[]) = [x]$
$x \preceq y \rightarrow \mathtt{insert}\bigl(x, [y] + R\bigr) = [x,y] + R$
$\neg x \preceq y \rightarrow \mathtt{insert}\bigl(x, [y] + R\bigr) = [y] + \mathtt{insert}(x,R)$

Again, a recursive implementation is straightforward.



In [ ]:

    
def insert(x, L):
    if L == []:
        return [x]
    y, R = L[0], L[1:]
    if x <= y:
        return [x] + L
    else:
        return [y] + insert(x, R)



In [ ]:

    
insert(5, [1,3,4,7,9])



In [ ]:

    
sort([7, 8, 11, 12, 2, 5, 3, 7, 9])



In [ ]: