(2020-07-17) lambda 3 の解析

ユーザーブログ:Merliborn/［sikigamig］Lambda-zip を解析する。

型付け

型を利用してラムダ式の停止性を検証する。これはプログラムが正しく実装できているのであればプログラムの停止性へと直接的に繋がる。ここでは System F で解釈を行う。一番目に元々の式を書き、二番目に型についての情報を加えた式を書き、三番目に型を書く。

自然数を表現する項は \( \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \) という型を持っているものとする。これは Böhm–Berarducci encoding と呼ばれる物である（リンク１、リンク２、リンク３）。なお、細かいことだが \( \forall A \ldotp A \rightarrow ( A \rightarrow A ) \rightarrow A \) の方が data Nat = Z | S Nat というような定義と順序が同じになって好きである。

---

\begin{eqnarray*} \mathbf{B} & \equiv & \lambda x y z \ldotp x ( y z ) \\ \mathbf{B}' & \equiv & \Lambda A B C \ldotp \lambda x ^ { B \rightarrow C } y ^ { A \rightarrow B } z ^ A \ldotp x ( y z ) \\ & : & \forall A B C \ldotp ( B \rightarrow C ) \rightarrow ( A \rightarrow B ) \rightarrow A \rightarrow C \\ \end{eqnarray*}

関数の合成である。 Haskell では (.) 演算子に該当する。

---

\begin{eqnarray*} \mathtt{h} _ 0 & \equiv & \lambda m n \ldotp n m \\ { \mathtt{h} _ 0 }' & \equiv & \Lambda A B \ldotp \lambda m ^ A n ^ { A \rightarrow B } \ldotp n m \\ & : & \forall A B \ldotp A \rightarrow ( A \rightarrow B ) \rightarrow B \\ \end{eqnarray*}

自然な型付けを行うと、関数の適用となる。 Haskell では (&) 演算子に該当する。しかし、エンコードされた自然数を引数に取る時は、この型付けではダメである。

\begin{eqnarray*} { \mathtt{h} _ 0 }' & \equiv & \lambda m ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } n ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } \ldotp \Lambda A \ldotp n ( A \rightarrow A ) ( m A ) \\ & : & ( \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A ) \rightarrow ( \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A ) \rightarrow \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \\ \end{eqnarray*}

このように型付けすると、二つの自然数を取り一つの自然数を返す関数となる。これは累乗を表す関数となる。

---

次は \( \mathrm{H} _ 3 \) を型付けしたいところだが、これは複雑すぎるため後回しにしておく。これは内側の型と外側の型から攻めていきたい。なので \( \lambda _ 3 \) の型を考える。

\begin{eqnarray*} \lambda _ 0 & \equiv & \Lambda _ 3 \underline{\mathtt{3}} \underline{\mathtt{3}} \\ { \lambda _ 0 }' & \equiv & { \Lambda _ 3 }' { \underline{\mathtt{3}} }' { \underline{\mathtt{3}} }' \\ & : & \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \\ \end{eqnarray*}

これの型は当然自然数となる。というより、そうならなかったら巨大数ではない。

---

次は \( \underline{\mathtt{3}} \) の型付けを行う。

\begin{eqnarray*} \underline{\mathtt{3}} & \equiv & \lambda f x \ldotp f ( f ( f x ) ) \\ { \underline{\mathtt{3}} }' & \equiv & \Lambda A \ldotp \lambda f ^ { A \rightarrow A } x ^ A \ldotp f ( f ( f x ) ) \\ & : & \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \\ \end{eqnarray*}

これも名前と値から考えて自然数である。

---

上記の二つの式の型から \( \Lambda _ 3 \) の型を計算することが可能になる。

\begin{eqnarray*} \Lambda _ 3 & \equiv & \lambda m n \ldotp n \mathrm{H} _ 3 \mathtt{h} _ 0 m m \\ { \Lambda _ 3 }' & \equiv & \textrm{???} \\ & : & ( \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A ) \rightarrow ( \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A ) \rightarrow \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \\ \end{eqnarray*}

ここでようやく全体像が見えてくる。つまり、 \( \mathtt{h} _ 0 \) 、すなわち冪乗を何らかの形式で繰り返したものが \( \Lambda _ 3 \) であり、冪乗の繰り返しを行うのが \( \mathrm{H} _ 3 \) だと予想される。

\[ \lambda m ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } n ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } \ldotp [ n \mathrm{H} _ 3 \mathtt{h} _ 0 m m ] : \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \]

ここで \( [ \_ ] \) はまだ型付けがされていない式を表す穴である。ここでは自然数であるべき箇所が示されている。

\[ \lambda m ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } n ^ { \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A } \ldotp \Lambda A \ldotp [ n \mathrm{H} _ 3 \mathtt{h} _ 0 m m ] : ( A \rightarrow A ) \rightarrow A \rightarrow A \]

\( A \) を外側に括りだしてみる。この先の推論が上手く行かないため、これは失敗である。

\[ \lambda m ^ \mathbb{N} n ^ \mathbb{N} \ldotp [ n \mathrm{H} _ 3 \mathtt{h} _ 0 m m ] : \mathbb{N} \]

