0
Help us understand the problem. What are the problem?

posted at

updated at

【はじめてのIT勉強会】関数型プログラミング初学者はプログラミングが魔法でないことを知りました ~証明を添えて~

はじめに

本記事は はじめてのIT勉強会アドベントカレンダー '21 1日目の記事です。

はじめまして、はじめてのIT勉強会副代表のうにすけと申します (@uniuni__8282)

本記事では関数型プログラミング初学者が「プログラミングって魔法じゃなかった..!」そんな感動を抱いた学びを共有できればと思っております。最後までどうぞお付き合いください。

使うもの

Coqという定理証明支援形を用います。Coqは定理証明支援形の一つで自然言語に頼らない形式化された証明を書くことに役立ちます。そして、関数型プログラミング言語と仕様記述言語の特徴を持っていて、Coqの中でプログラムを書いて、またそのプログラムを実行することなく証明という手段で検証することができます。

Coqの上でかくプログラムは関数型プログラミングの特徴を持っています。一機能としてOcamlなどの別の関数型プログラミング言語で書かれたプログラムに変換する機能を持ち、証明で動作が保証されたプログラムを他プロジェクトに展開することも可能です。

やってみる

リストを扱う

list型の定義

以下がX型のlistの定義になります。

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

なんでこれがlistの定義になっているのか。この定義は以下のように解釈できます。

  • nil (空のlist) はlistである
  • lがlistに属していればcons x lもlistに属する。これは直感的にはlがリストであればその先頭にxを追加したリストもリストである、ということです。

一つリストを定義してみます。

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

nilは空のリスト
cons 3 nilは3を要素に持つリスト
cons 2 (cons 3 nil)は2,3を要素に持つリスト
cons 1 (cons 2 (cons 3 nil))は1,2,3を要素に持つリスト

このように1,2,3と3つの要素を持つリストを定義できていることがわかります。同様に様々なリストを定義できるのですが、少し表記としてわかりにくいのでプログラムを書くうえで表記を定義します。

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).

この表記の定義によってcons 1 (cons 2 (cons 3 nil))[1;2;3]と表記されます。これで少し見慣れたリストに近付いたのではないでしょうか。

リストを結合する関数を作ってみる

この関数で得たいのはJavaScriptでいうconcat() メソッド、Pythonだったら配列同士の+演算だけで実現できる結果です。私は関数型言語を書くまで、これかくだけで配列の結合ができる!魔法か?と思っていましたが、関数型言語でかいて魔法じゃない!となった一つめのポイントです。

Coqをはじめとする多くの関数型言語ではパターンマッチを用いて関数の定義が可能です。また再帰的な定義も可能です。関数の定義に自身が登場する関数です。

Fixpoint app {X : Type} (l1 l2 : list X)
             : (list X) :=
  match l1 with
  | nil => l2
  | h :: t => h :: (app t l2)
  end.

[1;2;3][4;5;6]の結合を具体例として考えてみます。

app [1;2;3] [4;5;6] -> 1::(app [2;3] [4;5;6])
                    -> 1::2::(app [3] [4;5;6])
                    -> 1::2::3::(app nil [4;5;6])
                    -> 1::2::3::[4;5;6]
                    -> [1;2;3;4;5;6]

このようにapp関数をnilにたどり着くまで繰り返し呼び出すことによってリストの結合ができることがわかります。

map関数を定義する

JavaScriptのmapメソッドは以下のような挙動になります。

var items = [1,2,3,4,5];

var result = items.map(( value ) => {

    return value * 2;

});

console.log( result ); //[2, 4, 6, 8, 10]

配列のそれぞれの要素に対して引数で与えた関数を適用した配列を生成していることがわかります。

mapメソッドをはじめとする配列に関する操作もとにかく配列の各値に何かをしてその配列が返ってくる便利なメソッドだ!くらいの認識でしたが、これも関数型言語で書いてみたら魔法じゃない!になった点の一つです。

Coqでは引数や結果に関数をとること無名関数を用いることができます。無名関数は引数として繰り返し使われることのない関数を定義することなくその場で関数を作ることができる、ということです。

ここまででのリストを先頭の値と後に続く配列、として見るパターンが多いことになんとなく気づいた方は想像がついているかもしれません。map関数は以下のように定義されます。

Fixpoint map {X Y: Type} (f:X->Y) (l:list X) : (list Y) :=
  match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.

X->YはX型の値を引数にとりY型の値を返す関数型を表します。つまりX型の値を引数にとりY型の値を返す関数fを引数として定めています。

具体例として引数に3足した値を返す関数を引数にとった結果を見てみましょう。

Compute map (fun x => plus 3 x) [2;0;2]. 
     = [5; 3; 5]
     : list nat

(Computeは続く処理を実行してくれる命令です)
このようにリストの各値に対して渡した関数を適用したリストが得られたことがわかります。評価の過程は以下です。

map (fun x => plus 3 x) [2;0;2]
-> 5 :: map (fun x => plus 3 x) [0;2]
-> 5 :: 3 :: map (fun x => plus 3 x) [2]
-> 5 :: 3 :: 5 :: map (fun x => plus 3 x) []
-> 5 :: 3 :: 5 :: [] = [5; 3; 5]

