日々の流転

λ. Agda

Agda をインストールした。AgdaはCoqやIsabelle/HOLなんかと同様の定理証明系(証明支援系)。特徴は証明を関数型言語のプログラムとして書く点だろうか。文法はHaskellに似ているが、dependent type も扱える。証明を独自の言語で書くのではなく、関数型言語の一般的な notation で書けるのは、私のようなプログラマには嬉しそうだ。

使ってみてまず驚いたのは再帰的な定義が好き勝手に出来る点。例えば、bottom (P :: Set) :: P = bottom P なんて定義も出来てしまう。Isabelle/HOL なんかでは「再帰呼び出しのときに、引数がある意味で必ず小さくなることを示すことが必要」だったけど、Agdaはこれで問題ないのだろうか!?

[2005-05-19 追記] Why Dependent Types Matter. Thorsten Altenkirch Conor McBride James McKinna には次のように書いてあった。

It's reasonable to allow arbitrary recursion in type-level programs, provided you have some sort of cut-off mechanism which interrupts loops when they happen in practice. This is the approach taken by the Agda proof system, Cayenne and by Haskell with `undecidable instances' —Haskell's overloading resolution amounts to executing a kind of `compile-time Prolog'. Agda restores logical soundness by a separate termination check, performed after typechecking. The basic point is that you include recursive programs in types at your own risk: mostly they're benign and typechecking behaves sensibly.

[2006-03-25 追記] 上記の bottom のような定義は、C-c C-x C-t で agda-check-termination にかけると "The call: bottom\n might lead to non-termination" と判定してくれる。停止性の保障に使ってるアルゴリズムは何なんだろう? Size Change Termination (SCT)?

もっとも、以下のように定義すると停止性チェックは通ってしまう。 このような場合をちゃんと扱うにはどうすればよいか?　また、これは GHCのinlinerの問題と似ているように思うがどうなのか?

data T (P::Set) = PsiInv (x :: T P -> P)
 
psi (|P::Set) (x::T P) :: T P -> P
  = case x of
    (PsiInv y) -> y
 
fix (|P::Set) (f::P -> P) :: P
  = let g (x::T P) :: P = f (psi x x)
    in g (PsiInv g)
 
id (|P::Set) (x::P) :: P = x
 
bottom (P::Set) :: P = fix id

[2006-03-25 追記] いや、以下のアッカーマン関数の停止性を認識できないので、SCTではないか。ソースを見ると、src/Termination.hs には「Based on "foetus" type checker of Andreas Abel and Thorsten Altenkirch (Ludwigs-Maximilians-University, 1997-1999).」と書いてあるので、Andreas Abel. foetus Termination Checker for Simple Functional Programs が元になっているのかな。まあ、どうでもいいけど。

data Nat = Zero | Succ (m::Nat)
 
ack (m::Nat) (n::Nat) :: Nat
  = case m of 
    (Zero   )-> Succ n
    (Succ m')->
      case n of 
      (Zero   )-> ack m' (Succ Zero)
      (Succ n')-> ack m' (ack m n')

λ. ホーンティング

安直で分かりやすい構図。ホラーという感じはあまりしないな。

λ. 五月病!?

どうもやる気が出ない。やらなくちゃいけないことは幾つかあるのだけど、取り掛かる気が億劫で仕方ない。困った。——困っていたら、これがひょっとしていわゆる五月病って奴なのではないかと思った。なるほど。そう考えたら、なんだか少し気が楽になった。気が楽になっただけで、問題は一切解決してないけど。