日々の流転

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

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

λ. "Sketches: Outline with references"

を後で読んでみよう。

λ. 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

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