CPLの練習

addTrace01.txt

★★★19/10/27　理解できた
★★★19/10/22　理解できなかった
cpl> simp add1.pair(o, s.s.o)
0:add1.pair(o,s.s.o)*I
1[1]:pair(o,s.s.o)*I
2:add1*pair(o,s.s.o)
  let add1 = ev.prod(pr(cur(pi2), cur(s.ev)),     nat);   add1が
  let add3 = ev.pair(pr(cur(pi2), cur(s.ev)).pi1, pi2);   add3と同じになってる
3:ev.pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(o,s.s.o)
4[1]:pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(o,s.s.o)
5: ev*pair(pr(cur(pi2),cur(s.ev)).pi1,pi2).pair(o,s.s.o)  <- pair(a, b).c => pair(a.c, b.c)
-- -----------------------------------------------------
            6: pr(cur(pi2),cur(s.ev)).pi1*pair(o,s.s.o)   <- a.c
                7[1]:pi1*pair(o,s.s.o)
                8[1]:o*I
            9:pr(cur(pi2),cur(s.ev))*o
            10:cur(pi2)*I
-- -----------------------------------------------------
            pi2.pair(o, s.s.o)                            <- b.c
-- -----------------------------------------------------
11-0: ev.pair(cur(pi2).I, pi2.pair(o, s.s.o))             <- ev.pair(cur(X).I, Y)
11:pi2*pair(I, pi2.pair(o, s.s.o))                                => X.pair(I, Y)
12:pi2.pair(o,s.s.o)*I
13[1]:pair(o,s.s.o)*I
14:pi2*pair(o,s.s.o)
15:s.s.o*I
16[1]:s.o*I
17[2]:o*I
18[1]:s*o
19:s*s.o
20:I*s.s.o
s.s.o
    : 1 -> nat

cpl> simp add1.pair(s.s.o, o)
0:add1.pair(s.s.o,o)*I
1[1]:pair(s.s.o,o)*I
2:add1*pair(s.s.o,o)
3:ev.pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(s.s.o,o)
4[1]:pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(s.s.o,o)
5:ev*pair(pr(cur(pi2),cur(s.ev)).pi1, pi2).pair(s.s.o,o)  <- pair(a, b).c => pair(a.c, b.c)
-- -----------------------------------------------------
6:pr(cur(pi2),cur(s.ev)).pi1*pair(s.s.o,o)                <- a.c
7[1]:pi1*pair(s.s.o,o)
8[1]:s.s.o*I
9[2]:s.o*I
10[3]:o*I
11[2]:s*o
12[1]:s*s.o
13:pr(cur(pi2),cur(s.ev))*s.s.o
14:cur(s.ev).pr(cur(pi2),cur(s.ev))*s.o
15[1]:pr(cur(pi2),cur(s.ev))*s.o
16[1]:cur(s.ev).pr(cur(pi2),cur(s.ev))*o
17[2]:pr(cur(pi2),cur(s.ev))*o
18[2]:cur(pi2)*I
19[1]:cur(s.ev)*cur(pi2)
20: cur(s.ev)*cur(s.ev).cur(pi2)
-- -----------------------------------------------------
            pi2.pair(s.s.o,o)                             <- b.c
-- -----------------------------------------------------
21-0: ev*pair(cur(s.ev).cur(s.ev).cur(pi2), pi2.pair(s.s.o,o))  <- ev.pair(cur(X).Z, Y)
21: ★s★.ev*pair(cur(s.ev).cur(pi2),pi2.pair(s.s.o,o))           => X.pair(Z, Y)
22[1]:ev*pair(cur(s.ev).cur(pi2),pi2.pair(s.s.o,o))       <- ev.pair(cur(X).Z, Y)
-- -----------------------------------------------------
            23[1]:cur(s.ev).cur(pi2)*I
            24[2]:cur(pi2)*I
            25[1]:cur(s.ev)*cur(pi2)
-- -----------------------------------------------------
26[1]:★s★.ev*pair(cur(pi2), pi2.pair(s.s.o,o))                  => X.pair(Z, Y)
27[2]:ev*pair(cur(pi2), pi2.pair(s.s.o,o))                <- ev.pair(cur(X).I, Y)
-- -----------------------------------------------------
            28[2]:cur(pi2)*I
