「二つの後者を持つ自然数」で遊んでみた話

どうもAaronです。
今回の記事ではれんくす(twitter:@Lenqth)さんにかなり多くの協力をいただいています。この場を借りてお礼申し上げます。
ということで（どういうことで？）早速今回も遊んでいきましょう！
今回は少し前に話題になったQiitaの記事(https://qiita.com/yumura_s/items/e06b5cf7b80c9c5effe3)で導入された「二つの後者を持つ自然数」で遊んでみたいと思います。

１．「二つの後者を持つ自然数」は実数（連続体）なのか？

これは少なくとも濃度の観点から言えば、はっきりNoという事ができます。
これを見るために以下のような変換を考えてみましょう。（以下今回の記事で「二つの後者を持つ自然数」の型をDualPeanoあるいは縮めてDPと呼びます。）

data DualPeano = Zero|LeftSucc DualPeano|RightSucc DualPeano

Listize::DualPeano->[Boolean]
Listize Zero=[]
Listize(LeftSucc x)=False::(Listize x)
Listize(RightSucc x)=True::(Listize x)

なお、これを書いてるAaron先生はHaskellを書いたことがなく、適当に見様見真似で書いてる上に動作チェックもしてないので、これをコピペしても動く保証はない…というより動かないと思います。
（ちゃんとHaskellが書けるれんくすさんに書いていただいた参考コードのリンクは最後に貼っておきます。）
このコードは、意味さえ分かっていただければ僕の目的は遂げられるのでHaskell類似の疑似コードぐらいに思って読んでもらったほうがいいかと思います。

要するにこの型は自然な形でBool値のリスト型に1対1変換することができる、という事が大事なのです。
ここでBool値のリスト型が実はωで順序付け可能なことを見ましょう。
まじめに数式で写像を構成してもよいのですが、そうするまでもないので直観に訴えかける方法でやります。

[]<[False]<[True]<[False, False]<[False, True]<[True, False]<[True, True]<[False, False, False]<...

という順序、すなわち

  1. 二つのリストの長さが異なったならば長いほうが大きい。
  2. 二つのリストの長さが同じならば、(False<Trueとして)辞書式順序で比較する。

という順序はω型の順序です。2ステップに分かれていることが重要で所謂「任意長さ辞書式順序」は整列順序ですらないことに注意してください。
これによって「二つの後者を持つ自然数」は濃度の意味では可算程度の表現能力をだけ持つことがわかります。
ただしこれは、有限の長さのterm、あるいは同じことですが正格評価できるようなtermの場合にのみ妥当する説明です。
Haskellには所謂Lazy termがあるため、実際には「無限に長い」termのことも考えるともう少し気を使わなくてはなりません。(が、その場合でも結局は可算に過ぎないことは証明できます。アイデアだけを述べれば無限に長いLazy termを作るにはtermの形を記述するプログラムが必要ですが、そのプログラム自身が有限の長さの文字列なので今と同じような仕組みで可算にされてしまうのです。)

2.型レベル固定小数点数としてのDualPeano

さて前章で述べた通り、DualPeanoの全体は可算なのですが、一方でこれが「実数に似ている」という直感はある意味では正しくて、これは自然な形で[0,1)の固定小数点数だとみなすことができます。
このための方法論は簡単で、さきほど作ったBool値リストをFalse->0,True->1と対応させ、最初に「0.」があると思って2進小数として読めばよいのです。
「2進分数全体の集合」は単位区間上稠密なので、その意味で「この型を『連続体を表現する』のに使うことができる」という主張は真たりえます。
これで数値計算を行ってみるのが、今回のメインになります。

3.精度と区間意味論

この章は数値計算に多少の知識がある方なら読み飛ばして大丈夫だと思います。

さて、固定小数点数での数値計算においては小数点以下の桁数がそのまま保証精度になるので、有効数字とか精度とかの意味論は、浮動小数点数よりはるかに簡単に済みます。
しかしここで最も基本的なところで「精度」とはどのようなものでしょうか。
ここでは僕が勝手に「区間意味論」と呼んでいる手法によって「精度」を説明いたします。

まず精度0とは、(今の場合)[0,1)区間上、真の値がどこにあるのか前半分なのか後ろ半分なのかすら見当がつかない状態です。
精度1の数は0.0と0.1の二つがあります。
これは直感的には「小数第一位まではわかる」という状況ですが、実はこう言いかえることもできます。

「真の値が[0,1)開区間上前半分にあるか、後ろ半分にあるかはわかる！」

つまりこの意味論では数は単なる値ではなく、真の値が存在する可能性がある区間を意味するのです。
むろん以降は精度、即ち小数点以下の桁数が増えるごとに「真の値がその前か後ろの半分のうち、さらにその前半分にあるか後ろ半分にあるかはわかる」、「さらにさらにその前半分にあるか後ろ半分にあるか…」と続いていきます。
なぜこれを説明したかというと僕自身が自分の与えたDualPeanoと固定小数点数の対応においてZeroがどういう意味を持つかきちんと説明できなかったからです。これに意味をつけてくれたのがやはりれんくすさんで、先ほど言ったように「単位区間の前半分にあるか後ろ半分にあるかという情報すらない」という状況を割り当てることによって非常に整合的に扱えることを発見していただきました。

4.精度と普通の自然数の関係

この章は末尾にのせてあるリンクのサンプルコードをみながら読んでもらうとよいと思います。

さきほどお話ししたように、固定小数点数の精度とは「長さ」そのものですから、上で述べた(Bool値リストを経由した対応を通して)DualPeanoにとっては「Zeroにいくつコンストラクターがついてるか数え上げる関数」です。
サンプルコードのacc(すなわちaccuracy)はまさにそのように実装しています。

ところで突然ですがこのDualPeanoと普通の自然数ってどんな関係なのでしょう?
普通の自然数はZeroと唯一のSuccessorを持つ体系ですから、このDualPeanoのふたつのSuccの「区別をやめて」しまえば、自然数に「押しつぶす」ことができそうです。
すなわちこうです。

data NormalPeano = Zero |Succ NormalPeano

simplify::DualPeano->NormalPeano
simplify Zero=Zero
simplify (LeftSucc x) =　Succ (Simplify x)
simplify (RightSucc x) =Succ (Simplify x)

例によってコードは適当です。

要するに
「SuccがLeftとRightに「分裂」していることがDualPeanoの複雑さの源ですから、それを1個にすれば普通の自然数に戻るというのも当然の話です。」
というのがsimplifyの意図です。
さて、ここでaccとsimplifyを見比べてみてください。
値域が、型レベル自然数とHaskellに最初から用意されているIntegerで異なるという違いこそあれ同じ形をしているではありませんか！

つまり

(この解釈の元で)「二つのSucc」がincrementしていたのは「固定小数点数としての精度」だった！

のです！

これによって我々はDualPeanoがどんな意味で「実数っぽい」のかを知ることができましたし、それが普通の自然数のSuccとどう対応しているのか知ることができたわけです。


サンプルコードはこのあと型レベル固定小数点数としての意味論をより明確にするために加算器を実装しましたが、加算器については僕も付け焼刃の知識しかないので説明できません…すいません。

読者の方々、ここまで読んでいただきありがとうございました。
そしてご協力いただいたれんくす君には重ねてお礼を申し上げます。
記事の誤り、また添付のサンプルコードも簡単な動作チェックしかしていないためバグなどありましたらAaron(twitter:@sanjutsu_yu)までおしらせください。

サンプルコード(byれんくすさん):
Ideone.com - ie13ir - Online Haskell Compiler & Debugging Tool

reference:
https://qiita.com/yumura_s/items/e06b5cf7b80c9c5effe3