Poly: 多相性と高階関数
この章では、関数型プログラミングの基本的なコンセプトを進めていきます。
特に重要な新しいアイディアは、「多相性(polymorphism)」（関数が扱うデータの型に関する抽象化）と「高階関数(higher-order function)」（関数のデータとしての取り扱い）です。
まず多相性から始めましょう。
ここまでは、数値のリストについて学んできました。
もちろん、数値以外の、文字列、ブール値、リストといったものを要素として持つリストを扱えるプログラムは、より興味深いものとなるでしょう。
これまで学んできたことだけでも、実は新しい帰納的なデータ型を作ることはできるのです。
例えば次のように...
... しかし、こんなことをやっていると、すぐに嫌になってしまうでしょう。
その理由の一つは、データ型ごとに違ったコンストラクタの名前をつけなければならないことですが、もっと大変なのは、こういったリストを扱う関数（length、revなど）を、新しく対応した型ごとに作る必要が出てくることです。
この無駄な繰り返し作業を無くすため、Coqは多相的な帰納的データ型の定義をサポートしています。
これを使うと、多相的なリストは以下のように書くことができます。
これは、前の章にあるnatlistの定義とほとんどそっくりですが、コンストラクタconsの引数の型がnatであったのに対し、任意の型を表すXがそれに変わっています。
このXはヘッダに加えられたXと結びつけられ、さらにnatlistであったものがlist Xに置き換わっています。
（ここで、コンストラクタにnilやconsといった名前を付けられるのは、最初に定義したnatlistがModuleの中で定義されていて、ここからはスコープの外になっているからです。）
それでは、listとはいったい何なのか、ということを正確に考えて見ましょう。
これを考える一つの手がかりは、リストが「型を引数にとり、帰納的な定義を返す関数である」と考えることです。
あるいは「型を引数にとり、型を返す関数」と考えてもいいかもしれません。
任意の型Xについて、list Xという型は、帰納的に定義されたリストの集合で、その要素の型がXとなっているものと考えることもできます。
定義中のlistのパラメータXはコンストラクタであるnilやconsの引数にもなります。
つまり、nilもconsも多相的なコンストラクタになっているということです。
コンストラクタの使用時には、何のリストを作るかを第一引数として与える必要があります。
例えば、nil natはnatの空リストを構成します。
Similarly, cons nat adds an element of type nat to a list of
type list nat. Here is an example of forming a list containing
just the natural number 3.
What might the type of nil be? We can read off the type list X
from the definition, but this omits the binding for X which is
the parameter to list. Type -> list X does not explain the
meaning of X. (X : Type) -> list X comes closer. Coq's
notation for this situation is forall X : Type, list X.
Similarly, the type of cons from the definition looks like
X -> list X -> list X, but using this convention to explain the
meaning of X results in the type forall X, X -> list X -> list
X.
(Side note on notation: In .v files, the "forall" quantifier
is spelled out in letters. In the generated HTML files and in the
way various IDEs show .v files (with certain settings of their
display controls), forall is usually typeset as the usual
mathematical "upside down A," but you'll still see the spelled-out
"forall" in a few places. This is just a quirk of typesetting:
there is no difference in meaning.)
リストのコンストラクタに毎回型引数を与えることは無駄な手間だと感じるかもしれません。
すぐにこれを回避する方法について見ていきます。
それでは少し話を戻して、以前書いたリスト処理関数を多相版に作り直していきましょう。
repeat関数は以下のようになります。
Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
match count with
| 0 => nil X
| S count' => cons X x (repeat X x count')
end.
As with nil and cons, we can use repeat by applying it
first to a type and then to an element of this type (and a number): nilやconsと同様に、repeatも型を最初に適用してからその型の要素（そして続いて数）に適用できます。
このrepeatを別の型のリストに使いたい場合は、適切な型を与えるだけで済みます。
Module MumbleGrumble.
Inductive mumble : Type :=
| a
| b (x : mumble) (y : nat)
| c.
Inductive grumble (X:Type) : Type :=
| d (m : mumble)
| e (x : X).
☐
それでは、repeat関数の定義をもう一度書いてみましょう。
ただし今回は、引数の型を指定しないでおきます。
Coqはこれを受け入れてくれるでしょうか？
Fixpoint repeat' X x count : list X :=
match count with
| 0 => nil X
| S count' => cons X x (repeat' X x count')
end.
うまくいったようです。
Coqがrepeat'にどのような型を設定したのか確認してみましょう。
両者は全く同じ型であることが分かります。
Coqは「型推論(type inference)」という機構を持っていて、これを使い、Xとxとcountの型が何であるべきかを、その使われ方から導き出します。
例えば、Xがconsの最初の引数として使われたことがあれば、consが最初の引数としてTypeを期待しているのでそれに違いありません。
さらにcountが0やSとマッチされているので、それはnatに違いない、といった具合です。
このパワフルな機構の存在は、型情報を常にそこら中に書かなければならないわけではない、ということを意味します。
しかし、型を明示的に書くことは、ドキュメントとして、または整合性を確かめるという点で意味があるので、以降もほとんどは型を書いていきます。
これからは自分の書くコードで、型指定を書くところ、書かないところのバランスを考えていく必要があります（多すぎればコードが目障りな型指定で読みにくくなりますし、少なすぎるとプログラムを読む人に型推論させなければならなくなります）。
多相的な関数を使うには、通常の引数に加えて型を一つ以上渡さなければなりません。
例えば、repeat関数内での再帰呼び出しには、型Xとして渡されたものをそのまま渡すことになります。
しかしrepeatの二つ目の引数がX型である以上、最初の引数は明らかにX以外あり得ないのではないか、とも考えられます。
それならばなぜわざわざそれを書く必要があるのでしょう。
幸いなことに、Coqではこの種の冗長性を避けることができます。
型を引数に渡すところではどこでも「穴(hole)」_を書くことができるのです。
これは「ここにあるべきものを見つけてください」という意味です。
もう少し正確に言うと、Coqが_を見つけると、手近に集められる情報を集めて「単一化(unify)」します。
集められる情報は、適用されている関数の型や、その適用が現れている文脈から予想される型などですが、それを使って_と置き換えるべき具体的な型を決定するのです。
これを聞くと、型推論と同じじゃないかと思われるかもしれません。
実際、この二つの機能は水面下にあるメカニズムではつながっています。
次のように単に引数の型を省略する代わりに
repeat' X x count : list X :=
このように、型を_で書くことができるということです。
repeat' (X : _) (x : _) (count : _) : list X :=
いずれも、Coqに、欠落している情報を推論させるもので、ちょうど引数を構成することに相当します。
穴を使うと、repeat関数は以下のように書けます。
repeat' X x count : list X :=
repeat' (X : _) (x : _) (count : _) : list X :=
Fixpoint repeat'' X x count : list X :=
match count with
| 0 => nil _
| S count' => cons _ x (repeat'' _ x count')
end.
この例では、Xを_に省略することをあまりしていません。
しかし多くの場合、入力の容易さと読みやすさの両方で違いが現れます。
例えば、1,2,3の三つの数値を保持するリストを書きたい場合を考えてみましょう。
以下のように書く代わりに...
...穴を使って以下のように書くことができます。
さらに先に進めて、プログラムにほとんど_を書かなくてすむように、特定の関数の引数については「常に」型推論するよう指定できます。
Arguments命令は関数（や構成子）に対し、引数の名前を波括弧で覆うことで暗黙のものとすることができます。
（構成子でよく起こるのですが、もし名前がない変数を暗黙にしたい場合はワイルドカードパターンとして_を指定します。）
Now, we don't have to supply type arguments at all:
また、関数定義の中で、引数を暗黙のものにすることもできます。
その際は、次のように引数を丸括弧の代わりに波括弧で囲みます。
Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
match count with
| 0 => nil
| S count' => cons x (repeat''' x count')
end.
（ここで注意してほしいのは、再帰呼び出しのrepeat'''ではもうすでに型を引数で指定していない、ということです。
また、渡そうとするのは誤りとなります。）
これからは、定義時に指定する後者の書き方をできるだけ使っていくことにします。
ただし、Inductiveの構成子ではArgumentsを明示的に書くようにします。
というのも、帰納型のパラメータを暗黙にするのは、型そのもののパラメータを暗黙にするのであって、構成子のパラメータだけを暗黙にするわけではないからです。
例えば、以下のようにlistを定義したとしましょう。
Because X is declared as implicit for the entire inductive
definition including list' itself, we now have to write just
list' whether we are talking about lists of numbers or booleans
or anything else, rather than list' nat or list' bool or
whatever; this is a step too far.
Let's finish by re-implementing a few other standard list
functions on our new polymorphic lists...
Fixpoint app {X : Type} (l1 l2 : list X)
: (list X) :=
match l1 with
| nil => l2
| cons h t => cons h (app t l2)
end.
Fixpoint rev {X:Type} (l:list X) : list X :=
match l with
| nil => nil
| cons h t => app (rev t) (cons h nil)
end.
Fixpoint length {X : Type} (l : list X) : nat :=
match l with
| nil => 0
| cons _ l' => S (length l')
end.
Example test_rev1 :
rev (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity. Qed.
Example test_rev2:
rev (cons true nil) = cons true nil.
Proof. reflexivity. Qed.
Example test_length1: length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity. Qed.
引数を暗黙的に宣言することには、小さな問題が一つあります。
時折、Coqが型を特定するために必要な情報を十分に集められない時があるのです。
そういう場合には、その時だけ明示してやります。
例えば、もし次のように書いたとします。
（Definitionの前にあるFailという修飾子は、実行すると失敗することを表します。
この修飾子はどのコマンドにも使えます。
もし指定したコマンドが失敗すると、Coqがエラーメッセージを出しますが、処理を続行します。）
この定義ではCoqがエラーを出します。
nilにどんな型を与えれば良いかわからないからです。
このようなときは、型宣言を明示的に行うことができます（これによってnilを何に「適用したか」という情報が与えられます）。
それとは別に、関数名の前に@を付けることで暗黙的に宣言された引数を明示的に与えることができます。
引数の構成と暗黙の引数をつかうことで、リストに関する便利な表記法を定義できます。
コンストラクタの型引数を暗黙的に記述すれば、Coqはその表記法を使ったときに型を自動的に推論してくれます。
Notation "x :: y" := (cons x y)
(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
(at level 60, right associativity).
これで、我々の望む書き方ができるようになりました。
練習問題: ★★, standard, optional (poly_exercises)
Theorem app_nil_r : forall (X:Type), forall l:list X,
l ++ [] = l.
Proof.
Admitted.
Theorem app_assoc : forall A (l m n:list A),
l ++ m ++ n = (l ++ m) ++ n.
Proof.
Admitted.
Lemma app_length : forall (X:Type) (l1 l2 : list X),
length (l1 ++ l2) = length l1 + length l2.
Proof.
Admitted.
☐
Here are some slightly more interesting ones...
Exercise: 2 stars, standard, optional (more_poly_exercises)
Theorem rev_app_distr: forall X (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
Admitted.
Theorem rev_involutive : forall X : Type, forall l : list X,
rev (rev l) = l.
Proof.
Admitted.
☐
次も同様に、前の章で作った数値の対を多相的な対に一般化することを考えます。
これは「直積(products)」とも呼ばれます。
リストと同様、型引数を暗黙にし、その表記法を定義します。
また、直積「型」の、より標準的な表記法も登録しておきます。
（type_scopeというアノテーションは、この省略形が、型を解析する際のみ使われることを示しています。
これによって、*が乗算の演算子と衝突することを避けています。
最初のうちは、(x,y)とX*Yの違いに混乱するかもしれません。
覚えてほしいのは、(x,y)が対の「値」を二つの値から構成するもので、X*Yは対の「型」を二つの型から構成するものだということです。
値xがX型で、値yがY型なら、値(x,y)はX*Y型となります。
対の最初の要素、2番目の要素を返す射影関数は他のプログラミング言語で書いたものと大体同じになります。
Definition fst {X Y : Type} (p : X * Y) : X :=
match p with
| (x, y) => x
end.
Definition snd {X Y : Type} (p : X * Y) : Y :=
match p with
| (x, y) => y
end.
次の関数は二つのリストを引数にとり、一つの"対のリスト"を作成します。
他の関数型言語でzip関数と呼ばれているものですが、ここではCoqの標準ライブラリに合わせる形でcombineと呼ぶことにします。
Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
: list (X*Y) :=
match lx, ly with
| [], _ => []
| _, [] => []
| x :: tx, y :: ty => (x, y) :: (combine tx ty)
end.
練習問題: ★, standard, optional (combine_checks)
- 関数combineの型は何でしょう （Check @combineの出力結果は？）
- それでは
Compute (combine [1;2] [false;false;true;true]).は何を出力する？
練習問題: ★★, standard, recommended (split)
Fixpoint split {X Y : Type} (l : list (X*Y))
: (list X) * (list Y)
. Admitted.
Example test_split:
split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof.
Admitted.
☐
最後に、多相的なオプションに取り組みます。
この型は、前の章のnatoptionを一般化したものになります。
（optionは標準ライブラリで定義されていて、後ほどそちらを使いたいので、ここでは定義をモジュール内に入れています。）
Module OptionPlayground.
Inductive option (X:Type) : Type :=
| Some (x : X)
| None.
Arguments Some {X} _.
Arguments None {X}.
End OptionPlayground.
nth_error関数を、色々な型のリストで使えるように定義し直しましょう。
Fixpoint nth_error {X : Type} (l : list X) (n : nat)
: option X :=
match l with
| [] => None
| a :: l' => if n =? O then Some a else nth_error l' (pred n)
end.
Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [[1];[2]] 1 = Some [2].
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [true] 2 = None.
Proof. reflexivity. Qed.
再び、暗黙の引数を明示してみましょう。
関数名の前に@をつければいいのでしたね。
Check @hd_error.
Example test_hd_error1 : hd_error [1;2] = Some 1.
Admitted.
Example test_hd_error2 : hd_error [[1];[2]] = Some [1].
Admitted.
☐
他の多くの近代的なプログラミング言語（MLやHaskell、Scheme、Scala、Clojureなどの関数型言語を含む）同様、Coqは関数を第1級に属するものとして取り扱います。
第1級に属するということは、他の関数の引数として渡したり、結果として返したり、データ構造の中に含めたりできる、ということです。
関数を操作する関数を、一般に「高階(higher-order)」関数と呼びます。
例えば次のようなものです。
Check @doit3times.
Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.
Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.
次に紹介するのは、もっと有用な高階関数です。
これは、X型のリストと、Xについての述語（Xを引数にとり、boolを返す関数）を引数にとり、リストの要素に「フィルター(filter)」をかけて、述語の結果がtrueとなった要素だけのリストを返す関数です。
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.
Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.
Definition length_is_1 {X : Type} (l : list X) : bool :=
(length l) =? 1.
Example test_filter2:
filter length_is_1
[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
= [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.
Definition countoddmembers' (l:list nat) : nat :=
length (filter oddb l).
Example test_countoddmembers'1: countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2: countoddmembers' [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3: countoddmembers' nil = 0.
Proof. reflexivity. Qed.
少し悲しいことに、上の例では、filterの引数とするために、多分以降全く使われないであろう関数length_is_1をわざわざ定義して名付けなければなりませんでした。
このようなことは、この例だけの問題ではありません。
高階関数を使うときは、引数として以降では全く使わない「一度きり」の関数を渡すことがよくあります。
こういう関数にいちいち名前を考えるのは、退屈以外の何物でもありません。
幸いなことに、いい方法があります。
関数を、トップレベルで宣言することも名前を付けることもなく、「その場で(on the fly)」作ることができるのです。
次はfilterの例を、無名関数を使って書き換えた例です。
Example test_filter2':
filter (fun l => (length l) =? 1)
[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
= [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.
練習問題: ★★, standard (filter_even_gt7)
Definition filter_even_gt7 (l : list nat) : list nat
. Admitted.
Example test_filter_even_gt7_1 :
filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
Admitted.
Example test_filter_even_gt7_2 :
filter_even_gt7 [5;2;6;19;129] = [].
Admitted.
☐
練習問題: ★★★, standard (partition)
partition : forall X : Type,
(X -> bool) -> list X -> list X * list X
Definition partition {X : Type}
(test : X -> bool)
(l : list X)
: list X * list X
. Admitted.
Example test_partition1: partition oddb [1;2;3;4;5] = ([1;3;5], [2;4]).
Admitted.
Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
Admitted.
☐
もう一つ、便利な高階関数として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.
これは、関数fとリスト l = [n1, n2, n3, ...] を引数にとり、関数fをlの各要素に適用した [f n1, f n2, f n3,...] というリストを返します。
例えばこのようなものです。
入力されるリストの要素の型と、出力されるリストの要素の型は同じである必要はありません。
mapは、2つの型変数XとYを取ります。
これにより、次の例では、数値のリストと、数値を受け取りbool値を返す関数から、bool型のリストを返しています。
Example test_map3:
map (fun n => [evenb n;oddb n]) [2;1;2;5]
= [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity. Qed.
Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
map f (rev l) = rev (map f l).
Proof.
Admitted.
☐
練習問題: ★★, standard, recommended (flat_map)
flat_map (fun n => [n;n+1;n+2]) [1;5;10]
= [1; 2; 3; 5; 6; 7; 10; 11; 12]
Fixpoint flat_map {X Y: Type} (f: X -> list Y) (l: list X)
: (list Y)
. Admitted.
Example test_flat_map1:
flat_map (fun n => [n;n;n]) [1;5;4]
= [1; 1; 1; 5; 5; 5; 4; 4; 4].
Admitted.
☐
Definition option_map {X Y : Type} (f : X -> Y) (xo : option X)
: option Y :=
match xo with
| None => None
| Some x => Some (f x)
end.
練習問題: ★★, standard, optional (implicit_args)
さらにパワフルな高階関数foldに話を移します。
この関数はGoogleの分散フレームワーク「map/reduce」でいうところの「reduce」操作の元になったものです。
Fixpoint fold {X Y: Type} (f: X->Y->Y) (l: list X) (b: Y)
: Y :=
match l with
| nil => b
| h :: t => f h (fold f t b)
end.
直観的にfoldは、与えられたリストの各要素の間に、与えられた二項演算子fを挟み込むように挿入していくような操作です。
例えば、 fold plus [1,2,3,4] は、直感的に1+2+3+4と同じ意味です。
ただし正確には、二番めの引数に、fに最初に与える"初期値"が必要になります。例えば
fold plus [1;2;3;4] 0
は、次のように解釈されます。
1 + (2 + (3 + (4 + 0)))
もう少し例を見ていきましょう。
fold plus [1;2;3;4] 0
1 + (2 + (3 + (4 + 0)))
Check (fold andb).
Example fold_example1 :
fold mult [1;2;3;4] 1 = 24.
Proof. reflexivity. Qed.
Example fold_example2 :
fold andb [true;true;false;true] true = false.
Proof. reflexivity. Qed.
Example fold_example3 :
fold app [[1];[];[2;3];[4]] [] = [1;2;3;4].
Proof. reflexivity. Qed.
練習問題: ★, advanced (fold_types_different)
☐
これまで見てきた高階関数は、ほとんどが関数を引数にとるものでした。
ここでは、関数が別の関数の戻り値になるような例を見ていきましょう。
まず、（型Xの）値xを引数としてとり、「nat型の引数からX型の戻り値を返す関数」を返す関数を考えます。
返す関数は、与えられたnat型の引数に関係なく、生成時に与えられた値xを常に返すものです。
Definition constfun {X: Type} (x: X) : nat->X :=
fun (k:nat) => x.
Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.
Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.
実は、我々がすでに見た、複数の引数を持つ関数は、関数をデータとして渡すサンプルになっているのです。
どういうことかは、plus関数の型を思い出せば分かります。
->は、型同士の二項演算子です。
さらに、この演算子は右結合であるため、plus関数の型はnat -> (nat -> nat)の省略です。
これをよく読むと「plusはnat型の引数を一つ取り、引数がnat型一つでnat型を返す関数を返す」となります。
以前の例ではplusに二つの引数を一緒に与えていましたが、もし望むなら最初の一つだけを与えることもできます。
これを「部分適用(partial application)」といいます。
Definition plus3 := plus 3.
Check plus3.
Example test_plus3 : plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' : doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' : doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.
Definition fold_length {X : Type} (l : list X) : nat :=
fold (fun _ n => S n) l 0.
Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.
fold_lengthが正しいことを証明しなさい。
（ヒント：reflexivityはsimplよりも簡単化を進めます。
そのため、simplでは何も起こらないのにreflexivityが証明してしまうようなゴールもありえます。）
☐
☐
練習問題: ★★, advanced (currying)
カリー化は以下のように定義できます。
練習問題として、その逆のprod_uncurryを定義し、二つの関数が互いに逆関数であることを証明しなさい。
As a (trivial) example of the usefulness of currying, we can use it
to shorten one of the examples that we saw above:
考える練習: 次のコマンドを実行する前に、prod_curryとprod_uncurryの型を考えなさい。
Check @prod_curry.
Check @prod_uncurry.
Theorem uncurry_curry : forall (X Y Z : Type)
(f : X -> Y -> Z)
x y,
prod_curry (prod_uncurry f) x y = f x y.
Proof.
Admitted.
Theorem curry_uncurry : forall (X Y Z : Type)
(f : (X * Y) -> Z) (p : X * Y),
prod_uncurry (prod_curry f) p = f p.
Proof.
Admitted.
☐
練習問題: ★★, advanced (nth_error_informal)
Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
match l with
| [] => None
| a :: l' => if n =? O then Some a else nth_error l' (pred n)
end.
forall X n l, length l = n -> @nth_error X l n = None
☐
以降の練習問題では、自然数を定義する他の方法として、「チャーチ数(Church numerals)」と呼ばれる、数学者アロンゾ・チャーチ(Alonzo Church)にちなむ方法を見ていきます。
自然数nを、関数fを取りfをn回繰り返し適用するものとして表現します。
ではこの方法でどのように数値を表すのか見ていきます。
fを1回だけ適用するというのは、単に適用するだけです。
つまり、次のようになります。
zeroの定義は少し変わっています。
0回関数を適用するとは一体どういうことでしょうか？
答えは簡単です：単に引数に何もしなければいいのです。
一般に、数値nはfun X f x => f (f ... (f x) ...)のような形で、fがn回出現するものになります。
つまり、以前定義したdoit3times関数は実はちょうどチャーチ数での3を表していることになります。
以下の関数の定義を完成させなさい。
また、reflexivityを使えば証明できる以下の単体テストを通過することを確かめなさい。
Definition succ (n : cnat) : cnat
. Admitted.
Example succ_1 : succ zero = one.
Proof. Admitted.
Example succ_2 : succ one = two.
Proof. Admitted.
Example succ_3 : succ two = three.
Proof. Admitted.
. Admitted.
Example succ_1 : succ zero = one.
Proof. Admitted.
Example succ_2 : succ one = two.
Proof. Admitted.
Example succ_3 : succ two = three.
Proof. Admitted.
☐
二つの自然数の加算：
Definition plus (n m : cnat) : cnat
. Admitted.
Example plus_1 : plus zero one = one.
Proof. Admitted.
Example plus_2 : plus two three = plus three two.
Proof. Admitted.
Example plus_3 :
plus (plus two two) three = plus one (plus three three).
Proof. Admitted.
. Admitted.
Example plus_1 : plus zero one = one.
Proof. Admitted.
Example plus_2 : plus two three = plus three two.
Proof. Admitted.
Example plus_3 :
plus (plus two two) three = plus one (plus three three).
Proof. Admitted.
☐
乗算：
Definition mult (n m : cnat) : cnat
. Admitted.
Example mult_1 : mult one one = one.
Proof. Admitted.
Example mult_2 : mult zero (plus three three) = zero.
Proof. Admitted.
Example mult_3 : mult two three = plus three three.
Proof. Admitted.
. Admitted.
Example mult_1 : mult one one = one.
Proof. Admitted.
Example mult_2 : mult zero (plus three three) = zero.
Proof. Admitted.
Example mult_3 : mult two three = plus three three.
Proof. Admitted.
☐
冪：
（ヒント：ここでは多相性が非常に重要な役割を果たします。
しかし、適切な型を指定するのは結構面倒です。
もし"Universe inconsistency"というエラーに遭遇した場合、他の型を試してみてください。
cnatに関してcnatで繰り返すのは問題を起こすものなのです。）
Definition exp (n m : cnat) : cnat
. Admitted.
Example exp_1 : exp two two = plus two two.
Proof. Admitted.
Example exp_2 : exp three zero = one.
Proof. Admitted.
Example exp_3 : exp three two = plus (mult two (mult two two)) one.
Proof. Admitted.
☐