「リストは自分自身のfoldr関数として定義される」について

「リストは自分自身のfoldr関数として定義される」について
=========

2014_05_11 @suharahiromichi


# はじめに
TAPL（参考文献1.)には、p.47とp.275の2箇所に渡って、「リストは自分自身のfoldr関数として定義される」と書かれている。しかし、前後の説明を読んでもこの一文の意味することはよくわからなかった。
また、別なところ（同 p.277）で、「(System Fは)fixに頼ることなく純粋な言語でソート関数のようなものが書ける…」と極めて重要なことが書いてある。これは、チャーチ数やリストのチャーチ表現がそのような性質を持つのであって、System Fはそれらを扱える（型付けをすることができる）と理解するべきなのだろう。
以上のことを納得するために、数やリストについて、

1. Inductiveな定義
2. チャーチ表現
3. fold関数

の関係を調べてみる。証明はCoq SSRefelctで行う。
この文章のソースコードは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_church_number.v



```coq:

Require Import ssreflect ssrbool ssrnat.


```

# チャーチ数


## チャーチ数(CNat)


```coq:

Definition CNat := forall X, (X -> X) -> X -> X.

Definition C0 : CNat := fun X => fun s : X -> X =>
                                   fun z : X => z.
Definition C1 : CNat := fun X => fun s : X -> X =>
                                   fun z : X => s z.
Definition C2 : CNat := fun X => fun s : X -> X =>
                                   fun z : X => s (s z).
Definition CSucc : CNat -> CNat :=
  fun n : CNat => fun X =>
                    fun s : X -> X =>
                      fun z : X => s (n X s z).
Eval compute in CSucc C0.


```

## InductiveなNatの定義


```coq:

Inductive Nat : Type :=
| O
| S of Nat.


```

## CNatとNatの間の変換

### CNatをNatに変換する関数


```coq:

Definition CNat2Nat (c : CNat) : Nat :=
  c Nat S O.

Eval compute in CNat2Nat C2.

```

= S (S O) : Nat
これはチャーチ数cに、Sをfoldしているとみることもできる。


### Fold関数
Inductiveに定義したNatに対しては、Foldを定義しなければならない。


```coq:

Fixpoint foldNat (X : Type) (s : X -> X) (z : X) (n : Nat) : X :=
  match n with
    | O => z
    | S n' => s (foldNat X s z n')
  end.

Check foldNat.

```

 : forall X : Type, (X -> X) -> X -> Nat -> X


### NatをCNatに変換する関数


```coq:

Definition Nat2CNat (n : Nat) : CNat :=
  fun X =>
    fun s : X -> X =>
      fun z : X => foldNat X s z n.

Eval compute in Nat2CNat (S (S O)).

```

 = fun (X : Type) (s : X -> X) (z : X) => s (s z) : CNat
Inductiveに定義された整数nに、sをFoldし、そのsをλ抽象すると、チャーチ数が得られる。


## 証明

### C0とOが同じ、CSuccとSの結果が同じになることの証明


```coq:

Theorem CNat_Nat_zero :
  CNat2Nat C0 = O.
Proof.
    by [].
Qed.

Theorem CNat_Nat_succ :
  forall c n,
    CNat2Nat c = n -> CNat2Nat (CSucc c) = S n.
Proof.
  rewrite /CNat2Nat /CSucc.
    by move=> c n ->.
Qed.


```

### CNat2NatとNat2CNatで元に戻ることの証明


```coq:

Theorem CNat2Nat_Nat2CNat :
  forall n : Nat, CNat2Nat(Nat2CNat n) = n.
Proof.
  rewrite /CNat2Nat /Nat2CNat.
  elim.
    by [].
  by move=> /= n0 ->.
Qed.


```

# 自然数のリスト
要素の自然数は、SSReflectのnatの定義を使う。

## チャーチ表現


```coq:

Definition CListNat := forall R, (nat -> R -> R) -> R -> R.

Definition CNil : CListNat :=
  fun R => fun c : nat -> R -> R =>
             fun n : R => n.                (* [] *)
Definition CL1 : CListNat :=
  fun R => fun c : nat -> R -> R =>
             fun n : R => c 1 n.            (* [1] *)
Definition CL2 : CListNat :=
  fun R => fun c : nat -> R -> R =>
             fun n : R => c 1 (c 2 n).      (* [1,2] *)
Definition CL3 : CListNat :=
  fun R => fun c : nat -> R -> R =>
             fun n : R => c 1 (c 2 (c 3 n)). (* [1,2,3] *)
Definition CCons : nat -> CListNat -> CListNat :=
  fun hd : nat =>
    fun tl : CListNat =>
      fun R =>
        fun c : nat -> R -> R =>
          fun n : R => c hd (tl R c n).
Eval compute in CCons 1 CNil.


```

## Inductiveな定義


```coq:

Inductive ListNat : Type :=
| Nil
| Cons of nat & ListNat.


```

## clistとlistの間の変換

### clistをlistに変換する関数


```coq:

Definition clist2list (c : CListNat) : ListNat :=
  c ListNat Cons Nil.

Eval compute in clist2list CL2.

```

= Cons 1 (Cons 2 Nil) : ListNat
clist2listは、チャーチ表現のリストcに、Consをfoldrしているとみることもできる。


### Foldr関数
Inductiveに定義したlistに対しては、Foldを定義しなければならない。


```coq:

Fixpoint foldr (R : Type) (c : nat -> R -> R) (n : R) (l : ListNat) : R :=
  match l with
    | Nil => n
    | Cons x l' => c x (foldr R c n l')
  end.

Check foldr.

```

 : forall R : Type, (nat -> R -> R) -> R -> ListNat -> R


### listをclistに変換する関数


```coq:

Definition list2clist (l : ListNat) : CListNat :=
  fun R =>
    fun c : nat -> R -> R =>
      fun n : R => foldr R c n l.

Eval compute in list2clist (Cons 1 (Cons 2 Nil)).

```

 = fun (R : Type) (c : nat -> R -> R) (n : R) => c 1 (c 2 n) : CListNat
Inductiveに定義されたリストlに、cをFoldrし、そのcをλ抽象すると、チャーチ表現で表したリストが得られる。


## 証明

### CNilとnilが同じ、CConsとConsの結果が同じになることの証明


```coq:

Theorem clist_list_nil :
  clist2list CNil = Nil.
Proof.
    by [].
Qed.

Theorem clist_list_cons :
  forall c l n,
    clist2list c = l ->
    clist2list (CCons n c) = Cons n l.
Proof.
  rewrite /clist2list /CCons.
    by move=> c l n ->.
Qed.


```

## clist2listとlist2clistで元に戻ることの証明



```coq:

Theorem clist2list_list2clist :
  forall l : ListNat, clist2list(list2clist l) = l.
Proof.
  rewrite /clist2list /list2clist.
  elim.
    by [].
  by move=> /= n l ->.
Qed.


```

# まとめ
わかったこと。チャーチ数やリストのチャーチ表現は、それ自身にFoldの機能を持っていること。また、Inductiveに定義したnatやlistは、Fold関数によってチャーチ表現に変換できること。
参考文献2.は、無限大のチャーチ数と不動点演算子の関係をHaskellで論じたもので、FoldNatの定義などを参考にさせていただいた。


# 参考文献

1. Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
2. 酒井 「不動点演算子はチャーチ数での無限大?」 http://msakai.jp/d/?date=20100628


```