map関数がわかればfilter関数の定義も楽しく見れると思うのでおまけ程度に載せておきます。

Fixpoint filter {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | [] => []
  | h :: t => if test h then h :: (filter test t) else filter test t
  end.

(おまけ)証明してみる

証明がCoqを使ってきた醍醐味です。上で定義したappの性質を証明してみます。app関数では結合を行う順番は結果に関係ない、この性質を証明してみます。まずこの性質をプログラムに起こすと以下のようになります。Theoremキーワードは続く記述が定理であることを示します。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.

再帰的な定義と証明、ベースケースと一つ前の要素を参照する定義と証明、、、なんとなくこの再帰的な定義が帰納法と相性が良いことが想像つきませんか?帰納法を使うとこの性質を証明することができます。

Coqで証明を進めると証明の過程が分割された画面の右上に表示されます。
スクリーンショット 2021-12-01 0.17.01.png

証明を始めます。

証明はじめ

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.

Proof.で証明の開始を宣言します。この時点で証明の状態は以下のようになっています。

1 subgoal
______________________________________(1/1)
forall (A : Type) (l m n : list A), l ++ m ++ n = (l ++ m) ++ n
  • 1 subgoalが示すべきゴールが1つであること
  • 線の上は仮定
  • 線の下は今示すべきゴール

をそれぞれ示しています。

値の導入

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
    intros A l m n.
1 subgoal
A : Type
l, m, n : list A
______________________________________(1/1)
l ++ m ++ n = (l ++ m) ++ n

intros A l m n.を実行することでゴールの一部だった 値の情報が仮定に移動したことがわかります。

帰納法の導入

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
2 subgoals
A : Type
m, n : list A
______________________________________(1/2)
[ ] ++ m ++ n = ([ ] ++ m) ++ n
______________________________________(2/2)
(h :: t) ++ m ++ n = ((h :: t) ++ m) ++ n

inductionタクティクがそれに続く値(今の場合はl)に関する帰納法の帰結にゴールを変更します。
示した命題をPとしたときリストに関する帰納法で示すべき2つの帰結は以下です。

  • まず、 l が nil のとき P が l について成り立つことを示す。
  • それから、 l が cons n l' であるとき、ある数 n とより小さいリスト l' に対して、 P が l' について成り立つと仮定すれば P が l についても成り立つことを示す。

inductionタクティクの実行によって帰結が二つにわかれたことが確認できます。

帰納法1つ目の帰結

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - 
1 subgoal
A : Type
m, n : list A
______________________________________(1/1)
[ ] ++ m ++ n = ([ ] ++ m) ++ n

帰結が成り立っていることが判断できると思いますが、simpl.タクティクで両辺を簡単にします。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl.
1 subgoal
A : Type
m, n : list A
______________________________________(1/1)
m ++ n = m ++ n

左辺と右辺が見るからに同じ等式は、reflexivityタクティクを使って証明を終わらせることができます。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl. reflexivity. 

帰納法2つ目の帰結

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl. reflexivity. 
  - 
1 subgoal
A : Type
h : A
t, m, n : list A
IHt : t ++ m ++ n = (t ++ m) ++ n
______________________________________(1/1)
(h :: t) ++ m ++ n = ((h :: t) ++ m) ++ n

2つ目の帰結においてはlがh::tの形をしており、またIHtという過程が存在することがわかります。IHtがいわゆる帰納法の仮定で、P(a)a ++ m ++ n = (a ++ m) ++ nとしたとき、P(t)P(h :: t)の証明の1つの仮定として用いることができます。この時点では仮定が使用できないのでsimplタクティクで両辺を簡単にします。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl. reflexivity. 
  - simpl.
1 subgoal
A : Type
h : A
t, m, n : list A
IHt : t ++ m ++ n = (t ++ m) ++ n
______________________________________(1/1)
h :: t ++ m ++ n = h :: (t ++ m) ++ n

帰結の左辺の一部とIHtの左辺が一致していることがわかります。仮定を用いて帰結を書き換える場合にはrewriteタクティクを用います。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl. reflexivity. 
  - simpl. rewrite -> IHt. 
1 subgoal
A : Type
h : A
t, m, n : list A
IHt : t ++ m ++ n = (t ++ m) ++ n
______________________________________(1/1)
h :: (t ++ m) ++ n = h :: (t ++ m) ++ n

書き換えによって両辺が一致したことがわかりますので一つ目の帰結と同様にreflexivityタクティクを実行して証明が完了します。証明するべきゴールがなくなったらQedキーワードで証明の完了を宣言します。

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [|h t IHt].
  - simpl. reflexivity. 
  - simpl. rewrite -> IHt. reflexivity. Qed.

終わりに

ご拝読ありがとうございました。

プログラムの証明に関連した記事は今後たくさん書いていきたいと思っているので興味があればぜひ読みにきてください!

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Sign upLogin
0
Help us understand the problem. What are the problem?