-- -----------------------------------------------------
29[2]:pi2*pair(I, pi2.pair(s.s.o,o))                             => X.pair(I, Y)
30[2]:pi2.pair(s.s.o,o)*I
    31[3]:pair(s.s.o,o)*I
32[2]:pi2*pair(s.s.o,o)
33[2]:o*I
34[1]:s*o
35:s*s.o
36:I*s.s.o
s.s.o
    : 1 -> nat
cpl>


-- -----------------------------------------------------
  let add2 = ev.prod(pr(cur(pi2), exp(s, I)),     I);                    add2が
3:ev.pair(pr(cur(pi2), cur(ev.pair(pi1, s.pi2))).pi1, pi2)*pair(o,s.s.o) これになってる、こちらは保留

addTrace02.txt

★★★ addTrace01.txt を直したから、こちらは見なくて良い

★★★19/10/23　理解できた
cpl> simp full add1.pair(o, s.s.o)
0:add1.pair(o,s.s.o)*I
    1[1]:pair(o,s.s.o)*I
    2[1]:o*I
    3[1]:s.s.o*I
    4[2]:s.o*I
    5[3]:o*I
    6[2]:s*o
    7[1]:s*s.o
8:add1*pair(o,s.s.o)
9:ev.pair( pr(cur(pi2), cur(s.ev)).pi1, pi2 )*pair(o, s.s.o)
    10[1]:pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(o,s.s.o)  ← pair(a, b).c => pair(a.c, b.c)
-- -----------------------------------------------------
    11[1]:     pr(cur(pi2),cur(s.ev)).pi1     *pair(o,s.s.o)
    12[2]:                            pi1     *pair(o,s.s.o)
    13[2]:                                          o*I
    14[1]:     pr(cur(pi2),cur(s.ev))*o
    15[1]:        cur(pi2)*I                ← cur(pi2.pair(pi1,pi2)) = cur(X)
-- -----------------------------------------------------
    16[1]:pi2*pair(o,s.s.o)
    17[1]:s.s.o*I
    18[2]:s.o*I
    19[3]:o*I
    20[2]:s*o
    21[1]:s*s.o                             ← Y
-- -----------------------------------------------------
22:ev*pair(cur(pi2.pair(pi1,pi2)), s.s.o)
23:pi2.pair(pi1,pi2)*pair(I,s.s.o)          ← ev.pair(cur(X), Y)がX.pair(I, Y)になった
    24[1]:pair(pi1,pi2)*pair(I,s.s.o)
    25[1]:pi1*pair(I,s.s.o)
    26[1]:I*I
    27[1]:pi2*pair(I,s.s.o)
    28[1]:s.s.o*I
    29[2]:s.o*I
    30[3]:o*I
    31[2]:s*o
    32[1]:s*s.o
33:pi2*pair(I,s.s.o)
34:s.s.o*I
    35[1]:s.o*I
    36[2]:o*I
    37[1]:s*o
38:s*s.o
39:I*s.s.o
s.s.o
    : 1 -> nat

divmod.cpl

# > chcp 65001
# > cpl -i divmod.cpl

# 終対象
right object 1 with ! is
end object;

# 積
right object prod(A, B) with pair is
  pi1: prod -> A
  pi2: prod -> B
end object;

# 冪
right object exp(A, B) with cur is
  ev: prod(exp, A) -> B
end object;

# 自然数
left object nat with pr is
  o: 1   -> nat
  s: nat -> nat
end object;

# 真偽値
left object bool with if is
    true:  1 -> bool
    false: 1 -> bool
end object;


# デクリメント
let pred = pi2.pr(pair(o, o), pair(s.pi1, pi1));
# let pred2(x) = pred3(pred.x)
# let pred3(x) = pred2(pred.x)

# 加算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);

# 加算4
let add4(x1, x2) = pr(x2, s).x1;
# 減算
let sub4(x1, x2) = pr(x1, pred).x2
# 乗算
let mul4(x1, x2) = pr(o, pr(x2, s)).x1;


