BNFで定義したプログラムを自然演繹スタイルの推論規則として記述することができる。注意すべき点は実際には推論規則ではなく推論規則のスキーマ(C++的に言えばテンプレート)であるということ。実際にはメタ変数tには任意の項が入ってくる。 これらの構造に対する深さ、大きさなどを定義している。また、構造的な帰納法を定義している。
上の項（プログラムと言ってもいい）がどのような意味を持つかを定義する。ここでは抽象機械を想定して意味を考えていく。 まず、項の意味というのは最終的には値である。とりあえずbooleanを考えるならtrueとfalseが値である。項を値になるまで簡約 (reduction)していくのが評価 (evaluation)ということになるが、この本ではreductionのステップを評価と読んでいる。本の流儀に合わせて評価と呼ぶことにしよう。 ここでも自然演繹スタイルの推論規則として評価関係を考えている。数学的に言う関係とは、例えば2項関係であれば特定のs∈S, t∈Tに対してR(s, t)が言える時のRであった。要は「ある項tを持ってきて評価すると項t'になるよ」ってことだ。
- 定義3.5.2. 「規則が満たされる」というのは評価関係と評価規則との間での自明な間柄なのか?
- 定義3.5.3. 導出可能の意味がちょっとわかってない。