伊德里斯的快速排序 [英] Quicksort in Idris

问题描述

我正在学习 Idris，我想我会尝试为 Vect 类型实现快速排序.

I'm learning Idris and I thought I'd try to implement Quicksort for Vect types.

但是我在使用实用方法时遇到了困难，该方法应该给定一个主元元素和一个向量，将向量一分为二，一个元素 ≤ 枢轴，另一个元素 > 枢轴.

But I'm having a hard time with the utility method that should, given a pivot element and a vector, split the vector in two, one with the elements ≤ pivot and another with those > pivot.

这对于列表来说是微不足道的:

This is trivial for lists:

splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e)
splitListOn pivot [] = ([], [])
splitListOn pivot (x :: xs) = let (ys, zs) = splitListOn pivot xs in
                              if x <= pivot then (x :: ys, zs) 
                                            else (ys, x :: zs)

*Test> splitListOn 3 [1..10]
([1, 2, 3], [4, 5, 6, 7, 8, 9, 10]) : (List Integer, List Integer)

但是对于 Vect，我需要表达这样一个事实，即两个返回的 Vect 的长度之和等于输入 Vect 的长度.

But for Vect I need to express the fact that the sum of the lengths of the two returned Vects is equal to the length of the input Vect.

我显然需要返回一个依赖对.元素数 ≤ pivot 似乎是第一个值的好候选，但我的第一次尝试:

I clearly need to return a dependent pair. The number of elements ≤ pivot seems a good candidate for the first value, but my first try:

splitVectOn : Ord e => e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e))

抱怨(确实如此)它不知道是否 k ≤ n:

complains (rightly so) that it doesn't know whether k ≤ n:

When checking type of Main.splitVectOn:
When checking argument smaller to function Prelude.Nat.-:
        Can't find a value of type 
                LTE k n

我可以在类型签名中添加这样的东西LTE kn来让类型检查器放心，但是我不知道如何递归创建返回值k通过谓词.

I can add such a thing LTE k n to the type signature to reassure the type checker, but then I don't know how to recursively create a return value k that passes the predicate.

我的意思是，即使对于 n = k = 0 的基本情况也不是:

I mean, not even for the base case, where n = k = 0:

splitVectOn : Ord e => LTE k n =>
              e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e))
splitVectOn _ [] = (_ ** ([], []))

错误同时提到了 k1 和 k，这表明类型签名可能有问题:

The error mentions both a k1 and a k, which suggests that there might be something wrong with the type signature:

When checking right hand side of splitVectOn with expected type
        (k1 : Nat ** (Vect k e, Vect (0 - k) e))

When checking argument a to constructor Builtins.MkPair:
        Type mismatch between
                Vect 0 e (Type of [])
        and
                Vect k e (Expected type)

        Specifically:
                Type mismatch between
                        0
                and
                        k

我也想过用一个Fin来表达不变量:

I also thought of using a Fin to express the invariant:

splitVectOn : Ord e => e -> Vect n e ->
              (k : Fin (S n) ** (Vect (finToNat k) e, Vect (??? (n - k)) e))

但后来我不知道如何执行减法(这应该是可能的，因为 Fin (S n) 总是≤ n)

but then I don't know how to perform the subtraction (which should be possible, because a Fin (S n) is always ≤ n)

推荐答案

您可以像这样将所需的证明添加到输出类型:

You can add the required proof to the output type like so:

(k ** pf : LTE k n ** (Vect k e, Vect (n - k) e))

这里是我们如何定义这个函数:

Here is how we can define this function:

-- auxiliary lemma
total
minusSuccLte : n `LTE` m -> S (m `minus` n) = (S m) `minus` n
minusSuccLte {m} LTEZero = cong $ minusZeroRight m
minusSuccLte (LTESucc pf) = minusSuccLte pf

total
splitVectOn : Ord e => (pivot : e) -> Vect n e ->
                        (k ** pf : LTE k n ** (Vect k e, Vect (n - k) e))
splitVectOn pivot [] = (0 ** LTEZero ** ([], []))
splitVectOn pivot (x :: xs) = 
  let (k ** lte ** (ys, zs)) = splitVectOn pivot xs in
  if x <= pivot then (S k ** LTESucc lte ** (x :: ys, zs))
  else
    let xzs = replace {P = \n => Vect n e} (minusSuccLte lte) (x :: zs) in
    (k ** lteSuccRight lte ** (ys, xzs))

解决同一问题的另一种方法是为 splitVectOn 函数提供以下规范:

Another approach to the same problem is to give the following spec to the splitVectOn fucntion:

total
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
              (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e))

即我们(存在性地)量化输出向量的长度，并添加这些长度的总和必须等于输入向量的长度的条件.这个k1 + k2 = n条件当然可以省略，这样会大大简化实现.

i.e. we (existentially) quantify over the lengths of the output vectors and add the condition that the sum of those lengths must be equal to the length of the input vector. This k1 + k2 = n condition can be omitted, of course, which would simplify the implementation a lot.

这是具有修改规范的函数的实现:

Here is an implementation of the function with the modified spec:

total
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
              (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e))
splitVectOn pivot [] = (0 ** 0 ** (Refl, [], []))
splitVectOn pivot (x :: xs) =
  let (k1 ** k2 ** (eq, ys, zs)) = splitVectOn pivot xs in
  if x <= pivot then (S k1 ** k2 ** (cong eq, x :: ys, zs))
  else let eq1 = sym $ plusSuccRightSucc k1 k2 in
       let eq2 = cong {f = S} eq in
       (k1 ** S k2 ** (trans eq1 eq2, ys, x :: zs))

这篇关于伊德里斯的快速排序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！