Formal Verification of a Merge-Sort Program with Static Semantics

Paul E. Black

National Institute of Standards

and Technology (NIST) paul.black@nist.gov

George Becker^{∗}

Department of Computer Science

University at Albany - SUNY becker@cs.albany.edu

Neil V. Murray^{∗}

Department of Computer Science University at Albany - SUNY nvm@cs.albany.edu

Abstract

Proving correctness of programs is a desirable, but not yet practically solved, problem. Conventional verification techniques do not scale to larger “real-life” programs. In order to overcome problems with the semantics of conventional languages, researchers define subsets of these languages for verification. We take this approach one step further; rather than defining a subset, we apply a new theory based on relaxed single-threading to achieve completely static semantics (i.e. referential transparency) of programs. Our programs with static semantics have complete control over aliasing, the correct order dependencies are enforced, and uninitialized variables are prevented.

Due to the static semantics of these programs, first-order logic can be used directly to verify them. Using Merge-Sort as an example, we demonstrate that first-order logic proofs of programs with static semantics are fully composable and thus scale freely to larger programs. We also report on our work towards a fully formal, machine-checked proof. This work is one more step towards facilitating the design of more easily verified programs.

1 Introduction

The desirability of proving programs correct with respect to their specifications has been suggested many times [Dij, Flo, Gri, Ho1, Ho2, Man, McM, BW]. However, program proving appears to be a very costly and difficult exercise [MLP]. A variety of principles of program proving, or verification, have been applied successfully to some small programs [Ho2]. The applicability of program verification to larger, “real-life” programs has been disputed [MLP].

One of the main difficulties in applying the known techniques of program verification is the combinatorial complexity of large proofs. Due to the lack of composability of these techniques, they do not scale to larger, “real-life” programs. Using first-order logic instead facilitates program verification. This is much easier for programs with static semantics.

Formal verification can become practical and successful in having a significant impact on practice if verification is more tractable, more productive, and costeffective. Due to problems with semantics of conventional programming languages, researchers in formal verification define subsets of those languages. For example, the Penelope system [EHH] developed by Odyssey Research Associates, Inc. uses a subset of Ada. Their intent is to verify, by static semantic checks, that programs are free from improper aliasing, undisciplined side effects, incorrect order dependencies, and uses of uninitialized variables.

We take such approaches one step further. Rather than defining a subset of a conventional language, we adopt the single-assignment style to achieve static semantics (i.e., referential transparency) of our programs. Our use of single-assignment is in the declarative sense of functional programming, that is as a definition, rather than in the operational sense of imperative programming as a side effect. Programs with these static semantics have complete control over aliasing, correct order dependencies are enforced, and uninitialized variables are prevented. Most importantly, due to the static semantics, first-order logic can be used directly to verify programs, thus avoiding difficult verification techniques based on temporal first-order logics [MP] or Floyd-Hoare axiomatization [Flo, Ho1]. Since we are able to use a few predefined higher-order functions rather than recursion in our programs, we can apply mathematical induction. Due to the full compositionality of programs with static semantics, our approach can freely scale to larger programs.

Section 2 discusses theoretical foundations of our work. Section 3 presents our Merge-Sort program consisting of four function definitions. Section 4 then gives the proof of program correctness. We report our progress toward a machine proof in Section 5 and discuss extensions, implications, and future work in Section 6. Appendix A lists standard operators and functions we use, and Appendix B formally defines program primitives.

∗ Supported in part by NSF Grant CCR-9404338.

2 Theoretical Basis

We developed an underlying theory [BM] that makes it possible to achieve a completely static semantics. Our approach is motivated by single-threading (i.e. using a value only once) of aggregate data (e.g., arrays, lists, trees, tuples). Linear LISP [Bak] makes singlethreading explicit at the programmer’s level. This approach restricts a functional programming language so that only singly-threaded programs can be expressed. However, rigid enforcement of single-threading is a severe constraint on the expressiveness of a programming language, and thus appears to be self-defeating.

