前回
今回は加算をやろうと思う。
ネットで見たところ、少なくとも3つの定義があった。
# 加算1 let add1 = ev.prod(pr(cur(pi2), cur(s.ev)), nat); # 加算2 let add2 = ev.prod(pr(cur(pi2), exp(s, I)), I); # 加算3 let add3 = ev.pair(pr(cur(pi2), cur(s.ev)).pi1, pi2);
加算2は保留しようと思う。
加算1を簡約すると、加算3になる。
加算3が標準的ぽい。なので加算3で考える。
詳細は貼り付け先を見ていただくとして、
以下の公式?を使うと分かりやすいと思う。
pair(a, b).c => pair(a.c, b.c) ev.pair(cur(X).Z, Y) => X.pair(Z, Y)
加算の第一引数のs.s...s.o
のo
を第二引数に置換しているのかなと思って、
こういう加算を考えたけど、ダメだった。
cpl> simp pi1.pair(pr(pi2, s).pi1, I).pair(s.s.o, s.o) ↑s.oを取ってこれない types do not unify
うさぎ小屋のOnaka氏が言っていたのは、こういう事だったんだ。
cplには値の束縛の概念がないため、使いたい値は使う場所まで運ばねばなりません。
高階関数を用いる際だけでなく、原始帰納法prの内側などの直接値を運べない場所から
外部の値を参照する時などにも関数空間が活躍します。
デクリメントの場合は、引数?が自然数1つだから、直接pr
をかませた。
加算の場合は、引数?はpair(,)
なので、pair
の要素をpr
の内側へ運ぶには、
cur
を使うしかない。
let add3 = ev.pair(pr(cur(pi2), cur(s.ev)).pi1, pi2);
だから加算はこの形になるのか。