第七回 7/9
p140
週二回二ヶ月 15万円 形式理論集中講義
Variants vs. Datatypes
type T = l1 of T1
| l2 of T2
| ...
| ln of Tn
ML のものとほぼ同じ
OCaml では「データ型」は小文字、データ型コンストラクタは大文字
OCamlとのちがい
1
2
li(t)
タギング p136
「教育」
cannt shared between diffrent datatypes
3.
OCamlでは
type Weekday = monday of Unit
| tuesday of Unit
| wednesday of Unit
| thursday of Unit
| friday of Unit
type Weekday = monday | tuesday | wednesday | yhursday | friday
と書ける
4.
A Datatype definition may be recursive -- ie., the type being defined is allowed
An OCaml datatype can be parameterized on a tyep variable
type 'a List = nil
| cons of 'a * 'a List
Variants as Disjoint Unions
Type Dynamic
One attractive way of accomplishing this is to add a type Dynamic whose values
are pairs of a value v and a type tag T whew v has Type T.
11.11 General Recursion
cannot be defined om the simply typed lambda-calculus.
Indeed,
p143
ff = λie:Nat→Bool.
λx:Nat.
if iszero x then true
else if iszero (pred x) then false
else ie (pred (pred x));
ff : (Nat→Bool) → Nat → Bool
iseven = fix ff;
iseven : Nat → Bool
iseven 7;
false : Bool
11-12
t ::= ...
fix t
fix(λx:T1・t2)
→ [x|-> (fix (λx:T1・t2))]|t2
11.11.1 Exercise [**]
Define equal, plus, times, and factorial using fix.
ff = λe:Nat→Nat→Bool.
λx:
plus = fix (λp:Nat→Nat→Nat.)
times
λe
λx.λy.
if iszero x then 0
else plus y (e (pred x) y))
factorial
if iszero m then 1 else times m (f (pred m)))
ff = λieio:{iseven:Nat→Bool, isodd:Nat→Bool}.
{iseven = λx:Nat.
if iszero x then true
else ieie.isodd (pred x),
isodd = λx:Nat.
if iszero x then false
else ieio.iseven (pred x)}
ff : {iseven:Nat→Bool, isodd:Nat→Bool}
→{iseven:Nat→Bool,isodd:Mat→Bool}
diverge
The ability to form the fixed point of a function of type T→T for any T has
some surpising consequences. In particular, it implies that ever type is
inhabited by some term.
def
letrec x:T1=t1 in t2 = let x = fix (λx:T1・t1) in t2
letrec times =
λx.λy.
if iszero
else plus y (times pred x) y)
p145
letrec iseven : Nat → Bool =
λx:Nat.
if iszero x then true
else if iszero (pred x) then false
else iseven (pred (pred x)))
in
iseven 7;
11.12 Lists
11.12.1
Exercise [***]
verify that the progress and preservation therems hold for the simply typed
lambda-calculs with boolean and lists.
solution: surprise!
11.12.2 [**]
Can all the type annotations be deleted?
solution: not quite all:
12 Normalization
12.1 Normalization for Simple Typews
the fact that the evaluation of a well-typed program is guratted to halt in a finite
number of steps -- ie., every well-typed term is normalizable.
full-blown programming languages
§30-3
Another reason for studying normalization proof is that they are some of the most beatiful
type theory literature
12.1 normalization for simple types
The language sutdied in this chapter is the simply typed lambda-calculus (Figure 9-1)
with a single base type A (11-1).
12.1.1 Exercise[*]
Where do we fail if we attempt to prove nomalization by a straightforward induction on
the size of a well-typed term?
id = λx:T.x
The key issue here is finding a strong enough induction hypthesis.
12.1.2 definition
Ra(t) iff t halts.
RT1→T2 (t) iff t halts and, whenever RT1(S), we have RTw(t s)
12.1.3
LEMMA if RT(t), then t halts.
the second step is broken into two lemmas.
first, we remark that membership in RT is invariant under evaluation.
12.1.4
LEMMA
Proof
Next, we want ot show that every term of type T belongs
T2 T2
(t s) → (t' s)
↑
T1→T2 T1
RT(S)
RT1→T2(t)→RT1→RT2(t')
we generalize it to cover all closed instances of an open term t.
12.1.5
LEMMA:
induction on a derivation of
Case T-Var: t = xi T=T1
Case T-ABS
obviously, [x1 → v1] … [xn→vn]
t = λx:S1・S
------ ↑
↑value [x1→v1]
by the induction hypothesis,
Rs2([x1→v1]…[xn→vn][x→v]s2)
12.1.5ではTの構造について論じている?
Case T-APP
12.1.6 theorem
12.1.7 exercize[***]
次回は9/10
gyk
最終更新:2012年02月11日 21:51