taketoncheir.log

Like the Decatoncheir by Poseidon Industrial, This blog is Yet Another Storage for My Long Term Memories.

TaPL chap.3 ~ Untyped Arithmetic Expressions

未だ型のない世界。
型について語る前に、プログラミング言語について知っておくべき事柄がある。
ここではプログラムのシンタックスと意味論についての表現方法とその意味付けを学ぶ。

※以下、英単語をそのまま用いたところは訳語について悩むことを避けたところ

3.1 Intro

ひとつの簡単な言語を仮定する。
そのシンタックスは以下。

t ::=
true
false
if t then t else t
0
succ t
pred t
iszero t

標準BNFに近い表記。

  • (t ::=) は、これからterms(複数の項)を定義しますよ、ということを表している。
  • 下に列記されている中で現れるtは、他のtermに置き換え可能。このtをmetavariableと呼ぶ。
  • この段階ではtermとexpressionはほぼ同じ。chap.8以降はterm, type, kindによって構成されるのがexpression.

例えば、succ(succ(succ(0)))をevaluateしたら、3になる。
evaluateしきったtermを、values(値)と呼ぶ。

この段階では、succ trueとかif 0 then 0 else 0といった意味のない表現が可能。後のchapterでtype(型)を生み出すことにより、この存在を消すことができる。

3.2 Syntax

  • 3.2.1 Definition
    • あるtermの集合に属するtermとsyntaxから構成された表現は、そのtermに属するよ、ということかな
  • 3.2.2 Definition
    • 3.2.1を違う表現で書いてみた、と。

$\frac{t_{1} \in \tau}{succ \ t_{1} \in \tau}$
この場合、上段がpremiseで、そのpremiseが満たされていれば下段のconclusionが導き出せると。また、t_{1} \in \tauのように単体で表記されたものをaxiomと呼ぶ。

  • 3.2.3 Definition
    • termからなるSetを定義できるよ、と
  • 3.2.6 Proposition
    • \tau = Sなんだよ、と。

ここまでによって、自然数が導出できていることに留意。0は空集合なので特殊とありますが0は自然数かどうかとか自分よくわかってないです。

3.3 Induction on Terms

もしもt \in \tauなら以下の3つのうちどれかが言えるよ、と。

  • tはconstant
  • tはsucc t1, pred t1, iszero t1のどれかをもつ。t1はtより小さいterm.
  • tはif t1 then t2 else t3 をもつ。t1, t2, t3はtより小さいterm.
  • 3.3.1 Definition
    • あるterm tから導出したconstantはそのterm tに含まれる、と?よくわかってない。
  • 3.3.2 Definition
    • sizeとかdepthとか。abstract syntax treeのノード数がsize,深さがdepthに対応する?
  • 3.3.3 Lemma
    • |Consts(t)| <= size(t)だよ、と。
  • 3.3.4
    • わからにゃい。多分次回の勉強会で誰かが証明してくれるはず!

3.4 Semantic Styles

termをいかに評価(evaluate)するかについて正確な記述が必要だ。以下に3つあげる。

  • Operational semantics
  • Denotational semantics
    • termを数学的に見る。多分、関数によってどう状態が表現されうるのか、とか。
  • Axiomatic semantics
    • termを論理的な等式変換として見る。
  • 80年代の研究によって、数学的な操作を言語のオペレーションに落としこむ方法が確立されていった。
    • Structural Operational Semantics (1981, Plotkin)
    • Natural Semantics (1987, Kahn)
    • CCS (1980; 1989; 1999, Milner)

3.5 Evaluation

termをどう評価しようか。まずはbooleanに対するoperational semanticsを考えてみよう。
Syntaxとして2種類のexpressionを用意する。

t ::=
true
false
if t then t else t

v ::=
true
false

tはterms, vはvalues (a subset of terms)を表している。

termに対する評価関係 (evaluation relation) t -> t'を以下のように記述する。

  • if true then t2 else t3 -> t2 (E-IFTRUE)
  • if false then t2 else t3 -> t3 (E-IFFALSE)
  • $\frac{t_{1} -> \ t_{1}'}{if \ t_{1} \ then \ t_{2} \ else \ t_{3} -> \ if \ t_{1}' \ then \ t_{2}' \ else \ t_{3}'}$ (E-IF)

E-IFTRUEやE-IFFAlseはcomputation rule, E-IFはcongruence ruleと呼ばれる。その意味は、E-IFはガード条件の評価しか行わない、ということ。

  • 3.5.1,3.5.2 Definition
  • 3.5.3 Definition
    • one-step evaluationによって評価がひとつ進む。取りうる評価は先のE-IFTRUE, E-IFFALSE, E-IFのどれか。導出の過程はtreeになるけど、このtreeは枝を持たない。
  • 3.5.4 Theorem
    • if t -> t' and t -> t'' , then t' = t''
  • 3.5.6
    • これ以上評価できないtermを"normal form"と呼ぶ。
  • 3.5.7, 3.5.8 Theorem
    • すべてのvalueはnormal formだしnormal formはvalueだ。
    • でも一般的にはnormal formがvalueでないこともある。後述のstuck。これを検出するとrun-time errorを出すことができる。
  • 3.5.9 Definition
    • multi step evaluation (->*)もあるよ、と。
  • 3.5.11 Theorem
    • t ->* uとt ->* u'が成り立ってuとu'がnormal formなら、u = u'

以上の性質は、すべてのtermはvalueに評価できるという事を表しているが、これもまた一般的ではない。recursive functionではvalueにならない。Chap.12で停止性について議論を行う。

  • 3.5.12 Theorem
    • 全てのterm tについて t ->* t'を満たすnormal form t'が存在する

ここまで、booleanのみを考慮したtermについて評価を行なってきた。次にそれを算術式に拡張する。先ほどまでと異なり,succ tやpred tがtermとして追加されている。
ここで、pred 0 やsucc falseをどう扱うべきかという問題が生じる。
pred 0はevaluation ruleに pred 0 -> 0と定義されているので、0に落ちる。
しかし、succ falseはt -> t'となるt'が存在しないので、normal formでありながら値に落ちない。このようなtermをstuckと呼ぶ。

  • 3.5.15 Definition
    • normal formではあるが、valueでないものをstuckと呼ぶ

この”stuckness”はrun-timeエラーを引き起こすものとなる。

Types and Programming Languages

Types and Programming Languages