Sorting is a frequently used operation that has the following standard representation in virtual code.
sort]] p = ((nil,nil),((p,nil),(nil,nil)))
When an application in this form is evaluated with an operand representing a list, the result is a sorted version of the list.
The way a list is sorted depends on what order is of interest. For example, numbers could be sorted in ascending or descending order, character strings could be sorted lexically or by length, etc.. The value of p is therefore needed in sorting applications to specify the order. It contains the virtual code for a partial order relational operator. This operator can be evaluated with any pair of items selected from a list, and should have a value of true if the left one should precede the right under the ordering. For example, if numbers were to be sorted in ascending order, then p would compute the “less or equal” relation, returning true if its operand were a pair of numbers in which the left is less or equal to the right.
The virtual code semantics for sorting applications is given by these
two properties, wherein p is a non-nil tree, and
insert is a silly mnemonic to be defined next.
sort]] p) nil = nil
sort]] p) (x,y) = ([[insert]] p)
(x,([[sort]] p) y)
These properties say that the empty list is already sorted, and
a non-empty list is sorted if its tail is sorted and the head is then
inserted in the proper place. This specification of sorting has nothing
to do with the sorting algorithm that avram really uses.
The meaning of insertion is convenient to specify in virtual code itself. It should satisfy these three equations.
insert]] p) (x,nil) = (x,nil)
insert]] p) (x,(y,z)) =
(y,([[insert]] p) (x,z))
if p(x,y) = nil
insert]] p) (x,(y,z)) =
(x,(y,z)) if p(x,y) is a non-nil tree
Intuitively, the right argument, whether nil or
(y,z), represents a list that is already sorted. The
left argument x therefore only needs to be compared to the
head element, y to ascertain whether or not it belongs at
the beginning. If not, it should be inserted into the tail.
A possible implementation of insert in silly is given in
Insert.