TL;DR
- 「今やること」の項と「後でやること」の継続を分けて持つ抽象機械を使うと、ラムダ計算の評価を効率よく実現できる。
- Scala の cats-effect の
IOFiberは、このような抽象機械の形をしている。
内容
抽象機械
評価のたびに簡約する箇所を探すのはコストが高い。そこで、「今やること」とされる項（control string）と、「後でやること」を持つスタック（継続）を持ち、これらを組み替える機械（抽象機械）を考えるとよい。このような抽象機械を CK 機械と呼ぶことがある。プログラムの評価は、control string と継続を分け、次の 2 つを繰り返せば実現できる。
- control string を評価できなくなるまで分解する
- control string が評価できなくなったら（値になったら）、継続を切り崩す
環境
ラムダ計算には変数の概念があり、β 簡約のときに置換（代入）が行われる。代入をするには記憶が必要で、この記憶領域を環境と呼ぶ。左の部分木で置換が終わっていないのに右の部分木を評価し始めることがあるので、環境を機械のグローバルな状態として置くのは不適切である。そこで、環境を項に付与する。
cats-effect
cats-effect は Scala の非同期ランタイムのライブラリである。IO[A] は成功すると A の値を結果として返す。IOFiber[A] は IO[A] を評価する仮想マシンで、CEK 機械のような形になっている。この整理は Rust、F#、Kotlin の軽量スレッドを理解するのにも役立つ。ただし、それらの仕組みは、最適化のかかり方などが IOFiber と違う。