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

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

<証明No.8>コラッツ予想に非自明ループが無い事の証明

コラッツ予想

排中律：負に未知のループは無い ∨ 負に未知のループは有る
負に未知のループは無い ⇒
　負のビットパターンは、正の下位ビットパターンと一致する。
　負で(下位)ビットパターンがループしてない時点で、正のループは無い
負に未知のループは有る ⇒
　このループを正に写そうとしても、
　結局、二進数で上位に「1」を無限に積まないといけない※
⇒ 分岐論法により証明できた □
※上位から供給を受ける必要があるので、
ループするビットから上位何ビットかは1にする必要がある。
それもループするビットに含まれるので、
さらに上位何ビットかは1にする必要がある。
この手続きは連鎖するので、
結局、ループするビットから上位は無限に1で埋める必要がある。


◆ -5 のループ(2の補数使用) ...は無限に1が続く
...1011 -5
...1001 -7
..1011 -5


CPL で Stateモナド

CPL

CPL で Stateモナド を作ってみた。ちゃんと出来てるかどうかは分からない。

参考記事

圏論プログラミング言語CPL入門 - うさぎ小屋

コード

# State Monad
# newtype State s a = State { runState :: s -> (s, a) }
right object State(S, A) with state is
  runState: State -> Exp(S, Prod(A, S))
end object;

let run(x) = ev.pair(runState.state(cur(x)), s.o);

ev.pairの第二引数1(s.o)が初期状態だ。

実行結果

> let run(x) = ev.pair(runState.state(cur(x)), s.o)
x: Prod(1,nat) -> Prod(*a,nat)
------------------------------
run(x): 1 -> Prod(*a,nat)
cpl> simp full run(Prod(true, s))
pair(true,s.s.o)
    : 1 -> Prod(bool,nat)
cpl> simp full run(Prod(true.!, s).Prod(true, s))
pair(true.!,s.s.s.o)
    : 1 -> Prod(bool,nat)
cpl>

Stateモナド の実体としては、カリーcurをかぶせたProdを置く。
第一引数には返したい結果、第二引数には状態を更新する関数(ここではnat->nat)を置く。
連鎖させることもできる※1。Prod(true.!, s).Prod(true, s)のように。(!は後方の合成射を全て消すものです)
(※1 bind じゃないよな？)

で、bind(>>=)は？

分からない......