# divmodで挫折したwが改めて理解した
let swap = pair(pi2,pi1);
let sub = ev.prod(pr(cur(pi2),cur(pred.ev)),nat).swap;
let zeroq = pr(true,false.!);
let and = ev.prod(if(cur(pi2),cur(false.!.pi2)),I);
let or  = ev.prod(if(cur( true.!.pi2),cur(pi2)),I);
let not = if(false,true);
let eq = and.prod(zeroq,zeroq).pair(sub,sub.swap);
let gt = and.prod(not.zeroq,zeroq).pair(sub,sub.swap);
let ge = or.pair(gt,eq);

# cpl> simp full divmod.pair(s.s.s.s.s.s.s.o, s.s.s.o)
# pair(s.s.o.!,s.o)
#     : 1 -> prod(nat,nat)
# cpl>
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)
      )                # =X

    ).s.pi1,
    I
  );

# let divmod =
#   ev.pair(pr(Y, X).s.pi1, I);
# ev.pair(X.X.X.Y, pair(s.s.o, s.o))
#         ~~~~~~ループ回数

# 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)
#    .pair(X.X.Y, pair(s.s.o, s.o))

# 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.pair(X.X.Y, pair(s.s.o, s.o)), pair(s.s.o, s.o))
#        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ =Z

# Z =
#   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.pair(X.Y, pair(s.s.o, s.o)), pair(s.s.o, s.o))
#          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ =U

# U =
#   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.pair(Y, pair(s.s.o, s.o)), pair(s.s.o, s.o))
#          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ =V

# V = pair(o.!, pi1).pi2.pair(I, pair(s.s.o, s.o))
#   = pair(o.!, pi1).pair(s.s.o, s.o)
#   = pair(o.!, s.s.o)

# U =
#   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(pair(o.!, s.s.o), pair(s.s.o, s.o))
#   =
#   ev.pair(if(cur(pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2),cur(pi1.pi2)).ge.pair(pi2.pi1,pi2.pi2).pair(pair(o.!, s.s.oこっち), pair(s.s.o, s.o)
#           pair(pair(o.!, s.s.o), pair(s.s.o, s.o))
#          )
#   =
#   ev.pair(if(cur(pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2),cur(pi1.pi2)).ge.pair(s.s.o, s.o),
#           pair(pair(o.!, s.s.o), pair(s.s.o, s.o))                                     ★ 2 >= 1
#          )
#   =
#   ev.pair(cur(pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2),
#           pair(pair(o.!, s.s.o), pair(s.s.o, s.o))
#          )
#   = pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2.pair(I, pair(pair(o.!, s.s.o), pair(s.s.o, s.o)))
#   = pair(s.pi1.pi1, sub.pair(pi2.pi1,pi2.pi2)).pair(pair(o.!, s.s.oこっち), pair(s.s.o, s.o))
#   = pair(s.o.!, sub.pair(s.s.o, s.o))
#   = pair(s.o.!, s.o)

# Z =
#   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(pair(s.o.!, s.o), pair(s.s.o, s.o))                                           ★ 1 >= 1
#   = pair(s.s.o.!, o)

# 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(pair(s.s.o.!, o), pair(s.s.o, s.o))                                             ★ 0 >= 1
# =
# ev.pair(cur(pi1.pi2),
#         pair(pair(s.s.o.!, o), pair(s.s.o, s.o))
#        )
# = pi1.pi2.pair(I, pair(pair(s.s.o.!, o), pair(s.s.o, s.o)))
# = pair(s.s.o.!, o) できたー！

```haskell
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);
# : uncurry2
#X# => ev.pair(X, I)
$ : curry
ff : fst.fst
ss : snd.snd
fs : fst.snd
sf : snd.fst
ev.pair(cur(X).Z, Y) => X.pair(Z, Y)
let divmod =
  #pr(
    $p(o.!, fst).snd$, 
    $#if($p(s.ff, sub.p(sf, ss)).snd$, $fs$).ge.p(sf, ss)#.p(ev, snd)$
  ).s.fst#;
```

# ぼつ
# cpl> set trace on
# cpl> simp full divmod.pair(o, o)                    
# 0:divmod.pair(o,o)*I
# 1[1]:pair(o,o)*I
# 2[1]:o*I
# 3[1]:o*I
# 4:divmod*pair(o,o)

