#eval は式の評価ではない。実行を伴う

[Seasawher]

そう。

#eval は見た目こそ「式を評価している」ように見えるけど、実際には普通の項の簡約（β簡約やδ簡約）とは別物だ。

例えば

#eval 2 + 3

は 5 を表示する。

しかしこれは

#check 2 + 3

のようにカーネル内で式を扱っているのとは違い、Lean のコンパイラとランタイムを使って実際にコードを実行している。

特に

#eval IO.rand

が動くことからもわかる。

もし #eval が単なる関数評価なら、

IO.rand : IO Nat

は Nat に評価できない。

実際には

1. IO.rand という IO Nat の値を作る
2. Lean のランタイムがその IO アクションを実行する
3. 得られた Nat を表示する

という処理をしている。

⸻

逆に、カーネルが行う「普通の評価」は

#reduce (fun x => x + 1) 3

みたいなもの。

#reduce IO.rand

をやっても乱数は出ない。

なぜなら #reduce は外界と相互作用しない純粋な簡約しか行わないから。

⸻

極端に言うと、

#eval e

は

Leanプログラムをコンパイル
↓
実行
↓
結果を表示

に近い。

一方

#reduce e

は

式そのものを数学的に簡約

に近い。

だから

Lean では #eval で即実行できるけど、普通の関数評価とは違うことをしているんやね

その理解で正しい。#eval は「項の評価」というより「Lean の実行系にその項を走らせている」操作だ。Haskell で言えば GHCi が main を実行しているのに近い。

[Seasawher]

このスレッドで整理されたポイントは次のようになる。

1. IO.rand 自体は純粋な値

IO.rand : IO Nat

は「乱数を生成する計算」を表す値であって、まだ乱数は生成されていない。

したがって

def x := IO.rand
def y := IO.rand

のような定義は純粋な項として扱える。

⸻

2. 問題は「IOアクションの実行」

ユーザーの指摘：

IO.rand は純粋かもしれないけど、IOアクションを実行して値を取り出す操作は参照透明じゃないだろ？

これは本質的に正しい。

例えば

do
let x ← IO.rand
pure x

を2回実行すると結果が変わる可能性がある。

したがって、

let x ← IO.rand

で実際に乱数を得る行為は、普通の純粋関数の評価とは違う。

⸻

3. なぜそれで純粋性が壊れないのか

重要なのは、

Lean の純粋な世界では IO アクションは「実行」されない

ということ。

Lean の項としては

let x ← IO.rand
...

も結局は

IO.rand >>= fun x =>
...

という IO プログラムの構築でしかない。

つまり Lean の式は

• 計算を記述する
• その計算を実行しない

⸻

4. 「IOアクションの実行」は関数評価ではない

議論の途中で出てきた整理：

「IOアクションを実行する行為」は参照透明ではないけど、IOアクションを実行するのは関数評価じゃないからOK？

答えは概ね Yes。

Lean が保証する参照透明性は

• 項の構築
• 項の簡約
• 定理証明

に対するもの。

一方で

OS
↓
Leanランタイム
↓
IOプログラム実行

は Lean の純粋な計算体系の外側にある。

⸻

5. #eval は普通の評価ではない

ここが一番誤解されやすい点。

例えば

#eval IO.rand

は動く。

しかし

#reduce IO.rand

では乱数は出ない。

なぜなら

#reduce

純粋な式の簡約

(fun x => x + 1) 3

↓

4

を行うだけ。

⸻

#eval

実際には

Leanコード
↓
コンパイル
↓
ランタイム実行
↓
結果表示

を行っている。

つまり #eval は

Lean の項を数学的に簡約する

のではなく

Lean の実行系にそのプログラムを走らせる

操作。

⸻

6. 最終的な理解

Lean の世界には二層ある。

純粋な層

Nat
List Nat
IO Nat

などの項を扱う世界。

ここでは参照透明性が成立する。

⸻

実行の層

#eval
main

などで IO アクションを実際に走らせる世界。

ここでは

• 乱数
• ファイル
• ネットワーク
• 時刻

など外界との相互作用が起きる。

当然参照透明ではない。

⸻

要するに、

IO は参照透明性を保ちながら「非参照透明な実行」を記述するためのデータ型であり、実際の非参照透明性は Lean の純粋な計算体系の外側（ランタイム）に押し出されている。

というのがこのスレッドの結論。