- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在写一篇关于依赖类型有用性的本科论文。
我正在尝试构造一个容器,它只能构造成一个排序列表,以便证明它是按构造排序的:
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/
我正在学习 Idris 并且我陷入了一个非常简单的引理,该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式,但 Idris 拒绝使用以下错误消息: RegExp.idr line 3
灵感来自 this blog post和 this code我想我会使用 Idris 的接口(interface)(类型类)在 Idris 中尝试一些类别理论。 我定义了Category如下,效果很好
借此我可以构建一个匿名的临时记录;那是可编辑的、可附加的、可修改的,其中每个值可以具有不同的异构类型,以及编译器检查消费者类型期望是否与所有给定键处生成的记录的类型一致? 类似于 Purescript
是否有一种简单的方法可以为数据类型编写相等 ( DecEq ) 实例?例如,我希望下面的 DecEq 中有 O(n) 行声明,其中 ?p很简单: data Foo = A | B | C | D in
是否有任何关于 postulate 的性质和用途的最新信息?在 idris build ?教程/手册中没有关于该主题的任何内容,我似乎也无法在 wiki 中找到任何内容。 TIA。 最佳答案 我认为我
在玩了一下 Idris 及其效果教程示例后,我终于弄清楚了如何链接效果。不确定链是否是正确的词,但我基本上是指一种效果是根据另一种效果实现的。 在这个例子中,我有一个效果,我称之为 Lower。它直接
Idris 中是否存在有理数的现有实现? 例如Data.Ratio 来自 Haskell 的端口。 最佳答案 通过快速搜索,我找到了 this , 如果它可能很有趣 关于idris - Idris 中
在官方 Idris wiki 上的非官方常见问题解答(官方是因为它在该语言的 git 仓库中),它是 stated that in a total language [e.g. Idris] we d
我在看 Idris tutorial .我无法理解以下代码。 disjoint : (n : Nat) -> Z = S n -> Void disjoint n p = replace {P = d
在 Idris 中定义我们在其他语言中称为常量的惯用方式是什么?是这个吗? myConstant : String myConstant = "some_constant1" myConstant2
在 idris 0.9.17.1 中, 灵感来自 https://wiki.haskell.org/Prime_numbers , 我编写了以下代码来生成素数 module Main concat:
我编写了一个函数doSomething,它接受一个左括号或右括号并返回相应的Int: doSomething : (c : Char) -> {auto isPar : c == '(' || c =
这实际上是我的第一行 Idris 代码。当我查阅文档时,一切都显得正确: Idris> data T = Foo Bool | Bar (T -> T) (input):1:6: | 1 | da
我正在使用 Idris 进行类型驱动开发,学习如何定义具有可变数量参数的函数。我有点野心,想写一个 mapN将映射 (n : Nat) 的函数的函数参数到 n一些 Applicative 的值类型。
我正在尝试编写一个函数 mSmallest需要两个自然数,n和 m作为输入并产生一个向量。输出向量包含 m有限集的最小成员 n成员。 例如 mSmallest 5 3应该生产 [FS (FS Z),
我在 Idris 中将幺半群定义为 interface Is_monoid (ty : Type) (op : ty -> ty -> ty) where id_elem : () -> ty
我正在阅读 Type driven development with Idris ,其中一个练习要求读者定义一个类型 TupleVect ,这样一个向量可以表示为: TupleVect 2 ty =
试图证明以下断言: equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n 我找到了 plusCommutes在图书馆里,但没有平
为什么 Idris 要求函数按照定义的顺序出现,并使用 mutual 声明的相互递归? 我希望 Idris 执行函数之间的第一次依赖分析,并自动对它们进行重新排序。我一直相信 Haskell 是这样做
我一直无法让 Idris 整体检查器相信我的功能是完整的。这是我遇到的问题的一个简单示例版本。假设我们有一个如下形式的非常简单的表达式类型: data SimpleType = Prop | Fn S
我是一名优秀的程序员,十分优秀!