let valの公理

Call-By-Valueのlet束縛に関する公理、http://www.cs.bham.ac.uk/~pbl/papers/universalcbv.pdf より：

1. (let val x = x in M) ≡ M
2. (let val x = N in x) ≡ N (xはフレッシュ）
3. (let val x = M in (let val y = N in L)) ≡ (let val y = (let val x = M in N) in L) (xはフレッシュ）

明示的代入演算子だと：

1. M[x:=x] = M
2. x[x:=N] = N
3. L[y:=N][x:=M] = L[y:=N[x:=M]]

図式順だと：

1. [x>:x]M = M
2. [N>:x]x = N
3. [M>:x]( [N>:y] L) = [( [M>:x]N )>:y]L

to-thenだと：

1. x to x then M = M
2. N to x then x = N
3. M to x then (N to y then L) = (M to x then N) to y then L

to-then結合を >x; のように表すと：

1. x >x; M = M
2. N >x; x = N
3. M >x; (N >y; L) = (M >x; N) >y; L