エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

中間報告(2)

証明図を切り詰めることの極限として無限に続く入出力を表すこと(形式的冪級数のように)を考えています。これは以下のような問題に対応するためです。

サーバー上で(理論的には)無限の時間にわたって動作しているプログラムと、それと連携したブラウザーで実行されるプログラムの組み合わせは、全体としては無限に続く入出力を扱うプログラムと考えることができます。この全体をうまく書き表す方法が見つからないので、無限に続く入出力について考えることが難しいという問題があると考えています。この問題を解決したいと考えています。

この記述方法により、サーバー側のプログラムを変更せずに、プラウザー側からの入力によってサーバー側のプログラムが変更されたような動作をさせることができるようになることを目的としています。

上記の方法で無限に続く入出力を書き表すこと自体はできなくはないと思うのですが、その手順を普通のプログラミング言語のように記述すると複雑になるのではないかと思われます。適当な代数的構造を見つけて、それに関する数式の変形のような動画によって記述するということを考えています。これはどういうことかというと、数式の変形を繰り返した最終的な形を定義とするというものです。これは一つだと帰納的な定義と同じことのようですが、複数の定義を組み合わせることにより複雑な定義ができると思われます。

代数的構造と数式の組み合わせのヒントを得るため、現在群論圏論などについて調べています。

上記のような記述方法ができれば、たとえばクイズに答えていくことによりサーバー側のプログラムを変更したような動作をさせることができるようになります。

また、「どのようなプログラミング言語が10年後でも使えるのか」という問題があります。1つのプログラミング言語について言えば、どのプログラミング言語も10年後には使えないとは思うのですが、無限に続く入出力の考え方は有効ではないかと考えています。