\( \mathbb{N} \equiv \forall A \ldotp ( A \rightarrow A ) \rightarrow A \rightarrow A \) を導入する。

\[ \lambda m ^ \mathbb{N} n ^ \mathbb{N} \ldotp n ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) { \mathrm{H} _ 3 }' { \mathtt{h} _ 0 }' m m \]

\( n \) が何を繰り返すのか考えるとこうなる。まず、 \( { \mathtt{h} _ 0 }' m m : \mathbb{N} \), \( { \mathrm{H} _ 3 }' { \mathtt{h} _ 0 }' m m : \mathbb{N} \), \( { \mathrm{H} _ 3 }' ( { \mathrm{H} _ 3 }' { \mathtt{h} _ 0 }' ) m m : \mathbb{N} \), ... であることを押さえておく。すると、 \( \mathrm{H} _ 3 \) は自然数に関する二項演算子を受け取って自然数に関する二項演算子を返す関数となる。これは \( n \) で繰り返し可能な操作である。

\begin{eqnarray*} \Lambda _ 3 & \equiv & \lambda m n \ldotp n \mathrm{H} _ 3 \mathtt{h} _ 0 m m \\ { \Lambda _ 3 }' & \equiv & \lambda m ^ \mathbb{N} n ^ \mathbb{N} \ldotp n ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) { \mathrm{H} _ 3 }' { \mathtt{h} _ 0 }' m m \\ & : & \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \\ \end{eqnarray*}

最終的にこうなる。

---

この結果から \( { \mathrm{H} _ 3 }' : ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \) であると分かる。

\begin{eqnarray*} \mathrm{H} _ 3 & \equiv & \lambda H m n \ldotp H n n ( \lambda T L k \ldotp L k \mathtt{h} _ 0 k k T \mathbf{B} ) ( \lambda L k \ldotp k ( \lambda F x y \ldotp L y F x x ) ) \mathtt{h} _ 0 m m \\ { \mathrm{H} _ 3 }' & \equiv & \textrm{???} \\ & : & ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \\ \end{eqnarray*}

つまり、こうである。

\begin{eqnarray*} \mathrm{H} _ 3 & \equiv & \lambda H m n \ldotp H n n ( \lambda T L k \ldotp L k \mathtt{h} _ 0 k k T \mathbf{B} ) ( \lambda L k \ldotp k ( \lambda F x y \ldotp L y F x x ) ) \mathtt{h} _ 0 m m \\ { \mathrm{H} _ 3 }' & \equiv & \lambda H ^ { \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} } m ^ \mathbb{N} n ^ \mathbb{N} \ldotp \textrm{???} \\ & : & ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \\ \end{eqnarray*}

さらに、簡単に分かる範囲の式を埋めていく。

\begin{eqnarray*} \mathrm{H} _ 3 & \equiv & \lambda H m n \ldotp H n n ( \lambda T L k \ldotp L k \mathtt{h} _ 0 k k T \mathbf{B} ) ( \lambda L k \ldotp k ( \lambda F x y \ldotp L y F x x ) ) \mathtt{h} _ 0 m m \\ { \mathrm{H} _ 3 }' & \equiv & \lambda H ^ { \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} } m ^ \mathbb{N} n ^ \mathbb{N} \ldotp ( H n n \mathsf{T} ( [ \lambda T L k \ldotp L k \mathtt{h} _ 0 k k T \mathbf{B} ] : \mathsf{T} \rightarrow \mathsf{T} ) ( [ \lambda L k \ldotp k ( \lambda F x y \ldotp L y F x x ) ] : \mathsf{T} ) : \mathsf{T} ) { \mathtt{h} _ 0 }' m m \\ & : & ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \\ \end{eqnarray*}

さらに、未知の型 \( \mathsf{T} \) を使って埋めてやる。ここで、未知の型 \( \mathsf{T} \) は \( ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \) のことだと分かる。そのため、 \( \mathsf{T} \equiv ( \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} ) \rightarrow \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} \) とする。

\( [ \lambda T L k \ldotp L k \mathtt{h} _ 0 k k T \mathbf{B} ] : \mathsf{T} \rightarrow \mathsf{T} \) にフォーカスしよう。

\[ \lambda T ^ \mathsf{T} L ^ { \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N} } k ^ \mathbb{N} \ldotp [ L k \mathtt{h} _ 0 k k T \mathbf{B} ] : \mathbb{N} \rightarrow \mathbb{N} \]

このようになる。

関連項目

式神巨大数は、私が開催している巨大数の大会です。 2020 年に最初の式神巨大数が開催されました。その後、 2021 年の式神巨大数の開催に向けて、複数回の開催のための規則が追加され、また規則が全面的に整理されている途中です。

2020 年の歴史

ここでは、2020 年の式神巨大数のポータルから見れない歴史に限って書きたいと思います。

