日々の流転

λ. 雪

雪だ雪だー

写真

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

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

λ. ∀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)。