We relax single-threading to restore expressiveness [BM] while still being able to benefit from the limited single-threading that remains. The central idea is to divide function input arguments into two categories called inert inputs and active inputs. This distinction is crucial because aggregate data arguments are passed by reference for efficiency. Inert inputs are used for (aggregate) data not subject to updating; e.g., when evaluating the length of a list or computing the sum of a vector of numbers. Such operations require no copying of data. Active inputs are used for aggregate data subject to updating in a given operation.

Our relaxed single-threading has two aspects. First, our structured function composition defines legal uses of inert and active inputs when composing functions. Second, our memory axioms stipulate how predefined primitive functions must be implemented. We have shown [BM] that evaluation of any structured function composition of primitive functions is free of aliasing, i.e. single-threading is preserved. Thus static semantics, also known as referential transparency, is achieved despite in-place updating of active input data.

3 Merge-Sort Program

We illustrate our approach on a Merge-Sort program for lists of (real) numbers. The program applies to any type of element as long as elements are comparable.

Inert and active inputs can be distinguished by either a separator (the bar character in [BM]) or by suitable annotations (keywords). Since annotations of inert and active inputs do not change the semantics of the program, they have no effect on the program proof. Since this paper concentrates on verification, we omit these annotations in our Merge-Sort program. The annotations are only needed for compilers to determine legal programs and to translate programs correctly. The various “utility” functions used in the program are formally defined in the Appendix B.

The program’s top-level function, merge sort, first converts the input data into a list of singleton lists. Since each singleton list has only one element, they are trivially sorted. The core of merge sort is repeatedly applying the function msort step. The function msort step sorts and merges the list of many singleton lists into a list of one sorted list containing all the input elements. The function flatten gives the result as a simple list.

Function msort step splits its list-of-lists argument into two halves, then merges each list from the first half with a (corresponding) list from the second half. Successive applications of msort step combine “inner lists,” keeping each inner list sorted, which shortens the “outer list.” Eventually the outer list has just one list: a sorted inner list with all the original elements.

Function ord merge just merges its two list arguments. Since we keep the two argument lists sorted, the resulting list is sorted as well. Function merge step is an auxiliary function that performs one step of the ordered list merge by choosing the smaller element of two lists. The chosen element is then transferred to the list holding the intermediate result of merging.

                                                  function merge_sort(list(real) A):
                                                      int B = ceiling(log2(max(size(A),1))),
                                                      list(list(real)) C = explode_list(A),
                                                      list(list(real)) Y = iter(B,msort_step,C),
                                                      list(real) Z = flatten(Y),
                                                      result (Z).
                                                  function msort_step(list(list(real)) C):
                                                      (list(list(real)) D, list(list(real)) E)
                                                                               = split_list(C),
                                                      list(list(real)) X
                                                                    = map2_fill(ord_merge,D,E),
                                                      result (X).
                                                  function ord_merge(list(real) D,
                                                                     list(real) E):
                                                      int F = size(D) + size(E),
                                                      (list(real) U, list(real) V, list(real) W)
                                                            = iter(F,merge_step,D,E,empty_list),
                                                      result (W).
                                                  function merge_step(list(real) D,
                                                                    list(real) E, list(real) G):
                                                      bool H = size(D)==0 or first_greater(D,E),
                                                      (list(real) P, list(real) Q)
                                                                               = swap_if(H,D,E),
                                                      (list(real) R, list(real) S)
                                                                             = headlist_tail(P),
                                                      list(real) T = concat(G,R),
                                                      result (Q,S,T).

4 Proof of Program Correctness

We prove the correctness of this program by proving four theorems. Each theorem specifies the properties of one of the functions in the program. Our proof is a brief sketch with many details left out because of length. Appendix B defines two predicates (sorted, permut) and three functions (concat, concat3, flatten) that we also use in the proof. The term permut(A, B) means that A is a permutation of B. Appendix B also defines sequence comparison (e.g., list comparison) which we denote by ⪯.

4.1 Function merge step First, we give the necessary precondition (1) for this function:

\begin{matrix}sorted(D) ∧ sorted(E) ∧ sorted(G) \\ ∧ \\ (G ⪯ D) ∧ (G ⪯ E) \end{matrix} \}  (1)

Now, we give the desired postcondition (2) for the results of applying function merge_step:

\begin{matrix}sorted(Q) ∧ sorted(S) ∧ sorted(T) \\ ∧ \\ (T ⪯ Q) ∧ (T ⪯ S) \\ ∧ \\ permut(concat3(Q, S, T), concat3(D, E, G)) \\ ∧ \\ (size(Q) + size(S) = \\ max(0, size(D) + size(E) − 1)) \end{matrix} \} (2)

Theorem 1 If function merge step is applied to arguments satisfying precondition (1), then the function results satisfy postcondition (2).

Proof: Assume that the precondition (1) holds. The value of variable H is true, if and only if either list D is empty or lists D and E are both non-empty and the first element of list D is greater than the first element of list E. Otherwise, the value of H is false. For all of these cases, the following condition (3) holds:

\begin{matrix}sorted(P) ∧ sorted(Q) \\ ∧ \\ (size(P) = 0 ∨ size(Q) = 0 \\ ∨ min(P) ≤ min(Q)) \\ ∧ \\ permut(concat(P, Q), concat(D, E)) \end{matrix} \} (3)

We note that P and Q are sorted. If P and Q are also non-empty, then the first element of P is equal to min(P), and the first element of Q is equal to min(Q). Since the first element of P is less than or equal to the first element of Q, min(P) ≤ min(Q). We use the condition min(P) ≤ min(Q) since it is better for carrying out the proof.

From the precondition (1) and from properties of function headlist_tail, we obtain the following formula (4) for lists R and Q:

\begin{matrix}(size(R) = min(1, size(P))) \\ ∧ \\ sorted(R) ∧ sorted(S) ∧ (R ⪯ Q) ∧ (R ⪯ S) \\ ∧ \\ permut(concat(R, S), P) \end{matrix} \} (4)

From (1), (3), (4) and properties of function concat, we get the formula (5) for list T:

sorted(T) ∧ permut(T, concat(G, R))  (5)

The postcondition (2) for function merge_step can be obtained from (1), (3), (4) and (5).

4.2 Function ord merge

We formulate the necessary precondition (6) for this function:

sorted(D) ∧ sorted(E)  (6)

We give the desired postcondition (7) for the results of applying function ord_merge:

sorted(W) ∧ permut(W, concat(D, E))  (7)

Theorem 2 If function ord merge is applied to arguments satisfying precondition (6), then the function results satisfy postcondition (7).

Proof: Assume that the precondition (6) holds. We proceed by induction on F, the number of applications of function merge_step. We define predicate Pr1(F) as follows:

Pr1(F) = sorted(U) ∧ sorted(V) ∧ sorted(W) ∧

(W ⪯ U) ∧ (W ⪯ V) ∧

permut(concat3(U, V, W), concat(D, E)) ∧ (size(U) + size(V)

= max(0, size(D) + size(E) − F))

Base Case: Let F = 0. Then U = D, V = E, and W = empty list, and so Pr1(0) holds. Ind. Step: Assume that Pr1(F) holds for some nonnegative integer. We get for F + 1:

iter(F + 1, merge step, D, E, empty list)

= merge step(iter(F, merge step, D, E, empty list))

From the induction hypothesis Pr1(F), the precondition (6) for the (F+1)-th application of function merge_step is satisfied. Thus we can apply Theorem 1. The permutation clause of Pr1(F + 1) results from Pr1(F), Theorem 1 and transitivity of permutation. As each application of function merge_step decreases size(U) + size(V) by one (unless already zero), the last clause in Pr1(F + 1) also holds. □ As we have F = size(D) + size(E), we obtain:

\begin{matrix}size(U) & + & size(V) \\ & = & max(0, size(D) + size(E) − F) \\ & = & max(0, F − F) = 0 \end{matrix} \} (8)

From predicate Pr1(F) and (8), we get:

permut(W, concat(D, E))  (9)

The postcondition (7) for function ord_merge follows immediately from predicate Pr1(F) (i.e. sorted(W)) and (9).

4.3 Function msort step We formulate the necessary precondition (10) for this function:

∀_{1≤i≤size(C)} i : sorted(c_{i})  (10)

We give the necessary postcondition (11) for the results of applying function msort_step:

