Chapter 1: 所有権の理論的背景
学習目標
- アフィン型システムの理論を理解する
- 線形論理と所有権の関係を学ぶ
- メモリ安全性の形式的証明を理解する
- 所有権がもたらす保証を深く理解する
- 歴史的な背景とRustの独自性を学ぶ
---
1.1 アフィン型システム（Affine Type System）
1.1.1 型システムの分類
┌─────────────────────────────────────────────────────────┐
│ 型システムの階層 │
├─────────────────────────────────────────────────────────┤
│ │
│ 線形型（Linear Types） │
│ - 値は正確に1回だけ使われる │
│ - 使用後は破棄必須 │
│ - 厳格すぎて実用的でない │
│ │
│ アフィン型（Affine Types）← Rustはここ │
│ - 値は最大1回使われる │
│ - 使用せずに破棄してもOK │
│ - 実用性と安全性のバランス │
│ │
│ 関連型（Relevant Types） │
│ - 値は最低1回使われる │
│ │
│ 通常の型（Unrestricted Types） │
│ - 何回でも使える │
│ - 大半の言語はここ │
│ │
└─────────────────────────────────────────────────────────┘
1.1.2 線形論理との関係
Curry-Howard対応：
プログラム ←→ 証明
型 ←→ 命題
線形論理の直感的理解：
// 線形論理: A ⊸ B（Aを消費してBを生成）
fn consume(x: String) -> usize {
// ^^^^^^^^^
// Aを消費
x.len() // Bを生成
} // xは消費され、もう使えない
// Rustの所有権はこれを型システムで強制
---
1.2 メモリ安全性の形式的保証
1.2.1 保証される性質
1. Spatial Safety（空間的安全性）
// 保証: バッファオーバーフローなし
let arr = [1, 2, 3];
// arr[10]; // コンパイル時またはパニック
// 保証: ダングリングポインタなし
fn dangle() -> &i32 {
let x = 5;
&x // コンパイルエラー
}
2. Temporal Safety（時間的安全性）
// 保証: Use-after-freeなし
let s = String::from("hello");
let r = &s;
drop(s);
// println!("{}", r); // コンパイルエラー
3. Thread Safety（スレッド安全性）
// 保証: データ競合なし
let mut data = vec![1, 2, 3];
let r1 = &data;
// let r2 = &mut data; // コンパイルエラー
1.2.2 型理論的な保証
Subject Reduction（主辞簡約）：
- 型付けされたプログラムは実行しても型を保つ
- Rustの場合：安全なコードは実行しても安全
Progress（進行性）：
- 型付けされたプログラムは停止しないか値を返す
- Rustの場合：panicまたは正常終了
---
1.3 所有権の設計原則
1.3.1 RAII（Resource Acquisition Is Initialization）
// C++から継承した概念
struct File {
handle: FileHandle,
}
impl Drop for File {
fn drop(&mut self) {
// スコープを抜けると自動的に呼ばれる
self.handle.close();
}
}
// 使用例
{
let f = File::open("data.txt");
// fを使う
} // ここで自動的にcloseが呼ばれる
RAII + 所有権 = 最強の組み合わせ：
┌─────────────────────────────────────────────────────────┐
│ RAII vs Rustの所有権 │
├─────────────────────────────────────────────────────────┤
│ │
│ C++ RAII: │
│ - デストラクタで自動クリーンアップ │
│ - しかしダングリングポインタは防げない │
│ │
│ Rust所有権 + RAII: │
│ - デストラクタで自動クリーンアップ │
│ - かつダングリングポインタもコンパイル時に防止 │
│ │
└─────────────────────────────────────────────────────────┘
1.3.2 Move Semantics の理論
値カテゴリの分類：
値（Value）
├─ lvalue（左辺値）: 名前を持つ、アドレスがある
│ 例: 変数
│
└─ rvalue（右辺値）: 一時的、アドレスがない
例: リテラル、関数の戻り値
Rustのムーブ：
let s1 = String::from("hello"); // s1 は lvalue
let s2 = s1; // s1 から s2 へムーブ
// s1 は使用不可に
// 理論的には:
// s1 の型: String
// s1 ムーブ後の型: ⊥（bottom type、使用不可）
---
1.4 借用の型理論
1.4.1 参照の種類と型
不変参照（Shared Reference）：
let s = String::from("hello");
let r1 = &s; // 型: &String
let r2 = &s; // 型: &String
// 複数の不変参照は共存可能
可変参照（Mutable Reference）：
let mut s = String::from("hello");
let r = &mut s; // 型: &mut String
// 可変参照は排他的
1.4.2 借用規則の形式化
Aliasing XOR Mutability：
∀ x: T,
(∃! r: &mut T, r points to x) ∨ (∃ R: Set<&T>, ∀r ∈ R, r points to x)
訳: 任意の値 x について、
- 可変参照が1つ存在する
または
- 不変参照が複数存在する
（両方は同時に不可）
なぜこれが重要か：
// もし両方が同時に存在したら
let mut v = vec![1, 2, 3];
let r1 = &v[0]; // 不変参照
v.push(4); // 可変参照（内部的に）
// r1 はダングリングポインタになる可能性
---
1.5 歴史的コンテキスト
1.5.1 Rustより前の試み
Cyclone（2006）：
- C言語に領域ベースのメモリ管理を追加
- 手動でリージョンを管理
- 複雑すぎて普及せず
ATS（2008）：
- 線形型と依存型を統合
- 非常に強力だが学習曲線が急
- アカデミックな成功
Rust（2010-2015）：
- アフィン型を採用
- エルゴノミクスを重視
- 産業界で採用される
1.5.2 Rustの独自性
┌─────────────────────────────────────────────────────────┐
│ Rustと他の言語の比較 │
├─────────────────────────────────────────────────────────┤
│ │
│ C/C++: │
│ - 手動メモリ管理 │
│ - 高速だが危険 │
│ │
│ Java/Go: │
│ - ガベージコレクション │
│ - 安全だが遅い │
│ │
│ Rust: │
│ - コンパイル時にメモリ安全性を検証 │
│ - 実行時オーバーヘッドなし │
│ - アフィン型システム │
│ │
│ → 「高速」「安全」「実用的」の三位一体 │
│ │
└─────────────────────────────────────────────────────────┘
---
1.6 所有権システムの限界
1.6.1 表現できないパターン
自己参照構造体：
struct SelfRef {
data: String,
ptr: &String, // エラー！ライフタイムが必要
}
// Pin<T> で部分的に解決可能
グラフ構造：
struct Node {
value: i32,
children: Vec<Node>, // OK
parent: ???, // 親への参照が難しい
}
// Rc<T> や RefCell<T> で解決
1.6.2 トレードオフ
学習曲線：
- 所有権の概念は初学者には難しい
- "fighting with the borrow checker"
表現力の制限：
- 一部のパターンは unsafe が必要
- GCなら簡単なコードが複雑になることも
しかし、これらは意図的な設計：
- 安全性を最優先
- unsafeで逃げ道を提供
- コミュニティが成熟したパターンを開発
---
1.7 まとめ
1.7.1 理論的な基盤
所有権システムは以下に基づく：
- アフィン型システム: 値は最大1回使用
- 線形論理: リソースの消費を型で表現
- RAII: スコープベースのリソース管理
- Move Semantics: 所有権の明示的な移動
- メモリ安全性（空間的・時間的）
- スレッド安全性
- ゼロコスト抽象化
- 予測可能なパフォーマンス
1.7.2 実用的な保証
1.7.3 次のステップ
次章では、借用チェッカーの内部動作を詳しく見ていきます。
---
練習問題
問題1
なぜRustはアフィン型を採用し、線形型を採用しなかったのか説明しなさい。問題2
以下のコードがコンパイルエラーになる理由を型理論の観点から説明しなさい。let s = String::from("hello");
let r1 = &s;
let r2 = &mut s;
---