ある日、ChatGPTとGeminiに以下の問題を投げました。

ChatGPTはログアウトした状態、Geminiはパーソナライズなしで行いました。

実際の問題↓

これは、自作言語のライフタイムに関する問題です。

はじめに

まず、変数・フィールドの集合$V$とライフタイム集合$Lt = V_{Lt} \cup G_{Lt} \cup X_{Lt}$があります。
$V_{Lt}$と$G_{Lt}$、$X_{Lt}$は以下の関係です

$V_{Lt} \cap G_{Lt} = \emptyset$
$G_{Lt} \cap X_{Lt} = \emptyset$
$X_{Lt} \cap V_{Lt} = \emptyset$

ここで、$\operatorname{lt}$関数と$\operatorname{ltime}$関数、$\operatorname{lref}$関数を導入します。それぞれ、

$\operatorname{lt}(v \in V)$：$v$のライフタイムの集合
$\operatorname{ltime}(l \in Lt)$：$l$のライフタイム有効点の集合
$\operatorname{lref}(l \in V_{Lt}^\complement) = \{ v \in V | \exists t \in \operatorname{lt}(v), t \cong l \}$

です。

この時、

$\forall v \in V, \forall l \in V_{Lt}, \exists t \in \operatorname{lt}(v), t \cong l \not\iff \operatorname{lref}(l) = \{ v \}$
$\forall l1, l2 \in V_{Lt}^\complement,$
$\operatorname{ltime}(l1) \subseteq \operatorname{ltime}(l2) \not\iff l1 \sqsubset l2 \lor l1 \sqsubseteq l2 \lor l1 \cong l2$
$\forall l1, l2 \in Lt,$
$l1, l2 \in G_{Lt} \lor l1, l2 \in X_{Lt} \not\Rightarrow \operatorname{lref}(l1) = \operatorname{lref}(l2)$

です。

ライフタイム規則

$Lt$の規則は以下のとおりです

$\forall v \in V, \forall l \in \operatorname{lt}(v) \Rightarrow \operatorname{ltime}(l) \subseteq \operatorname{scope}(v)$
　
$\forall v \in V, \forall l1 \in V_{Lt}^\complement, \exists l2 \in \operatorname{lt}(v),$
$l1 \sqsubset l2 \lor l1 \sqsubseteq l2 \Rightarrow \operatorname{ltime}(l1) \subseteq \operatorname{ltime}(l2)$
　
$\forall v1, v2 \in V, \exists l1 \in \operatorname{lt}(v1), \exists l2 \in \operatorname{lt}(v2),$
$\operatorname{pointer}(v1) = \operatorname{pointer}(v2) \Rightarrow l1 \cong l2$
　
$\forall l1, l2 \in V_{Lt}^\complement,$
$l1, l2 \in G_{Lt} \lor l1, l2 \in X_{Lt} \land \operatorname{lref}(l1) = \operatorname{lref}(l2) \Rightarrow l1 \sqsubseteq l2$
$l1, l2 \in G_{Lt} \lor l1, l2 \in X_{Lt} \land \operatorname{lref}(l1) \neq \operatorname{lref}(l2) \Rightarrow l1 \not\sqsubseteq l2$
$l1 \in G_{Lt} \land l2 \in X_{Lt} \land \operatorname{lref}(l1) = \operatorname{lref}(l2) \Rightarrow l1 \sqsubset l2$
$l1 \in G_{Lt} \land l2 \in X_{Lt} \land \operatorname{lref}(l1) \neq \operatorname{lref}(l2) \Rightarrow l1 \not\sqsubset l2$
　
$\forall l1, l2 \in G_{Lt} \Rightarrow \emptyset \subseteq \operatorname{ltime}(l1) \cap \operatorname{ltime}(l2)$
　
$\forall l1 \in V_{Lt}^\complement, \forall l2 \in X_{Lt},$
$l1 \sqsubset l2 \lor l1 \sqsubseteq l2 \Rightarrow \operatorname{ltime}(l1) \cap \operatorname{ltime}(l2) = \emptyset$
$\text{otherwise} \Rightarrow \emptyset \subseteq \operatorname{ltime}(l1) \cap \operatorname{ltime}(l2)$

