Idrisでふんわり眺める依存型

2022/07/04

どうも，よわよわエンジニアです．前回の記事では，TAPLを読んで型システムに入門しました．

その記事の中で，1つ腑に落ちなかったことがあります．そう， 依存型 です．

依存型は，TAPLでも発展的内容として深く触れないんだっピ…

よわよわエンジニアがTAPL（型システム入門）を読んだら

依存型は，関数型，全称型，型演算子に続いてラムダキューブを完成させる最後のピースでした．

それが埋まらず，日々ストレスを貯める一方だったのですが，はてブのコメントで「実戦で色々試したくなったらIdrisがあるよ!!」と親切な方が教えてくださったので，

依存型の雰囲気を味わうためにIdrisへふんわり入門してみます．

依存型ってなんやねん
型にプログラムが書けるってどういうこと
プログラミングと証明に何の関係があるんだ

といった疑問を解決するまでの日記です．

Idrisとは

Idris = Haskell + 依存型

と言われているそうです．

Haskellとは，言わずとしれた関数型プログラミング言語です．え？ Haskellを知らないからこの先読めるか不安？ ハハハ， 私もHaskellまったくわからん ので大丈夫ですよ（？）

依存型とは，TAPLによれば「項でインデックス付けされた型」であり，型の中にプログラムが書けると言っています．なんのこっちゃ．さらに依存型は，定理証明支援系とも関係があるとのことです．はえー．

というわけで，試しにいくつかの証明をIdrisで書いてみたいと思います．がんばるぞ．

$ idris --version
1.3.4-git:PRE

ウォーミングアップ：モーダスポネンス

最初は依存型を使わずに，簡単な命題を証明してみます．

以下の例を見てください．

俺，戦争から戻ったら結婚するんだ……
俺，戦争から戻ったんだ……
俺，結婚するんだ……

ちょっと長いので，以下の記号で短く書き換えてみます．

戦争から戻る： $p$
結婚する： $q$
ならば（たら）： $\rightarrow$

すると

$p \rightarrow q$
$p$
$q$

となり，もうちょっと短く書くと

((p \rightarrow q) かつ p) \rightarrow q

と表現できます．これが俺くんによる主張の論理構造であり， それを正しいと証明するIdrisのコードは以下のとおりです．

modusPonens : ((p -> q), p) -> q
modusPonens (hpq, hp) = hpq hp

どういうことなのか，順を追って説明させてください．

まずは構文

上記のコードではmodusPonensという名前の関数を定義しています．関数定義の構文は以下のようになっています．

関数名 : 関数の型
関数名 引数1 引数2 … = 関数のプログラム本体

つまり，

関数名：modusPonens
関数の型：((p -> q), p) -> q
第1引数：(hpq, hp)
関数のプログラム本体：hpq hp

です．

関数型は引数 -> 戻り値と書きます．p -> qは，「p型の値を受け取ってq型の値を返す関数の型」です．

タプル型は(要素1, 要素2…)と書きます．

第1引数(hpq, hp)では，タプルを分割して受け取っています．ちなみに引数名のhpqは「仮定（h ypothesis）の $p \rightarrow q$ 」の略として命名しました．

プログラム本体のhpq hpは関数呼び出しで，CやJavaScript風に書くとhpq(hp)です．

カリー＝ハワード同型対応

ここまでで，

プログラムを書くことが証明にどう関係するのか？

と思われたかもしれません．

実を言うとこのコードは， 命題： $((p \rightarrow q) かつ p) \rightarrow q$ をIdrisの型で，またその証明をIdrisのプログラムで表現したもの になっているんです．

modusPonens : ((p -> q), p) -> q
modusPonens (hpq, hp) = hpq hp

以下のような論理とコードの対応関係は，カリー＝ハワード同型対応として知られています．

論理	Idris
命題	型
証明	プログラム
かつ	タプル`(要素1, 要素2…)`
$\rightarrow$ （ならば）	関数型`引数 -> 戻り値`

