Chapter 1: ライフタイムの形式的理解

この章の目標

この章を読み終えると、以下のことが理解できるようになります：

Tofte-Talpin領域推論理論とRustライフタイムの関係
Variance（変性）の3種類とその意味
Higher-Ranked Trait Bounds（HRTBs）の理論と実践
ライフタイム制約の形式的な解法
他言語のメモリ管理アプローチとの比較

なぜ形式的理解が重要か

ライフタイムは「参照が有効な期間」という直感的理解だけでは不十分です。なぜなら：

コンパイラエラーの根本原因が分からない
複雑な状況での設計ができない
型システムの限界が見えない
他の関数型言語とのつながりが理解できない

形式的理解により、ライフタイムを数学的に操作できるようになります。

1. ライフタイムの数学的定義

1.1 ライフタイムとは何か

形式的定義：

ライフタイム α は、プログラムの実行における
時間区間の集合である。

α = {[start₁, end₁), [start₂, end₂), ...}

where startᵢ, endᵢ ∈ プログラムポイント

プログラムポイント（Program Point）は、コード中の各位置を表す抽象的な概念です。

具体例：

fn example() {
    let x = 5;        // ← P1: x の開始
    let r = &x;       // ← P2: r の開始
    println!("{}", r); // ← P3: r の使用
}                     // ← P4: スコープ終了

// 'x のライフタイム: [P1, P4)
// 'r のライフタイム: [P2, P4)

1.2 ライフタイムの包含関係（Outlives）

定義：

'a outlives 'b  ⟺  'a ⊇ 'b
記法: 'a: 'b

つまり、'aが有効な期間は'bが有効な期間を完全に包含する

Rustでの使用：

fn longer<'a, 'b>(x: &'a str, y: &'b str) -> &'a str
where
    'a: 'b,  // 'a outlives 'b
{
    if x.len() > y.len() {
        x
    } else {
        // yを返すには 'b: 'a も必要
        // ここでは型エラー
        // x
        x  // 'a のみ返せる
    }
}

視覚化：

時間軸 ──────────────────────────►

'a:      ┌──────────────────────────┐
         │                          │
'b:      │    ┌──────────┐          │
         │    │          │          │
         └────┴──────────┴──────────┘

'a: 'b が成立（'a は 'b を包含）

1.3 ライフタイムの代数的性質

ライフタイムは半順序集合（Partially Ordered Set）を形成します：

(Lifetimes, ⊇) は半順序集合

性質:
1. 反射律（Reflexivity）:  'a ⊇ 'a
2. 反対称律（Antisymmetry）: 'a ⊇ 'b ∧ 'b ⊇ 'a ⇒ 'a = 'b
3. 推移律（Transitivity）:  'a ⊇ 'b ∧ 'b ⊇ 'c ⇒ 'a ⊇ 'c

実用例：

fn chain<'a, 'b, 'c>(x: &'a i32) -> &'c i32
where
    'a: 'b,  // 'a outlives 'b
    'b: 'c,  // 'b outlives 'c
    // 推移律により 'a: 'c も成立
{
    x  // OK: &'a i32 は &'c i32 として使える
}

---

2. Tofte-Talpin領域推論理論

2.1 歴史的背景

Tofte-Talpin Region Inference（1994）は、関数型言語のメモリ管理のための理論です。

提案者: Mads Tofte と Jean-Pierre Talpin
目的: ガベージコレクションなしでメモリを自動管理
影響: Rustのライフタイムシステムの理論的基盤

2.2 領域ベース型システム

基本概念：

型 τ ::= int | bool | τ₁ → τ₂ | ref^ρ τ
                     領域注釈 ──┘

ρ: 領域（region）≈ Rustのライフタイム

領域（region）は、メモリの管理単位です。Rustのライフタイムは、領域の具体化です。

2.3 型付け規則

参照の生成：

Γ ⊢ e : τ    ρ fresh
─────────────────────  (REF)
Γ ⊢ ref e : ref^ρ τ