\begin{matrix}(size(X) = ⌈size(C)/2⌉) \\ ∧ \\ (∀_{1≤i≤size(X)} i : sorted(x_{i})) \\ ∧ \\ permut(flatten(X), flatten(C)) \end{matrix} \}  (11)

Theorem 3 If function msort step is applied to arguments satisfying precondition (10), then the function results satisfy postcondition (11).

Proof: Assume that the precondition (10) holds. From this precondition and properties of function

split_list, we get:

\begin{matrix}(size(D) = ⌈size(C)/2⌉) \\ ∧ \\ (size(E) = ⌊size(C)/2⌋) \\ ∧ \\ (∀_{1≤i≤size(D)} i : sorted(d_{i})) \\ ∧ \\ (∀_{1≤j≤size(E)} j : sorted(e_{j})) \\ ∧ \\ permut(flatten(C), \\ concat(flatten(D), flatten(E)) \end{matrix} \} (12)

From (12), properties of function map2_fill and Theorem 2, we obtain:

\begin{matrix}(size(X) = ⌈size(C)/2⌉) \\ ∧ \\ (∀_{1≤i<size(X)} i : sorted(x_{i})) \\ ∧ \\ (∀_{1≤j<size(X)} j : permut(x_{j}, concat(d_{j}, e_{j})) \\ ∧ \\ if odd(size(C)) \\ then permut(x_{size(X)}, d_{size(D)}) \\ else permut(x_{size(X)}, \\ concat(d_{size(D)}, e_{size(E)})) \end{matrix} \} (13)

The size(C) is either odd or even. In both cases, the postcondition (11) follows from (13) and (12).

4.4 Function merge sort Precondition: None We formulate the desired postcondition (14) for the results of applying function merge_sort:

permut(Z, A) ∧ sorted(Z)  (14)

Theorem 4 Applying the function merge sort satisfies the postcondition (14).

Proof: From properties of function explode_list, we obtain:

\begin{matrix}(size(C) = size(A)) \\ ∧ \\ (∀_{1≤i≤size(C)} i : sorted(c_{i})) \\ ∧ \\ permut(flatten(C), A) \end{matrix} \}  (15)

We continue by induction on B, the number of applications of function msort_step. We define Pr2(B) as follows:

Pr2(B) = (∀_{1≤j≤size(Y)} j : sorted(y_{j})) ∧

permut(flatten(Y), flatten(C)) ∧

(size(Y) ≤ max(1, 2^{⌈log_{2}(max(size(A),1)⌉−B}))

Base Case: Let B = 0. Then Y = A, and so Pr2(0) holds. Ind. Step: Assume Pr2(B) holds for some nonnegative integer. We get for B + 1:

iter(B + 1, msort step, C)

= msort step(iter(B, msort step, C))

From the induction hypothesis Pr2(B), the precondition (10) for the (B+1)-th application of function msort_step is satisfied. Thus we can apply Theorem 3. The permutation clause of Pr2(B + 1) results from Pr2(B), Theorem 3 and transitivity of permutation. As each application of function msort_step decreases the upper bound of log_{2}(max(size(Y), 1)) by one (unless size(Y) ≤ 1 already), the last clause of Pr2(B + 1) also holds. □ As we have B = ⌈log_{2}(max(size(A), 1))⌉, size(Y) ≤ max(1, 2 ∗ ∗0) = 1. Since the elements of Y are sorted, size(Y) ≤ 1 means that sorted(flatten(Y)) is true. We further obtain from Pr2(B) and (15):

\begin{matrix}permut(flatten(Y), flatten(C)) \\ ∧ \\ permut(flatten(C), A) \end{matrix} \}  (16)

From (16) and from the facts that sorted(flatten(Y)) is trivially true and Z = flatten(Y), we obtain the postcondition (14) for the function merge_sort. Naturally, size(Z) = size(A) is also true.

5 Machine Proofs Efforts

To be practical for more and larger programs, proofs of correctness must be at least partially automated. To this end we are working on fully formal, machinechecked proofs in HOL [GM] and PVS [ORS]. To prove correctness we need three formally defined components: a specification, an implementation model, and rules of inference [BHJ+].

