情報科学 › コンピュータサイエンス基礎 › プログラミング言語論
参照透過性
評価関係が決定的であり、式の評価結果が自由変数への束縛のみに依存し、評価が計算機の状態(変数の書き換え、入出力、時刻など)を変化させないとき、その言語は参照透過であるという。
閉包の状態
定義
定義は閉包の起点です(証明を要しません)。
印の意味: ✓公理まで証明済み ・ △証明あり(閉包未完)・ ※主張のみ。テーマごとの集計は 閉包の状況。
これを使っている定理 証明で参照している 1 件
- 共通部分式除去の健全性✓命題 6.4・プログラミング言語論