定理証明手習い(電子書籍のみ)

定理証明手習い(電子書籍のみ)

通常価格 ¥2,800(税込¥3,080) 特別価格

  • PDFのみの提供です(購入後すぐにダウンロードが可能です)

プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック

  • Daniel P. Friedman, Carl Eastlund 著、中野圭介 監訳
  • 240ページ
  • A5判
  • 電子書籍の形式:PDF
  • ISBN:978-4-908686-02-3
  • 2017年10月23日 第1版第1刷 発行
  • 正誤情報

あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。

なんだか難しそうに聞こえるかもしれませんが、その世界観を丁寧にときほぐして解説したのが、本書の原書にあたる "The Little Prover" です。

執筆者紹介

Daniel P.Friedman(原著者)

インディアナ大学計算機科学科教授。著書に“The Little Schemer (fourth edition)”( 邦題『Scheme手習い』)、“The Reasoned Schemer”、“The Seasoned Schemer” (邦題『Scheme 修行』)、“Essentials of Programming Languages (third edition)” (以上、The MIT Press)。

Carl Eastlund(原著者)

ソフトウェアエンジニア。Jane Street Capital(ニューヨーク)勤務。

中野圭介(監訳者)

東京大学理学部数学科中退。京都大学大学院理学研究科数学・数理解析専攻数理解析系博士後期課程単位取得退学。東京大学大学院情報理工学系研究科産学官連携研究員などを勤め、現在、電気通信大学大学院情報理工学研究科准教授。
証明支援系、関数型プログラミング、形式言語理論、双方向変換に関する研究に従事しつつ「ジグソーパズルによる関数型プログラミング」や「余帰納的にジャグリングをしよう(訳題)」など風変わりな論文も執筆。博士(理学)。

目次

  ((目次)
   (監訳者序文)
   (序文)
   (はじめに)
   (((1.いつものゲームに新しいルールを)) (例))
   (((2.もう少し、いつものゲームを)) (例))
   (((3.名前に何が?)) (証明))
   (((4.これが完全なる朝食)) (証明))
   (((5.何回も何回も何回も考えよう)) (証明))
   (((6.最後まで考え抜くのです)) (証明))
   (((7.びっくりスター!)) (証明))
   (((8.これがルールです)) (証明))
   (((9.ルールを変えるには)) (証明))
   (((10.いつかはスターで一直線)) (証明))
   ((A.放課後))
   ((B.デザートには証明を))
   ((C.小さなお手伝い))
   ((D.休んでなんていられない?))
   (あとがき)
   (索引))