# Types: 型システム

Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Arith.Arith.
From PLF Require Import Maps.
From PLF Require Import Imp.
From PLF Require Import Smallstep.

Hint Constructors multi.

# 型付きの算術式

## 構文

    t ::= tru
| fls
| test t then t else t
| zro
| scc t
| prd t
| iszro t

そして形式的には以下の通りです。

Inductive tm : Type :=
| tru : tm
| fls : tm
| test : tm -> tm -> tm -> tm
| zro : tm
| scc : tm -> tm
| prd : tm -> tm
| iszro : tm -> tm.

Inductive bvalue : tm -> Prop :=
| bv_tru : bvalue tru
| bv_fls : bvalue fls.

Inductive nvalue : tm -> Prop :=
| nv_zro : nvalue zro
| nv_scc : forall t, nvalue t -> nvalue (scc t).

Definition value (t : tm) := bvalue t \/ nvalue t.

Hint Constructors bvalue nvalue.
Hint Unfold value.
Hint Unfold update.

## 操作的意味論

1ステップ関係について、まず非形式的なものを見ます。
                   -------------------------------                  (ST_TestTru)
test tru then t1 else t2 --> t1

-------------------------------                  (ST_TestFls)
test fls then t1 else t2 --> t2

t1 --> t1'
----------------------------------------------------       (ST_Test)
test t1 then t2 else t3 --> test t1' then t2 else t3

t1 --> t1'
------------------                             (ST_Scc)
scc t1 --> scc t1'

---------------                           (ST_PrdZro)
prd zro --> zro

numeric value v1
-------------------                          (ST_PrdScc)
prd (scc v1) --> v1

t1 --> t1'
------------------                             (ST_Prd)
prd t1 --> prd t1'

-----------------                        (ST_IszroZro)
iszro zro --> tru

numeric value v1
----------------------                       (ST_IszroScc)
iszro (scc v1) --> fls

t1 --> t1'
----------------------                         (ST_Iszro)
iszro t1 --> iszro t1'


そして形式的なものです。

Reserved Notation "t1 '-->' t2" (at level 40).