2020/04/17: Alwe さんがグーゴロジストの社交場（仮）という Discord のサーバーで「次の巨大数のコンテストはいつあるのか」という旨の投稿をしました。そこから巨大数のコンテストについて話しているうちに、 2020 年には東方巨大数が開かれないため巨大数のコンテストの空白期間が生まれることに気付きました。また、プログラミングを使った巨大数のコンテストは、今まで一度も日本語圏では開かれていないことに気付きました。この二つの空白に、巨大数のコンテストを開くチャンスがあるのではないかと思うようになりました。

2020/04/20: コンテストに式神巨大数という名前を付けました。詳しい命名の過程は覚えていないのですが、東方巨大数と幻想巨大数に命令の法則を合わせるのと、コンピュータという要素を入れるのを目指した結果として、式神巨大数となったのは覚えています。

2020/04/20: 規則の作成を開始し、素版を作り上げました。グーゴロシストの社交場（仮）で、ルールの素版を公開しました。

2020/04/20-21: 甘露東風さんと Nayuta Ito さんと Okkuu さんからグーゴロジストの社交場（仮）で質問があり、それらに返答しました。

2020/04/25: Twitter で式神巨大数を開催することを予告しました。

2020/04/29: 巨大数研究 Wiki のユーザーブログで式神巨大数を開催することを予告しました。ここで、 2020/05/08 からという具体的な日時を定めています。これをきっかけとして Alwe さんと JUNKUN さんが巨大数研究 Wiki にアカウントを作ったようです。

2020/04/30-2020/05/01: Okkuu さんと Nayuta Ito さんからグーゴロジストの社交場（仮）で質問があり、それらに返答しました。 Okkuu さんの「審査員は、どのくらい数学の能力を持っていれば大丈夫なのか」という質問に対して、私は「 \(n < 1 \) ならば \( n ! < n ^ n \) 」の証明が出来るのなら大丈夫なのではないかと返答しました。

2020/05/03: Okkuu さんがユーザーブログ:Okkuu/「 n ＞ 1 ならば n! ＜ n^n 」の証明を投稿すると共に審査員に応募しました。

2020/05/03: Nayuta Ito さんがユーザーブログ:Nayuta Ito/「 n ＞ 1 ならば n! ＜ n^n 」の証明を投稿すると共に審査員に応募しました。

2020/05/23: Antimony Star さんが「日本語が話せなくても式神巨大数に参加できるか」という旨の投稿を巨大数研究 Wiki でしました。

2020/05/24: Nayuta Ito さんが Antimony Star さんについて質問を行いました。 Nayuta Ito さんとグーゴロシストの社交場（仮）において協議した結果として、 Antitomy Star さんに「参加できる」という旨の返答をしました。

2020/07-2021/01: 審査の難航と私の精神状態の悪化が重なって審査期間の延長を繰り返していました。

2020/12/17: Okkuu さんから「そろそろ締めましょう」という旨の提言がありました。

2021/01/31: 2020 年の式神巨大数が終了しました。

2021/01/31: グーゴロシストの社交場（仮）において Okkuu さんにより式神巨大数が終了したことが告知されました。

2021 年の歴史

2021/01/31: ドメイン駆動開発におけるドメイン知識……物事に関する知識を主体が何であるのか意識しながら纏めるという概念を知ったので、何らかのものに適用したくなりました。それで身の回りにあるものを探すと、式神巨大数の規則という丁度良いものがありました。そこで、これを式神巨大数の規則に適用しようとしました。

2021/02/05: 反省を組み込みながら式神巨大数の規則を纏めなおしたものが完成しました。

2021/02/05: 表示などを確認するために、巨大数研究 Wiki に投稿しました。

2021/02/14: ユーザー:Hexirp/式神巨大数/2021/規則へのリンクをグーゴロシストの社交場（仮）へ投稿しました。

2021/02/18: 2021 年度の式神巨大数には YH 数列システム 3.0 を投稿する予定であることをツイートしました。

2021/02/18: 甘露東風さんが式神巨大数に参加するのをやめた理由をツイートしました。

2021/02/19: 甘露東風さんの意見を受けて、チャットを使って投稿すると定めた理由をツイートしました。

2021/03/18: 投稿の敷居が高いという問題を解決する良いアイデアを思い付いた旨をグーゴロシストの社交場（仮）に書き込みました。

2021/03/18: 甘露東風さんの意見に対応するために、規則へ代理投稿の条項を加えました。

用語

式神巨大数に関連した言葉を集めます。

四季神巨大数

四季神巨大数は、審査期間の延長が繰り返された結果として、開催期間が四季の全てに掛かることになってしまった式神巨大数のことです。

武伸臣丈類

武伸臣丈類は、 "車万臣丈類2" と "車万臣丈類3" という東方巨大数の裏話を投稿するためのハッシュタグを元にして私が作った式神巨大数の裏話を投稿するためのハッシュタグです。

逆式神巨大数

逆式神巨大数とは、 p進大好きbot さんによれば「有限的手続きを一切取ってはいけない」大会であり、私によれば「みんなが巨大数を計算するプログラムに作られて競い合わされる——すなわち、この世界は巨大数を抽出するためにエミュレートされていて、その中でみんなが巨大数を作ったり私が式神巨大数を開いていたりしているのである——」大会です。

関連項目

• 2020 年の式神巨大数
• 2021 年の式神巨大数