# ★cpl> simp full cur(pair(o.!,pi1).pi2)
# cur(pair(o.!,pi1).pi2.pair(pi1,pi2))
#     : *c -> exp(prod(*a,*b),prod(nat,*a))

# 5: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)*pair(o,o)
# 5:ev.pair(pr(cur(Y), cur(X)).s.pi1, I).pair(o, o)
#  :ev.pair(pr(cur(Y), cur(X)).s.o, pair(o, o))
#   where
#     Y = pair(o.!,pi1).pi2、　　cur(Y)を簡約するとcur(Y.pair(pi1, pi2))になる★
#     X = 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)
#   ◇ pr(B, A).s.o → A.B を使う
# →ev.pair(cur(X).cur(Y.pair(pi1, pi2)), pair(o, o))
#   ◇ ev.pair(cur(X).Z, U) => X.pair(Z, U) を使う
# →19へ繋がる X.pair(cur(Y.pair(pi1,pi2)), pair(o, o))

# 6[1]: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)*pair(o,o)
# 7[1]: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*pair(o,o)
# 8[2]:s.pi1*pair(o,o)
# 9[3]:pi1*pair(o,o)
# 10[3]:o*I
# 11[2]:s*o
# 12[1]: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.o
# 13[1]: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)).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)))*o
# 14[2]: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)))*o
# 15[2]:cur(pair(o.!,pi1).pi2)*I
# 16[1]: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))*cur(pair(o.!,pi1).pi2.pair(pi1,pi2))     
# 17[1]:I*pair(o,o)
# 18:ev*pair(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).pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2)).pi1,pi2)),pair(o,o))

# 19: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)
#        .pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2)).pi1,pi2)*pair(I,pair(o,o))

# 20[1]:pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2)).pi1,pi2)*pair(I,pair(o,o))
# 21[1]:cur(pair(o.!,pi1).pi2.pair(pi1,pi2)).pi1*pair(I,pair(o,o))
# 22[2]:pi1*pair(I,pair(o,o))
# 23[2]:I*I
# 24[1]:cur(pair(o.!,pi1).pi2.pair(pi1,pi2))*I
# 25[1]:pi2*pair(I,pair(o,o))
# 26[1]:pair(o,o)*I
# 27[1]:o*I
# 28[1]:o*I

# 29: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)
#      .pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2).pair(pi1,pi2)), pair(o,o))
#                                               ~~~~~~~~~~~~~~
#   ◇ pair(A, B).C => pair(A.C, B.C) を使う
# --: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.pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2).pair(pi1,pi2)), pair(o,o)),
#            pi2.pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2).pair(pi1,pi2)), pair(o,o)) )
#
#   ◇ ev.pair(cur(X).Z, U) => X.pair(Z, U) を使う
# --: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(pair(o.!, o第一引数),
#            pair(o,o))
#
# --:ev.pair(if(cur(pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2),cur(pi1.pi2))
#             .ge.pair(o第一引数, o第二引数)),
#            .pair(pair(o.!, o), pair(o,o))
#           )
# →311へ繋がる

# 30[1]: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)*pair(cur(pair(o.!,pi1).pi2.pair(pi1,pi2).pair(pi1,pi2)),pair(o,o))
# ...
# 310[1]:I*pair(pair(o.!,o),pair(o,o))

# 311:ev*pair(cur(pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2.pair(pi1,pi2)),
#                                                          ~~~~~~~~~~~~~~~~~~簡約したらpi2
#             pair(pair(o.!, o),pair(o, o)) )

# 312:pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2.pair(pi1,pi2)*
#      pair(I,
#           pair(pair(o.!,o),pair(o,o)) )

# 313[1]:pair(pi1,pi2)*pair(I,pair(pair(o.!,o),pair(o,o)))
# 314[1]:pi1*pair(I,pair(pair(o.!,o),pair(o,o)))
# 315[1]:I*I
# 316[1]:pi2*pair(I,pair(pair(o.!,o),pair(o,o)))
# 317[1]:pair(pair(o.!,o),pair(o,o))*I
# 318[1]:pair(o.!,o)*I
# 319[1]:o.!*I
# 320[2]:!*I
# 321[1]:o*!
# 322[1]:o*I
# 323[1]:pair(o,o)*I
# 324[1]:o*I
# 325[1]:o*I

