株式会社サイエンス社 株式会社新世社 株式会社数理工学社
ホーム 会社案内 社員募集 ご意見・ご感想 リンク 当サイトの利用  



ライブラリ 情報学 コア・テキスト 24

「プログラミング言語の基礎概念」

五十嵐淳(京都大学教授) 著

定価:1,998円(本体1,850円+税)
発行:サイエンス社
発行日:2011-07-25
ISBN 978-4-7819-1285-1 / A5判/192頁


<内容詳細>
関数型言語MLの一種Objective Camlを題材としてプログラミング言語の意味論,型システム,プログラミング言語の基礎概念,これらの概念間の数学的な関連を学ぶ.オンライン演習システムを用いて,「証明」を解答とする演習問題の正誤をWeb上で自動判定することもできる.

<目次>
第1部 導出システム入門
 第1章 自然数の加算・乗算・比較
  1.1 自然数の加算・乗算:導出システム Nat
  1.2 推論規則と導出の記法
  1.3 自然数の比較:導出システム ComparaNat1-3
  1.4 算術式の評価と簡約
 第2章 メタ定理と帰納法による証明
  2.1 メタ理論とメタ定理
  2.2 数学的帰納法
  2.3 構造帰納法
  2.4 帰納法による定義
  2.5 導出に関する帰納法
  2.6 整礎帰納法

第2部 MLの操作的意味論
 第3章 整数・真偽値式の評価
  3.1 ML1とその評価:導出システム EvalML1
  3.2 実行時エラー
 第4章 定義,変数束縛と環境
  4.1 letによる定義
  4.2 変数宣言の有効範囲
  4.3 let式の評価と環境
  4.4 導出システム EvalML2
 第5章 関数と再帰
  5.1 fun式と関数定義
  5.2 高階関数
  5.3 静的有効範囲と関数閉包
  5.4 導出システム EvalML3(その1)
  5.5 再帰的定義
  5.6 導出システム EvalML3(その2)
  5.7 EvalML3のメタ定理
 第6章 静的有効範囲と名前無し表現
  6.1 名前無し表現
  6.2 名前無し式への変換:導出システム NamelessML3
  6.3 名前無し式の評価:導出システム EvalNamelessML3
  6.4 名前無し表現に基づく評価の正しさ
 第7章 リストとパターンマッチング
  7.1 リスト
  7.2 導出システム EvalML4
  7.3 一般的なパターンマッチング
  7.4 導出システム EvalML5

第3部 MLの型システム
 第8章 単純型システム
  8.1 型
  8.2 型付け判断,型環境と型付け規則
  8.3 導出システム TypingML4
  8.4 型安全性
 第9章 多相的型システム
  9.1 単純な型システムの問題点
  9.2 多相的型システム
  9.3 let多相の型システム
  9.4 導出システム PolyTypingML4
  9.5 多相型システムの型安全性
 第10章 型推論
  10.1 型推論のためのアイデア
  10.2 型推論問題の定義と主要型
  10.3 方程式の抽出
  10.4 一階の単一化
  10.5 型推論アルゴリズムとその性質
  10.6 PolyTypingML4での型推論

さらに勉強したい人へ
索引