エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

クロージャーの調査(1)

プログラム電卓の仕様

クロージャーの基礎となる代数的構造の調査をしていましたが、今回はプログラム電卓クロージャーを導入するとどうなるか、という方向で考えていきます。まず関数の定義を導入していきます。現在、一つの式で定義できる関数以外、関数の定義はできません。データはクロージャーを含まない代数的構造として定義することができます。

プログラム電卓では実行を中断できるようになっています。指定した回数のステートメントを実行した後いったん停止して、そのときに「Break」ボタンを押すと中断することができます。中断した後「Cont」ボタンを押すと実行を再開できます。いったん停止したとき何もしない場合は、指定した時間の後自動的に再開されます。

また、「STOP」ステートメントを実行することによっても、実行を中断することができます。この場合も、中断した後「Cont」ボタンを押すと実行を再開できます。

「INPUT」ステートメントを実行すると、いったん停止して入力ができるようになります。入力した後「OK」ボタンを押すと、実行が再開されます。「GET」ステートメントを実行すると、いったん停止して入力ができるようになります。こちらは何も入力しなくても指定した時間が経過すると実行が再開されます。

実行が再開されるとき、中断する前に最後に実行したステートメントの次のステートメントから再開されます。

プログラム電卓への関数の定義の追加

これに複数のステートメントからなる関数の定義を追加することを考えます。関数の実行中に中断できるようにします。実行が再開されると、中断する前に最後に実行したステートメントの次のステートメントから再開され、関数の実行が終了すると、関数が使われている式が再開されます。

これを実現するには式についても「次の位置」から再開できるようにする必要があります。現在は、式の内部に「次の位置」というものはないのですが、FORTH電卓と同様の処理にすれば「次の位置」を導入することができます。FORTH電卓では、式とステートメントのような区別はなく、すべて逆ポーランド記法で記述するようになっています。これによってプログラム電卓と同様の

を実現しています。

QuickBASIC(wikipedia:QuickBASIC)の仕様では、関数の定義は

  • 定義の内部で使われている変数は引数かローカル変数
  • 外部の変数を使うことはできない
  • 引数は参照で渡される

となっていますが、引数に変数を追加すれば外部の変数を使うことと同じことになります。

  • 関数定義の内部で関数を定義できる
  • 関数を引数や戻り値にすることができる
  • 「引数に追加した変数」のアドレスは、その関数定義の外部の関数で使われるローカル変数のアドレス

とすれば、クロージャーとして使うことができます。

このとき中断するにはどうすれば良いか考えていきます。

FORTH電卓へのクロージャーの実装

FORTH電卓では関数(FORTHの用語ではワード)定義の内部で関数は定義できない、ローカル変数は使えないという仕様になっています。これは、JavaScriptで実装するためアドレスを使えるようにする意味があまりないのと、FORTHの仕様が不明だったためです。これを

  • 関数定義の内部で関数を定義できる
  • ローカル変数が使える
  • さらに、関数のアドレスを使うことができる

