Coq-style implementation of Insertion sort
Coq-style implementation of Insertion sort
Bug-free programming in the Wolfram Language
by Jose Manuel Rodriguez Caballero
Abstract. Following the programming paradigm of Coq, we develop a bug-free implementation of the sorting algorithm known as Insertion Sort.
Introduction
Introduction
The Coq's approach to avoid bugs in programming is to develop the algorithms in such a way that they coincide with their proofs of correctness via the Curry-Howard correspondence. In the present computational essay, we express the property of a list to be ordered via induction. Then, we invoke the inference rules of sorting and only these rules, to sort a list.
Inductive definition of list
Inductive definition of list
Constructor of lists, ConstList[a, l] will be abbreviated as a::l.
In[]:=
ConsList[a_,l_]:=Insert[l,a,1]
Pattern matching in lists.
In[]:=
MatchList[x_]:=If[Length[x]==0,{},(*MatchList[{}] = 0*){First[x],Rest[x]}] (*MatchList[Cons[t,h]] = {t, h} *)
Definition of functions with lists as arguments using fixpoints.
In[]:=
FixpointList[x_,F_,G_]:=If[#=={},F,(*x={}*)G[First[#],Last[#]] (*x = First[#] :: Last[#]*)]&[MatchList[x]]
Definition of functions having lists as arguments using induction.
In[]:=
InductionList[x_,F_,G_]:=If[#=={},F,(*x={}*)Function[{t,h},(*x=t::s*)G[t,h,InductionList[h,F,G]]][First[#],Last[#]]]&[MatchList[x]]
Lexicographical ordering
Lexicographical ordering
The function LexOrder[x, y] returns True if and only if x precedes y in lexicographical order.
In[]:=
LexOrderList[x_,y_]:=FixpointList[x, True,(*x={}*) Function[{t,h},(*x=t::h*) FixpointList[y, False,(*y={}*) Function[{tt,hh},(*y=tt::hh*) If[t <tt, True, If[t==tt, LexOrderList[h,hh], False ] (*end of If*) ](*end of If*) ](*end of Function*) ](*end of Fixpoint with respect to y*) ](*end of Function*) ] (*end of Fixpoint with respect to x*)
In[]:=
LexOrder[x_,y_]:=LexOrderList[ToCharacterCode[x],ToCharacterCode[y]]
Inductive definition of sorted list
Inductive definition of sorted list
In[]:=
Sorted/:MakeBoxes[sorted:Sorted[l_List],form_]:=With[{format=ToBoxes[Inactive[Sorted][l],form]},InterpretationBox[format,sorted,Tooltip"Sorted"]]
An empty list is sorted.
In[]:=
SortedNil[]:=Sorted[{}]
A list containing a single element is sorted.
In[]:=
Sorted1[x_]:=Sorted[{x}]
If x < y and y :: l is sorted, then x :: y :: l is sorted.
In[]:=
SortedCons[order_,x_,y_,l_,e_Sorted]:= If[order[x,y], If[e===Sorted[ConsList[y,l]], Sorted[ConsList[x,ConsList[y,l]]],(*result of the deduction*) Null],(*the deduction cannot be made*) Null] (*the deduction cannot be made*)
Bug-Free insertion sort algorithm
Bug-Free insertion sort algorithm
The algorithm InsertSort[order, x] sorts a list x according to the lexicographical order by applying the inductive definition of sorted list.
In[]:=
InsertSort[order_,x_]:=InductionList[x, SortedNil[],(*x={}*) Function[{t,h,hh},(*x=t::h*) (*induction hypothesis: hh=InsertSort[order,h]*) InductionList[Last[hh], Sorted1[t],(*hh={}*) Function[{a,l},(*hh=a::l*) If[order[t,a], SortedCons[order,t,a,l,hh],(*insertion at the beginning*) Function[r,(*insertion after the beginning*) SortedCons[order,a,First[Last[r]],Rest[Last[r]],r] ][InsertSort[order,ConsList[t,l]]] ] ] ] ]]
In[]:=
InsertSort[LexOrder,{}]
Out[]=
Sorted[{}]
In[]:=
InsertSort[LexOrder,{"b"}]
Out[]=
Sorted[{b}]
In[]:=
InsertSort[LexOrder,{"b","c"}]
Out[]=
Sorted[{b,c}]
In[]:=
InsertSort[LexOrder,{"c","b"}]
Out[]=
Sorted[{b,c}]
In[]:=
InsertSort[LexOrder,{"b","a","z","g","e","a","x"}]
Out[]=
Sorted[{a,a,b,e,g,x,z}]