つまり今回の命題は

論理	Idris
$((p \rightarrow q) かつ p) \rightarrow q$	`((p -> q), p) -> q`

と対応します．

カリー＝ハワード同型対応により， ある命題の証明を書く のは， ある型のプログラムを書く のと同じだとわかります．示したい命題に対応する型のプログラムが書ければ，もとの命題を示したことになるわけです．

コードができるまで

以上を踏まえて，今回のコードが書かれるまでを追ってみます．

示したい命題： $((p \rightarrow q) かつ p) \rightarrow q$ にカリー＝ハワード同型対応する型は((p -> q), p) -> qです．

これは関数型なので，そのような型が付くmodusPonensという関数を実装できれば証明完了です．ここまでで，以下のところまで書けます．

modusPonens : ((p -> q), p) -> q
modusPonens ...ここを埋める...

肝心のmodusPonensの実装を考えてみます．ここでの目標は「q型の値」を返すことです．いま，「(p -> q)型の値」と「p型の値」がもらえるので，単純にpを(p -> q)へ渡してしまえば「q型の値」が得られます． これが証明です

modusPonens : ((p -> q), p) -> q
modusPonens (hpq, hp) = hpq hp

hpqやhpにどのような値が来ようが，modusPonensは100％確実にq型の値を返します．このことは，型検査で容易に確かめられます．

そして実際に，このコードをidris --checkで型検査すると成功しますので，先程の論理構造は正しいと証明されました．ご結婚おめでとうございます．

ウォーミングアップまとめ

今回のお題は自明すぎて，

なぜこんなに回りくどいことをする必要があるのか？

と思われたかもしれません．簡単すぎて依存型の出番もなく，イマイチしっくりきていないのも事実です．

というわけで，もうちょっと難しい 実践編 で依存型に触れてみましょう．

実践編：高校数学

想像してください．我々は高校生で，今は数学の試験中です．

問題

$n$ が自然数であるとき，次の等式が成り立つことを証明せよ．
$1 + 2 + 3 + \cdots + n = \frac{n(n + 1)}{2}$
出典: https://www.geisya.or.jp/~mwm48961/kou2/inductive_method4.htm#A1

――――――

――――

――

よし， 「Idrisで回答するな」 とは書かれていない．

Idrisで証明していく

総和関数の実装

はじめに，問題中にある総和関数 $1 + 2 + 3 + \cdots + n$ を次のように実装します．

sum : Nat -> Nat
sum Z = Z
sum (S k) = S k + sum k

ここでは，Idrisの標準ライブラリにある自然数型Natを使用しています．Zは $0$ の値，Sは後者関数で $+ 1$ の意味です．例えば，S S Zは $2$ を表します．

総和関数sumは，「自然数n」を受け取って，「 $0$ からnまでの合計の自然数」を返すため，Nat -> Nat型が付きます．

プログラム本体は2つのパターンで書いています．sum Z = Zのパターンでは，

sum(0) = 0

を定義しています．自明ですね．

sum (S k) = S k + sum kのパターンでは，

sum(n) = n + sum(n - 1)

のように，再帰的な定義を採用しています．sumの第1引数をS kの形で受け取っているので，kは第1引数 - 1の数になるのがポイントです．

実際に動くのかIdrisのREPLで確かめてみます．

*> sum 0
0 : Nat

*> sum 2
3 : Nat

*> sum 10
55 : Nat

いいですね！

依存型で命題を書く

ではさっそく，総和関数を用いて命題を型で表しましょう，と言いたいところですが，ここでちょっとおまじないをさせてください．等式の両辺を2倍して分母を払います．

(1 + 2 + 3 + \cdots + n) \times 2 = n(n + 1)

というのも，命題に割り算を使ってしまうと証明が結構複雑になりそうだからです．ゼロ除算やら切り捨てやらを考えないためです．

