15.txt

# 2.1

S = {x:Nat, y:Nat, z:Nat}
T = {y:Nat}
U = {y:Nat, x:Nat, z:Nat}

S <: T を示す。

---------- (S-RCDPERM)   ------------- (S-RCDWIDTH)
  S <: U                    U <: T
---------------------------------- (S-TRANS)
              S <: T


# 2.2

T-SUBを無駄にかまし、導出を変えることができる。

e.g.)
                ------------ (S-REFL)
⊢ f xy : Nat     Nat <: Nat
---------------------------- (T-SUB)
          ⊢ f xy : Nat


# 2.3

(1)
- {a:Top, b:Top}
- {a:Top}
- {b:Top}
- {}
- Top

(2)
S0: {}
S1: {a:Top}
S2: {a:Top, b:Top}
...

or

{}, {}, {}, ...

(3)
S0: {a:Top}
S1: {}
S2: {}
...

or

{}, {}, {} ...


# 2.4

後のBotである

Top -> Bot


# 2.5

不正な型付けを許容してしまうため良くない。

e.g.)

                  ------------------ (S-PRODWIDTH)
⊢ v : NatxBool     NatxBool <: Nat
------------------------------------ (T-SUB)
          ⊢ v : Nat


# 3.1

- 保存 => 増やすと不正な型付けを許容する可能性がある (15.2.5とか)
- 進行 => 省略すると行き詰まる可能性がある


# 3.2

「S <: T1 -> T2 ならば S: S1 -> S2」 が必要？


# 3.6

略