We formalize the preconditions and postconditions from Section 4 as the specifications. We translate the program from Section 3 into functional descriptions in the built-in first-order logics as the implementation. (This is a “shallow” embedding.) Our models refer to sorting natural numbers (non-negative integers), instead of real numbers, since they are a “native type” and thus a little easier to reason about. We use the standard, built-in rules of logic, math, and function composition for rules of inference.

With the specification and a model of the implementation described formally, the “theorem provers” check that each step of the proof is correct. Although HOL and PVS prove some of the simplest steps automatically, the fully formal proof is still many times more complex than the proofs in this paper. For instance, obvious and technical lemmas such as (sorted(G)∧∀y ∈ G : x ≥ y) ⇒ sorted(append(G, x)) must be proved in great detail.

Our work so far in formalizing and proving the specifications and program found some typographical errors which had escaped earlier manual checking.

6 Discussion

The purpose of our Merge-Sort program is to provide a good illustration of our proof method on a familiar algorithm. Even though actual applications of the Merge-Sort algorithm tend to operate on external data (e.g., magnetic tapes), for purposes of illustration, this Merge-Sort program operates on internal data. We chose to represent sequences as lists, since lists are more natural and better suited for expression of the Merge-Sort algorithm. Unlike a Merge-Sort algorithm coded in conventional sequential languages (e.g., Pascal, Modula-2, Ada, C/C++, etc.), our Merge-Sort is, in principle, a parallel program. In particular, the higher order function map2 fill can be viewed as a data-parallel construct.

Our Merge-Sort program uses higher order functions and is nonrecursive. Its call-graph is a (rooted) tree. We carry out its proof by simple induction. The “loop invariants” of conventional proofs are captured by our induction predicates. The proof proceeds in a “bottom-up” fashion from leaves of the call-graph tree towards its root. Naturally, when proving that a function corresponding to an interior node of the call-graph tree, we use intermediate proof results from children of the interior node. Other than that, however, proofs of individual functions making up a program are independent of each other. Consequently, our proofs are composable and thus can scale to larger programs.

Conventional proof methods show total correctness by establishing partial correctness of a program and separately proving program termination. Our method shows correctness entirely by proving that an inputoutput transformation of a program satisfies the given specification. If the input-output transformation is a total function, the termination of a program follows. In the case of our Merge-Sort program, there is no possibility of non-termination since no construct in our program admits infinite iteration. Formally speaking, the input-output transformation of Merge-Sort is primitive recursive, and thus total.

The classical proof of Find, which performs partial sorting, is described in Sections 2, 3, and 4 of [Ho2], and includes the following reservation in Section 5:

In the proof of Find, one very important aspect of correctness has not been treated, namely, that the program merely rearranges the elements of the array A, without changing their values.

The proof of our Merge-Sort program shows directly that the output is a permutation (i.e. rearrangement) of the input. Currently, we are considering proving the program Find [Ho2] by our method. In the future, we wish to further demonstrate compositionality of our method. Since compositionality is a necessary condition for scalability and thus for the success of any verification technique, we plan to show scalability by verifying larger programs, including a simple text analyzer (histogram generator) and a maximum network flow program.

Acknowledgments

We express our sincere thanks to Richard E. Stearns and S. S. Ravi for helpful discussions on this paper. We thank Trent N. Larson and William Majurski for their work on the machine proof.

References

[Bak] Henry G. Baker. A ‘Linear Logic’ Quicksort. In ACM Sigplan Notices, Feb 1994.

[BM] George Becker and Neil V. Murray. Efficient execution of programs with static semantics. In ACM Sigplan Notices, April 1995.

[BMS] George Becker, Neil V. Murray, and Richard E. Stearns. Refined single-threading for parallel functional programming. In Languages, Compilers and Run-Time Systems for Scalable Computers (Eds.: Boleslaw K. Szymanski and Balaram Sinharoy), Kluwer Academic Publishers, 1996.

[BHJ+] Paul E. Black, Kelly M. Hall, Michael D. Jones, Trent N. Larson, and Phillip J. Windley. A brief introduction to formal methods. In Proc. of CICC ’96, pages 377–380, 1996.

