論理と計算のしくみ

命題論理・述語論理など形式論理の基礎を学んだあと,ゲーデル不完全性やラムダ計算について学習する.

論理と計算のしくみ
このエントリーをはてなブックマークに追加
著者 萩谷 昌己 , 西崎 真也
ジャンル 書籍 > 自然科学書
刊行日 2007/06/27
ISBN 9784000061919
Cコード 3055
体裁 A5 ・ 上製 ・ カバー ・ 270頁
在庫 品切れ
論理と計算の概念は,いまでは計算機科学の基盤となっている.本書は,命題論理や述語論理,そして様相論理など形式論理の基礎を学んだあと,ゲーデル不完全性定理を通して「計算」の意味を理解する.さらに計算モデルの典型であるラムダ計算について学習し,論理と計算の関係だけでなく,両者をつなぐ「仕組み」を理解する.

■著者からのメッセージ

形式論理とは,古来から数学に現れる演繹の過程を,記号に対する操作として定式化した形式体系である.(中略)
 計算機科学においても形式論理は,計算機の機能や性質,計算機に関連する様々な現象を的確に表現するための枠組を与えてくれる.命題論理と述語論理は,そのための最も基本的な形式論理である.(中略)
 これらの形式論理が計算機科学にとって重要である理由の一つは,これらが構文論と意味論の区別と関係について学ぶためのモデルケースになっているからである.構文論は,論理式がどのような記号からどのような文法によって作られるかを与える.(略)これに対し意味論は,そのような論理式が何を意味するのかを数学的に厳密に定義する.そして,構文論と意味論をつなぐ概念として健全性と完全性がある.(略)
  形式論理だけでなく,自然言語やプログラミング言語も含む,およそどのような言語も,構文論と意味論の二つの側面を有している.言語に関して議論する際には,これらの二つの側面を明確に区別することが重要である.計算機科学,特にソフトウェア科学の主役であるプログラミング言語や仕様記述言語も例外ではない.特に,プログラミング言語の意味論を定義することは,ソフトウェア科学の中心的課題の一つであり続けている.命題論理と述語論理を通して,構文論と意味論の区別,それらの間の関係について学ぶことは決して無駄にはならない.
(本書「学習の手引き」より一部抜粋)
はしがき
  学習の手引き

第1章 集合と関係
  §1.1 集合
  §1.2 関係

第2章 命題論理と述語論理
  §2.1 命題論理
  §2.2 一階述語論理
  §2.3 高階述語論理とその部分体系

第3章 様相論理と直観主義論理
  §3.1 命題様相論理
  §3.2 多重様相論理
  §3.3 時相論理
  §3.4 命題直観主義論理

第4章 計算可能性
  §4.1 チューリング機械
  §4.2 帰納的関数
  §4.3 不完全性定理
  §4.4 プレスバーガ算術
  §4.5 述語論理の決定不能性と決定可能な部分体系

第5章 λ計算
  §5.1 λ項
  §5.2 簡約
  §5.3 型付きλ計算
萩谷昌己(はぎや まさみ)
1957年生まれ.1980年東京大学理学部情報科学科卒.京都大学数理解析研究所助手,助教授を経て,1992年より東京大学理学部情報科学科助教授,教授.2001年より組織変更により,東京大学大学院情報理工学研究科教授,現在に至る.
著書に,『ソフトウェア科学のための論理学』(岩波講座ソフトウェア科学),『論理と計算』(岩波講座応用数学),他多数.
西崎真也(にしざき しんや)
1967年生まれ.1994年京都大学大学院理学研究科数理解析専攻博士課程修了.理学博士.岡山大学工学部情報工学科,千葉大学理学部数学・数理情報学科を経て,現在,東京工業大学大学院情報理工学研究科計算機工学専攻助教授.専門は,プログラミング理論,ソフトウェア検証など.

受賞情報

第17回大川出版賞(2008年)
ページトップへ戻る