日々の流転

λ. バグ?

以下のゴールをrefineしようとすると、「Id |(Wrap A) (In a1) (In a2) = ?197 is unsolvable since Expression a1 is not equal to a」等と言われてしまう。この文脈ではa,a1,a2の間には definitional equality が成り立っていないといけないと思うので、これはバグっぽい気がする。

--#include "Hedberg/SET.alfa"
open SET use Id, refId, Zero

data Wrap (A::Set) = In (a::A)

Bug (A::Set) (x,y::Wrap A) (p::Id x y) :: Set
Bug = case x of
        (In a1)->
            case y of
              (In a2)->
                  let f (q::Id a1 a2) :: Set
                      f = case q of
                            (ref a)->
                                {! Id p (refId (In a)) !}
                  in Zero

λ. モデル検査法のソフトウェア検証への応用. 中島震

コンピュータソフトウェア, Vol.23, No.2 (2006), pp.72-86.

を読んだ。 チュートリアルというよりはサーベイのような気がしないでもない。