問題

以上のライフタイムの基、以下のような未知の言語をコンパイルできるかできないかを判定しなさい。

ただし、所有者のライフタイムは$V_{Lt}$と、不変借用は$G_{Lt}$と、可変借用は$X_{Lt}$と対応し、不変借用のライフタイムは'a、可変借用のライフタイムは^aとなる。また、$\operatorname{lref}$関数の値を明示すること。

(1)

struct Point2<^a, 'b> {
    pub x: PointX<^a>,
    pub y: PointY<'b>,
}

fn main() {
    let mut p = Point2::new();
    let px_m = &mut p.x;
    let py_im = &p.y;

    do_something(px_m);
    do_something2(py_im);
}

(2)

struct Point3<^a, 'b> {
    pub x: PointX<^a>,
    pub y: PointY<^a>,
    pub z: PointZ<'b>,
}

fn main() {
    let mut p = Point3::new();
    let px_m = &mut p.x;
    let py_im = &p.y;
    let pz_im = &p.z;

    do_something(px_m);
    do_something2(py_im);
    do_something3(pz_im);
}

解答

(1)解答例

コードから、$V = \{ p, p.x, p.y, px_m, py_{im} \}$であることがわかります。

今回は規則1と2を満たしているので、これについては言及しません。また、規則5も不変借用が1つしか登場していないため、適用されません。

規則3より、$p.x$と$px_m$、$p.y$と$py_{im}$それぞれのライフタイムは同じものとしてみなせます（ライフタイムの期間は異なります）。

よって、$px_m$のライフタイムを$l_x$、$py_{im}$を$l_y$とすると、それぞれ

$\operatorname{lref}(l_x) = \{ p, p.x \}$
$\operatorname{lref}(l_y) = \{ p, p.y \}$

となります。

そして、規則4より、$l_y \not\sqsubset l_x$、また$l_y \not\sqsubseteq l_x$です。

従って、規則6から(1)のコードはコンパイル可能です。

(2)解答例

コードから、$V = \{ p, p.x, p.y, p.z, px_m, py_{im}, pz_{im} \}$であることがわかります。

今回は規則1と2を満たしているので、これについては言及しません。また、規則5も不変借用が1つしか登場していないため、適用されません。

規則3より、$p.x$と$px_m$、$p.y$と$py_{im}$、$p.z$と$pz_{im}$それぞれのライフタイムは同じものとしてみなせます（ライフタイムの期間は異なります）。

よって、$px_m$のライフタイムを$l_x$、$py_{im}$を$l_y$、$pz_{im}$を$l_z$とすると、それぞれ

$\operatorname{lref}(l_x) = \{ p, p.x, p.y \}$
$\operatorname{lref}(l_y) = \{ p, p.x, p.y \}$
$\operatorname{lref}(l_z) = \{ p, p.z \}$

となります。

そして、規則4より、$l_y \sqsubset l_x$, $l_z \not\sqsubset l_x$, $l_z \not\sqsubseteq l_y$、また$l_z \not\sqsubseteq l_x$です。

$l_y \sqsubset l_x$であるから、規則6より(2)のコードはコンパイル不可能です。

ここからは、ChatGPTとGeminiの解答を載せます。まず、Geminiです。

Geminiの解答

ご提示いただいた定義・規則に基づき、(1) と (2) のプログラムがコンパイル可能かどうか、および各ライフタイムにおける $\operatorname{lref}$ の値を解析して判定します。

(1) の判定

1. $\operatorname{lref}$ 関数の値

px_m (&mut p.x) のライフタイム $l_{px} \in X_{Lt}$
$\operatorname{lref}(l_{px}) = { p.x }$
py_im (&p.y) のライフタイム $l_{py} \in G_{Lt}$
$\operatorname{lref}(l_{py}) = { p.y }$

