divmodがやっと理解できたので、書く。
定義
let divmod =
ev.pair(
pr(
cur(pair(o.!, pi1).pi2),
cur(
ev.pair(
if(
cur(pair(s.pi1.pi1, sub.pair(pi2.pi1, pi2.pi2)).pi2),
cur(pi1 .pi2)
).ge.pair(pi2.pi1, pi2.pi2),
I
).pair(ev, pi2)
)
).s.pi1,
I
);
# = ev.pair(pr(Y, X).s.pi1, I) とおく
# cpl> simp full divmod.pair(s.s.o, s.o)
# pair(s.s.o.!,o)
# : 1 -> prod(nat,nat)
# 2 = 1 * 2 + 0
公式
- pr(Y, X).s.s.s.o => X.X.X.Y
- pair(a, b).c => pair(a.c, b.c)
- ev.pair(cur(X).Z, Y) => X.pair(Z, Y)
解説
第一引数のsの数+1回、Xをループする。
例では、3回Xをループする。
Yの中
pair(o.!, pi1)が蓄積変数といったところか。
例では、初期値は(o.!, s.s.o)になる。
例では
ifで
1回目 2 >= 1 真なので、pair(o.!, s.s.o)からpair(<+1>s.o.!, <2-1=1>s.o)に更新する
2回目 1 >= 1 真なので、pair(s.o.!, s.o)からpair(<+1>s.s.o.!, <1-1=0>o)に更新する
3回目 0 >= 1 偽なので、pair(s.s.o.!, o)から変更しない。もしループ回数が余分にあっても、このペアから変わる事はない。
このペアが答えである。
ソースコードとログ