意味：

式 e が型 τ を持つ
新しい領域 ρ を割り当てる
ref e は領域 ρ の参照型を持つ

Rustでの対応：

let x = 5;        // e: i32
let r = &x;       // ref^'a x: &'a i32

参照の読み取り：

Γ ⊢ e : ref^ρ τ
────────────────  (DEREF)
Γ ⊢ !e : τ

Rustでの対応：

let x = 5;
let r = &x;       // r: &'a i32
let y = *r;       // y: i32

2.4 Rustへの適用

Tofte-Talpin理論は、以下のようにRustに適用されています：

Tofte-Talpin              Rust
────────────────────────────────────
領域（region）         →  ライフタイム（lifetime）
領域変数（ρ）          →  ライフタイム変数（'a）
領域推論              →  ライフタイム推論
領域注釈（ref^ρ τ）    →  参照型（&'a T）

---

3. Variance（変性）の理論

3.1 Varianceとは

定義: 型構築子がサブタイピング関係をどう扱うかの性質

Rustのライフタイムシステムでは、Varianceは安全性の要です。

3.2 3種類のVariance

┌─────────────────────────────────────────────────────────┐
│          Variance の3種類                                │
├─────────────────────────────────────────────────────────┤
│                                                         │
│  Covariant（共変）:                                      │
│  'a: 'b  ⟹  F<'a> <: F<'b>                            │
│  ライフタイムの順序を保つ                                 │
│  例: &'a T, *const T, Box<T>                            │
│                                                         │
│  Contravariant（反変）:                                  │
│  'a: 'b  ⟹  F<'b> <: F<'a>                            │
│  ライフタイムの順序を反転                                 │
│  例: fn(&'a T)                                          │
│                                                         │
│  Invariant（不変）:                                      │
│  サブタイピング関係なし                                  │
│  例: &'a mut T, Cell<T>                                 │
│                                                         │
└─────────────────────────────────────────────────────────┘

3.3 Covariant（共変）の詳細

定義：

'a: 'b  ⟹  &'a T <: &'b T

意味: 長いライフタイムの参照は、短いライフタイムの参照として使える

具体例：

fn covariant_example() {
    let s = String::from("hello");  // 's: 'static 相当の長いライフタイム

    {
        let r: &str = &s;  // r: &'short str
        // &'long str <: &'short str
        // OK: 長いライフタイムは短いライフタイムに縮められる
    }
}

fn explicit_covariant<'long, 'short>(x: &'long i32) -> &'short i32
where
    'long: 'short,  // 'long outlives 'short
{
    x  // OK: &'long i32 <: &'short i32
}

安全性の理由：

長いライフタイム → 短いライフタイムへの変換は安全

なぜなら、長く生きるものを短く扱う分には、
ダングリングポインタは発生しない

時間軸 ──────────────────────────►

'long:   ┌────────────────────────┐
         │                        │
'short:  │    ┌──────────┐        │
         │    │          │        │
         └────┴──────────┴────────┘
              ↑ この範囲で使用 → 安全

3.4 Contravariant（反変）の詳細

定義：

'a: 'b  ⟹  fn(&'b T) <: fn(&'a T)

意味: 関数の引数のライフタイムは反転する

具体例：

fn contravariant_example() {
    // 長いライフタイムを受け取る関数
    let f: fn(&'static str) = |s| println!("{}", s);

    // 短いライフタイムを受け取る関数型に代入
    let g: fn(&str) = f;
    // fn(&'static str) <: fn(&'a str)
    // OK: より長いライフタイムを受け取れる関数は、
    //     より短いライフタイムを受け取る関数として使える

    let local = String::from("local");
    g(&local);  // 短いライフタイムで呼び出してもOK
}

安全性の理由：

関数が長いライフタイムを要求 → 短いライフタイムで呼び出す

関数内部では、引数が長く生きると仮定しているが、
実際にはもっと長く生きるものを渡すので安全

呼び出し側:     'short の参照を渡す
関数の仮定:     'long の参照を要求（'short: 'long）
結果:          OK（実際には 'short > 'long なので安全）

3.5 Invariant（不変）の詳細

定義：

&'a mut T は invariant
サブタイピング関係なし

なぜInvariant？

もし &'a mut T がcovariantだったら：

// 危険な例（実際にはコンパイルエラー）
fn evil<'a>(short: &'a mut &'static str) {
    let local = String::from("local");

    // もし &'a mut T が covariant なら...
    // &'a mut &'a str <: &'a mut &'static str と仮定

    *short = &local;
    // 'a で終わる参照に、'short（'a より短い）を代入
    // → ダングリングポインタ！
}

形式的な証明：

仮定: &'a mut T が covariant
      'long: 'short とする

すると:
&'long mut &'long i32 <: &'short mut &'short i32

しかし、以下が可能になってしまう:
1. r: &'short mut &'short i32 を作る
2. r に &'long mut &'long i32 を代入（covariantなので）
3. *r に &'short i32 を代入
4. もとの &'long mut &'long i32 が &'short i32 を指す
5. 'short が終わってもアクセス可能 → ダングリングポインタ！

矛盾により、&'a mut T は covariant ではない

正しい例：

fn invariant_example<'a, 'b>(x: &'a mut i32, y: &'b mut i32) {
    // エラー: &'a mut i32 と &'b mut i32 は型が異なる
    // let z: &'a mut i32 = y;  // コンパイルエラー
}

3.6 Varianceの表

型	Variance	理由
`&'a T`	Covariant	読み取り専用、安全に縮められる
`&'a mut T`	Invariant	書き込み可能、サブタイピング不可
`*const T`	Covariant	生ポインタ、読み取り専用
`*mut T`	Invariant	生ポインタ、書き込み可能
`fn(&'a T)`	Contravariant	引数、より長く生きるものを受け入れ可
`fn() -> &'a T`	Covariant	戻り値、安全に縮められる
`Box`	Covariant	所有型、サブタイピング可
`Cell`	Invariant	内部可変性、サブタイピング不可

---

4. Higher-Ranked Trait Bounds（HRTBs）

4.1 HRTBsとは

定義: 全称量化されたライフタイムを持つトレイト境界

for<'a> F: Fn(&'a i32) -> &'a i32
│││││││
└─────┘ 全ての 'a について

4.2 必要性

問題: 通常のライフタイムでは表現できないケース

// これはダメ
fn apply<'a, F>(f: F, x: &'a i32) -> &'a i32
where
    F: Fn(&'a i32) -> &'a i32,
    //     ^^
    //     'a は関数シグネチャで固定されている
{
    f(x)
}

// これだと、apply を呼ぶ前に 'a を決めないといけない
// でも、異なるライフタイムで呼びたい

解決策: HRTBs

fn apply<F>(f: F, x: &i32) -> &i32
where
    F: for<'a> Fn(&'a i32) -> &'a i32,
    //  ^^^^^^^
    //  任意の 'a について成立
{
    f(x)
}

