TAPL 読書会@東京 第3回 - tokyotaplreading @ ウィキ

第三回

beamer
(TeX のパッケージ)

5.3.7
Exercise 3.5.16 gave an alternative presentation of the operational semantics of booleans
and arithmetic ecpressions in which stuck terms are defined to evaluate to a special constant
"wrong". Extend this semantics to λNB

定義できる?
λ式自体の型

型とのペアにする
λNB
問題の解釈

第六章
評価中にα変換したい

6.1.1
c0 λs.λz. z;
c2 s z

 successor zero

plus λm.λn.λs.λz. m s (n s z) #記述間違い修正

6.1.2

 p69 5.3.1の定義と対比 自由変数の個数をきちんと見ている

λx.x はλ.0

元々wだった0と重ならないようにcontextをずらす
自由変数の扱い シフティング
「上から与えられた環境があるのではないか」、外側の環境の変数と
自由変数と区別がつかないんじゃないの?
再帰関数のため

α変換
λリフティング

6.1.3
Bruijn index
context Γ = xn, xn-1, ... x1, x0

6.1.4
等価であることを示せ

τ' ∈ τ_n+1_^i+1^

6.1.5 exercise Recomended

1. Define a function removenamesΓ(t) that takes naming context gamma and
an ordinary term t (with FV(t) dom(gamma) and yields the corresponding nameless term.

2. Define a function restorenamesΓ(t) that takes a nameless term t and a naming
context Γ and produces an ordinary term. (To do this, you will need to "make up"
names for the variable bound by absctractions in t.
You may assume that the names in Γ are pairwise distinct and that the set ν
of variable names is orderd, so that it makes sense to say
"choose the first variable name that is not already in dom(Γ)"

This pair of functons should have the property that

  removenamesΓ(restorenamesΓ(t)) = t

for any nameless term t, and similarly

  restorebanesΓ(removenamesΓ(t)) = t,

up to renaming of bound variables, for any ordinary term t.

解答例にtypo

 rs

0 → p

    rs

λ.0 →λp.p

λ.(1 0) → λp. q p

Γ={}
λf.(λx. f (λy. (x x) y)) (λx.f (λy. (x x) y))

= λ.rm{f} ( (λx.f (λy. (x x) y)) (λx.f (λy. (x x) y)))

= λ.rm{f} (λx.f (λy. (x x) y))

               rm{f} (λx.f (λy. (x x) y))

= λ.(λ.rm{f.x} (f (λy. (x x) y)))

     (λ.rm{f.x} (...))

= λ.(rm{f.x}(f) rm{f.x} (λy. (x x) y))
= λ.(λ.1 λ.rm{f.x.y} (*1) (...)
= λ.(λ.1 λ.(1 1) 0) (...)

rs{} (λ.(λ.1 λ. (1 1) 0) (λ.1 λ.(1 1) 0))

= λf.rs{f} (*2)
= λf.rs{f} (λ.1 λ.(1 1) 0) rs{f} (λ.1 λ. (1 1) 0)
= λf.(λx.rs{f,x} (1 λ.(1 1) 0)) rs{f.x}(...)

= λf.(λx.f(λy.(x x) y)) (...)

6.2 shifting and substitution

6.2.1
definition

6.2.2
exercise

↑^2 (λ.λ.1(0 2))
=λ.λ↑^2_1 1 (0 2))
=λ.λ.↑^2_2 1 ↑^2_2 (0 2))
=λ.λ.1 (↑^2_2 0 ↑^2_2 2)
=λ.λ. 1(0 4)

6.2.3
exercise
show that if t is an n-term, then ↑^d_c(t) is an (n+d)-term

---

*1 x x) y

*2 λ.1 λ.(1 1) 0) (λ.1 λ.(1 1) 0