トップ «前の日記(2005-03-03) 最新 次の日記(2005-03-08)» 月表示 編集

日々の流転


2005-03-04 [長年日記]

λ.

雪だ雪だー

写真

λ. 情報理論勉強会@古川研

テキストは 『情報理論の基礎 — 情報と学習の直観的理解のために —』, 村田 昇 。難い。

λ. ∀A: N→*. A(zero) → (∀n: N. A(n)→A(succ(n))) → ∀n: N. A(n)

N,zero,succをそれぞれ

  • N = λX: *. X→(X→X)→X
  • zero = λX: *. λz: X. λs: X→X. z
  • succ = λn: N. (λX: *. λz: X. λs: X→X. s (n X z s))

とする。Calculus of Constructions (CC) では、この定義からは ∀A: N→*. A(zero) → (∀n: N. A(n)→A(succ(n))) → ∀n: N. A(n) *1 という型の関数を導出できないそうだ。そこで素朴な疑問なのだが、N,zero,succ の定義を適切に変更すれば、CCでこれを導出出来るのだろうか?

ちなみに、Haskellで無理やり書くとこんな感じか。

data Z = Z
newtype S n = S n
 
class N n where
    ind :: t Z -> (forall m. N m => t m -> t (S m)) -> t n
 
instance N Z where
    ind z _ = z
 
instance N n => N (S n) where
    ind z s = s (ind z s)

これと同様の方法を使って簡単な行列ライブラリをHaskellで書いてみた(2005-04-06)。

*1 正確に書くなら ∏A: (∏n: N. *). A(zero) → (∏n: N. A(n)→A(succ(n))) → ∏n: N. A(n)