とすればどうなるか考えていきます。

  • 関数の引数、戻り値はスタックに入れる(パラメータースタック)
  • ローカル変数はスタックのような構造(ただし参照されているデータは消去されない)で実装(C#ではImmutableStackでできそうです。これをローカル変数スタックとします。)
  • 関数のアドレスをスタックに入れることができ、関数のアドレスから関数を呼び出すことができる

とすればクロージャーを実現できそうです。関数呼び出しの情報は関数呼び出しスタック、ループ情報はループ情報スタックに保存するとします。

  • パラメータースタック(引数、戻り値)
  • ローカル変数スタック
  • 関数呼び出しスタック
  • ループ情報スタック

を保存すれば、クロージャー実行中に中断して、入出力の後戻って来ることができます。

BASIC、FORTHの仕様は以下の本を参考にしています。

galapagosstore.com

多重集合・自由可換モノイド(1)

エレファントな整数論では、素因数分解の一意性のわかりやすい記法を考えていたのですが、良い方法ができず止まっていました。ここでは、数式ではなくプログラミング言語を使って書くとどうなるか考えていきたいと思います。まず、エレファントな整数論(18)、(19)で書いた内容を書いておきます。

整数の素因数分解の多重集合としての一意性

重複度を含めた集合を多重集合(wikipedia:多重集合参照)と呼びます。多重集合  \{| x_1, x_2, \cdots , x_m |\} とは、通常の集合とは異なり、 x_1, x_2, \cdots , x_m の中に重複するものがあったとき、その出現する回数が異なれば多重集合としては異なるものとするものです。

多重集合  \{| x_1, x_2, \cdots , x_m |\} \{| y_1, y_2, \cdots , y_n |\}全単射  g: \{1, 2, \cdots, m\} \to \{1, 2, \cdots, n\} が存在して任意の  i \in \{1, 2, \cdots, m\} に対して  x_i = y_{g(i)} であるとき  \{| x_1, x_2, \cdots , x_m |\} = \{| y_1, y_2, \cdots , y_n |\} とします。

多重集合  \mathcal{X} = \{| x_1, x_2, \cdots , x_m |\} \mathcal{Y} = \{| y_1, y_2, \cdots , y_n |\} に対して

  •  \{| x_1, x_2, \cdots , x_m, y_1, y_2, \cdots , y_n |\} \mathcal{X} + \mathcal{Y} と書くことにします。
  •  \mathcal{X} + \mathcal{Z} = \mathcal{Y} となる多重集合  \mathcal{Z} が存在するとき  \mathcal{X} \le \mathcal{Y} \mathcal{Z} = \mathcal{Y} - \mathcal{X} と書くことにします。
  •  m \# \mathcal{X}と書くことにします。
  •  \displaystyle \prod_{i=1}^m x_i \displaystyle \prod \mathcal{X} と書くことにします。 \# \mathcal{X} = 0 のときは  \displaystyle \prod \mathcal{X} = 1 とします。

 \mathcal{Y} \le \mathcal{X} のとき  (\mathcal{X} - \mathcal{Y}) + \mathcal{Y} = \mathcal{X} となります。

 e: S \to \mathbb{N} に対して  \mathrm{supp}(e) \mathrm{supp}(e) = \{ x \in S \mid e(x) \ne 0 \} とおきます。

集合  S に対して  \mathrm{Bag}(S) \mathrm{Bag}(S) = \{ e: S \to \mathbb{N} \mid \mathrm{supp}(e) \ は有限集合 \} とおきます。

 e \in \mathrm{Bag}(S) \mathrm{supp}(e) = \{ x_1, \cdots, x_n \} のとき、 e は多重集合  \mathcal{X} = \{| \underbrace{x_1, \cdots, x_1}_{e(x_1)個}, \cdots, \underbrace{x_n, \cdots, x_n}_{e(x_n)個} |\} と同一視することができます。

 S \subseteq \mathbb{N} のとき  \displaystyle \prod \mathcal{X} = \prod_{x \in \mathrm{supp}(f)} x^{e(x)} が成り立ちます。

整数  a の倍数全体の集合を  (a) とします。
 \begin{eqnarray*}
P & = & \{ p \in \mathbb{N} \setminus \{0, 1\} \mid (x)(y) \subseteq (p) \implies (x) \subseteq (p) \lor (y) \subseteq (p) \} \\
 & = & \{ p \in \mathbb{N} \setminus \{0, 1\} \mid p \mid xy \implies p \mid x \lor p \mid y \}
\end{eqnarray*}
とおくとエレファントな整数論での議論より  P素数全体の集合となります( a \mid b b a で割り切れること、 \land は「かつ」、 \lor は「または」を表します)。

 \mathcal{P}, \mathcal{Q} \in \mathrm{Bag}(P) のとき、 \prod \mathcal{P} = \prod \mathcal{Q} ならば  \mathcal{P} = \mathcal{Q}

[証明]  \{| p |\} \le \mathcal{P} となる  p が存在しないとすると  \prod \mathcal{P} = 1 となります。 \prod \mathcal{P} = \prod \mathcal{Q} ならば  \prod \mathcal{Q} = 1 となって  \# \mathcal{Q} = 0 となるので  \mathcal{P} = \mathcal{Q} となります。

 \{| p |\} \le \mathcal{P} となる  p が存在するならば、 P の定義より  \{| p |\} \le \mathcal{Q} となります。 \mathcal{P}' = \mathcal{P} - \{| p |\} \mathcal{Q}' = \mathcal{Q} - \{| p |\} とおくと  \prod \mathcal{P} = \prod \mathcal{Q} より  \prod \mathcal{P}' = \prod \mathcal{Q}' となります。このとき  \mathcal{P}' = \mathcal{Q}' と仮定すると、 \mathcal{P} = \mathcal{P}' + \{| p |\} = \mathcal{Q}' + \{| p |\} = \mathcal{Q} となります。

よって  \# \mathcal{P} に関する機能法により主張が成り立ちます。[証明終わり]

これを数式の変形で書きます。
 \# \mathcal{P} = m とすると
 \begin{eqnarray*}
 &  & \left[ \ \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \# \mathcal{P} = 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 &  & \land \left[ \ \# \mathcal{P} \ne 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \# \mathcal{P} \ne 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_1 + \{| p_1 |\} \land \prod \mathcal{P}_1 = \prod ( \mathcal{Q} - \{| p_1 |\} ) \implies \mathcal{P}_1 = \mathcal{Q} - \{| p_1 |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_2 + \{| p_1, p_2 |\} \land \prod \mathcal{P}_2 = \prod ( \mathcal{Q} - \{| p_1, p_2 |\} ) \implies \mathcal{P}_2 = \mathcal{Q} - \{| p_1, p_2 |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_3 + \{| p_1, p_2, p_3 |\} \land \prod \mathcal{P}_3 = \prod ( \mathcal{Q} - \{| p_1, p_2, p_3 |\} ) \right. \\
 & & \left. \implies \mathcal{P}_3 = \mathcal{Q} - \{| p_1, p_2, p_3 |\} \ \right] \\
 & \Longleftarrow & \\
 & \vdots & \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_m + \{| p_1, \cdots, p_m |\} \land \prod \mathcal{P}_m = \prod ( \mathcal{Q} - \{| p_1, \cdots, p_m |\} ) \right. \\
 & & \left. \implies \mathcal{P}_m = \mathcal{Q} - \{| p_1, \cdots, p_m |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_m + \{| p_1, \cdots, p_m |\} \land \prod \mathcal{P}_m = \prod ( \mathcal{Q} - \{| p_1, \cdots, p_m |\} ) \right. \\
 & & \implies \left. \mathcal{P}_m = \mathcal{Q} - \{| p_1, \cdots, p_m |\} \ \right] \\
\end{eqnarray*}
となります。ここで  \mathcal{X} =_\exists \mathcal{Y} + \mathcal{Z} \mathcal{X} = \mathcal{Y} + \mathcal{Z} となる  \mathcal{Y} \mathcal{Z} が存在することを表すとします。最後の項は  \# \mathcal{P}_m = 0 なので成り立ちます。よって  \prod \mathcal{P} = \prod \mathcal{Q} ならば  \mathcal{P} = \mathcal{Q} となります。

中間報告(11)

Optimistic Mathematicsのサイトにフラクタル関連の記事をいくつか公開しているのですが、Javaで書いたものがあり、それらをJavaScriptで書き直した方が良いのではないかということで現在書き直している途中です。

書き直したものは数学とソフトウェアのページに公開しています。

その他フラクタル関連以外でも書き直した方が良いものは書き直しています。新規で作成しているものもあります。

フラクタルクロージャーの調査に使えるかもしれないということで調べていたのですが、この作業が終わったらクロージャーの調査に戻ろうと考えています。

クロージャーを定義するときに使うデータにクロージャーを含まないようにすることができるかどうか、フラクタルを例として考えることはできないかと考えています。

フラクタル(2)

ウェブリブログからSeesaaブログ(数学とソフトウェアのメモ2)に移行することになったので、数学とソフトウェアのメモ2の方に数学とソフトウェアのページのサイトの説明を書いていこうと思います。

フラクタル関連の項目の説明はこのブログにも書く予定です。

中間報告(10)

「ラムダ計算と無限ラムダ多項式」では呼び出しの深さが有限のクロージャーを含む式を表すための「有限ラムダ多項式」を定義しましたが、これは「一般マグマの多項式」と同様のものでした。呼び出しの深さが有限なのでクロージャーを除去することはできると思われるのですが、式にクロージャーを含むようにしたほうが良いのでこれも考えていきたいと思います。これは「有限ラムダ代数」という名前に変更したいと思います。

「たらい回し関数」はクロージャーの変数を「変更できない変数」にする方法のために調査していたのですが、これはできそうにないので中断しています。「アッカーマン関数」の項の中で書いた関数の分類は使えるかもしれません。

フラクタル」もこの目的に使えるかもしれないので調査しています。このブログでは有限時間で終了する論理プログラミングと無限の時間動作する論理プログラミングの関係をフラクタルの考え方で表すことはできないかと考えていましたが、中断しています。クロージャーを表すために使えるかどうかも考えてみたいと思っています。

またMathematics and Computingで書いたフラクタルのプログラムをJavaScriptで書き直しているので、その件もこのブログに書こうと思っています。

フラクタル(1)

このブログでは有限時間で終了する論理プログラミングと無限の時間動作する論理プログラミングの関係をフラクタルの考え方で表すことはできないかと以前考えていましたが、その件は今は中断しています。今後はクロージャーではどうなるか考えてみたいと思っています。

Mathematics and Computingフラクタルの図形を描画できるようになっていたのですが、JavaActiveXで書いてあるので今は動作しないようです。これは今後書き換えていきたいと思います。

Vectorのサイトに上記のサイトのプログラムに「ソースコード」を作成するエディタを追加したものが登録してあります。(WindowsFractal Diagram Editorの詳細情報 : Vector ソフトを探す!JavaFractal Diagram Editor(Javaアプリケーション版)の詳細情報 : Vector ソフトを探す!)

フラクタル: 混沌と秩序のあいだに生まれる美しい図形 アルケミスト双書』や『アートで魅せる数学の世界』に書かれている「Lシステム」のような形で描画できるシステムを作成してみましたが、それだとあまり複雑なことはできそうにない感じです。

そこでMathematics and Computingのシステムを発展させてC#のコードのように書けるようにしたいと思ったのですが、まだうまくできていません。

まずMathematics and Computingを書き換えてみたいと思います。

アッカーマン関数(3)

関数の再帰的定義

ここではある形の関数の再帰的定義について考えます。

 g: X \to X に対して  g^+: \mathbb{N} \times X \to \mathbb{N} \times X g^+(n, x) = (n+1, f(x)) と定義します。

 \mathcal{S}(g^+, (n, x)) = \{ S \mid S \subseteq \mathbb{N} \times X, (n, x) \in S, g^+(S) \subseteq S \} \overline{g^+}(n, x) = \bigcap \mathcal{S}(g^+, (n, x)) とおきます。

 \mathcal{S}_0 = \mathcal{S}(g^+, (0, a)) R = \overline{g^+}(0, a) = \bigcap \mathcal{S}_0 とおくと  R
 \begin{cases}
(0, a) \in R \\
(n, x) \in R \implies (n+1, g(x)) \in R
\end{cases}
を満たす最小の集合となります。

 S \subseteq \mathbb{N} \times X に対して  \pi_1(S) = \{ n \in \mathbb{N} \mid (n, x) \in S \ \text{を満たす} \ x \in X \ \text{が存在する}\} と定義します。

 R_1 = \pi_1(R) とおくと
 \begin{cases}
0 \in R_1 \\
n \in R_1 \implies n+1 \in R_1
\end{cases}
が成り立つので、自然数の性質より  R_1 = \mathbb{N} となります。

計算可能性の議論にはこれだけでも良いとは思うのですが
 f(n) = x \iff (n, x) \in R
によって関数  f: \mathbb{N} \to X を定義するには、任意の  n \in \mathbb{N} と任意の  x, y \in X に対して  (n, x) \in R かつ  (n, y) \in R ならば  x = y が成り立つ必要があります。以下でこれを示します。

 \{(0, a)\} \cup \overline{g^+}(g^+(0, a)) \in \mathcal{S}_0 となるので  R \subseteq \{(0, a)\} \cup \overline{g^+}(g^+(0, a)) となります。

 (0, x) \in R とすると  (0, x) \notin \overline{g^+}(g^+(0, a)) なので  (0, x) \in \{(0, a)\} となります。よって  x = a となります。

よって  n = 0 のときには成り立ちます。

次に  n のときには成り立つと仮定します。 (n, b) \in R とします。

 R_n = \{(k, x) \in R \mid k \le n\} c = g(b) とおくと  (n+1, c) \in R となります。

 R_n \cup \{(n+1, c)\} \cup \overline{g^+}(g^+(n+1, c)) \in \mathcal{S}_0 となるので  R \subseteq R_n \cup \{(n+1, c)\} \cup \overline{g^+}(g^+(n+1, c)) となります。

 (n+1, x) \in R とすると  (n+1, x) \notin R_n \cup \overline{g^+}(g^+(n+1, c)) なので  (n+1, x) \in \{(n+1, c)\} となります。よって  x = c となって  n+1 のときにも成り立ちます。

よって帰納法により任意の  n \in \mathbb{N} と任意の  x, y \in X に対して  (n, x) \in R かつ  (n, y) \in R ならば  x = y が成り立ちます。よって
 f(n) = x \iff (n, x) \in R
によって関数  f: \mathbb{N} \to X を定義することができます。