1/10 言語モデル論ノート

型体系（１）
- 練習問題２
- - 2x + 3y = 7, x = y = 4
  - x = a, y = 3a + 5
  - 後者の方が解けている感がある。
  - 出てくる変数が＝の左右で完全に分離されているか
  - p27の４つ目の制約おかしくない？＝＞α=β->τ[4]
  - 単一化についてプリントでいろいろ話された
  - 単一化
  - 1. t[2]
      - t = a -> b -> t[3]
      - t[2] = b -> t[3]
      - a = t[4] -> t[3]
      - a = b -> t[4]
    2. a
      - t = (t[4] -> t[3]) -> b -> t[3]
      - t[2] = b -> t[3]
      - a = t[4] -> t[3]
      - t[4] -> t[3] = b -> t[4]
    3. 四つ目の制約を分解
      - t = (t[4] -> t[3]) -> b -> t[3]
      - t[2] = b -> t[3]
      - a = t[4] -> t[3]
      - t[4] = b
      - t[3] = t[4]
    4. t[4]
      - t = (b -> t[3]) -> b -> t[3]
      - t[2] = t -> t[3]
      - a = b -> t[3]
      - t[4] = b
      - t[3] = b
    5. t[3]
      - t = (b -> b) -> b -> b -- twiceの主型
      - t[2] = t -> b
      - a = b -> b
      - t[4] = b
      - t[3] = b
- p28
  - ad hoc polymorphism(overloading)
  - subsumption(包摂) polymorphism
  - parametric polymophism
- p29
  - 同じようなことするデータ構造がいっぱいあるからオーバーロードとかあると便利でしょ
- p30
- p31
  - FLを拡張（多相型にする）
- p32
- p33
  - ＞は「同等以上に具体的」を表す（記号としては=はつかない）
  - 定義がよくわからん
  - 三つ目の例はβを一般化しているのでアウト。
- p34
  - 赤文字の部分を追加
- p35
- p36
  - (var)は、σがτより一般的ならσをτに置き換えていいという意味（instanciate）
- p37
- p38
- p39
- p40
- - 即値の部分の型は変数を立てずに直接boolとかintとかって書いてる（紙面の都合）
  - Γは「f:∀α.τ[2]」の略。紙面の都合上略記してるだけ
  - 制約
  - - t = t[3] * t[4]
    - t[2] = a -> a
    - ∀a.t[2] > int -> t[3]
    - ∀a.t[2] > bool -> t[4]
  - 単一化
  - 1. t[2]
      - t = t[3] * t[4]
      - t[2] = a -> a
      - ∀a.(a -> a) > int -> t[3]
      - ∀a.(a -> a) > bool -> t[4]
    2. instanciate
      - t = t[3] * t[4]
      - t[2] = a -> a
      - t[5] -> t[5] = int -> t[3](t[5]を新たに作った)
      - t[6] -> t[6] = bool -> t[4](t[6]を新たに作った)
    3. 以下略。結果は
      - t = int * bool
      - t[2] = a -> a
      - t[3] = t[5] = int
      - t[4] = t[6] = bool
型体系（２）
- p41
- p42
  - 反対称律は使わないので別に成り立たなくてよい
- p43
- p44
- p45
- p46
  - TopはScalaのTopクラス。すべてのクラスにとってのスーパークラス
- p47
- p48
- p49
- p50
- p51
- p52
- p53
- p54
- p55
- p56
- p56
- p57