さて，では気を取り直して，今度こそ上記の命題を型で表してみましょう． 依存型を使用して 以下のように書けます．

(n : Nat) -> (sum n) * 2 = n * (n + 1)

日本語で読むと「ある自然数nを受け取り，『(sum n) * 2型とn * (n + 1)型が等しいという型』を返す関数型」となります．

注目すべきは，nがNat型の値であることです．この関数型の 戻り値の型(sum n) * 2 = n * (n + 1)は，引数のnという値に依存しています． つまり，プログラム（値）に依存した型，依存型です．¹

返り値の型を更に詳しく見て行きましょう．まず，=というのは「両辺の型が等しいこと」を表す，主に証明系で使われる型です．次に，我々が普段プログラムの世界で使用している+と*ですが，自然数の加算・乗算として型の中に書けちゃいます．また，先ほど我々が定義した，正真正銘プログラムであるはずのsum関数もまた，しれっと型の中に書けています．依存型の中では，型とプログラムのどっちを書いているのか混乱しますね……．

Natという自然数全体ではなく，ある特定の自然数nに型が依存することで，(sum n) * 2 = n * (n + 1)のような等式を表現できました．

これが依存型のパワー……！この驚くべき表現力によって様々な命題を型に変換し，ついには数学の難問もコード上で証明してしまったというのですからヤバすぎます．

証明を書こう

それでは(n : Nat) -> (sum n) * 2 = n * (n + 1)型の値を書いていきます．これは関数型なので関数を宣言するために

p: (n : Nat) -> (sum n) * 2 = n * (n + 1)
p ...ここを埋める...

と書きます．pは p roposition（命題）の略として命名しました．

ここでは数学的帰納法を用います．つまり関数pが呼び出されるパターンを，第1引数Natによって，ZとS kに分けて考えていきます．

`p Z`の場合

\begin{aligned} sum(0) \times 2 &= 0 \times (0 + 1) \\ 0 \times 2 &= 0 \times 1 \\ 0 &= 0 \\ \end{aligned}

なので自明ですね．このような場合次のように書きます．

 p: (n : Nat) -> (sum n) * 2 = n * (n + 1)
+p Z = Refl

Reflという名前は反射関係（reflexive relation）に由来すると思われます．

`p (S k)`の場合

帰納法なので，p kを仮定してp (S k)を示します．

とりあえず帰納法の仮定inductiveHypothesisをローカル変数で宣言します．あとから必要になるはず．

 p: (n : Nat) -> (sum n) * 2 = n * (n + 1)
 p Z = Refl
+p (S k) =
+  let inductiveHypothesis = p k in
+    ...ここを埋める...

そしてここから証明を書いていくわけですが，

今回は，これまでの 実際にプログラムを書く 方法ではなく タクティク を連ねることで証明を行います．

タクティクとは証明戦略とも呼ばれ，型検査器に様々な指示を与えます．例えば，命題の式を整理したり変形したりできます．（すみません，ここらへんよくわかっていません）

この指示を繰り返すことで型検査器を誘導し，「あ，この命題は自明っす」と言わせてみましょう．

まず，コードを次のように変更します．

 p: (n : Nat) -> (sum n) * 2 = n * (n + 1)
 p Z = Refl
 p (S k) =
   let inductiveHypothesis = p k in
-    ...ここを埋める...
+    ?proofP

これにより，Idrisに「proofP部分の証明を手伝ってや〜」と伝えられます．

REPLを起動して，:prove proofPでインタラクティブ証明モードを起動します．² 現在の証明の状態が以下のように表示されました．

----------                 Goal:                  ----------
{hole_0} : (k : Nat) -> (sum k * fromInteger 2 = k * (k + fromInteger 1)) -> S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (mult k (S (plus k 1))))

なにがなんだか

まぁ落ち着いてintrosという呪文（タクティク）を唱えます．すると

