このブログの目標
初期の目標
インターネット上にはユーザーが入力したものが多数ありますが、それを取り込んでプログラムをアップデートしていくことを考えます。
本来はインターネット上のテキストやゲームの入力などを取り込んでほしいのですが、現在はおそらく人間がアップデートしていると考えられます。生成AIなどはありますが、それでアップデートできるかどうかは、ちょっと調べてみた限りでは不明です。これはなぜなのかという疑問を解決することが、このブログの初期の目標でした。
将来AIが発展したとき人間がやることの一つの選択肢になる可能性がありますが、私はAIの専門家ではないので、このブログはこれを目標にするということではありません。
問題を解決するための手法
動き続けているプログラムがあって(インターネット上のサーバーのイメージ)、そこにユーザーの入力が常に反映されるようにすれば良いのですが、現在の状況はユーザーごとの個別の情報だけが反映されているのではないかと考えました。この状況を仮定したとき、サーバーのプログラムが参照透過性を持つものであれば、ユーザーの九力を差分としてプログラムに取り込むことができるのではないかと考えました。
そこで論理プログラミングまたは関数プログラミングの参照透過性を持つプログラムの無限の列を考えます。
これを説明するものを探したのですが、見つかりませんでした。関数プログラミングに関する入門的な記事では、無限の場合には成り立つかどうかよくわからないものが多く、無限の場合に成り立つかどうか調べる方法がほしいと感じました。
このブロクで扱うテーマ
このブログでは、プログラムを記述するための数学的な理論で専門的な技法を使わないものについて考えていきます。
専門家は専門的な技法を使うものを主に研究するため、専門的な技法を使うものについてはちゃんとした用語がありますが、そうではないものについては、おそらく誰かはやっているとは思うのですが、一般的な用語は決まっていないため、検索しても見つからないのだと思います。ガロア理論は群という言葉がない時代に考えられたらしいですが、私にはそのような能力はないので、用語を定義していきます。言葉がなくても考えることができる能力がほしいです。
探しても見つからないものはいくらでもあります。このブログでは、そのようなものを扱っていきます。そのようなものの中で、疑問を解決するために必要なものがあります。それについて考えていきます。
最近の課題
数学的帰納法や多項式の変形については、自動的にできるものがありますが、通常は自動的に行うことはありません。また、順序に依存しないような対称性のある手順であっても順に実行するしかありません。これらの問題を解決することを考えます。数式の変形は、人間が操作すると、複雑すぎてわかりにくいので、ビジュアル・プログラミングの手法を使いたいと考えています。このようにユーザーの入力をプログラムに取り込み、アップデートしていきます。これはゲームのように実行することができるので、初期の目標の一つとなっています。
コンピューターによる証明をエレファントな証明と呼んだということにちなんで、このブログでは数式を自動的に変形して証明などを行うことを「エレファントな…」と呼ぶことにしています。ビジュアル・プログラミングの手法を使って数式を自動的に変形して証明などを行うものを「エレファント・ビジュアライザー」と呼ぶことにしています。このブログのタイトル「エレファント・ビジュアライザー調査記録」はこれを表しています。
このブログのタイトルについて
このタイトルは何を指しているのかわかりにくいので変更したいとは考えているのですが、初期の方針から考えると「アップデート用自動数式変形ゲーム」または「アップデート・ゲーム」としても良いですけどこれもわかりにくいので検討中です。
このような問題を考察するとき、紙に数式を書いて考えていますが、これについてもゲーム的に、何かの文字のようなものを書いたとき自動的に数式に変換してほしいです。
現在の状況
人工知能的代数学
「モノイドの左逆元・右逆元」の問題を ChatGPT を使うとどうなるかということを最初は考えていたのですが、正しく動作しているかどうかを確認する方法がない、疑問点を指摘するための言葉がないということが問題となっています。そこでモノイドまたは半環を使って動作を記述することを検討しています。
この動作は Prolog の動作と同様の部分があるので、これを使って Prolog の動作を説明できないかと考えています。
単一化アルゴリズム
まずそのために単一化アルゴリズムをモノイドまたは半環を使って動作を記述することを考えます。
本に書かれている単一化アルゴリズムの証明がわかりにくいので以前書き直したのですが、やはりわかりにくかったので、これをもう一度書き直しています。
モノイドの素因数分解
単一化アルゴリズムの処理に現れる、イテレーターのようなものをモノイドまたは半環への写像で表すことを考えます。これは素因数分解の手順を一般化したようなもので、何と呼べば良いかわからないので ChatGPT で調べたら素因数分解という言葉しか見つからなかったので素因数分解としています。
これは探しても見つからないものの一つです。
これで単一化アルゴリズムがモノイドや半環で記述できるようになり、「モノイドの左逆元・右逆元」の問題をモノイドまたは半環で書き直すことができるようになったはずなので、今後実際に書き直していく予定です。
準同型定理
これはまだ調査中です。
モノイドの素因数分解について調べているときに、「集合の準同型定理」や「マグマの準同型定理」について書かれた文献を見つけました(素因数分解の用語については書かれていませんでした)。以前このブログでも写像の理論で群の準同型定理を表す記事を書いていました。集合→マグマ→半群→モノイド→群の順で写像を使って説明する予定だったのですが、一部しかできていませんでした。この文献に従って再び見ていきます。この文献では普遍代数によって説明しているようなので、写像を基礎として説明してみたいと思います。
これは探しても見つからないものの一つだと思っていたのですが、少し違いますが同様のものがありました。
普遍代数についてもモノイドや半環で説明できないか調査したいと思います。
今後の予定
イテレーターの調査
現在のプログラミング言語には、プログラムの無限の列を扱う機能がないと思われるので、その機能を実現するためのものとしてイテレーターを使うことを考えます。
サーバーの機能をイテレーターで実現することについて以前このブログでも調べていましたが、これも継続して調べていきます。
クロージャーの調査
イテレーターをクロージャーを使って表すとき、クロージャーの変数が変更可能な場合と変更不可能な場合の違いについて調べています。クロージャーの一般的な定義が不明なので、ここでまずクロージャーの定義をして、変数が変更可能なものと変更不可能なものの間の関係を調べます。
クロージャーに似たものとして、ブロック、名前呼び、関数ポインター、クラス、デリゲート、コールバック、コンストラクターによる分岐についても調べます。
イテレーターによってサーバーを記述するための言語
一つは、イテレーターによってサーバーを記述するための言語です。これはクロージャー調査用の言語の元になったもので、「関数プログラミングと無限論理多項式」で平方根を計算するサンプルを書くために作成した言語です。変数の変更可能なものを変更不可能に変更するとどうなるか調べています。
これは C# で実装しています。通常のプログラミング言語の形式と C# のコードとして書く形式があります。そのほか F#、TypeScript、Go にも移植しています。Lisp、LOGO も検討しています。TypeScript から Python に移植できるかどうかも検討中です。
以前調査していたもの
関数型言語の拡張
「関数型言語に無限に動作するための機能を追加する」ということをやっていましたが、現在も保留中です。「クロージャー調査用の言語」または「イテレーターによってサーバーを記述するための言語」で調べていくことができそうです。
関数プログラミングのクロージャー
「関数型言語の拡張」の続きで「変数を変更することができるクロージャーを変数を変更することができないクロージャーに変換する」ということをやっていましたが、現在も保留中です。これも「クロージャー調査用の言語」または「イテレーターによってサーバーを記述するための言語」で調べていくことができそうです。
人工知能的写像の理論
「群論の計算」の「写像による分類」(さらにその後の「写像の計算」)に書いたような写像と同値類の関係についてまとめています。群の準同型定理の説明をなるべく写像の性質と群の性質に分けて議論しようとしています。この準同型定理に関する部分は「準同型定理」に書いていく予定です。
