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

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

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

演算が「多重集合・自由可換モノイド(2)」と同じようになったので書き方を戻すことにします。単項イデアル整域のイデアル全体の集合の作る半環について考えます。単項イデアル整域の素元分解が可能であることの説明を数式で書いてみたのですが、少し長くなり…

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

「数学ではできるがコンピューターではできないこと」、「コンピューターではできるが数学ではできないこと」があると考えられていると、私の感想ですが、思います。これらは実際にできないということではなく、それを記述する方法がないのではないかと、私…

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

ここでは、データの順序に依存しないアルゴリズムをプログラミング言語のデータ構造で表すことを考えています。単項イデアル整域のイデアルの演算を抽象化したものを考えます。いったん今までの結果をまとめます。 を可換モノイドで簡約可能とします。単位元…

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

「単項イデアル整域では既約元は素元である」ということの証明を書いていなかったので付け加えます。以下の条件を考えます。 の任意の元 の最大公約数 が存在する(ここでは は最大公約数を表すとします)。 が成り立つとします。 [証明] とし とします。 であ…

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

とおいて書き直します。 を可換モノイドとします。 は簡約可能とします。 は順序をもちます。 積は順序を保存します。 は最小元となります。 このような代数的構造の名前は何かありそうですが、調べてみましたが見つからないのでこのまま進めます。 とおき、…

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

エレファントな整数論(13)の証明が間違っていたので書き直します。整域 の素元全体の集合を 、既約元全体の集合を とします。 のイデアル ( で生成された単項イデアル)を と書きます。 に対して を と書きます。 のイデアル全体の集合を とおきます。 を と…

中間報告(12)

クロージャーの調査 「クロージャーの調査」では、以下のようなことを考えていく予定です。関数プログラミングのデータ(クロージャーを含んでも良い)の代数的構造を「無限関数プログラミングデータ」とします。次に、クロージャーの呼び出しの深さが有限のあ…

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

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

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

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

中間報告(11)

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

フラクタル(2)

ウェブリブログからSeesaaブログ(数学とソフトウェアのメモ2)に移行することになったので、数学とソフトウェアのメモ2の方に数学とソフトウェアのページのサイトの説明を書いていこうと思います。フラクタル関連の項目の説明はこのブログにも書く予定です…

中間報告(10)

「ラムダ計算と無限ラムダ多項式」では呼び出しの深さが有限のクロージャーを含む式を表すための「有限ラムダ多項式」を定義しましたが、これは「一般マグマの多項式」と同様のものでした。呼び出しの深さが有限なのでクロージャーを除去することはできると…

フラクタル(1)

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

アッカーマン関数(3)

関数の再帰的定義 ここではある形の関数の再帰的定義について考えます。 に対して を と定義します。、 とおきます。、 とおくと は を満たす最小の集合となります。 に対して と定義します。 とおくと が成り立つので、自然数の性質より となります。計算可…

アッカーマン関数(2)

ハイパー演算子 『計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)』の「問 1.3.17 (4)」が簡単にはできそうにないので、まず『コンピュータと数学 (現代基礎数学)』の第5章を見ていきます。第5章では「ハイパー演算子」(wikipedia:ハイパ…

アッカーマン関数(1)

アッカーマン関数についても調査します。アッカーマン関数は以下のように非負整数 と に対して帰納的に定義された関数です(wikipedia:アッカーマン関数、計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座) 参照)。 \begin{cases} f(0, y) & =…

たらい回し関数(6)