----------              Assumptions:              ----------
 k : Nat
 inductiveHypothesis : sum k * fromInteger 2 = k * (k + fromInteger 1)
----------                 Goal:                  ----------
{hole_2} : S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (mult k (S (plus k 1))))

仮定（Assumptions）が現れました．ここではkが自然数Natであることと，帰納法の仮定inductiveHypothesisが使えます．inductiveHypothesisの型sum k * fromInteger 2 = k * (k + fromInteger 1)は，ちゃんとp k型になっています．あたりまえですね．

示したい命題（Goal）は，ちょっと複雑ですがp (S k)になっています．Idrisがある程度式変形してくれているのでごちゃごちゃしているだけです．数式で書いて元のp (S k)に戻してみましょう．

\begin{aligned} 2(k + sum(k)) + 1 + 1 &= k + 1 + k(k + 1 + 1) + 1 \\ 2k + 2sum(k) + 1 + 1 &= k + 1 + k(k + 1 + 1) + 1 \\ 2k + 2sum(k) + 2 &= k + 1 + k(k + 1 + 1) + 1 \\ 2(sum(k) + (k + 1)) &= k + 1 + k(k + 1 + 1) + 1 \\ 2sum(k + 1) &= k + 1 + k(k + 1 + 1) + 1 \\ 2sum(k + 1) &= k(k + 2) + (k + 2) \\ 2sum(k + 1) &= (k + 1)(k + 2) \\ \end{aligned}

よし，確かに戻りました．

さて，ここからの証明ではrewriteという呪文をめっちゃ唱えます．これは式変形を行ってくれるタクティクです．試しに1つ唱えてみましょう．rewrite sym (multRightSuccPlus k (k + 1))！

するとゴールのようすが…？

 ----------              Assumptions:              ----------
  k : Nat
  inductiveHypothesis : sum k * fromInteger 2 = k * (k + fromInteger 1)
 ----------                 Goal:                  ----------
-{hole_2} : S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (mult k (S (plus k 1))))
+{hole_3} : S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (plus k (mult k (plus k 1))))

変わった！右辺の一部で

k \times (1 + (k + 1)) \\ k + k(k + 1)

みたいな変形が起こりました．これを可能にしたのがIdrisの標準ライブラリにあるmultRightSuccPlusという定理です．

multRightSuccPlus : (left, right : Nat) -> left * (S right) = left + (left * right)
出典: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr#L526

multRightSuccPlusにkと(k + 1)を与えるとk * (S (k + 1)) = k + (k * (k + 1))型が返ります．rewriteは=型を受け取り，ゴールの中から右辺のパターンを見つけて左辺に書き換えます．ただし今回の場合は逆をやってほしかったので，symを使って等式の左右を反転しています．

sym : {left:a} -> {right:b} -> left = right -> right = left
出典: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Builtins.idr#L95

ちなみに，multRightSuccPlusの証明はもっと簡単な定理で構成されていて，それは更に簡単な定理で…というように続き，最終的には「自然数の定義より自明」となるところで終わります．

厳密な演繹をコマンドで簡単に実行できるのは便利ですね．

標準ライブラリには，他にも証明済みの定理がたくさん入っています．今回は，それらを使って式変形していくことで(左辺) = (右辺)を示せます．最終的な式変形は以下のとおりです．

                         S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (mult k (S (plus k 1))))
                         S (S (mult (plus k (sum k)) 2)) = S (plus (plus k 1) (plus k (mult k (plus k 1))))
                         S (S (mult (plus k (sum k)) 2)) = S (plus (plus k (mult k (plus k 1))) (plus k 1))
                         S (S (mult (plus k (sum k)) 2)) = S (plus (plus k (mult k (S k))) (S k))
                         S (S (mult (plus k (sum k)) 2)) = S (S (plus (plus k (mult k (S k))) k))
                         S (S (mult (plus k (sum k)) 2)) = S (S (plus k (plus k (mult k (S k)))))
                S (S (plus (mult k 2) (mult (sum k) 2))) = S (S (plus k (plus k (mult k (S k)))))
             S (S (plus (mult k 2) (mult k (plus k 1)))) = S (S (plus k (plus k (mult k (S k)))))
                  S (S (plus (mult k 2) (mult k (S k)))) = S (S (plus k (plus k (mult k (S k)))))
         S (S (plus (plus k (mult k 1)) (mult k (S k)))) = S (S (plus k (plus k (mult k (S k)))))