[BW] Paul E. Black and Phillip J. Windley. Formal verification of secure programs in the presence of side effects. In Proc. of HICSS-31, vol. III, pages 327–334, 1998.

[Dij] Edsger W. Dijkstra. A Discipline of Programming. Englewood Cliffs/Prentice-Hall, 1976.

[EHH] Carl T. Eichenlaub, C. Douglas Harper and Geoffrey Hird. Using Penelope to Asses the Correctness of NASA Ada Software: A Demonstration of Formal Methods as a Counterpart to Testing. NASA Contractor Report 4509, May 1993.

[Flo] Robert W. Floyd. Assigning meanings to programs. In Proc. of Symposium in Applied Mathematics, pages 19–32, 1967.

[GM] Michael J. C. Gordon and Tom F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

[Gri] David Gries. The Science of Programming. Springer-Verlag, 1981.

[Ho1] C. A. R. Hoare. An axiomatic basis for computer programming. In Comm. of ACM, 12 (10), pages 576–583, 1969.

[Ho2] C. A. R. Hoare. Proof of a program FIND. In Comm. of ACM, 14 (1), pages 39–45, 1971.

[Man] Zohar Manna. Mathematical Theory of Computation. McGraw-Hill, 1974.

[MP] Zohar Manna and Amir Pnueli. Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.

[McM] John McCarthy. Towards a mathematical science of computation. In IFIP 62, pages 21– 29, Amsterdam. North-Holland, 1962

[MLP] Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis Social processes and proofs of theorems and programs. In Comm. of ACM, 22 (5), pages 271–280, 1979.

[ORS] Sam Owre, John M. Rushby, and Natarajan Shankar. PVS: a prototype verification system. In 11th CADE, vol. 607 of Lecture Notes in Artificial Intelligence, pages 748–752, 1992.

A Standard Operators and Functions

In our logical formulas and in the program, we use standard arithmetic, relational and logical operators +, −, ∗, /, <, ≤, =, ¬, ∧, ∨. In the program, we use “or” for the logical operator ∨, as well as == for the relational operator =. We also use the functions max, min, ceiling (⌈x⌉), binary exponentiation (2^{x}) and binary logarithm (log_{2}) with their standard meaning. In our logical formulas (but not in the program), the function min is not only a binary function but is extended in the usual way to non-empty sequence operands.

Except for the data being sorted, all other atomic data types are either boolean or integer. In fact, both the program and the proof require only natural numbers, not integers. Since we wish to avoid defining additional functions and complicating our logical formulas, these formulas do contain a few occurrences of arithmetic subexpressions that can evaluate to negative integers. Similarly, a few arithmetic subexpressions may evaluate to real values. However, these subexpressions occur only within integer expressions.

B Definitions of Primitive Functions and Predicates

We use the following functions, as well as the predicates odd, sorted, permut, and ⪯ (sequence comparison) in our logical formulas and/or in the program.

Definition 1 Predicate odd: odd(n) = ¬(∃m ∈ Nat : n = 2 ∗ m)

Let Q = q_{1}, q_{2}, q_{3}, ..., q_{k} be a finite sequence (of, e.g., numbers).

Definition 2 Size (length or number of elements) of a sequence Q:

