gpt4 book ai didi

list - idris中的排序列表(插入排序)

转载 作者:行者123 更新时间:2023-12-03 23:59:02 31 4
gpt4 key购买 nike

我正在写一篇关于依赖类型有用性的本科论文。
我正在尝试构造一个容器,它只能构造成一个排序列表,以便证明它是按构造排序的:

import Data.So

mutual
data SortedList : (a : Type) -> {ord : Ord a) -> Type where
SNil : SortedList a
SMore : (ord : Ord a) => (el: a) -> (xs : SortedList a) -> So (canPrepend el xs) -> SortedList a

canPrepend : Ord a => a -> SortedList a -> Bool
canPrepend el SNil = True
canPrepend el (SMore x xs prf) = el <= x
SMore需要运行时证明被前置的元素小于或等于排序列表中的最小(第一个)元素。

为了对未排序的列表进行排序,我创建了一个函数 sinsert它接受一个排序列表并插入一个元素并返回一个排序列表:
sinsert : (ord : Ord a) => SortedList a {ord} -> a -> SortedList a {ord}
sinsert SNil el = SMore el SNil Oh
sinsert (SMore x xs prf) el = either
(\p =>
-- if el <= x we can prepend it directly
SMore el (SMore x xs prf) p
)
(\np =>
-- if not (el <= x) then we have to insert it in the tail somewhere
-- does not (el <= x) imply el > x ???

-- we construct a new tail by inserting el into xs
let (SMore nx nxs nprf) = (sinsert xs el) in
-- we get two cases:
-- 1) el was prepended to xs and is now the
-- smalest element in the new tail
-- we know that el == nx
-- therefor we can substitute el with nx
-- and we get nx > x and this also means
-- x < nx and also x <= nx and we can
-- prepend x to the new tail
-- 2) el was inserted somewhere deeper in the
-- tail. The first element of the new tail
-- nx is the same as it was in the original
-- tail, therefor we can prepend x to the
-- new tail based on the old proof `prf`
either
(\pp =>
SMore x (SMore nx nxs nprf) ?iins21
)
(\npp =>
SMore x (SMore nx nxs nprf) ?iins22
) (choose (el == nx))
) (choose (el <= x))

我在构建证明时遇到了麻烦( ?iins21?iins22 ),我将不胜感激。我可能依赖一个不成立的假设,但我看不到它。

我还想鼓励您为构建排序列表提供更好的解决方案(也许是一个带有证明值的普通列表,它是排序的?)

最佳答案

我认为您的证明的主要问题在于,正如 Cactus 在评论中指出的那样,您没有插入排序证明工作所需的传递性和反对称等属性。但是,您仍然可以创建一个多态容器:contrib 中 Decidable.Order 的 Poset 类包含您想要的属性。但是,Decidable.Order.Order 在这种情况下更好,因为它封装了关系的整体,确保对于任何两个元素,我们都可以得到其中一个更小的证据。

我有另一种使用 Order 的插入排序算法;它还显式分解 Empty 之间的区别和 NonEmpty列出并保存 max (现在可以添加到列表中的最大元素)类型为 NonEmpty 的值列表,这在一定程度上简化了证明。

我也在学习Idris,所以这段代码可能不是最地道的;另外,非常感谢#idris Freenode IRC channel 上的 Melvar 和 {AS} 帮助我弄清楚为什么以前的版本不起作用。

奇怪的with (y) | <pattern matches on y> sinsert 中的语法有没有为了绑定(bind)y对于 assert_smaller ,因为,由于某种原因,y@(NonEmpty xs)不起作用。

我希望这是有帮助的!

import Data.So
import Decidable.Order

%default total

data NonEmptySortedList : (a : Type)
-> (po : a -> a -> Type)
-> (max : a)
-> Type where
SOne : (el : a) -> NonEmptySortedList a po el
SMany : (el : a)
-> po el max
-> NonEmptySortedList a po max
-> NonEmptySortedList a po el

data SortedList : (a : Type) -> (po : a -> a -> Type) -> Type where
Empty : SortedList _ _
NonEmpty : NonEmptySortedList a po _ -> SortedList a po

head : NonEmptySortedList a _ _ -> a
head (SOne a) = a
head (SMany a _ _) = a

tail : NonEmptySortedList a po _ -> SortedList a po
tail (SOne _) = Empty
tail (SMany _ _ xs) = NonEmpty xs

max : {m : a} -> NonEmptySortedList a _ m -> a
max {m} _ = m

newMax : (Ordered a po) => SortedList a po -> a -> a
newMax Empty x = x
newMax (NonEmpty xs) x = either (const x)
(const (max xs))
(order {to = po} x (max xs))

either' : {P : Either a b -> Type}
-> (f : (l : a) -> P (Left l))
-> (g : (r : b) -> P (Right r))
-> (e : Either a b) -> P e
either' f g (Left l) = f l
either' f g (Right r) = g r

sinsert : (Ordered a po)
=> (x : a)
-> (xs : SortedList a po)
-> NonEmptySortedList a po (newMax xs x)
sinsert x y with (y)
| Empty = SOne {po = po} x
| (NonEmpty xs) = either' { P = NonEmptySortedList a po
. either (const x) (const (max xs))
}
insHead
insTail
(order {to = po} x (max xs))
where insHead : po x (max xs) -> NonEmptySortedList a po x
insHead p = SMany x p xs
max_lt_newmax : po (max xs) x -> po (max xs) (newMax (tail xs) x)
max_lt_newmax max_xs_lt_x with (xs)
| (SOne _) = max_xs_lt_x
| (SMany _ max_xs_lt_max_xxs xxs)
= either' { P = po (max xs) . either (const x)
(const (max xxs))}
(const {a = po (max xs) x} max_xs_lt_x)
(const {a = po (max xs) (max xxs)} max_xs_lt_max_xxs)
(order {to = po} x (max xxs))
insTail : po (max xs) x -> NonEmptySortedList a po (max xs)
insTail p = SMany (max xs)
(max_lt_newmax p)
(sinsert x (assert_smaller y (tail xs)))

insSort : (Ordered a po) => List a -> SortedList a po
insSort = foldl (\xs, x => NonEmpty (sinsert x xs)) Empty

关于list - idris中的排序列表(插入排序),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24105461/

31 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com