タイガーブックと等式推論
次、どうしようかなということでふらふらと彷徨っているシリーズ続行中です。言わずと知れたタイガーブック。特に脈絡もなく手に取って、眺めています。
15章の「関数型プログラミング言語」で、興味深い記述を見つけました。
純関数型（Pure functional）プログラミング言語とは、数学においてと同様に等式推論が機能するプログラミング言語のことである。
命令型（Imperative）プログラミングも類似の構文（引用者略）をもつ。しかし（引用者略）副作用（side effect）をもつかもしれないのだ。
等式推論（equational reasoning）という用語がいきなり出てきて、それによって関数型プログラミング言語を定義しているのが印象的でした。
等式推論、で検索してみると、CafeOBJに関して書かれたPDFが出てきます。そしてそこには等式推論の定義が載っています。
なんとなく想像はついていたものの、大体は想像通りの定義でした。ただ、条件付き等式というのがいまいちピンときません。
CafeOBJ 仕様の公理を構成する等式は，ceq l = r if c の形をしている.条件部 if c がない等式は，c = true の条件付き等式と同一視できる.
どういうことだろう、と思ってCafeOBJの本を引っ張り出してきます。
関係ないけど、このページ、全然検索で出てこないな。
ともかく、条件付き等式の話は24ページに見つかりました。
cq wPayWap(Hpay:Nat, WwHours:Nat) = WwHours + 60 * sd(WwHours,24) if WwHours > 24 cq wPayWap(Hpay:Nat, WwHours:Nat) = Hpay * WwHours if not(WwHours > 24)
なんとなくわかります。労働時間が24時間を超えるかどうかで払われる報酬が違うという関数の定義ですよね、たぶん。等式だけに比べれば、確かに表現力が桁違いですね。ここから書籍では項書換系の話になって、停止性や合流性について議論されます。
コンパイラの本を読んでいたのに、意外な方向に進みました。ひとまず今日はここまで。