size(Q) = \{ \begin{matrix}k & if Q is non-empty \\ 0 & otherwise \end{matrix} Definition 3 Prefix of length n of a sequence Q: prefix(n, Q) = Q′, such that size(Q′) = min(n, size(Q)) and ∀_{1≤i≤size(Q′)} q′_{i} = q_{i}

Definition 4 Suffix of length n of a sequence Q: suffix(n, Q) = Q′, such that size(Q′) = min(n, size(Q)) and ∀_{1≤i≤size(Q′)} q′_{i} = q_{i+size(Q)−size(Q′)}

Definition 5 Tail of a sequence: tail(Q) = suffix(max(0, size(Q) − 1), Q)

Definition 6 Prepend an element q_{p} to a sequence Q: prepend(q_{p}, Q) = Q′, such that size(Q′) = size(Q) + 1, q′_{1} = q_{p}, and Q = tail(Q′)

Definition 7 Sorted Property (in a non-decreasing order) of a sequence Q: sorted(Q) = ∀_{1≤i<size(Q)} i : q_{i} ≤ q_{i+1}

Definition 8 Counting elements of sequence S having given value v: count(v, S) = ∑_{1≤i≤size(S)} (if s_{i} = v then 1 else 0)

Definition 9 Sequence comparison: Let S_{1} and S_{2} be sequences of comparable elements. S_{1} ⪯ S_{2} = ∀s_{1} ∈ S_{1}, s_{2} ∈ S_{2} : s_{1} ≤ s_{2}

Definition 10 Minimum element value in a sequence (e.g., a list):

min(Q) = \{ \begin{matrix}min(q_{1}, min(tail(Q))) & if size(Q) > 1 \\ q_{1} & if size(Q) = 1 \\ undefined & otherwise \end{matrix}

Definition 11 Comparison of first elements of two sequences R and S: first greater(Q, S)

= (size(Q) > 0 ∧ size(S) > 0 ∧ q_{1} > s_{1})

Definition 12 Conditional swapping of two arguments:

swap if(Cond, x, y) = \{ \begin{matrix}y, x & if Cond \\ x, y & otherwise \end{matrix}

Definition 13 Concatenation of two sequences: concat(Q, R) = S such that size(S) = size(Q) + size(R), Q = prefix(size(Q), S), R = suffix(size(R), S).

Definition 14 Concatenation of three sequences: concat3(Q_{1}, Q_{2}, Q_{3}) = concat(Q_{1}, concat(Q_{2}, Q_{3}))

Definition 15 Permutation as a binary relation on sequences: Let Q and S be sequences of comparable elements. permut(Q, S)

= ∀e ∈ concat(Q, S) : (count(e, Q) = count(e, S))

Definition 16 Exploding a sequence (e.g., a list) into a sequence of singleton sequences: explode list(Q)

= \{ \begin{matrix}prepend(prefix(1, Q), \\ explode list(tail(Q))) & if size(Q) > 0 \\ empty-sequence & otherwise \end{matrix}

Definition 17 Flattening (i.e. generalized concatenation) of a sequence of sequences Y: flatten(Y)

= \{ \begin{matrix}concat(y_{1}, flatten(tail(Y))) & if size(Y) > 0 \\ empty-sequence & otherwise \end{matrix}

Definition 18 Splitting a sequence (e.g., a list):

split list(Q) = R, S

such that size(R) = ⌈size(Q)/2⌉, size(S) = ⌊size(Q)/2⌋, and Q = concat(R, S).

Definition 19 Applying a given function to corresponding elements of two sequences (e.g., lists): map2 fill(f, Q, R)

= \{ \begin{matrix}prepend(f(q_{1}, r_{1}), \\ map2 fill(f, tail(Q), tail(R))) \\ if size(Q) > 0 ∧ size(R) > 0 \\ prepend(q_{1}, map2 fill(f, tail(Q), R)) \\ if size(Q) > 0 ∧ size(R) = 0 \\ prepend(r_{1}, map2 fill(f, Q, tail(R))) \\ if size(Q) = 0 ∧ size(R) > 0 \\ empty-sequence & otherwise \end{matrix}

Definition 20 Headlist and tail of a sequence Q:

headlist tail(Q) = prefix(1, Q), tail(Q)

Note that for an empty-sequence Q^{0} (i.e. size(Q^{0}) = 0), headlist tail(Q^{0}) = Q^{0}, Q^{0}.

Consider a function f such that:

f : (D_{1} × ⋯ × D_{k} × D′_{1} × ⋯ × D′_{m}) ↦ (D′_{1} × ⋯ × D′_{m}) Let x_{1} ∈ D_{1}, ..., x_{k} ∈ D_{k}, y_{1} ∈ D′_{1}, ..., y_{m} ∈ D′_{m}

Definition 21 Applying a function f n-times:

iter(n, f, x_{1}, ..., x_{k}, y_{1}, ..., y_{m})

= \{ \begin{matrix}f(x_{1}, ..., x_{k}, \\ iter(n − 1, f, x_{1}, ..., x_{k}, y_{1}, ..., y_{m})) & if n > 0 \\ y_{1}, ..., y_{m} & if n = 0 \end{matrix}