(過去のメモを掘り返した、いつ書いたか不明)

3.5 評価

項の評価は項をある機械の状態を見なした時に、項から項への変換 つまり状態遷移と例えることができる。

\(t \to t'\)

推論規則のインスタンス

メタ変数を持った推論規則の変数に、 具体的な項を束縛することをいう。

例) 下記の式は推論規則のインスタンスである

if (if false then true else false) then true else false

反例) 下記の式は推論規則のインスタンスではない

if t then true else false

tはメタ変数であり具体的な項へと束縛されてないため。

定義 3.5.2

規則がある関係によって満たされるというのは、 規則の任意のインスタンスについて結論がその関係に属するか、 または前提のうちの一つが属さないことを言う。

用語の整理

規則 = t → t' のような形をした何か 評価関係 = 関係というのは何か解らないな。評価関係かな。

評価関係Eとは項の集合Tのtからt'へと導出可能であるような射の集合。

評価関係は規則の集まりであると考えることができる。

\(E = { (t, t) : t \to t' | t, t' \in T}\)

• 前提はEの始域t: dom(E)
• 結論はEの終域t': cod(E)

定理 3.5.4 1ステップ評価の決定性

評価関係が合成的であるという性質を示すための定理のようだけど、 E-IFの帰納的な証明が難しい。。。

二項演算と閉包について

関係とはある集合Aの直積集合A×Aの部分集合。

\(A = {0, 1, 2}\)

\(\lt \equiv {(1,0), (2,0), (2,1)}\)

\(\le \equiv {(1,0), (2,0), (2,1)}\)

4.1 構文

termは抽象構文木ノードとなる。 あれ、リーフは？

5.ラムダ計算

λ計算と同じ並びでπ計算やオブジェクト計算などの手法があるらしい。

ラムダ計算においては、すべてが関数である。つまり、関数によって受け付けられる引数はそれ自身関数であり、関数が返す結果もまた関数である。 (p.40)

ということは項と値という分類は存在しないことになる。 評価の停止性をどうやって判断するのだろう。

5.1 基礎

λ計算の構文はたった3つからなる。（なんてシンプル！）

t ::=
  x
  λx. t
  t t

抽象構文と具象構文

プログラミング言語には2つのレベルがある。

具象構文: プログラマが直接読み書きする文字列のことを指す。 抽象構文: プログラムのより単純な内部的表現であり、ラベル付き木(AST)として表現される。

具象構文から抽象構文への変換は、 字句解析と構文解析という2つのステップからなる。

結合規則

1. 関数適用は左結合とする。
2. 抽象は右結合とする。

閉じた項はコンビネータと呼ぶ。大概の場合閉じている気がするけど。