Chapter 1: 所有権の理論的背景
この章の目標
この章を読み終えると、以下のことが理解できるようになります：
- アフィン型システムの理論とRustの所有権の関係
- 線形論理とCurry-Howard対応
- メモリ安全性の形式的保証（空間的・時間的・スレッド安全性）
- RAIIとMove Semanticsの理論的背景
- 所有権システムの設計原則と限界
- エラーメッセージの真の意味が分かる
- より高度なパターンを設計できる
- 他の関数型言語の概念とのつながりが見える
- なぜRustが「安全」と言えるのか証明できる
なぜ理論を学ぶのか
Rustの所有権システムは、単なる「便利な機能」ではなく、型理論と線形論理に基づく厳密な数学的基盤を持っています。この理論的背景を理解することで：
1. アフィン型システム（Affine Type System）
1.1 型システムの分類
プログラミング言語の型システムは、値の使用回数によって4つのレベルに分類できます：
┌─────────────────────────────────────────────────────────┐
│ 型システムの階層（使用回数の制約） │
├─────────────────────────────────────────────────────────┤
│ │
│ 線形型（Linear Types） │
│ - 値は正確に1回だけ使われる │
│ - 使用後は破棄必須 │
│ - 厳格すぎて実用的でない │
│ - 例: Clean言語のUniqueness Types │
│ │
│ アフィン型（Affine Types）← Rustはここ │
│ - 値は最大1回使われる（0回または1回） │
│ - 使用せずに破棄してもOK │
│ - 実用性と安全性のバランス │
│ - 例: Rust、Cyclone │
│ │
│ 関連型（Relevant Types） │
│ - 値は最低1回使われる（1回以上） │
│ - 未使用の変数はコンパイルエラー │
│ - 例: ATS │
│ │
│ 通常の型（Unrestricted Types） │
│ - 何回でも使える │
│ - 大半の言語はここ（C、Java、Python） │
│ │
└─────────────────────────────────────────────────────────┘
1.2 Rustのアフィン型の特徴
Rustはアフィン型を採用しています。これは以下を意味します：
// 値は最大1回使われる
let s1 = String::from("hello");
let s2 = s1; // s1からs2へムーブ（1回目の使用）
// let s3 = s1; // エラー！s1は既に使用済み（2回目は不可）
// 0回の使用もOK
let s = String::from("unused");
// sを使わずにドロップ → 問題なし
なぜアフィン型？
// 線形型だとこれはエラー
let x = 5;
// xを使わずに終了 → エラー
- アフィン型は実用的: 使わなくてもOK、でも2回は使えない
// アフィン型ではOK
let x = 5;
// xを使わなくてもドロップされるだけ
1.3 線形論理との関係
Rustの所有権システムは、線形論理（Linear Logic）に基づいています。
Curry-Howard対応
型理論とプログラミングには深い対応関係があります：
プログラム ←→ 証明
型 ←→ 命題
関数 ←→ 含意
この対応により、型システムで論理的な性質を表現できます。
線形論理の直感的理解
線形論理では、リソースの消費を扱います：
通常の論理:
A → B （Aが真ならBも真）
Aは何度でも使える
線形論理:
A ⊸ B （Aを消費してBを生成）
Aは一度しか使えない
Rustでの対応：
// 線形論理: A ⊸ B（Aを消費してBを生成）
fn consume(x: String) -> usize {
// ^^^^^^^^^
// Aを消費（型: String）
x.len() // Bを生成（型: usize）
} // xは消費され、もう使えない
// 呼び出し側
let s = String::from("hello");
let len = consume(s); // sを消費
// println!("{}", s); // エラー！sは消費済み
この対応により、Rustの型システムはメモリ安全性を論理的に証明できます。
2. メモリ安全性の形式的保証
2.1 保証される3つの安全性
Rustの所有権システムは、以下の3つの安全性をコンパイル時に形式的に保証します：
2.1.1 Spatial Safety（空間的安全性）
定義: メモリの範囲外アクセスを防ぐ
// 保証1: バッファオーバーフローなし
let arr = [1, 2, 3];
// arr[10]; // コンパイル時またはパニックで検出
// 保証2: ダングリングポインタなし
fn dangle() -> &i32 {
let x = 5;
&x // コンパイルエラー！
}
// error[E0515]: cannot return reference to local variable `x`
形式的保証：
∀ p: &T, ∀ t: Time,
valid(p, t) → ∃ obj: T, points_to(p, obj, t)
訳: 全ての参照pと時刻tについて、
pが有効ならば、pが指すオブジェクトが存在する
2.1.2 Temporal Safety（時間的安全性）
定義: 解放後のメモリアクセスを防ぐ
// 保証: Use-after-freeなし
let s = String::from("hello");
let r = &s;
drop(s); // sを明示的にドロップ
// println!("{}", r); // コンパイルエラー！
// error[E0505]: cannot move out of `s` because it is borrowed
形式的保証：
∀ p: &T, ∀ t1, t2: Time,
valid(p, t1) ∧ t2 > t1 → valid(object_of(p), t2)
訳: 参照pが時刻t1で有効なら、
時刻t2（t2 > t1）でもpが指すオブジェクトは有効
2.1.3 Thread Safety（スレッド安全性）
定義: データ競合を防ぐ
// 保証: データ競合なし
let mut data = vec![1, 2, 3];
let r1 = &data; // 不変参照
// let r2 = &mut data; // コンパイルエラー！
// error[E0502]: cannot borrow `data` as mutable because it is also borrowed as immutable
形式的保証：
∀ x: T, ∀ t: Time,
(∃! r: &mut T, borrows(r, x, t)) ∨ (∃ R: Set<&T>, ∀r ∈ R, borrows(r, x, t))
訳: 任意の値xと時刻tについて、
可変参照が1つ存在する、または、不変参照が複数存在する
（両方は同時に不可）
2.2 型理論的な保証
Rustの型システムは、以下の2つの重要な性質を満たします：
2.2.1 Subject Reduction（主辞簡約）
定義: 型付けされたプログラムは実行しても型を保つ
e: T ∧ e → e' ⇒ e': T
訳: 式eが型Tを持ち、eがe'に簡約されるなら、e'も型Tを持つ
Rustでの意味: 安全なコードは実行しても安全
fn process(s: String) -> String {
// sは型String
let s2 = s.to_uppercase();
// s2も型String（型は保たれる）
s2
}
2.2.2 Progress（進行性）
定義: 型付けされたプログラムは停止しないか値を返す
e: T ⇒ (e is value) ∨ (∃ e', e → e')
訳: 式eが型Tを持つなら、eは値であるか、さらに簡約できる
Rustでの意味: プログラムはpanicまたは正常終了する
fn main() {
let result = divide(10, 2); // 正常終了
// let result = divide(10, 0); // panic!（異常終了）
}
fn divide(a: i32, b: i32) -> i32 {
if b == 0 {
panic!("division by zero");
}
a / b
}
3. RAIIとMove Semanticsの理論
3.1 RAII（Resource Acquisition Is Initialization）
RAIIは、C++から継承した概念ですが、Rustではより強力です。
3.1.1 基本概念
struct File {
handle: FileHandle,
}
impl Drop for File {
fn drop(&mut self) {
// スコープを抜けると自動的に呼ばれる
self.handle.close();
println!("File closed");
}
}
// 使用例
{
let f = File::open("data.txt");
// fを使う
} // ここで自動的にdropが呼ばれる
3.1.2 RAII vs Rustの所有権
┌─────────────────────────────────────────────────────────┐
│ RAII vs Rustの所有権 │
├─────────────────────────────────────────────────────────┤
│ │
│ C++ RAII: │
│ ✓ デストラクタで自動クリーンアップ │
│ ✗ ダングリングポインタは防げない │
│ ✗ データ競合は防げない │
│ │
│ Rust所有権 + RAII: │
│ ✓ デストラクタで自動クリーンアップ │
│ ✓ ダングリングポインタもコンパイル時に防止 │
│ ✓ データ競合もコンパイル時に防止 │
│ │
│ → RAIIだけでは不十分、所有権で完全な安全性を実現 │
│ │
└─────────────────────────────────────────────────────────┘
3.2 Move Semanticsの理論
3.2.1 値カテゴリの分類
値（Value）
├─ lvalue（左辺値）
│ - 名前を持つ
│ - アドレスがある
│ - 例: 変数、参照
│
└─ rvalue（右辺値）
- 一時的
- アドレスがない
- 例: リテラル、関数の戻り値
3.2.2 Rustのムーブセマンティクス
let s1 = String::from("hello"); // s1 は lvalue
let s2 = s1; // s1 から s2 へムーブ
// s1 は使用不可に
// 理論的には:
// s1 の型: String
// s1 ムーブ後の型: ⊥（bottom type、使用不可）
Bottom Type（⊥）:
- 型理論における「到達不可能」を表す型
- ムーブ後の変数は実質的にbottom type
- これにより、コンパイラはムーブ後の使用を検出できる
4. 借用の型理論
4.1 参照の種類と型
4.1.1 不変参照（Shared Reference）
let s = String::from("hello");
let r1 = &s; // 型: &String
let r2 = &s; // 型: &String
// 複数の不変参照は共存可能
型理論的な解釈：
&T = 共有参照型
- 読み取り専用
- 複数同時に存在可能
- Aliasing: YES, Mutability: NO
4.1.2 可変参照（Mutable Reference）
let mut s = String::from("hello");
let r = &mut s; // 型: &mut String
// 可変参照は排他的
型理論的な解釈：
&mut T = 可変参照型
- 読み書き可能
- 排他的（1つのみ）
- Aliasing: NO, Mutability: YES
4.2 借用規則の形式化
4.2.1 Aliasing XOR Mutability
Rustの借用規則は、以下の論理式で形式化できます：
∀ 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); // 可変参照（内部的に）
// → vが再アロケートされる可能性
// println!("{}", r1); // r1はダングリングポインタに！
Rustはこのパターンをコンパイル時に拒否します：
error[E0502]: cannot borrow `v` as mutable because it is also borrowed as immutable
5. 歴史的コンテキスト
5.1 Rustより前の試み
5.1.1 Cyclone（2006）
Cycloneの例：
// Cycloneのリージョン
region r {
int *p = rmalloc(r, sizeof(int));
*p = 42;
} // rが破棄される
5.1.2 ATS（2008）
ATSの特徴：
5.1.3 Rust（2010-2015）
Rustの成功要因：
5.2 Rustの独自性
┌─────────────────────────────────────────────────────────┐
│ Rustと他の言語の比較 │
├─────────────────────────────────────────────────────────┤
│ │
│ C/C++: │
│ メモリ管理: 手動 │
│ 安全性: ✗ 実行時エラー │
│ 性能: ✓ 最高 │
│ │
│ Java/Go: │
│ メモリ管理: GC │
│ 安全性: ✓ GCが保証 │
│ 性能: △ GCオーバーヘッド │
│ │
│ Rust: │
│ メモリ管理: 所有権（コンパイル時） │
│ 安全性: ✓ コンパイル時に保証 │
│ 性能: ✓ ゼロコスト抽象化 │
│ │
│ → 「高速」「安全」「実用的」の三位一体 │
│ │
└─────────────────────────────────────────────────────────┘
6. 所有権システムの限界
6.1 表現できないパターン
6.1.1 自己参照構造体
struct SelfRef {
data: String,
ptr: &String, // エラー！ライフタイムが必要
}
// コンパイルエラー:
// error[E0106]: missing lifetime specifier
解決策: Pin で部分的に解決可能
use std::pin::Pin;
struct SelfRef {
data: String,
ptr: *const String, // 生ポインタ
}
// Pin<Box<SelfRef>> で固定
6.1.2 グラフ構造
struct Node {
value: i32,
children: Vec<Node>, // OK（所有）
parent: ???, // 親への参照が難しい
}
問題: 親と子が互いに参照し合う循環構造
解決策: Rc や RefCell で解決
use std::rc::Rc;
use std::cell::RefCell;
struct Node {
value: i32,
children: Vec<Rc<RefCell<Node>>>,
parent: Option<Rc<RefCell<Node>>>,
}
6.2 トレードオフ
6.2.1 学習曲線
課題:
対策:
6.2.2 表現力の制限
課題:
対策:
6.2.3 意図的な設計
これらの制限は意図的な設計です：
安全性 > 利便性
- デフォルトで安全
- unsafeで柔軟性を提供
- トレードオフを明示的に
まとめ
理論的な基盤
Rustの所有権システムは、以下の理論に基づいています：
実用的な保証
所有権システムは以下を保証します：
歴史的意義
Rustは、CycloneやATSの失敗から学び、実用性と安全性のバランスを実現しました。
限界と対策
所有権システムには限界がありますが、unsafe、Rc、RefCellなどで対処可能です。
次の章へ
次の章では、借用チェッカーの内部動作を詳しく見ていきます。コンパイラがどのように所有権を検証するのか、MIR、Non-Lexical Lifetimes、Poloniusなどの技術を学びます。
---