// 使用例
let identity = |x: &i32| x;
let result = apply(identity, &42);  // OK

4.3 形式的意味

型理論的表現：

∀ 'a. F: Fn(&'a i32) -> &'a i32

（任意のライフタイム'aについて、
  Fは&'a i32を受け取り&'a i32を返す関数）

これは多相型（Polymorphic Type）の一種です。

4.4 実践例

例1: クロージャを返す関数

// 間違い
fn returns_closure() -> Box<dyn Fn(&str) -> &str> {
    //                              ^^^^     ^^^^
    //                              ライフタイムが不明！
    Box::new(|x| x)
}

// 正しい: HRTBs使用
fn returns_closure() -> Box<dyn for<'a> Fn(&'a str) -> &'a str> {
    Box::new(|x| x)
}

例2: イテレータの変換

fn map_iter<I, F>(iter: I, f: F) -> impl Iterator<Item = &str>
where
    I: Iterator<Item = &str>,
    F: for<'a> Fn(&'a str) -> &'a str,
    //  ^^^^^^^ 任意のライフタイムで動作
{
    iter.map(f)
}

例3: 標準ライブラリの例

// Fn トレイトの実際の定義
pub trait Fn<Args>: FnMut<Args> {
    extern "rust-call" fn call(&self, args: Args) -> Self::Output;
}

