Introduction

数学の定義を理解するために、普通はその定義に関する計算などをやってみますが、 ここでは、それに代わって、コンピューターを使って対話的に操作をする ことによって理解するということを考えます。 そうすることによって、紙の上でできる計算よりも複雑な定義を 理解することができるということを目指しています。 しかし、それを実現するためには、現在普通に使われているユーザーインターフェイス では難しいと考えられます。 この問題を解決するため、新しいユーザーインタフェイスを考えていくことが第一の目標です。 さらに、(ここでの実現は難しいとは思いますが)もし可能ならば、 そのユーザーインタフェイスを使って 実際の数学の問題も解けるということも目標としています。 このような目標を実現するために、 ここではいろいろ実験的に作ったものを発表していく予定です。 ここに発表するものは、だいたい次のような目的を持っています。 個々の項目の大まかな目的は以下のようになります。

Mathematics

かけ算・わり算

10進法でのかけ算、わり算のやり方を、 対話的に操作をしながら理解することができるようになることが目的です。 かけ算をたし算とシフトで、わり算をひき算とシフトで行うという、 コンピューターの動作原理(大げさ？)を理解することができます。 電卓風のユーザーインターフェースは、PDA、携帯電話向けです。

ユークリッドの互除法

2つの整数(Z, Z[i], Z[ω])の最大公約数を求めるときの 操作をステップごとにやってみることことによって 理解することができるようになることが目的です。 また、最大公約数を求めるプログラムを作ることができます。 ただしこれはあまり使いやすくないので、改良したいと思っています。 それとこれを理解することは、「フェルマーの大定理の3の場合」の証明を 理解するために必要となります。

素因数分解

整数を素数の積に実際に分解することができます。 そのことによって実際に分解できることを理解できるようになることが目的です。 また、素数を求めるプログラムを作ることができます。 ただしこれはあまり使いやすくないので、改良したいと思っています。 それとこれを理解することは、「フェルマーの大定理の3の場合」の証明を 理解するために必要となります。

連立1次方程式

連立1次方程式を解くときの 操作をステップごとにやってみることことによって 理解することができるようになることが目的です。 電卓風のユーザーインターフェースは、PDA、携帯電話向けです。 また、代数方程式の解法、「フェルマーの大定理の3の場合」の証明を理解するために 必要となります。

代数方程式: 2次方程式の解法、 3次方程式の解法1、 3次方程式の解法2

根の置換を使って代数方程式をべき根によって解く方法を、 対話的に操作をしながら理解することができるようになることが目的です。 体の拡大との対応まで書けるとよいのですが、 体の拡大の説明ができていません。 これを説明するために、 「ある演算を持つ集合があって、その集合の元を代表してある文字で表すとし、 その文字をその集合に付け加えた集合に対しても演算の規則が成り立つとすると、 新しい集合を定義することができる」というようなことを、 他の項目で書いていく予定です。

フェルマーの大定理

「フェルマーの大定理」の3の場合を、イデアルを使って証明する手順を、 対話的に操作をしながら理解することができるようになることが目的です。 この証明は参考文献にある証明をイデアルを使って書き直したものです。 一般の場合の「フェルマーの大定理」が証明できればもっとよいのですが、 どうやって証明するのかを知りません。

環

環の定義を 対話的に操作をしながら理解することができるようになることが目的です。 環の定義だけからわかるいろいろなことを、実際に証明してみることができます。 群で同じようなことをやろうとしても、群の定義だけからわかる結果はあまりないです。

自然数の演算

自然数の定義を 対話的に操作をしながら理解することができるようになることが目的です。 また、式を組み合わせて帰納法の証明を行う方法を提案しています。 帰納法については、別の項目でも扱っています。 この方法を発展させて、もっと高度な証明をやりたいと思っています。

群: (a)群の定義、 (b)群の語の問題、 (c)群の定義2、 (d)群の等式の合成

群の定義を 対話的に操作をしながら理解することができるようになることが目的です。 (b)は、群の定義の一部から他のものを導くことができる、ということを (本来は)自動的に(ここではちがう)示すことができるというものです。 ここには、これ自体を発展させたものはありませんが、(a)(c)(d)の導入のためにあります。 これ自体も数学としても計算のためのシステムとしても面白いです。 (a)(c)は群の定義の一部を使って他の式を変形していくというものです。 (a)は電卓風、(c)は新しく作った式の操作をするユーザーインターフェイス(ペン向き)となっています。 どちらもPDA向き((a)は携帯電話でも可)になっています。 (d)は(c)と同様のユーザーインターフェイスで群の定義の一部の式を組み合わせて 群の定義を導くというものです。

Zornの補題: Zornの補題、 Zornの補題2

選択公理から「Zornの補題」を導く手順を、 対話的に操作をしながら理解することができるようにしようと思ったのですが、 今のところ説明だけで、動かすことはできません。

Fractals: (a)Fractals、 (b)Fractals2、 (c)Fractals3、 (d)Fractals4

Fractal図形を描画するプログラムを、木の操作をするユーザーインターフェイス を使って作る方法を提案するのが目的です。 (a)はGUIなし(テキストで入力)、(b)はTreeViewという、木の操作を行う一般的な部品を使ったもの、 (c)(d)は独自のユーザーインターフェイスによるものです。 (d)はPDA向けになっています。(Zaurus用あり)

定規とコンパスによる作図

定規とコンパスによる作図を実際にやってみることができます。 そのことによって作図の方法を理解できるようになることが目的です。 Zaurus用もあります。

円の面積

円の面積を多角形で近似するにことを実際にやってみることによって 円の面積を求める方法を理解できるようになることが目的です。 Zaurus用もあります。

式

順序に従って式を簡単にしていくことができます。 このことによって、式を簡単にしていくときの順序を 理解することができるようになることが目的です。 Zaurus用もあります。

かけ算の練習

10進法でのかけ算のやり方を、 対話的に操作をしながら理解することができるようになることが目的です。 上の「かけ算・わり算」とは違ってコンピューターは何も計算をやってくれません。 全部自分でやらなければいけません。 上の「かけ算・わり算」が手回し式計算機のようなものだとすると こちらは算盤のようなものです。 計算にもいろいろなレベルがあるので、こういう練習も必要ではないかということで 作成しました。 PDA向けになっています。(Zaurus用あり)

Computing

Prolog

論理プログラミング言語Prologの基本的なプログラムを実行することができます。 このことによって、論理プログラミングの考え方を 理解することができるようになることが目的です。

単一化(unification)

単一化アルゴリズムとその結果が最も一般的な単一化代入になることの証明と、 単一化アルゴリズムを論理プログラミング言語で記述する方法を説明しています。

帰納法

論理プログラミング言語で帰納法による証明をする例(自然数、群1、群2、リー代数) について説明しています。 このような証明をするプログラムを作ることが目的です。

帰納的に定義された構造: 帰納的に定義された構造、 帰納的に定義された構造2、 多項式

コンピューターでリスト、2分木、半群、可換半群、べき等律をみたす可換半群 自然数、重複を許す集合、自然数上の多項式、環上の多項式、木 を表す方法について説明しています。 これと、論理プログラミングを組み合わせて、 問題を解くプログラムを作ることが目的です。 また、コンピューターで上記のようなオブジェクトを表すときに、 オブジェクトの間に順序を導入することによってオブジェクト指向 のクラス間の関係を表すことができるということを将来的には説明したいと 考えています。 さらにこのプロセスは、ある代数的構造に要素を付け加えていって 別の代数的構造を作るということも表しています。 このことはまた別の項目で書きたいと考えています。