2. コンパイル判定：コンパイル可能

理由

構造体 Point2<^a, 'b> では、x の可変借用用ライフタイム ^a と y の不変借用用ライフタイム 'b が完全に関係付けられておらず独立しています。
規則より、$\operatorname{lref}(l_{py}) = { p.y }$ と $\operatorname{lref}(l_{px}) = { p.x }$ は等しくありません（$\operatorname{lref}(l_{py}) \neq \operatorname{lref}(l_{px})$）。
異なる変数・フィールドを参照しているため、$l_{py} \in G_{Lt}$ と $l_{px} \in X_{Lt}$ の間に包含関係（$l_{py} \sqsubset l_{px}$）は成り立ちません（規則：$\operatorname{lref}(l1) \neq \operatorname{lref}(l2) \implies l1 \not\sqsubset l2$）。
したがって、$\operatorname{ltime}(l_{py}) \cap \operatorname{ltime}(l_{px}) = \emptyset$（有効期間の排他）が要求されず、px_m と py_im の有効期間がオーバーラップしても矛盾は生じません。

(2) の判定

1. $\operatorname{lref}$ 関数の値

px_m (&mut p.x) のライフタイム $l_{px} \in X_{Lt}$
$\operatorname{lref}(l_{px}) = { p.x }$
py_im (&p.y) のライフタイム $l_{py} \in G_{Lt}$
フィールド y は型定義上、可変借用ライフタイム ^a を要求されています。
この共有ライフタイム ^a は x と y の両方に紐づいているため、^a の参照集合は $\operatorname{lref}(^a) = { p.x, p.y }$ となります。
したがって、py_im が紐づく不変借用ライフタイム $l_{py}$ において、参照先集合は $p.y$ だけでなく ^a を通じて $p.x$ と干渉することになります。
pz_im (&p.z) のライフタイム $l_{pz} \in G_{Lt}$
$\operatorname{lref}(l_{pz}) = { p.z }$

2. コンパイル判定：コンパイル不可（エラー）

理由

