フォロー記事あり前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。 今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。 扱えるλ式の制限 面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいが…