TAPL 読書会@東京 第7回

※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

第七回 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