構造体 Point3<^a, 'b> では、x と y の両方が**同じ可変借用ライフタイム ^a** を共有しています。
これにより、ライフタイム ^a の参照先集合 $\operatorname{lref}(^a)$ は ${ p.x, p.y }$ と定義されます。
let py_im = &p.y; で不変借用 $l_{py} \in G_{Lt}$ を作ろうとした際、$l_{py}$ と `^a \in X_{Lt}$ が同じオブジェクト構造を介して干渉します（$\operatorname{lref}(l_{py}) \cap \operatorname{lref}(^a) \neq \emptyset$）。
規則「$l1 \in G_{Lt} \land l2 \in X_{Lt} \land \operatorname{lref}(l1) = \operatorname{lref}(l2) \Rightarrow l1 \sqsubset l2$」および「$l1 \sqsubset l2 \Rightarrow \operatorname{ltime}(l1) \cap \operatorname{ltime}(l2) = \emptyset$」が適用されます。
つまり、x の可変借用（px_m）の生存期間と y の不変借用（py_im）の生存期間は積集合が空集合（＝同時に存在してはならない）にならなければなりません。
main 関数内では do_something(px_m) と do_something2(py_im) が順に実行されており、px_m と py_im の生存期間（$\operatorname{ltime}$）が重なっているため、規則違反となってコンパイルエラーとなります。

まとめ

問題	判定	補足
(1)	コンパイル可能	フィールド `x` と `y` のライフタイムパラメータが独立しているため。
(2)	コンパイル不可	`x` と `y` が同一の可変ライフタイム `^a` を共有しているため、不変借用と可変借用の生存期間が衝突する。

次に、ChatGPTです。

ChatGPTの解答

まず結論から言うと、あなたが定義した規則だけを見る限りでは、この2つはどちらもコンパイル可能と判定できます。

ただし、その理由は lref がどのように定義されるか と ^a と 'a が同じ所有者を指しているか に依存します。以下で順番に確認します。

まず `lref` を求める

(1)

struct Point2<^a, 'b> {
    x: PointX<^a>,
    y: PointY<'b>,
}

所有者は

p
 ├── x
 └── y

だけです。

借用は

px_m = &mut p.x
py_im = &p.y

なので

lref(^a) = { x }
lref('b) = { y }

となります。

(2)

struct Point3<^a, 'b> {
    x: PointX<^a>,
    y: PointY<^a>,
    z: PointZ<'b>,
}

今度は

x
y

が同じライフタイム ^a を持っています。

したがって

lref(^a) = { x, y }
lref('b) = { z }

になります。

(1) の判定

可変借用

px_m

は

^a

不変借用

py_im

は

'b

です。

ここで

lref(^a) = {x}
lref('b) = {y}

なので

lref(^a) ≠ lref('b)

です。

あなたの規則では

l1 ∈ G
l2 ∈ X
lref(l1) ≠ lref(l2)
⇒ l1 ⊄ l2

つまり

'b

と

^a

の間に包含関係はありません。

すると最後の規則

otherwise
⇒ ltime(l1)∩ltime(l2) ≠ ∅

が適用されます。

つまり

^a

と

'b

は同時に存在できます。

したがって

(1) はコンパイル可能

になります。

(2) の判定

ここでは

x : ^a
y : ^a
z : 'b

です。

したがって

lref(^a) = {x,y}
lref('b) = {z}

です。

やはり

lref(^a) ≠ lref('b)

です。

従って

'b

と

^a

は包含関係を持ちません。

最後の規則より

ltime(^a)∩ltime('b) ≠ ∅

なので、

&mut x

と

&z

は共存できます。

問題になるのは

&y

ですが、

実際には

py_im : &p.y

は

^a

ではなく

'b

です。

つまり

x → ^a
y → ^a

はフィールド自身の所有ライフタイムであり、

&p.y

という借用のライフタイムは

'b

になります。

したがって

px_m : ^a
py_im : 'b

となり、

lref(^a) = {x,y}
lref('b) = {z}

なので依然として

lref(^a) ≠ lref('b)

です。

従って

(2) もコンパイル可能

となります。

Rust と違う点

Rust が禁止するケースは

let px = &mut p.x;
let py = &p.y;

のように同じ構造体 p 全体に対する借用を保守的に扱う場合ですが、

あなたの体系では

lref(^a)

が

{x}

や

{x,y}

のように参照先フィールド集合で区別されます。

つまり

と

の lref が異なる限り、

&mut x

と

&y

は衝突しません。

これは Rust よりフィールド単位で細かく借用解析を行う体系になっています。

最終結果

問題	`lref`	判定
(1)	`lref(^a)={x}`, `lref('b)={y}`	コンパイル可能
(2)	`lref(^a)={x,y}`, `lref('b)={z}`	コンパイル可能

なお、もしあなたの意図が「Point3<^a, 'b> の y に対する &p.y も ^a に属する借用である」という設計であれば、py_im のライフタイムの扱いが変わるため、(2) の判定も変わる可能性があります。その場合は、「借用式 &field のライフタイムが、フィールドに付与されたライフタイム引数からどのように決定されるのか」を明示すると、判定をより厳密に行えます。

総評

Geminiは、個人的に「少し危なかったな」と思う部分がありましたが、答えへと導けていました。

しかし、ChatGPTは、(2)にてpx_m (py_im)とpz_imを比較し、px_mとpy_imを比較していませんでした。それができていれば正しく答えを導けていたはずです。

また、複数回試してもGeminiは安定して解答し、ChatGPTは正解こそしましたが、わけのわからない説明でした。

（あと普通にGeminiは解答だけ、ChatGPTは要らんことまで言う...）

終わりに

広く使われているChatGPTとGeminiですが、ここまで差が出るのですね。

「質問に対する答えの質ではGeminiがいいのでは」と考えます（別に「Geminiを使え」とは言いません）。¹

私はQwen推しなので... ↩