S (S (plus (plus k (plus k (mult k 0))) (mult k (S k)))) = S (S (plus k (plus k (mult k (S k)))))
         S (S (plus (plus k (plus k 0)) (mult k (S k)))) = S (S (plus k (plus k (mult k (S k)))))
                  S (S (plus (plus k k) (mult k (S k)))) = S (S (plus k (plus k (mult k (S k)))))
                  S (S (plus k (plus k (mult k (S k))))) = S (S (plus k (plus k (mult k (S k)))))

実行したrewriteは

rewrite sym (multRightSuccPlus k (k + 1)) -- 右辺の変形開始
rewrite plusCommutative (plus k (mult k (plus k 1))) (plus k 1)
rewrite plusCommutative 1 k
rewrite plusSuccRightSucc (plus k (mult k (S k))) k
rewrite plusCommutative k (plus k (mult k (S k)))
rewrite sym (multDistributesOverPlusLeft k (sum k) 2) -- 左辺の変形開始
rewrite sym inductiveHypothesis -- ここで帰納法の仮定を使った
rewrite plusCommutative 1 k
rewrite sym (multRightSuccPlus k 1)
rewrite sym (multRightSuccPlus k 0)
rewrite sym (multZeroRightZero k)
rewrite sym (plusZeroRightNeutral k)
rewrite plusAssociative k k (mult k (S k))

となりました．結論の等式が汚いのは，できるだけ少ないステップ数で証明を完了したかったからですごめんなさい．

まぁともかく，両辺が等しくなったのでtrivialタクティクを実行します．すると，示すべきゴールがなくなります．（つまり自明）

-Main.proofP> trivial
proofP: No more goals.

最後に満を持してqedコマンドを打てば……

-Main.proofP> qed
Proof completed!

――――――

――――

――

証明完了．

全域性チェック

おっと，重要なおまじないを忘れていました．コードの冒頭に以下の1行を追加します．

%default total

これにより，ファイル内のすべての関数定義でIdrisの全域性チェッカーが有効になります．

詳しくは割愛しますが，証明の場合分けが漏れていたり，再帰呼び出しの引数が減少していなかったりする場合に怒ってくれます．なので，とりあえずファイルの冒頭に書いておくと良いことあるお守りです．

ともあれ，全域性を保証することはできないので過信も禁物です．まぁ，関数の停止性を保証するなんて原理的に無理っぽいのはなんとなくわかりますよね．

実践編まとめ

最終的なコードは以下のようになりました．

%default total

sum : Nat -> Nat
sum Z = Z
sum (S k) = S k + sum k

p : (n : Nat) -> (sum n) * 2 = n * (n + 1)
p Z = Refl
p (S k) =
  let inductiveHypothesis = p k in
    ?proofP

---------- Proofs ----------

Main.proofP = proof
  intros
  rewrite sym (multRightSuccPlus k (k + 1)) -- transform right
  rewrite plusCommutative (plus k (mult k (plus k 1))) (plus k 1)
  rewrite plusCommutative 1 k
  rewrite plusSuccRightSucc (plus k (mult k (S k))) k
  rewrite plusCommutative k (plus k (mult k (S k)))
  rewrite sym (multDistributesOverPlusLeft k (sum k) 2)  -- transform left
  rewrite sym inductiveHypothesis
  rewrite plusCommutative 1 k
  rewrite sym (multRightSuccPlus k 1)
  rewrite sym (multRightSuccPlus k 0)
  rewrite sym (multZeroRightZero k)
  rewrite sym (plusZeroRightNeutral k)
  rewrite plusAssociative k k (mult k (S k))
  trivial

