プログラミング言語の基礎概念(本)
1
以下自然数とはほとんどの場合ペアノ自然数のことを指すとする
評価
式$ eが自然数$ nに評価されることを$ e \Downarrow nで表す
簡約
簡約，つまり式に規則を一回適応させること，が非決定的だと面倒（非決定的簡約） どの規則をどっから当てるんだよということになり困る
ここから当てましょうということをきちんと定める（決定的簡約） 式$ e_1が式$ e_2に非決定的に簡約されることを$ e_1 \to e_2で表す
式$ e_1が式$ e_2に決定的に簡約されることを$ e_1 \to_d e_2で表す
いくつかの非決定的簡約規則を式から自然数に弱化させることで決定的にしている
2
簡約についてのシステムReduceNatExpでは
簡約はいつか停止する，ある式はある自然数に必ず簡約される
簡約システムと評価システムは意味的に同じということが証明される
一旦2.4~2.5は後で