トップ «前の日記(2003-01-20) 最新 次の日記(2003-01-23)» 月表示 編集

日々の流転


2003-01-21 [長年日記]

λ. システムプログラミング

最後なのに質問一つなくて退屈だった。皆様他の授業で必死なんでしょうな。

λ. "Sketches: Outline with references"

を後で読んでみよう。

Tags: 圏論 論文

λ. CPLでアッカーマン関数

アッカーマン関数と高階原始帰納関数の続き。 書けた気がする。

  • ack(0,y) = y+1
  • ack(x+1,0) = ack(x,1)
  • ack(x+1,y+1) = ack(x,ack(x+1,y))

  • ack(0)(y) = y+1
  • ack(x+1)(y) = ack(x)y+1(1)

と書き直せるので、

cpl> let times = eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1, eval.pair(pi2.pi1, pi2))))), I)
times : prod(nat,exp(*a,*a)) -> exp(*a,*a)  defined
cpl> let ack_0 = curry(s.pi2)
ack_0 : *a -> exp(nat,nat)  defined
cpl> let ack_s = curry(eval.pair(times.pair(s.pi2, pi1), s.0.!))
ack_s : exp(nat,nat) -> exp(nat,nat)  defined
cpl> let ack = eval.prod(pr(ack_0, ack_s), I)
ack : prod(nat,nat) -> nat  defined

という感じで定義できる。確かに高階だけど原始帰納的な感じだ。

cpl> simp full ack.pair(s.s.s.0, s.0)
s.s.s.s.s.s.s.s.s.s.s.s.s.0.!
    : *a -> nat

む、簡約後に型を再計算しているので、 簡約前よりも型が緩くなってしまう可能性があるのか。 これは不味いかなぁ。

Tags: CPL