答案用紙に書くとこうなります．

教師は

答案で証明している型が，問題とカリー＝ハワード同型対応するか確かめる
答案をOCRしてidris --checkする

だけで採点が完了します．なお，最初から問題をIdrisで出題していればStep 1は不要になります．

どうですか，Idrisによりテスト回収〜返却までのリードタイムが大幅に短縮されそうです．したがって，テストが返ってくるまでの，あのイヤな数日感を過ごさなくて良くなるわけです．

また，表現が厳格なので「記述が微妙でバツをもらった」とか「教師によって採点の厳しさ・解釈が違う」ということもなくなります．（採点で使用するIdrisのバージョンは合わせておく必要があります）

これからは数学の授業をIdrisにしたほうが良いのかもしれません．

まとめ

Idrisにふんわり入門し，いろいろな証明を書いてみました．初めて定理証明支援系というものを触ってみましたが面白いですねこれ．

Idris歴3日なので，何か間違ったことを書いていればマサカリでご指摘ください．

ありがとうございました．

型は命題！（素振り）
型は命題！（素振り）
— 七十 (@sititou70) June 28, 2022

参考記事

プログラング言語Idrisに入門させたい（v0.9）
- 日本語，体系的，そして無料です．ここまでの入門テキストは，日本語では他に無い気がします．
- 本記事におけるウォーミングアップの題材はこちらを参考にしています．
- κeenさん，ありがとうございます．
Idrisの有界な自然数で遊んでみる(0)
- 先程の入門記事よりも証明について詳しく書かれています．実際のインタラクティブ証明器の操作方法なども書かれています．
- mod_poppoさん，ありがとうございます．
公式ドキュメント系（英語だけどわかりやすい）
- Theorem Proving
- Theorem Proving（チュートリアル）

フリー素材の出典

TAPL的にいうと，「 $\prod x:T_1.T_2$ という形を持つ依存関数型」でしょうか．詳しくはTAPL第1版第2刷 p.366を参照ください．↩
このモードは現在非推奨のようですが，推奨される新しいモードは情報が少なかったため，本記事ではいったん古い機能で入門しています．↩

Idrisでふんわり眺める依存型

Idrisとは

ウォーミングアップ：モーダスポネンス

まずは構文

カリー＝ハワード同型対応

コードができるまで

ウォーミングアップまとめ

実践編：高校数学

問題

Idrisで証明していく

総和関数の実装

依存型で命題を書く

証明を書こう

`p Z`の場合

`p (S k)`の場合

全域性チェック

実践編まとめ

まとめ

参考記事

フリー素材の出典

続けて読む…

よわよわエンジニアがTAPL（型システム入門）を読んだら

TypeScriptの型で素数を求めたい

TypeScriptにおける配列の共変性

TypeScriptで型レベルScheme

Gatsby製ブログで自然言語処理して関連記事を表示する

TypeScriptにおける代入可能関係の推移性

Idrisとは

ウォーミングアップ：モーダスポネンス

まずは構文

カリー＝ハワード同型対応

コードができるまで

ウォーミングアップまとめ

実践編：高校数学

問題

Idrisで証明していく

総和関数の実装

依存型で命題を書く

証明を書こう

p Zの場合

p (S k)の場合

全域性チェック

実践編まとめ

まとめ

参考記事

フリー素材の出典

続けて読む…

よわよわエンジニアがTAPL（型システム入門）を読んだら

TypeScriptの型で素数を求めたい

TypeScriptにおける配列の共変性

TypeScriptで型レベルScheme

Gatsby製ブログで自然言語処理して関連記事を表示する

TypeScriptにおける代入可能関係の推移性

`p Z`の場合

`p (S k)`の場合