Bağımlı türlerin kullanışlılığı üzerine bir lisans tezi yazıyorum.Idris'te sıralanan liste (ekleme sırası)
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
satırı haline elemanı daha küçük veya eşit olduğu bir çalışma zamanı kanıtı gerektirir: yapım göre sınıflandırılmaktadır kanıtlanmış böylece Ben sadece sıralı liste halinde inşa edilebilir bir kabı, inşa etmeye çalışıyorum sıralanmış listedeki en küçük (ilk) öğe.
sinsert
yarattık:
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))
sorun kanıtlar kurmaya yaşıyorum (?iins21
, ?iins22
) ve biraz yardım için minnettar olurum. Beklemeyen bir varsayımdan emin olabilirim, fakat göremiyorum.
Ben de sıralı bir liste oluşturmak için daha iyi bir çözüm sağlamak için teşvik etmek istiyorum (Bu sıralandığını bir kanıtı değerle belki normal bir liste?)
Agda'da bir cevabım var, postalamalı mıyım? – user3237465
Bu kanıtları yazabileceğinizi sanmıyorum çünkü 'SortedList' türünüz çok [kör] (https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/) siparişin karışıklıkları. Örneğin, 'Ord' typeclass yokken' Transitionalivity: Ord a => {x: a} -> So (x <= y) -> So (y <= z) -> So (x <= z) 'gibi bir şeyi ispat edemezsiniz. Herhangi bir ispat yükümlülüğü – Cactus
“a” ya da “x” yerine “x” yerine “x” (“x”) yerine “Nat” gibi ifadeleri kullanarak daha da fazla kazanabilirsiniz. – Cactus