2019-09-08

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

どうも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]<...

という順序、すなわち

二つのリストの長さが異なったならば長いほうが大きい。
二つのリストの長さが同じならば、(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

2019-05-26

基礎概念実装ゲームの薦め

どうもAaronです。
今回は何かの証明とかではなく自分が創始した数学ゲーム、「基礎概念実装ゲーム」の布教です。

基礎概念実装ゲームは「普段数学やプログラムであまりにも当たり前に使っている概念や操作」を「より簡単な概念や操作」から作ってみよう、という試みです。
基礎概念実装ゲームの簡単な例が

Aaron先生からの挑戦状

1.自然数の四則演算を後者関数(successor,SUC)と条件分岐と再帰を利用して定義せよ。
2.関数を第一級オブジェクトであるとして、実閉体を記述できる型を自然数型及び論理値型のみから実装せよ。
3.集合型をLispで実装し、所属関係と初歩的な集合演算を定義せよ。
— Aaron@基礎概念実装ゲーム初代師範 (@takum97) 2019年5月19日

にあります。
この他にも直積、スタック、キュー（待ち行列）など基礎概念は多くあります。

当面の問題は僕が不定期に出題する予定です。
回答はハッシュタグ #Aaronよその挑戦受けて立つで募集します。
皆さんも問題を思い付いたらハッシュタグ #基礎概念実装ゲームで投稿してください。
指定がない限り仕様とアルゴリズムが明らかであれば、フローチャートや疑似コードでも回答と認めますので、必ずしも何らかのプログラム言語で計算機上に実装する必要はありません。
また現在僕の知識の関係上Lisp系以外のソースコードを提出された場合、採点が困難です。メジャーなプログラム言語の知識に詳しい採点者が欲しいです（切実）。
というかとりあえず初代師範になってみましたが、正直このゲームもっと強い人が絶対居るのでさっさと師範譲りたいです。

一応まだ草案ながら基礎概念実装ゲームの詳細なルールはこうなっています。

0.「基礎概念実装ゲーム」は「多くのプログラム言語でサポートされているデータ型や関数、あるいは数学的によく使われる概念や操作を、指定された『より基礎的な』操作、関数、データ型等を用いて実装する」クイズである。
1. #基礎概念実装ゲームのハッシュタグで誰でも問題を投稿できる。問題投稿者は基本的に採点の義務を負わない。
2.「師範」はある程度の間隔で問題を投稿すること、その問題について希望者先着3名の採点・添削を行うこと、その問題の回答解説を発表すること、の努力義務が発生する(あくまで努力義務です。今の僕がそうであるようにリアルの時間やプログラム言語の知識は師範まで「昇進」するのとはそれほど関係ありませんが、この職務にはそれらがある程度必要だからです)。これがあまりに満たせない場合は出来るだけ早く他の方に「師範」を譲ってください。場合によっては会長として僕が譲位をお願いすることがあるかもしれませんがあまりしたくありません。
3.「師範」は原則3人体制をとり、「師範」の座を退きたい人は、自分、及び自分以外の師範一人以上が同意する実力者に、本人の同意のもとで「師範」の地位を譲位することとします。また「師範」を譲位された場合、新たに「師範」になっ「た人は「師範」になったことを宣言すると共に就任記念問題を出題することとします。記念問題の出題及び、2と同条件の採点、回答発表は必ず行ってください。必要があれば他の師範は協力をお願いします。

こんな感じです。現在初代師範を二人募集してます。

2019-05-04

可算非有界稠密全順序構造の一意性の別証明

どうもAaronです。

今日は普段やっている(というか体調不良と新生活の忙しさという口実で三日坊主中の)「算術の夢の楽園」ではなく単発です。

表題にもある通り非有界稠密全順序構造には $\aleph_0$ -categorical、即ち任意の可算モデルが(同型(当然だがここでは順序同型)を同じと見なす意味で)一意だという性質があり(これはモデル理論的にはそれなりに珍しい性質で、例えば通常「自然数の理論」といわれるPeanoの公理には、通常の自然数(標準自然数)のほかにも「超準自然数」と呼ばれるモデルがたくさんあることが知られており、実は可算モデルに限定してすら「自身が矛盾している」と主張しているかのように読めたり、ある意味で $\infty$ のように振舞ったりする奇妙な元を持った、性質の異なるモデルがあるのです)、このこと自体は古くから知られている(集合論の始まりであるCantorがもう示しているようです。この辺は単にある人とのpersonal communicationで聞いただけなので歴史的経緯について語る気はないですし、間違っててもご容赦を)のですが、通常の教科書に載っている(らしい)証明とは少し違うアプローチの別証明を思いついたので、モデル理論ができる方に査読をしてもらいたい(まあ恐らくどこかしらで既出だとは思いますが)事に加え、自分の備忘録もかねてここに書いておきます(Twitterでも同内容を書きましたが、はてブロのほうがある程度データの保管として信頼できるのと、結構訂正があってグダグダだったので清書を兼ねて)。

0.ちょっとだけ予備知識

別にモデル理論も順序集合論も(というか任意の数学の分野)詳しくないので説明できるような予備知識もないのですが、一応今回示したいことと背景だけ説明しときます。

今回示したいことは以下の(全て同値な)主張です。

ほとんど言葉遊びレベルでいろいろ言いかえてありますのでモデル理論の言葉が苦手な方は好きなステートメントで理解してください。

非有界稠密全順序構造は $\aleph_0$ -categoricalである。
可算非有界稠密全順序構造は同型を除いて一意である。
可算全順序集合の圏のうち、非有界で稠密な順序を持つ対象の為す部分圏は本質的に一点圏である。
任意の非有界稠密全順序構造の可算モデルは(通常の順序を備えた)有理数と順序同型を持つ。
任意の非有界稠密全順序構造の可算モデルは(有理数からの相対順序を備えた)2進分数と順序同型を持つ。

ちなみに今回僕が与える別証明では一番最後のステートメントを証明し、系として他の表現が従う形をとります。

さて先ほどから別証明といっているからには「普通こうやる」という証明があるわけですが、それは「往復論法」と呼ばれるものです。

Bernsteinの定理の証明を知っている人には、アレを順序の埋め込み写像に関して類似物を作ったような証明だと思ってもらえばいいかと思います。(因みに恥ずかしながら僕はこの証明一読したことがなく、「大体こんな感じ」というのだけ知らないのです。)。

この方法の利点は「任意にとってきた構造2つの間に直接同型が作れること」を示していることです。

反対に若干劣るのは2つの構造の間に作った同型が必ずしも具体的とは言えないところです。

そこで今回用いる方法は任意の可算構造から2進分数に順序同型を作る方法を具体的に与えるものなのです。

1.証明の仮定

今回の証明では1か所だけ、とあるトリックを用いています。

というのも可算非有界稠密全順序構造 $\rm (A,\preceq )$ の台集合 $\rm A$ は可算集合である限り、どのような集合でもよいので、具体的に与えるといっても中身のわからない集合に関する定義を書き下すのは困難だからです。

そこで台集合を自然数でエンコードします。これは可算性の定義からいつでも可能です。

少し気を使って書けば台集合 $\rm A$ に対して自然数全体の集合 $\omega$ から $\rm A$ への全単射 $\alpha$ (可算性とはまさにこのような $\alpha$ が存在することでした。)を一つ固定して、これによってあたかも自然数から他の集合 $\rm B$ への関数 $\rm f$ を、 $\rm A$ から $\rm B$ への写像であるかのように扱います。

本当ならば $\rm f(\alpha^{-1}(n))$ と書くべきところを、(ある種の記号の濫用により) $\rm f(n)$ と書いて済ませてしまったり、定義をするときでさえ $\rm f\circ\alpha^{-1}$ をなにか文字で措けば済むところを横着して $\rm f$ をして $\rm f:A \to B$ かと言い張るわけです。

計算論や算術に慣れている人にとっては台集合を $\omega$ に固定して、順序構造を2変数Bool値関数としてエンコードする、いつもやってるトリックだと思ってもらっても当然同じです。

但しこれには問題があり、議論の途中で $\rm A$ の順序ではなく通常の自然数の順序を使うところが多くあり(それだけでも十二分に紛らわしいのに、更には同型を飛ばす先である2進分数の空間の順序も使うのですから)、非常に分かりにくなることがあります。

そこで自然数の通常の順序には記号 $\leq$ を、 $\rm A$ の順序には $\preceq$ を、2進分数空間の順序には $\ll$ を使います。最大・最小などの記号も $\rm max_\leq,min_\leq,max_\preceq,min_\preceq,max_\ll,min_\ll$ のように書きます。

さて前置きが長くなりすぎました(もう2000字をはるかに越えている)。

次章で証明に入ります。

2.可算非有界稠密全順序構造 $\rm (A,\preceq)$ から2進整数の空間 $({\mathbb Z}/2^{\mathbb N},\ll)$ への関数 $\rm f$

この章では、ある固定された可算非有界稠密全順序構造 $\rm (A,\preceq)$ から2進整数の空間 $({\mathbb Z}/2^{\mathbb N},\ll)$ へある関数 $\rm f$ を定義します。

先に言ってしまえばこれが順序同型になっているのですが、それは次章以降で示すとしてその定義だけ先にやってしまうわけです。

その定義は再帰的に以下のようになります。

$Basis.\rm f(0)=0.\\\ \\ {\it Inductive\ Steps.} \\Let \\L_n^x:=\{f(m)|(m\leq n)\land (m\preceq x)\}\\G_n^x:=\{f(m)|(m\leq n)\land (x\preceq m)\}.\\\ \\f(n+1)=min_\ll(G_n^{n+1})-1\ (if\ L_n^{n+1}=\emptyset)\\f(n+1)=max_\ll(L_n^{n+1})+1\ (if\ G_n^{n+1}=\emptyset)\\f(n+1)=\frac{max_\ll(L_n^{n+1})+min_\ll(G_n^{n+1})}{2}\ (if\ G_n^{n+1},L_n^{n+1}\neq\emptyset)$

ここで $\rm \{m|m\leq n\}$ は有限集合だから、定義中の $\rm L_n^x,G_n^x$ もいつでも必ず有限集合で、よってその( $\ll$ に関する)最大値、最小値は必ず存在しますし、総当たり法で計算することも可能なことに注意してください。

またこれが関数を定めることは、(帰納法や帰納的定義の正当性を前提すれば)エンコーディング $\alpha$ が全単射であったことから従います。

これらにより $\rm f$ が確かに関数を定めうことが分かったのですが、次章にてこれが実は順序を保つこと、そして全単射であること即ち順序同型であることを示します。

3. $\rm f$ が広義順序を保つこと

この章では $\rm f$ が狭義順序を保つこと、論理式で書けば

$\rm\forall n\forall m.n\prec m\to f(n)\ll_s f(m)$

であることを示します。

ここで $\rm \prec,\ll_s$ は

$\rm n\prec m:\Leftrightarrow n\preceq m\land n\neq m\\n\ll_s m:\Leftrightarrow n\ll m\land n\neq m$

で定義される狭義順序と呼ばれるものです(狭義順序を使う場合、 $\preceq,\prec$ の様に元の順序(広義順序)を「狭義順序の記号と等号、もしくはそれを略した一本線を縦に重ねた記号」で表すのが普通なのですが、僕がTeXで出せる記号に限りがあったため $\ll$ の方はその流儀に従えず、小文字のs(狭義順序の英語strict orderの頭文字)を添えて表しました。分かりにくくて申し訳ないです。)。

写像が狭義順序を保つことは広義順序を保ちかつ単射(つまり順序埋め込み)であることと同値です。

さてそれでは証明に入ります。自然数の通常の順序に関する、通常の数学的帰納法により

「任意の自然数 $\rm n$ について $\rm m,l\lt n$ に対しては $\rm f$ は狭義順序を保つ。」

を示します(蛇足ながら $\lt$ は通常の自然数に関する狭義順序であることを付け加えておきます)。

Basis case、即ち $\rm n=0$ のとき、命題は自明です。

Inductive Stepsは3つの場合に分かれます。

(i) $\rm L_n^{n+1}=\emptyset$ のとき

$\rm L_n^x$ の定義から $\rm n+1$ は $\rm m\leq n$ のいずれよりも $\preceq$ の意味で小さく、また $\rm f(n+1)$ と $\rm G_n^{n+1}$ の定義から

$\rm f(n+1) \\=min_\ll(G_n^{n+1})-1\\\ll_s min_\ll(G_n^{n+1})\\\ll f(m)(\forall m\leq n)$

なので条件を満たします。

帰納法の仮定から $\rm l,m\lt n+1$ であるような $\rm l,m$ について条件が満たされることはわかっていますから、これによって命題が示されました。

(ii) $\rm G_n^{n+1}=\emptyset$ のとき

(i)と大小を逆にしただけで全く同様にして示されます。

(iii) $\rm L_n^{n+1},G_n^{n+1}\neq\emptyset$ のとき

帰納法の仮定と $\rm L_n^{n+1},G_n^{n+1}$ の定義、そして $\ll$ の推移性から

$\rm max_\ll(L_n^{n+1})\ll_s min_\ll(G_n^{n+1})$

となります。

ここで比較が狭義順序であることに注意してください。

というのも、帰納法の仮定から順序を保つことより

$\rm max_\ll(L_n^{n+1})=f(max_\preceq\{m|(m\leq n)\land(m\preceq n+1)\})\\min_\ll(G_n^{n+1})=f(min_\preceq\{m|(m\leq n)\land(n+1\preceq m)\})$

となり、しかも $\rm f$ の $m\leq n$ への制限は単射ですから、仮に等号が成り立つとすると

$\rm min_\preceq\{m|(m\leq n)\land(n+1\preceq m)\}=max_\preceq\{m|(m\leq n)\land(m\preceq n+1)\}$

となるよりなく、これは明らかに矛盾を生じるからです。

従って

$\rm (n\geq \forall m\prec n+1)\\\ \ \ \ \ f(m)\\\ll max_\ll(L_n^{n+1})\\\ll_s\frac{max_\ll(L_n^{n+1})+min_\ll(G_n^{n+1})}{2}\\\ll_s max_\ll(L_n^{n+1})\\\ll f(m)\\(n+1\prec \forall m\leq n)$

が得られます。

(i)の時同様、帰納法の仮定から $\rm l,m\lt n+1$ であるような $\rm l,m$ について条件が満たされることはわかっていますから、これによって命題が示されました。

以上より数学的帰納法によって

「任意の自然数 $\rm n$ について $\rm\forall m,l\lt n$ に対しては $\rm f$ は狭義順序を保つ。」

が示されました。

実は本当に示したいことは「 $\rm f$ が狭義順序を保つこと」だったわけですが、これは $\rm n$ が任意であったことから簡単に同値です。つまり我々は目標を達成したことになります。

さて、これで $\rm f$ が狭義順序を保つ写像であること、すなわち順序を保つ単射であること、即ち順序の埋め込みであることがわかりました。

ここでほんの少しだけ補足をしますと、順序集合の埋め込みは集合論的に単射であればそれで大丈夫で、引き戻した時の挙動を心配する必要はありません。

これは今の例では $\rm a\ll b$ に対して $\rm f^{-1}(a),f^{-1}(b)$ はそれぞれ存在すれば一意ですが、ここで両方の存在を仮定したうえで $\rm \lnot(f^{-1}(a)\preceq f^{-1}(b))$ とすると明らかに矛盾であることからわかります。

こうしてみると、わざわざ書くほどのことでもないのですが、位相空間の様に稀に集合論的に単射でも埋め込みとは言えない構造の例が存在するので、一応念押ししたまでのことです。

さて話を戻すと $\rm f$ は埋め込みだったのですから、あとは全射であることを言えば同型であることがわかります。

次章ではそれを証明します。

3. $\rm f$ の全射性

さて $\rm f$ の全射性を示したいのですが、ここでは少しトリッキーな帰納法を用います。

それは「2進分数の分母の指数に関する帰納法」です。

すなわち

(i)任意の整数に対して $\rm f$ に沿った引き戻しが存在すること。

を言い

(ii)分母が高々 $\rm 2^n$ であるような2進分数について、すべて $\rm f$ に沿った引き戻しが存在するなら分母の指数が $\rm 2^{n+1}$ であるような2進分数すべてについても引き戻しが存在すること

を言うわけです。

まず(i)を見ましょう。

定義から $\rm A$ には通常の順序と両立する $\prec$ に関する無限上昇列および無限下降列が存在します。

もしもないとしたら、ある $\rm n$ より $\prec$ の意味で大きいor小さい元が有限個しかないことになり明らかに矛盾だからです。

このことと自然数の整礎性により、固定された $\rm n$ に対して

$\rm min_\leq\{m|n\prec m\},min_\leq\{m|m\prec n\}$

は常にvalidですから2つの再帰的定義

$\rm A(0)=0\\A(m+1)=min_\leq\{x|A(m)\prec x\}\\\ \\B(0)=0\\B(m+1)=min_\leq\{x|x \prec B(m)\}$

もvalidです。

実はこの $\rm A(n),B(n)$ はそれぞれ正整数、負整数についての $\rm f$ に沿った引き戻しになっています。すなわち $\rm f(n)$ が整数ならば $\rm A(f(n))=n,B(-f(n))=n$ となります。

これを見るためにもう一度 $\rm f$ の再帰的定義を検証します。

まず

$\rm F(n):=max_\ll\{f(m)|m\leq n\}$

を考えます。

$\rm F(n)$ の値が変わるのは $\rm n$ が $\rm f$ の再帰的定義のinductive stepの(i)の条件を満たしたときかつそのときのみであり、1度この条件を満たすたびに $\rm F(n)$ の値は1だけ増えますから $\rm m$ 回目にこの条件を満たしたときの $\rm F(n)$ の値は $\rm m$ です。