今北産業pedia

一階述語論理の定理証明において、エルブランの定理に基づく初期の手法。

論理式の充足不能性を判定するために、基底例を順次生成して検証する。

計算効率に課題があったが、後の自動定理証明技術の基礎となった。

項書き換え系において、与えられた等式の集合を完備な書き換え系に変形する手法。

合流性と停止性を備えることで、項の等価性を効率的に判定可能にする。

自動定理証明や数式処理システムの最適化などに広く応用されている。

スペルチェック機能が、誤字を意図しない別の単語に自動修正してしまう現象。

かつて「cooperation」がアップル本社所在地の「Cupertino」に修正されたことに由来する。

文脈を無視した修正により、公文書などで奇妙な誤変換が発生することがある。

巡回セールスマン問題において、近似比1.5を保証する近似アルゴリズム。

最小全域木と最小重量マッチングを組み合わせ、オイラー閉路を構築する。

多項式時間で動作し、一般的な距離空間におけるTSPの解法として重要である。

完備半順序集合上のスコット連続な関数は、最小不動点を持つという定理。

計算機科学において、再帰的なプログラムの定義に数学的な意味を与える。

不動点はボトム要素からの近似の極限として構成的に求められる。

計算理論において、任意の計算可能な関数が自分自身のプログラムを参照できるという定理。

自己複製プログラム（クワイン）の存在を理論的に証明する根拠となる。

プログラムが自身のソースコードを知らなくても、その挙動をシミュレート可能にする。

任意の有限オートマトンが、単純群とリセットオートマトンの組み合わせで分解できるという定理。

代数的オートマトン理論における中心的な成果であり、構造の複雑さを分類する。

群論の知見を計算モデルの解析に応用した画期的な理論である。

コンピュータの計算量あたりの消費エネルギーが、約1.5年ごとに半減するという法則。

ムーアの法則のエネルギー版とも言われ、モバイル機器の普及を支える背景となった。

半導体の微細化や電力制御技術の向上により、長期間にわたって成立している。

並列計算において、問題サイズを大きくすれば並列化による加速効果も向上するという法則。

並列化できない部分が固定されていても、全体の処理量を増やせば効率が改善することを示す。

アムダールの法則が示す限界に対し、実用的な並列処理の有効性を肯定した。

「十分に複雑なCやFortranのプログラムは、Common Lispの半分を粗悪に実装したものを含む」。

フィリップ・グリーンスパンが提唱した、プログラミング言語の表現力に関する皮肉。

言語自体が持つ抽象化能力の欠如が、再発明やバグを招くことを警告している。

未整列のデータベースから特定のデータを探索する、量子コンピュータ向けのアルゴリズム。

古典的な探索がN回必要なのに対し、√N回の試行で目的のデータを見つけ出せる。

量子状態の振幅を増幅させる手法を用いており、暗号解読などへの応用が期待される。

暗号系の安全性は、鍵以外のすべてが公表されても保たれるべきであるという原則。

アルゴリズムの秘匿に頼る「隠蔽によるセキュリティ」の危険性を警告している。

現代の暗号設計における最も基本的な指針の一つである。