Inductive step : tm -> tm -> Prop :=
| ST_TestTru : forall t1 t2,
(test tru t1 t2) --> t1
| ST_TestFls : forall t1 t2,
(test fls t1 t2) --> t2
| ST_Test : forall t1 t1' t2 t3,
t1 --> t1' ->
(test t1 t2 t3) --> (test t1' t2 t3)
| ST_Scc : forall t1 t1',
t1 --> t1' ->
(scc t1) --> (scc t1')
| ST_PrdZro :
(prd zro) --> zro
| ST_PrdScc : forall t1,
nvalue t1 ->
(prd (scc t1)) --> t1
| ST_Prd : forall t1 t1',
t1 --> t1' ->
(prd t1) --> (prd t1')
| ST_IszroZro :
(iszro zro) --> tru
| ST_IszroScc : forall t1,
nvalue t1 ->
(iszro (scc t1)) --> fls
| ST_Iszro : forall t1 t1',
t1 --> t1' ->
(iszro t1) --> (iszro t1')

where "t1 '-->' t2" := (step t1 t2).

Hint Constructors step.

step 関係は元の式が大域的に意味を持つかは考慮せず、「次の」簡約操作が適切な種類の対象へ適用されることだけを確認していることに注意してください。 例えば、 scc tru は先に進むことはできませんが、明らかに同程度に無意味な項
scc (test tru then tru else tru)
は（行き詰まるまでに1ステップ）進めることができます。

## 正規形と値

この言語の step 関係について、まず注目に値するのは、 Smallstep 章の強進行性定理(strong progress theorem)が成り立たないということです。 すなわち、正規形ではあるのに（これ以上簡約できないのに）、値ではない項があるのです（これは、そのような項を想定する「簡約結果」と定義しなかったからです）。 そのような項は「行き詰まる(stuck)」ことになります。

Notation step_normal_form := (normal_form step).

Definition stuck (t : tm) : Prop :=
step_normal_form t /\ ~ value t.

Hint Unfold stuck.

#### 練習問題: ★★, standard (some_term_is_stuck)

Example some_term_is_stuck :
exists t, stuck t.
Proof.

ただし、この言語では値の集合と正規形の集合は同一ではありませんが、値の集合は正規形の集合の部分集合になっています。 これは重要なことで、さらに簡約できる値を定義してしまうことはないことを表しています。

#### 練習問題: ★★★, standard (value_is_nf)

Lemma value_is_nf : forall t,
value t -> step_normal_form t.
Proof.

（ヒント: 証明中で、数値であることがわかっている項に対して帰納的推論をしなければならないことになります。 この帰納法は、その項自体にして適用することもできますし、その項が数値であるという事実に対して適用することもできます。 どちらでも証明は進められますが、片方はもう片方よりもかなり短くなります。 練習として、ふたつの方法両方で証明を完成させなさい。）

#### 練習問題: ★★★, standard, optional (step_deterministic)

value_is_nf を使い、 step 関係もまた決定的であることを示しなさい。

Theorem step_deterministic:
deterministic step.
Proof with eauto.

## 型付け

Inductive ty : Type :=
| Bool : ty
| Nat : ty.

                           ---------------                     (T_Tru)
|- tru \in Bool

---------------                      (T_Fls)
|- fls \in Bool

|- t1 \in Bool    |- t2 \in T    |- t3 \in T
--------------------------------------------     (T_Test)
|- test t1 then t2 else t3 \in T

--------------                    (T_Zro)
|- zro \in Nat

|- t1 \in Nat
-----------------                    (T_Scc)
|- scc t1 \in Nat

|- t1 \in Nat
-----------------                    (T_Prd)
|- prd t1 \in Nat

|- t1 \in Nat
--------------------                 (T_IsZro)
|- iszro t1 \in Bool


Reserved Notation "'|-' t '\in' T" (at level 40).

Inductive has_type : tm -> ty -> Prop :=
| T_Tru :
|- tru \in Bool
| T_Fls :
|- fls \in Bool
| T_Test : forall t1 t2 t3 T,
|- t1 \in Bool ->
|- t2 \in T ->
|- t3 \in T ->
|- test t1 t2 t3 \in T
| T_Zro :
|- zro \in Nat
| T_Scc : forall t1,
|- t1 \in Nat ->
|- scc t1 \in Nat
| T_Prd : forall t1,
|- t1 \in Nat ->
|- prd t1 \in Nat
| T_Iszro : forall t1,
|- t1 \in Nat ->
|- iszro t1 \in Bool

where "'|-' t '\in' T" := (has_type t T).

Hint Constructors has_type.

Example has_type_1 :
|- test fls zro (scc zro) \in Nat.
Proof.
apply T_Test.
- apply T_Fls.
- apply T_Zro.
- apply T_Scc.
+ apply T_Zro.
Qed.

（型付け関係のすべての構成子をヒントデータベースに登録してあるので、実際には auto で証明を自動的に構築することができます。）

Example has_type_not :
~ ( |- test fls zro tru \in Bool ).
Proof.
intros Contra. solve_by_inverts 2. Qed.

#### 練習問題: ★, standard, optional (scc_hastype_nat__hastype_nat)

Example scc_hastype_nat__hastype_nat : forall t,
|- scc t \in Nat ->
|- t \in Nat.
Proof.

### Canonical forms

The following two lemmas capture the fundamental property that the definitions of boolean and numeric values agree with the typing relation.

Lemma bool_canonical : forall t,
|- t \in Bool -> value t -> bvalue t.
Proof.
intros t HT [Hb | Hn].
- assumption.
- induction Hn; inversion HT; auto.
Qed.

Lemma nat_canonical : forall t,
|- t \in Nat -> value t -> nvalue t.
Proof.
intros t HT [Hb | Hn].
- inversion Hb; subst; inversion HT.
- assumption.
Qed.

## 進行

#### 練習問題: ★★★, standard (finish_progress)

Theorem progress : forall t T,
|- t \in T ->
value t \/ exists t', t --> t'.

Complete the formal proof of the progress property. (Make sure you understand the parts we've given of the informal proof in the following exercise before starting -- this will save you a lot of time.)
Proof with auto.
intros t T HT.
induction HT...
-
right. inversion IHHT1; clear IHHT1.
+
apply (bool_canonical t1 HT1) in H.
inversion H; subst; clear H.
exists t2...
exists t3...
+
inversion H as [t1' H1].
exists (test t1' t2 t3)...

• 導出で直前に適用した規則が T_Test である場合、 t = test t1 then t2 else t3 かつ、 |- t1 \in Bool|- t2 \in T かつ |- t3 \in T である。 帰納法の仮定から、 t1 は値であるか、さもなければ何らかの t1' に簡約できる。
• t1 が値のとき、 canonical forms lemma と |- t1 \in Bool という事実から t1bvalue である。 すなわち、 tru または fls である。 t1 = tru のとき、 ST_TestTru より tt2 に簡約され、 t1 = fls のときは ST_TestFls から tt3 に簡約される。 どちらの場合も t の簡約は進められる。 これが示そうとしていたことである。
• t1 自体が簡約できるなら、 ST_Test を用いることで t もまた簡約できる。

この定理は Smallstep の章の強進行性定理よりも興味深いものです。 Smallstep の章では、正規形はすべて値でした。 本章では項が行き詰まることもありますが、行き詰まるようなものは型のつかないものだけです。

## 型保存

#### 練習問題: ★★, standard (finish_preservation)

Theorem preservation : forall t t' T,
|- t \in T ->
t --> t' ->
|- t' \in T.

Complete the formal proof of the preservation property. (Again, make sure you understand the informal proof fragment in the following exercise first.)

Proof with auto.
intros t t' T HT HE.
generalize dependent t'.
induction HT;

intros t' HE;

try solve_by_invert.
- inversion HE; subst; clear HE.
+ assumption.
+ assumption.
+ apply T_Test; try assumption.
apply IHHT1; assumption.

• 導出で直前に使った規則が T_Test の場合、 t = test t1 then t2 else t3、かつ |- t1 \in Bool|- t2 \in T かつ |- t3 \in T である。
ttest ... の形式であることとスモールステップ簡約関係を見ると、 t --> t' を示すために使えるのは ST_TestTruST_TestFls または ST_Test のみである。
• 直前の規則が ST_TestTru の場合、 t' = t2 である。 |- t2 \in T であるのでこれは求める結果である。
• 直前の規則が ST_TestFls の場合、 t' = t3 である。 |- t3 \in T であるのでこれは求める結果である。
• 直前の規則が ST_Test の場合、 t' = test t1' then t2 else t3' である。 ここで、 t1 --> t1' である。 |- t1 \in Bool であるので、帰納法の仮定から |- t1' \in Bool である。 また、 T_Test 規則から |- test t1' then t2 else t3 \in T であり、これは求める結果である。

#### 練習問題: ★★★, standard (preservation_alternate_proof)

さらに、同一の性質を型付けの導出ではなく、評価の導出に関する帰納法で証明しなさい。 先ほどの証明の最初数行を注意深く読んで考え、各行が何をしているのか理解することから始めましょう。 この証明でも設定はよく似ていますが、まったく同じというわけではありません。

Theorem preservation' : forall t t' T,
|- t \in T ->
t --> t' ->
|- t' \in T.
Proof with eauto.

## 型の健全性

Definition multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

Corollary soundness : forall t t' T,
|- t \in T ->
t -->* t' ->
~(stuck t').
Proof.
intros t t' T HT P. induction P; intros [R S].
destruct (progress x T HT); auto.
apply IHP. apply (preservation x y T HT H).
unfold stuck. split; auto. Qed.

## 追加演習

#### 練習問題: ★★, standard (variation1)

| T_SccBool : forall t,
|- t \in Bool ->
|- scc t \in Bool

• step の決定性
• 進行
• 型保存

#### Exercise: 2 stars, standard (variation2)

Suppose, instead, that we add this new rule to the step relation:
| ST_Funny1 : forall t2 t3, (test tru t2 t3) --> t3
Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

#### 練習問題: ★★, standard (variation2)

| ST_Funny1 : forall t2 t3,
(test tru t2 t3) --> t3

#### 練習問題: ★★, standard, optional (variation3)

| ST_Funny2 : forall t1 t2 t2' t3,
t2 --> t2' ->
(test t1 t2 t3) --> (test t1 t2' t3)

#### 練習問題: ★★, standard, optional (variation4)

| ST_Funny3 :
(prd fls) --> (prd (prd fls))

#### 練習問題: ★★, standard, optional (variation5)

| T_Funny4 :
|- zro \in Bool

#### 練習問題: ★★, standard, optional (variation6)

| T_Funny5 :
|- prd zro \in Bool