# 326:pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2)).pi2*pair(I,pair(pair(o.!,o),pair(o,o)))
# 327[1]:pi2*pair(I,pair(pair(o.!,o),pair(o,o)))
# 328[1]:pair(pair(o.!,o),pair(o,o))*I
# 329[1]:pair(o.!,o)*I
# 330[1]:o.!*I
# 331[2]:!*I
# 332[1]:o*!
# 333[1]:o*I
# 334[1]:pair(o,o)*I
# 335[1]:o*I
# 336[1]:o*I

# 337:pair(s.pi1.pi1,sub.pair(pi2.pi1,pi2.pi2))*pair(pair(o.!,o),pair(o,o))
# 338:s.pi1.pi1*pair(pair(o.!,o),pair(o,o))
# 339[1]:pi1.pi1*pair(pair(o.!,o),pair(o,o))
# 340[2]:pi1*pair(pair(o.!,o),pair(o,o))
# 341[2]:pair(o.!,o)*I
# 342[2]:o.!*I
# 343[3]:!*I
# 344[2]:o*!
# 345[2]:o*I
# 346[1]:pi1*pair(o.!,o)
# 347[1]:o.!*I
# 348[2]:!*I
# 349[1]:o*!
# 350:s*o.!
# 351:sub.pair(pi2.pi1,pi2.pi2)*pair(pair(o.!,o),pair(o,o))
# 352[1]:pair(pi2.pi1,pi2.pi2)*pair(pair(o.!,o),pair(o,o))
# 353[1]:pi2.pi1*pair(pair(o.!,o),pair(o,o))
# 354[2]:pi1*pair(pair(o.!,o),pair(o,o))
# 355[2]:pair(o.!,o)*I
# 356[2]:o.!*I
# 357[3]:!*I
# 358[2]:o*!
# 359[2]:o*I
# 360[1]:pi2*pair(o.!,o)
# 361[1]:o*I
# 362[1]:pi2.pi2*pair(pair(o.!,o),pair(o,o))
# 363[2]:pi2*pair(pair(o.!,o),pair(o,o))
# 364[2]:pair(o,o)*I
# 365[2]:o*I
# 366[2]:o*I
# 367[1]:pi2*pair(o,o)
# 368[1]:o*I
# 369:sub*pair(o,o)
# 370:ev.pair(pr(cur(pi2),cur(pred.ev)).pi1,pi2).swap*pair(o,o)
# 371[1]:pair(pr(cur(pi2),cur(pred.ev)).pi1,pi2).swap*pair(o,o)
# 372[2]:swap*pair(o,o)
# 373[2]:pair(pi2,pi1)*pair(o,o)
# 374[2]:pi2*pair(o,o)
# 375[2]:o*I
# 376[2]:pi1*pair(o,o)
# 377[2]:o*I
# 378[1]:pair(pr(cur(pi2),cur(pred.ev)).pi1,pi2)*pair(o,o)
# 379[1]:pr(cur(pi2),cur(pred.ev)).pi1*pair(o,o)
# 380[2]:pi1*pair(o,o)
# 381[2]:o*I
# 382[1]:pr(cur(pi2),cur(pred.ev))*o
# 383[1]:cur(pi2)*I
# 384[1]:pi2*pair(o,o)
# 385[1]:o*I
# 386:ev*pair(cur(pi2.pair(pi1,pi2)),o)
# 387:pi2.pair(pi1,pi2)*pair(I,o)
# 388[1]:pair(pi1,pi2)*pair(I,o)
# 389[1]:pi1*pair(I,o)
# 390[1]:I*I
# 391[1]:pi2*pair(I,o)
# 392[1]:o*I
# 393:pi2*pair(I,o)
# 394:o*I
# 395:I*pair(s.o.!,o)
# pair(s.o.!,o)
#     : 1 -> prod(nat,nat)
# cpl>

test01.cpl

# > chcp 65001
# > cpl -i test01.cpl

