通常は、tarballとってきてmake installでいけるのだが、使っているcoqをコンパイルしたときのocamlと
ssreflectのプラグインをコンパイルするときのocamlのバージョンが違っているとinterface mismatchが出る。
このとき、parsing.cmxなどのロード中のモジュール「on Pervasives」などと原因となったモジュールの名前が表示されるので、ocamlobjinfo /usr/local/lib/coq/parsiong.cmx | grep Pervasives等でハッシュを見ることで確認できる。
coqを現在の版のocamlで再度コンパイルしインストールしなおすことで対処する。
fail log
2012年1月4日水曜日
2011年11月8日火曜日
SoftWare Abstraction 6.4.3 Cache Memory
models/book/chapter6/memory/CacheMemory.alsを改変。
loadの対象となるアドレスをmainにありかつ、対象をキャッシュに載ってないものから弱化したものにした。
これを実行すると、a1 ≠ a2 => d3 = d2を満たさないという反例が出る。
writeの結果キャッシュ上のa2はd2を指すようになったのだが、loadの対象にa2が選ばれる事によりc'の時点でmainが指すd1をc''の時点で指すようになってしまっている。
これを解釈した結果が本文での「flushされる前にloadされた」なのだが、そのような見方がしっくりくるまでかなり手間取ったというお話。
loadの対象となるアドレスをmainにありかつ、対象をキャッシュに載ってないものから弱化したものにした。
module chapter6/memory/cacheMemory [Addr, Data] ----- the model from page 219
sig CacheSystem {
main, cache: Addr -> lone Data
}
pred init [c: CacheSystem] {
no c.main + c.cache
}
pred write [c, c': CacheSystem, a: Addr, d: Data] {
c'.main = c.main
c'.cache = c.cache ++ a -> d
}
pred read [c: CacheSystem, a: Addr, d: Data] {
some d
d = c.cache [a]
}
pred load [c, c': CacheSystem] {
some addrs: Addr |
c'.cache = c.cache ++ addrs <: c.main
c'.main = c.main
}
pred flush [c, c': CacheSystem] {
some addrs: some c.cache.Data {
c'.main = c.main ++ addrs <: c.cache
c'.cache = c.cache - addrs -> Data
}
}
// This command should not find any counterexample
LoadNotObservable: check {
all c, c', c": CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
{
read [c, a2, d2]
write [c, c', a1, d1]
load [c', c"]
read [c", a2, d3]
} implies d3 = (a1=a2 => d1 else d2)
}
これを実行すると、a1 ≠ a2 => d3 = d2を満たさないという反例が出る。
writeの結果キャッシュ上のa2はd2を指すようになったのだが、loadの対象にa2が選ばれる事によりc'の時点でmainが指すd1をc''の時点で指すようになってしまっている。
これを解釈した結果が本文での「flushされる前にloadされた」なのだが、そのような見方がしっくりくるまでかなり手間取ったというお話。
2011年4月26日火曜日
存在限量子を解釈する際に勘違い
松坂の集合位相入門P.19あたりにある集合系のすべての要素を対象にした和集合をCoqの帰納型で表現しようとしたが、それを使って本文の命題を証明するときに問題が発生した。
本文中では
∪V = {x|∃ A∈V (x∈A)}というような∃量化を使った定義だったが、 これをCoqで使われるような表記に直す際に
forall x:U, exists A:Ensemble U, A∈V -> x∈Aという解釈をしてしまい、AがVに含まれない場合を考慮しなければならなくなった。集合系Vに含まれる筈の集合Aを議論する際にそれはないだろうと。
本文中の式を日本語で「定義されるXの全ての要素に対して、xを含むようなVの元Aが存在する」というように解釈すると、なんとなく後半が含意でなく論理積を表現しているようなにおいがするんだけど・・・∃より∀の方が使い慣れているので、こちらを使った定義でよく使われる含意を使った形式につられてしまったのだろうか
{x : P | Q}というような表記を使う形式だとPを|の右側に持ってくる際に、∀の場合は含意、∃の場合は論理積というようなパターンだったので多分最初の定義が間違ってる筈。
2011年1月27日木曜日
IFPuH 3.5
P.78-80
- Rational Numbersとはなんぞや
- canonical representation
- RationalをHaskellに前述のcanonical representationを保証しつつ導入する
- Rationalをpairとしてではなく独自の解釈によるEqやOrd、Showのインスタンスにする
- derivingを使わずにinstance宣言を書いた意義
- gcdの仕様と実装について
- totalな仕様とeuclidean algorithmによる計算
- Fractionalのinstanceとすることもできる
2011年1月15日土曜日
IFPuH ex1.2.1
問題
「x*yを評価する為にはxとyがnormal formに簡約できるということが必要である」という前提のもと、square infinityの評価が停止するかどうか
回答
square infinityという式の簡約をそのまま考える。
foo = hoge hoge
2011年1月12日水曜日
部分関数
- http://en.wikipedia.org/wiki/Relation_(mathematics)の中程にあるfunctional(also called right-unique)のことらしい
- このSpecial_types_of_binary_relationsのcheatsheet的なものはあれば便利かも
登録:
投稿 (Atom)