2014-06-08 30 views
10

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.

sıralanmamış listesini sıralamak gerekirse, sıralı bir liste sıralı bir liste alır ve bir öğe ekler ve döndüren bir işlev 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?)

+1

Agda'da bir cevabım var, postalamalı mıyım? – user3237465

+0

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

+0

“a” ya da “x” yerine “x” yerine “x” (“x”) yerine “Nat” gibi ifadeleri kullanarak daha da fazla kazanabilirsiniz. – Cactus

cevap

1

Bence orada deliller ile temel sorun Cactus'un bir yorumda belirttiği gibi, ekleme sıralama ispatının çalışması için gerekli olan geçişlilik ve antisimetri gibi özelliklere sahip olmamanızdır. Bununla birlikte, hala bir polimorfik kapsayıcı yapabilirsiniz: Decidable.Order tarafından sağlanan Poset sınıfı, tam olarak istediğiniz özellikleri içerir. Ancak, Decidable.Order.Order bu durumda daha iyidir, çünkü ilişkinin bütünlüğünü kapsarken, herhangi iki unsur için birinin daha küçük olduğuna dair bir kanıt elde edebiliriz.

Sipariş kullanan bir başka ekleme sıralama algoritmam var; Ayrıca Empty ve NonEmpty listelerinin arasındaki ayrımı açıkça bozar ve(şimdi listeye eklenebilecek en büyük öğe) değerini NonEmpty listelerinin türünde tutar, bu da kanıtları biraz kolaylaştırır.

Ayrıca, İdris'i öğrenme sürecindeyim, bu yüzden bu kod en çok deyimsel olmayabilir; Ayrıca, önceki sürümlerin neden çalışmadığını anlamaya yardımcı olmak için #idris Freenode IRC kanalında Melvar ve {AS} çok teşekkürler.

sinsert garip with (y) | <pattern matches on y> sözdizimi nedense beri assert_smaller için y bağlamak için, orada [email protected](NonEmpty xs) çalışmaz.

Umarım bu yardımcı olur!

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