理論計算機科学（りろんけいさんきかがく、英語：theoretical computer science）または理論コンピュータ科学は、計算機を理論的に研究する学問で、計算機科学の一分野である。計算機を数理モデル化して数学的に研究することを特徴としている[1][2][3]。「数学的」という言葉は広義には公理的に扱えるもの全てを指すので、理論計算機科学は広義の数学の一分野でもある。理論計算機科学では、現実のコンピュータを扱うことも多いが、チューリングマシンなどの計算モデルを扱うことも多い。

この分野のテーマの例を以下に挙げる（特に意図や理由のある選出ではない）。

計算理論：ある関数に対する計算の可能性や複雑性を追求する学問。

ラムダ計算：計算機のモデルの一つであるラムダ計算を研究する学問。

アルゴリズム論：ある関数に対する具体的な算法の考案、あるいは既存の算法の解析を行う学問。

プログラム意味論: プログラムあるいはプログラミング言語の形式意味論[4]

範囲

正確な研究範囲を述べるのは容易ではないが、ACM の Special Interest Group on Algorithms and Computation Theory（英語版） (SIGACT) は同グループの目的を理論計算機科学の振興であるとしており、その対象範囲を次のように定義している[5]。.mw-parser-output .templatequote{overflow:hidden;margin:1em 0;padding:0 40px}.mw-parser-output .templatequote .templatequotecite{line-height:1.5em;text-align:left;padding-left:1.6em;margin-top:0}アルゴリズム、データ構造、計算複雑性理論、並列計算、分散計算、probabilistic computation、量子計算、オートマトン理論、情報理論、暗号理論、プログラム意味論と検証、機械学習、計算生物学、computational economics、計算幾何学、computational number theory and algebra。

ACMの学術誌 Transactions on Computation Theory ではこの一覧にさらに符号理論と計算論的学習理論（英語版）を加え、データベース、情報検索、経済モデル、ネットワークなどの理論計算機科学的側面をも含めている[6]。このように範囲は広いが、計算機科学の理論畑の人間は応用畑とは違うという意識を持っていることがあり、「コンピューティングを支えている（より基本的な）科学」を研究しているという意識をもっていることがある[7]。これは必ずしも対立を意味するものではなく、むしろ協力関係にあることを意味する。

P → Q {\displaystyle P\rightarrow Q}
数理論理学オートマトン数論グラフ理論
Γ ⊢ x : I n t {\displaystyle \Gamma \vdash x:Int}
型理論圏論計算幾何学量子計算

歴史

アルゴリズムは何千年も前から存在していたが（例えば、2つの数の最大公約数を求めるユークリッドの互除法は今も使われている[8][9]）、計算におけるアルゴリズムの定義を定式化したのはアラン・チューリング、アロンゾ・チャーチ、スティーヴン・クリーネで、1938年のことである。一方、二進法と数学の形式体系はそれ以前からあり、ゴットフリート・ライプニッツが17世紀に二進法を数学的に定式化し、19世紀にジョージ・ブールがブール論理/ブール代数を定式化した。[10]論理的推論と数学的証明は古代から存在したが、1931年クルト・ゲーデルは自身の不完全性定理で、公理体系には証明できない限界が存在することを証明した。