CPLの練習（pred）

圏論プログラミング言語CPLをやってみようと思う。
言語の説明は参考記事にまかせます。
まあ、Esotericな言語です。

参考記事

インストールだけど、
GitHubからクローンして、stack run cplが良いと思う。
（2回目からはexeを直接叩く）
cabalコマンドは使わない方が良いと思う。

今回のプログラムは、
終対象、積、冪、自然数を定義したのち、
関数predを定義する。
predは自然数を-1する関数で、pred 0は0のままだ。

で、predの定義がこちら。

let pred = pi2.pr(pair(o, o), pair(s.pi1, pi1));

さっぱり分かりませんね！
なので動きを追ってみましょう。
> set trace onで簡約の様子が見られるようになります。

......

自然数の仲介射prの動きがキモなのですが、
要は以下のように、sを第二引数に、oを第一引数に、置換するのです。

pr(X, Y).s.s.o => Y.Y.X
pi2.pr( pair(o, o), pair(s.pi1, pi1) ).s.s.o
  => pi2.pair(s.pi1, pi1).pair(s.pi1, pi1).pair(o, o) ...(ｲ)

pi1はpair(,)の第一要素を取り、pi2はpair(,)の第二要素を取ります。

(ｲ)において、s.pi1は元の自然数と同数あるのですが、
いちばん頭がpi2なので、sを一つ取らないのですね。
よってpredの動きが実現されるのです。

全然実用的じゃなーい！
パズルとしては面白いかも。