コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

CPLの練習 その2(加算)

前回

今回は加算をやろうと思う。
ネットで見たところ、少なくとも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.ooを第二引数に置換しているのかなと思って、
こういう加算を考えたけど、ダメだった。

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);

だから加算はこの形になるのか。