How to resolve the algorithm Sorting algorithms/Merge sort step by step in the ACL2 programming language

Published on 12 May 2024 09:40 PM
#Acl2

How to resolve the algorithm Sorting algorithms/Merge sort step by step in the ACL2 programming language

Table of Contents

Problem Statement

The   merge sort   is a recursive sort of order   nlog(n). It is notable for having a worst case and average complexity of   O(nlog(n)),   and a best case complexity of   O(n)   (for pre-sorted input). The basic idea is to split the collection into smaller groups by halving it until the groups only have one element or no elements   (which are both entirely sorted groups). Then merge the groups back together so that their elements are in order. This is how the algorithm gets its   divide and conquer   description.

Write a function to sort a collection of integers using the merge sort.

The merge sort algorithm comes in two parts: The functions in pseudocode look like this:

Note:   better performance can be expected if, rather than recursing until   length(m) ≤ 1,   an insertion sort is used for   length(m)   smaller than some threshold larger than   1.   However, this complicates the example code, so it is not shown here.

Let's start with the solution:

Step by Step solution about How to resolve the algorithm Sorting algorithms/Merge sort step by step in the ACL2 programming language

Source code in the acl2 programming language

(defun split (xys)
   (if (endp (rest xys))
       (mv xys nil)
       (mv-let (xs ys)
               (split (rest (rest xys)))
          (mv (cons (first xys) xs)
              (cons (second xys) ys)))))

(defun mrg (xs ys)
   (declare (xargs :measure (+ (len xs) (len ys))))
   (cond ((endp xs) ys)
         ((endp ys) xs)
         ((< (first xs) (first ys))
          (cons (first xs) (mrg (rest xs) ys)))
         (t (cons (first ys) (mrg xs (rest ys))))))

(defthm split-shortens
   (implies (consp (rest xs))
            (mv-let (ys zs)
                    (split xs)
               (and (< (len ys) (len xs))
                    (< (len zs) (len xs))))))

(defun msort (xs)
     (declare (xargs
            :measure (len xs)
            :hints (("Goal"
                     :use ((:instance split-shortens))))))
   (if (endp (rest xs))
       xs
       (mv-let (ys zs)
               (split xs)
          (mrg (msort ys)
               (msort zs)))))

You may also check:How to resolve the algorithm FizzBuzz step by step in the Arbre programming language
You may also check:How to resolve the algorithm Read entire file step by step in the Lasso programming language
You may also check:How to resolve the algorithm Sum digits of an integer step by step in the RPL programming language
You may also check:How to resolve the algorithm Loops/For with a specified step step by step in the 6502 Assembly programming language
You may also check:How to resolve the algorithm Variadic function step by step in the Batch File programming language