1

コンテキスト: Haskell クイックソートの実装に関するいくつかのプロパティを証明しています。次のコードは、非決定論的permute関数を定義するために必要なすべてです。Haskell の基本型LListではなく、使用していることに注意してください。[]問題の領域はpermute_LCons_expansion_correct定理です (定理というほどのものではありません)。

-- Data. A list is either `LNil` or constructed with a `vhead` element and a
-- `vtail` list.
data LList a = LNil | LCons {vhead :: a, vtail :: LList a}

-- Function. Append two lists.
{-@ reflect lappend @-}
lappend :: LList a -> LList a -> LList a
lappend LNil ys = ys
lappend (LCons x xs) ys = LCons x (lappend xs ys)

-- Function. Construct a list with 1 element.
{-@ reflect llist1 @-}
llist1 :: a -> LList a
llist1 x = LCons x LNil

-- Function. Construct a list with 2 elements.
{-@ reflect llist2 @-}
llist2 :: a -> a -> LList a
llist2 x y = llist1 x `lappend` llist1 y

-- Function. Map a list-function over a list and concatenate the resulting
-- lists (i.e. list-monadic bind).
{-@ reflect lbind @-}
lbind :: LList a -> (a -> LList b) -> LList b
lbind LNil f = LNil
lbind (LCons x xs) f = f x `lappend` lbind xs f

-- Function. Map a function over a list.
{-@ reflect lmap @-}
lmap :: (a -> b) -> (LList a -> LList b)
lmap f LNil = LNil
lmap f (LCons x xs) = LCons (f x) (lmap f xs)

{-@ reflect lmap2 @-}
-- Function. Map a binary function over two lists (zipping).
lmap2 :: (a -> b -> c) -> LList a -> LList b -> LList c
lmap2 f xs ys = lbind xs (\x -> lbind ys (\y -> llist1 (f x y)))

-- Function. Nondeterministically split a list into two sublists.
{-@ reflect split @-}
split :: LList a -> LList (LList a, LList a)
split LNil = llist1 (LNil, LNil)
split (LCons x xs) =
  split xs
    `lbind` \(ys, zs) ->
      llist1 (LCons x ys, zs) `lappend` llist1 (ys, LCons x zs)

-- Function. Nondeterministically permute a list.
{-@ reflect permute @-}
permute :: LList a -> LList (LList a)
permute LNil = llist1 LNil
permute (LCons x xs) =
  split xs `lbind` \(ys, zs) ->
    lmap2
      (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
      (permute ys)
      (permute zs)

-- Function. The expanded form of `permute` on an `LCons`.
{-@ reflect permute_LCons_expansion @-}
permute_LCons_expansion :: a -> LList a -> LList (LList a)
permute_LCons_expansion x xs =
  split xs
    `lbind` ( \(ys, zs) ->
                lmap2
                  (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
                  (permute ys)
                  (permute zs)
            )

-- Theorem. `permute_LCons_expansion` corresponds to `permute` on an `LCons`.
{-@
permute_LCons_expansion_correct :: x:a -> xs:LList a ->
  {permute (LCons x xs) = permute_LCons_expansion x xs}
@-}
permute_LCons_expansion_correct :: a -> LList a -> Proof
permute_LCons_expansion_correct x xs =
  permute (LCons x xs)
    ==. split xs
      `lbind` ( \(ys, zs) ->
                  lmap2
                    (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
                    (permute ys)
                    (permute zs)
              )
    ==. permute_LCons_expansion x xs
    *** QED

では、中央の式はケースの本体であり、 の定義でもあるpermute_LCons_expansion_correctため、方程式は正しいはずです。ただし、コンパイルすると、次の LH エラーが発生します。LConspermutepermute_LCons_expansion

❯ cabal build
Build profile: -w ghc-8.10.3 -O1
{{I have removed project files info}}

**** LIQUID: UNSAFE ************************************************************

src/Test.hs:83:9: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : (Test.LList (Test.LList a))
    .
    is not a subtype of the required type
      VV : {VV : (Test.LList (Test.LList a)) | permute (LCons x xs) == VV}
    .
    in the context
      xs : (Test.LList a)

      x : a
   |
83 |     ==. split xs
   |         ^^^^^^^^...

LH が暗黙の等価性を認識しないのはなぜですか? (==.)fromLanguage.Haskell.Equationalではなくfromを使用していることに注意してくださいLanguage.Haskell.ProofCombinators。

構成：

  • ghc バージョン 8.10.3
  • LiquidHaskell バージョン 0.8.6.0
  • カバル バージョン 3.2.0.0
4

0 に答える 0