// 使用例: Option::and_then
impl<T> Option<T> {
    pub fn and_then<U, F>(self, f: F) -> Option<U>
    where
        F: for<'a> FnOnce(&'a T) -> Option<U>,
        //  ^^^^^^^ HRTBs
    {
        // ...
    }
}

4.5 Early-bound vs Late-bound

Early-bound Lifetimes（早期束縛）:

fn foo<'a>(x: &'a i32) -> &'a i32 {
    //   ^^
    //   関数呼び出し時に決定
    x
}

// 呼び出し側で明示可能
foo::<'static>(&5);

Late-bound Lifetimes（遅延束縛）:

// HRTBで使用
fn bar(f: for<'a> fn(&'a i32)) {
    //        ^^^^^^^
    //        使用時に決定
}

// 内部で自動的にライフタイムが決まる

---

5. ライフタイム制約の解法

5.1 制約ベース推論

アルゴリズムの概要：

ステップ1: 各参照にライフタイム変数を割り当て
  let x = &y  ⟹  x: &'α T

ステップ2: 制約を生成
  - 代入:         x = y  ⟹  'α ⊇ 'β
  - 関数呼び出し: f(x)   ⟹  関数シグネチャから制約導出
  - スコープ:     { ... } ⟹  'α ⊆ スコープ

ステップ3: 制約を解く
  - 最小不動点を求める
  - 制約充足問題（CSP）として解く

ステップ4: 矛盾があればエラー

5.2 具体例

fn example() {
    let x = 5;        // 'x: [L1, L5)
    let y = 10;       // 'y: [L2, L5)
    let r = &x;       // 'r: [L3, L5)
    let s = &y;       // 's: [L4, L5)
    println!("{} {}", r, s);
}

// 制約:
// 'r ⊆ 'x  (r は x を借用)
// 's ⊆ 'y  (s は y を借用)
// 'r, 's は L5 まで有効

// 解:
// 'x = [L1, L5)
// 'y = [L2, L5)
// 'r = [L3, L5)
// 's = [L4, L5)

5.3 複雑な例

fn choose<'a>(x: &'a str, y: &'a str, flag: bool) -> &'a str {
    if flag { x } else { y }
}

fn main() {
    let s1 = String::from("hello");  // 's1
    let result;
    {
        let s2 = String::from("world");  // 's2 (shorter)
        result = choose(&s1, &s2, true);
        // 制約: 'a = 's1 ∩ 's2 = 's2
    }
    // println!("{}", result);  // エラー！'s2 は終了
}

制約解析：

choose の制約:
  'a ⊆ 's1
  'a ⊆ 's2
  result のライフタイム ⊆ 'a

解:
  'a = 's1 ∩ 's2 = 's2  (最小の共通期間)

しかし、result を 's2 より長く使おうとしている
→ コンパイルエラー

---

6. 他言語との比較

6.1 C/C++

C/C++:
- ライフタイムの概念なし
- 手動メモリ管理
- ダングリングポインタ可能

Rust:
- コンパイル時にライフタイムを検証
- 自動メモリ管理
- ダングリングポインタ不可能

C++の例：

int* dangle() {
    int x = 5;
    return &x;  // ダングリングポインタ！コンパイラは警告のみ
}

Rustの例：

fn dangle() -> &i32 {
    let x = 5;
    &x  // コンパイルエラー！
}

6.2 Haskell/OCaml

