HOME > 研究活動・産学官連携 > ネットジャーナル > ネットジャーナル33

ネットジャーナル33

解説

解説1:キーワードのあいまい一致と分割を導入したキーワードプログラミングシステム

統合開発環境(IDE)に付加して使用することができるキーワードプログラミングシステムを開発・実装。プログラムコードを入力する際、コードの一部を入力するだけでGoogleなどのWeb検索エンジンのようにポップアップに候補の一覧が表示される。人工知能技術を応用することにより、ユーザが正しいスペルをよく覚えていなくても、自信のある文字だけを入力あるいは打鍵数削減のために簡略化した単語を入力するだけで完全型のソースコードを生成することができる。また、1文字程度の間違いや置換や追加が起こった場合も、最適なソースコードがなるべく上位に来るよう設計されている。

図:画像処理とその応用

本文にもどる

解説2:関数型プログラミング言語

計算や処理などを関数の定義の組み合わせとして記述していくプログラミング言語。数学における関数と似た性質を持った関数の定義としてプログラミングを行う。現在の技術による1つのプロセッサの能力向上には限界がある(ムーアの法則)ため、複数のコアにより並列計算を行うマルチコア・プロセッサが普及してきている。それに合わせて、計算を逐次的に行わせる伝統的なプログラミング言語ではなく、並列計算の記述と実行に適した関数型プログラミング言語が今後普及すると考えられている。Haskellが特に有名。最近は、ErlangやScalaなど、注目すべき関数型プログラミング言語がつぎつぎと開発され、入門書が出版されている。

本文にもどる

解説3:項書換え系

関数型プログラミング言語の理論的なモデル。等式(たとえば、s=t)を左から右、または右から左に向き付けて得られる書換え規則(たとえば、s→t)の集合により計算システムを表現する。たとえば、自然数xより1だけ大きい数をs(x)というデータ表現でコーディングすると、つぎの2つの書換え規則

    plus(0,x) → x
    plus(s(x),y) → s(plus(x,y))

で定義された関数plusによって、つぎのように、plus(s(s(0)),s(0))は最終的にs(s(s(0)))に書き換えられる。

    plus(s(s(0)),s(0)) → s(plus(s(0),s(0)))
                              → s(s(plus(0,s(0))))
                              → s(s(s(0)))

実際、plus(x,y)はxとyの和を定義しており、上の書換えは2+1=3を計算している。このような計算が、コンピュータ上のデータや命令の具体的な表現とは独立に実行可能であるほか、この書換え規則(等式)に基づいて、関数plusの様々な数学的性質(たとえば、plus(x,y)=plus(y,x))をコンピュータで自動的に証明する道が開かれる。コンピュータで行われるどのような計算も、必ず項書換え系で表現することができる。

項書換え系

本文にもどる

解説4:項書換え系による帰納的定理の証明

項書換え系では、コンピュータにさまざまな関数の定義とそれらの満たすべき性質を与えると、コンピュータが数学的帰納法を用いてそれらの性質の自動証明を試みる。数学的帰納法とは、高校の数学で習ったように、任意の自然数nについて成り立つ命題を、(1)n=1のときに成り立つ、(2)n=kのとき成り立つと仮定するとn=k+1のときも成り立つ、の2つのことを示すことによって証明を行う方法。実際には、自然数のほかにも、コンピュータのプログラムで扱う様々なデータ(記号、記号の列、構造データなど)に言及する定理を、発見的に自動証明する方法が研究されている。

この技術により、有限個のnの値を与えてプログラムの正しさをテストすることに加えて、無限個あるすべてのnについてプログラムをテストしたのと同様の効果が得られる。また、わかりやすいが効率が悪い関数を、わかりにくいが効率が良い関数に定義しなおしたとき、両者が内容的に同じ関数であることも証明できる可能性がある。一般に、数学的帰納法を使わないと証明できない定理(帰納的定理)は、そうでない定理(論理的帰結)よりも自動証明が技術的に難しく、チャレンジングな研究テーマの1つとなっている。

項書換え系による定義と演算

本文にもどる

ページの先頭へ