プログラミング言語で使われている無限長リストについて ChatGPT で調べてもなかなか一般的な理論は出てこないということがわかってきたので、何かを無限の場合に拡張するという方向で考えていきます。
『新装版 プログラミング言語の基礎理論』、『プログラミング言語の形式的意味論入門』、『型システム入門 プログラミング言語と型の理論』という本を買ったのでこの中から題材を選びたいと思います。
まず『新装版 プログラミング言語の基礎理論』の「2.4 Λの表示的意味論」を見ていきたいと思います。これはもともと有限の話ではないと思いますので「無限の場合」というのも変ですが、そのあたりを考えていきたいと思います。
『新装版 プログラミング言語の基礎理論』の目次
- 第1章 プログラミング言語のモデル
- 1.1 計算モデルの必要性
- 1.2 本書で使用する集合に関する記法
- 1.3 言語の文法構造の定義
- 1.4 型無しラムダ計算
- 第2章 型付きラムダ計算
- 2.1 定数と基底型の導入
- 2.2 単純な型付きラムダ計算Λの定義
- 2.3 de Bruijnインデックスと束縛変数に関する約束
- 2.4 Λの表示的意味論
- 2.5 Λの公理的意味論
- 2.6 公理的意味論の健全性と完全性
- 2.7 Λのモデル間の論理関係
- 2.8 Λの簡約システム
- 2.9 Λの操作的意味論
- 第3章 型付きラムダ計算の拡張
- 第4章 型推論システム
- 第5章 多相型言語のモデル
- 5.1 プログラムの汎用性の表現
- 5.2 多相型ラムダ計算Λ∀
- 5.3 Λ∀の表示的意味論
- 5.4 Λ∀の公理的意味論および簡約関係
- 5.5 種々のデータ構造の表現
- 5.6 MLの多相型システム
- 第6章 レコード計算系の理論
- 6.1 レコード計算系の登場の背景
- 6.2 サブタイプを含むレコード計算
- 6.3 多相型レコード計算
『プログラミング言語の形式的意味論入門』の目次
- 集合論の基礎
- 入門：操作的意味論
- 帰納法の原理
- 帰納的な定義
- ＩＭＰの表示的意味論
- ＩＭＰの公理的意味論
- ホーア規則の完全性
- 領域理論入門
- 再帰方程式
- 再帰の技法
- 高階型を持つ言語
- 情報システム
- 付録Ａ 不完全性と決定不能性
-
- 第1章 はじめに
- 第2章 数学的準備
- 第1部 型無しの計算体系
- 第3章 型無し算術式
- 第4章 算術式のML実装
- 第5章 型無しラムダ計算
- 第6章 項の名無し表現
- 第7章 ラムダ計算のML実装
- 第2部 単純型
- 第8章 型付き算術式
- 第9章 単純型付きラムダ計算
- 第10章 単純型のML実装
- 第11章 単純な拡張
- 第12章 正規化
- 第13章 参照
- 第14章 例外
- 第3部 部分型付け
- 第15章 部分型付け
- 第16章 部分型付けのメタ理論
- 第17章 部分型付けのML実装
- 第18章 事例：命令的オブジェクト
- 第19章 事例：Featherweight Java
- 第4部 再帰型
- 第5部 多相性
- 第6部 高階の型システム
- 第29章 型演算子とカインド
- 第30章 高階多相
- 第31章 高階部分型付け
- 第32章 事例：純粋関数的オブジェクト
- 付録A 演習の解答
- 付録B 記法
