トップ «前の日記(2007-06-24) 最新 次の日記(2007-06-27)» 月表示 編集

日々の流転


2007-06-26 [長年日記]

λ. Coq の extraction

<URL:http://d.hatena.ne.jp/syd_syd/20070622#p1><URL:http://www.eva-01.jp/d/?date=20070623#p03> あたりを読んで、なるほどと思った。 Coqではextractionをそういう風に使うのね。 AgdaだとそもそもSetとPropの区別が無いから、extractionのようなことをあまり意識したことがなかった(Agdaで書くと下みたいになっちゃうし*1)。考え方の違いが面白い。

Decidable :: Set -> Set
Decidable P = P `Or` (Not P)

lemma :: (C::Context) -> (e::Expr) -> (t::Type) -> Decidable (C |- e : t))
lemma = ...

typeCheck :: (C::Context) -> (e::Expr) -> (t::Type) -> Bool
typeCheck C e t =
  case lemma C e t of
  (inl x) -> true
  (inr y) -> false
Tags: agda

*1 表記はちょっと誤魔化してるけど

本日のツッコミ(全2件) [ツッコミを入れる]
ψ ikegami (2007-06-29 20:28)

Agda2ではSetはSet, PropはPropになります。<br>http://www.cs.chalmers.se/~ulfn/darcs/Agda2/src/full/Syntax/Parser/Tokens.hs<br>(誰も見なさそうなコード)

ψ さかい (2007-06-29 21:33)

おお、そうなんですかー。<br>全然知りませんでした。ありがとうございます。<br>目的はやはりextractionというかerasure?のためなのでしょうか?