while の繰り返しが2回以下であることを考えると、以下のように書き直すことができます。これを見ると a2 と c2 は計算する必要がありません。 public static string Test() { int count = 0; int depth = 0; float tarai(float x, float y, float z, int d)…

たらい回し関数(5)

たらい回し関数についてはクロージャーの説明には使えそうにないので変数を使わないように書き直す意味はあまりないとは思いますが、やってみます。たらい回し関数をできるだけ変数を使わないように書き直します。このために前回「呼び出しの深さ」について…

たらい回し関数(4)

たらい回し関数(以下の または tarai)の呼び出しが重なっている(呼び出しが終了する前に呼び出しが行われる)回数の最大値を「呼び出しの深さ」と呼ぶことにします(以下の depth)。 public static string Test() { int count = 0; int depth = 0; float tarai…

たらい回し関数(3)

(3)の場合を に関する帰納法の仮定から証明することができます。 (3) かつ ならば のときは定義より 、 のときは に関する帰納法の仮定(*)より は定義されていて となります。よって

たらい回し関数(2)

前回の説明ではたらい回し関数が「定義されている」とはどういうことなのかという説明が不足していました。たらい回し関数の定義 は、以下の関数「tarai」の呼び出し回数(count)が有限(「tarai」が有限時間で終了する)のとき「定義されている」とします。こ…

たらい回し関数(1)

たらい回し関数は変数を取り除く例としては使えそうにないので別の項目にすることにしました。ここでは帰納法のパターンについて調べていきます。まず普通に帰納法で証明しようと思ったのですが、以下の順にしないとうまく証明できないようです。 たらい回し…

ラムダ計算と無限ラムダ多項式(18)

たらい回し関数の調査 たらい回し関数は変数を使わない例には使えそうにないですが、調査を継続します。「wikipedia:竹内関数」に書かれている高速化をやってみます。C# で書いた以下のプログラムについて考えます。 public static string Test() { int coun…

ラムダ計算と無限ラムダ多項式(17)

たらい回し関数の例 フィボナッチ数列の例ではクロージャーを変数を使わずに書く例としては単純すぎてわかりにくかったので、たらい回し関数が使えるかどうか調べてみます。まずたらい回し関数自体について調べてみます。たらい回し関数は以下のように定義さ…

ラムダ計算と無限ラムダ多項式(16)

フィボナッチ数列の例(4) クラスを使ったものを考えます。 private class FibClass { private int x = 0; private int y = 1; public int Next() { int z = x + y; x = y; y = z; return z; } } このクラスを使ったものは以下のようになります。 IEnumerable<int></int>…

ラムダ計算と無限ラムダ多項式(15)

フィボナッチ数列の例 繰り返しの回数が有限のときに、(有限個の)変更しない変数で書けることや関数の再帰的定義を取り除くことができること(また変数や関数定義を取り除くことができること)を示すための例を考えます。平方根の例は長いので、ここではフィボ…

ラムダ計算と無限ラムダ多項式(14)

有限ラムダ多項式 Lisp 「平方根の例」を移植するために Common Lisp のサブセットを目指した Lisp を作成します。これを「有限ラムダ多項式 Lisp」と呼ぶことにします。仕様は以下のようになります。 定数・変数 定数には数値、t (真を表す)、nil (偽を表す…

ラムダ計算と無限ラムダ多項式(13)

有限ラムダ多項式によるクロージャーの定義 有限ラムダ多項式 有限ラムダ多項式は以下のものから構成されます。 定数 変数 は演算子、 は有限ラムダ多項式 演算子 に対して演算子の項数 が決まっているとします。定数は項数 の演算子とします。 クロージャー…

ラムダ計算と無限ラムダ多項式(12)

有限の場合から無限の場合へ 有限の場合(任意の再帰的定義の関数の呼び出しの深さが有限の回数 以内の場合)、関数定義、無名関数、クロージャーを取り除くことができて、式の値は以前定義した「一般マグマの多項式」のような形にすることができます。これの…

ラムダ計算と無限ラムダ多項式(11)

有限の場合のポインター除去 再帰的定義の関数が有限の回数で終わるとき、再帰的定義がない形に書き直すことができます。C# で階乗を求める関数で考えてみます。 private int fac(int n) { if (n == 1) { return 1; } else { return n * fac(n - 1); } } 関…