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

第五回
第9章

λ_ simply typed lamda-calculus

9.2.2 Exercise

1. f:Bool -> Bool |- f (if false then true else false) : Bool
2. f:Bool -> Bool |- lambda x:Bool. f (if x then false else x) : Bool -> Bool

9.3 Properties of Typing

9.3.1 LEMMA
1.
2.
3.
4.
5.
6.
組み合わせ

9.3.4
lemma
1. If v is a value of type Bool, then v is either true of false.
2. If v is a value if Type T1 -> T2, then v = lambda x:T1・t2

value

9.3.2
Y combinator?
再帰する

toggetter
khibino

9.3.3
9.3.4

推論規則により正当化される

9.3.5 theorem

proof
Γ.x：T2 |- t1:T1

Γ
Γ

#Conceptual

Mathematics p125

9.3.6 permutation
カンマ演算子は可換

→ATAPL
集合の要素なので入れ替えても同じ

9.3.7 weakening

9.3.8 preservation of types under substitution

内側から評価しても外側から評価しても結果は同じ

9.3.9 theorem if Γ|- t:T and t→t', then Γ|-t':T
proof:

t = t1 t2 の場合
帰納法の仮定より

9.3.10
解答errata

(λx:Bool→Bool.λy:Bool.y)(λz:Bool.true true)

9.4 The Curry-Howard Correspondece

LOGIC PROGRAMMING LANGUAGE

callcc 排中律
住井さんのエントリ
kinabaさんのエントリ

9.5
9.5.1
erase(x) = x
erase(λx:T1・T2) = λx.erase(t2)
erase(t1 t2) = erase(t1) erase(t2)
評価規則は型に依存しない

9.6
Curry-Style vs. Church-Style

10 jump
a39