Haskell/OCaml:
- ガベージコレクション
- ライフタイムの概念不要
- 実行時オーバーヘッド

Rust:
- ライフタイムで静的管理
- ゼロコスト抽象化
- 実行時オーバーヘッドなし

6.3 他の線形型言語

ATS:

より強力な型システム（依存型）
学習曲線が急
実用性低い

Rust:

アフィン型（線形型の緩和）
実用性を重視
産業界で採用

---

7. ケーススタディ: Mozilla Firefox

7.1 実世界での応用

Mozillaは、Firefoxの並列レンダリングエンジンServoをRustで開発しました。

課題:

C++のUse-after-freeバグ
データ競合による不安定性
メモリリーク

解決策:

Rustのライフタイムシステムでコンパイル時に検証
所有権でメモリリーク防止
型システムでスレッド安全性保証

7.2 具体的な改善例

Before（C++）:

class Node {
    Node* parent;  // ダングリングポインタの可能性
};

After（Rust）:

struct Node<'a> {
    parent: Option<&'a Node<'a>>,
    // ライフタイムで親が子より長生きすることを保証
}

結果:

Use-after-freeバグがゼロ
データ競合がゼロ
メモリ安全性が証明される

---

まとめ

理論的基盤

Rustのライフタイムシステムは、以下に基づいています：

Tofte-Talpin領域推論: 領域ベースのメモリ管理
Variance: 型構築子のサブタイピング関係
HRTBs: 全称量化されたライフタイム
制約ベース推論: コンパイラが自動的に解決

実用的な意義

コンパイル時検証: 実行時エラーなし
ゼロコスト: 実行時オーバーヘッドなし
表現力: 複雑なパターンも表現可能
安全性: 数学的に証明された正しさ

次の章へ

次の章では、複数のライフタイムパラメータやライフタイム省略規則など、より実践的な複雑なライフタイム問題を学びます。

---

自己チェック問題

以下の質問に答えられるか確認してください：

問題1: 基本概念

ライフタイムの数学的定義を説明しなさい。

問題2: Outlives

'a: 'b の意味を、集合の包含関係で説明しなさい。

問題3: Tofte-Talpin

Tofte-Talpin理論とRustのライフタイムの対応を説明しなさい。

問題4: Variance

なぜ &'a mut T はinvariantなのか、反例を用いて説明しなさい。

問題5: Covariant

&'a T がcovariantである理由を、安全性の観点から説明しなさい。

問題6: Contravariant

関数引数のライフタイムがcontravariantである理由を説明しなさい。

問題7: HRTBs

for<'a> の意味を、全称量化の観点から説明しなさい。

問題8: 制約解法

以下のコードのライフタイム制約を書き出しなさい：

fn foo(x: &str, y: &str) -> &str {
    if x.len() > y.len() { x } else { y }
}

問題9: 他言語比較

Rustのライフタイムシステムと、C++/Haskellのメモリ管理の違いを説明しなさい。

問題10: 実世界応用

Mozillaがなぜ Servo を Rust で書いたのか、ライフタイムの観点から説明しなさい。

---

参考文献

Tofte, Mads, and Jean-Pierre Talpin. "Region-based memory management." Information and Computation 132.2 (1997): 109-176.
Weiss, Aaron, et al. "Oxide: The Essence of Rust." arXiv preprint arXiv:1903.00982 (2019).
Jung, Ralf, et al. "RustBelt: Securing the foundations of the Rust programming language." Proceedings of the ACM on Programming Languages 2.POPL (2017): 1-34.
Reed, Eric. "Patina: A formalization of the Rust programming language." University of Washington, Department of Computer Science and Engineering, Tech. Rep. UW-CSE-15-03-02 (2015).
The Rust Reference - Subtyping and Variance. https://doc.rust-lang.org/reference/subtyping.html
Rustonomicon - Subtyping and Variance. https://doc.rust-lang.org/nomicon/subtyping.html
Mozilla Research - Servo. https://servo.org/