情報は力ではない

VimとかC++とかCUDAとか。

TaPL

TaPL 演習4.2.2

問題 arithの実装におけるeval関数の定義を、大ステップスタイルに変えよ。 答案 もう少しうまく書きたい。 let rec eval1' t = try match t with TmIf(_, t1, t2, t3) -> ( let t1' = eval1'(t1) in match t1' with TmTrue(_) -> let v2 = eval1'(t2) in v2…

TaPL 演習3.5.14

問題 定理3.5.4が算術演算の評価関係に関しても成り立つことを示せ。 すなわち、 かつ ならば であることを示せ。 証明 の導出に関する帰納法を使用し、 の導出で最後に使った規則に対する場合分けにより証明する。 E-SUCCの場合 は という形であり、またあ…