# 終対象
right object 1 with ! is
end object;

# 積
right object prod(A, B) with pair is
  pi1: prod -> A
  pi2: prod -> B
end object;

# 冪
right object exp(A, B) with cur is
  ev: prod(exp, A) -> B
end object;

# 自然数
left object nat with pr is
  o: 1   -> nat
  s: nat -> nat
end object;


# デクリメント
let pred = pi2.pr(pair(o, o), pair(s.pi1, pi1));

# 加算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);

# 加算4（add4の中に直接書く以外に、x,yに値を渡す方法はない?!）
let add4(x, y) = pr(y, s).x;
# 乗算
let mul(x, y)  = pr(o, pr(y, s)).x;
#     いや、xは外から渡せる
# cpl> simp mul(pi1, s.s.s.o).pair(s.s.o, 1)
# s.s.s.s.s.s.o


# ----- result -----
# Active code page: 65001
# 
# E:\me\CPL>cpl -i test01.cpl
# Categorical Programming Language (Haskell version)
# version 0.1.0
# 
# Type help for help
# 
# > right object 1 with ! is
# > end object
# right object 1 is defined
# > right object prod(A, B) with pair is
# >       pi1: prod -> A
# >       pi2: prod -> B
# > end object
# right object prod(+,+) is defined
# > right object exp(A, B) with cur is
# >       ev: prod(exp, A) -> B
# > end object
# right object exp(-,+) is defined
# > left object nat with pr is
# >       o: 1   -> nat
# >       s: nat -> nat
# > end object
# left object nat is defined
# > let pred = pi2.pr(pair(o, o), pair(s.pi1, pi1))
# pred = pi2.pr(pair(o,o),pair(s.pi1,pi1))
#     : nat -> nat
# > let add1 = ev.prod(pr(cur(pi2), cur(s.ev)),     nat)
# add1 = ev.prod(pr(cur(pi2),cur(s.ev)),nat)
#     : prod(nat,nat) -> nat
# > let add2 = ev.prod(pr(cur(pi2), exp(s, I)),     I)
# add2 = ev.prod(pr(cur(pi2),exp(s,I)),I)
#     : prod(nat,nat) -> nat
# > let add3 = ev.pair(pr(cur(pi2), cur(s.ev)).pi1, pi2)
# add3 = ev.pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)
#     : prod(nat,nat) -> nat
# cpl> set trace on
# cpl> simp pred.s.s.o
# 0:pred.s.s.o*I
#     1[1]:s.s.o*I
#     2[2]:s.o*I
#     3[3]:o*I
#     4[2]:s*o
#     5[1]:s*s.o
# 6:pred*s.s.o
# ★7:pi2.pr(pair(o,o),pair(s.pi1,pi1))*s.s.o            ← Z.pr(X, Y)*s.s.o
#                     8[1]:  pr(pair(o,o),pair(s.pi1,pi1))*s.s.o
#     9[1]:  pair(s.pi1,pi1).pr(pair(o,o),pair(s.pi1,pi1))*s.o    ← sを一つ消して、頭にprの第二引数を付ける
#                     10[2]: pr(pair(o,o),pair(s.pi1,pi1))*s.o
#     11[2]: pair(s.pi1,pi1).pr(pair(o,o),pair(s.pi1,pi1))*o      ← sを一つ消して、頭にprの第二引数を付ける
#                     12[3]: pr(pair(o,o),pair(s.pi1,pi1))*o
#                       13[3]:  pair(o,o)*I                       ← oの時は、prの第一引数に置き換える
#     14[2]:pair(s.pi1,pi1)*pair(o,o)
#     15[1]:pair(s.pi1,pi1)*pair(s.pi1,pi1).pair(o,o)
# ★16:pi2*pair(s.pi1,pi1).pair(s.pi1,pi1).pair(o,o)     ← Z.Y.Y.X
# 17:pi1*pair(s.pi1,pi1).pair(o,o)
# 18:s.pi1*pair(o,o)
#     19[1]:pi1*pair(o,o)
#     20[1]:o*I
# 21:s*o
# 22:I*s.o
# s.o
#     : 1 -> nat
# cpl> exit
# 
# E:\me\CPL>