6

私はストリームに似たものを書いてきました。各ファンクターの法則を証明することはできますが、それが合計であることを証明する方法がわかりません。

module Stream

import Classes.Verified

%default total

codata MyStream a = MkStream a (MyStream a)

mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)

streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s = mapStream g (mapStream f s)
streamFunctorComposition (MkStream x y) f g =
  let inductiveHypothesis = streamFunctorComposition y f g
  in ?streamFunctorCompositionStepCase

---------- Proofs ----------
streamFunctorCompositionStepCase = proof
  intros
  rewrite inductiveHypothesis
  trivial

与えます:

*Stream> :total streamFunctorComposition
Stream.streamFunctorComposition is possibly not total due to recursive path:
    Stream.streamFunctorComposition, Stream.streamFunctorComposition

全体性チェッカーも通過するcodataに対するファンクターの法則を証明するトリックはありますか?

4

1 に答える 1

7

Daniel Peebles (copumpkin)から IRC に関する少しの助けを得ることができました。Daniel Peebles (copumpkin)は、codata に対して命題の等価性を使用できることは、通常は許可されていないことであると説明しました。彼は、Agda がData.Streamに対して定義する方法のように、カスタムの等価関係を定義することが可能であると指摘しました。

data _≈_ {A} : Stream A → Stream A → Set where
  _∷_ : ∀ {x y xs ys}
        (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys

この定義を Idris に簡単に翻訳することができました。

module MyStream

%default total

codata MyStream a = MkStream a (MyStream a)

infixl 9 =#=

data (=#=) : MyStream a -> MyStream a -> Type where
  (::) : a = b -> Inf (as =#= bs) -> MkStream a as =#= MkStream b bs

mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)

streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s =#= mapStream g (mapStream f s)
streamFunctorComposition (MkStream x y) f g =
  Refl :: streamFunctorComposition y f g

そして、これは単純な帰納法を行っているだけなので、全体性チェッカーを簡単に通過しました。

VerifiedFunctorこの事実は、ストリーム タイプに を定義できないことを意味しているように見えるので、少しがっかりします。

Daniel はまた、観察型理論ではcodata に対する命題の等価性が認められていることも指摘しました。これは検討すべきことです。

于 2015-05-26T04:18:10.800 に答える