プログラミング言語Idris自体についての詳しい話はここではしない。このブログの昔の記事で軽く紹介したかもしれないが他人の参考になるかは分からない。

この記事を読むにあたっては、

• ペアノ算術

は知ってないと厳しいと思われる。あとHaskell風の言語にも慣れていた方がいいか。

この記事で使うIdrisのバージョンは0.9.16である（執筆時点の最新版）。これと異なるバージョンだとコードの修正が必要かもしれない。

Idrisで自然数を表す型は Nat である。0 は Z，自然数 n の後続者(successor)は S n で表す。自然数 \(n\) を \(m\) 乗する関数はIdrisのPreludeで power という名前で定義されている。

Idrisは依存型を採用しているので、値に依存する型、例えば「n より小さい自然数の型」を定義できる。この型はIdrisでは Fin n という名前（この名前はもちろん有限集合(finite sets)に由来する）で呼ばれていて、標準ライブラリの Data.Fin モジュールで以下のように定義されている。（以前は Prelude に入っていたが追い出された。また、FZ, FS は以前はそれぞれ fZ, fS という名前だった。）

data Fin : (n : Nat) -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

具体的に Fin n がどういう値を持っているか見てみると、

• Fin Z という型は値を持たない(uninhabited)。
• Fin (S Z) (=Fin 1)という型は FZ という唯一の値を持つ。
• Fin (S (S Z)) (=Fin 2)という型は FZ, FS FZ という2種類の値を持つ。
• Fin 3 という型は FZ, FS FZ, FS (FS FZ) という3種類の値を持つ。

という具合だ。

さて、唐突だが自然数 \(k\) に \(2^k\) を対応させる関数の有界な自然数バージョンを作ってみよう。その関数は \(n\) 未満の自然数に \(2^n\) 未満の自然数を対応させるから、次のような型がつく。

finPower2 : {n:Nat} -> Fin n -> Fin (power 2 n)

\(n=0\) の場合、Fin 0 という型を持つ値は存在しないので、実装する必要がない。以下は全て \(n=\mathrm{S }m\) として考える。

Fin n という型の引数は、FZ か FS k のどっちかの形をしているはずなので、場合分けして実装してやる。

引数が FZ (=0) の場合は素朴に考えて2の0乗なので「1」に相当する FS FZ を返せば良い。

finPower2 {n=S m} FZ = FS FZ

のだが、これは型エラーが出る。

FZ は何らかの k について Fin (S k) という型を持っていて、FS は何らかの k' について Fin k' -> Fin (S k') という型を持っているので、FS FZ は何らかの k について Fin (S (S k)) という型を持つ。だが、ここで求められている型は Fin (power 2 n) である。

我々人間は、n は 0 でないから power 2 n は 2 以上であり、従って何らかの k について power 2 n = S (S k) と書けることを知っているが、Idrisのコンパイラはそんなことは知らない。よって、power 2 n が何らかの k について power 2 n = S (S k) と書けるという「証明」をコンパイラに与えないといけない。

準備として、2 の \(n\) 乗から 1 を引いた自然数を返す関数 power2m1 : Nat -> Nat を作る。

まず、\(n=0\) の場合、 \(2^0-1=0\) なので、

power2m1 Z = Z

と定める。

\(n = k+1\) の場合、 \(2^{k+1}-1 = 2\cdot 2^k-1 = 2\cdot (2^k-1)+1\) なので、

power2m1 (S k) = S (2 * power2m1 k)

と定める。

まとめると、次のようになる。

power2m1 : Nat -> Nat
power2m1 Z = Z
power2m1 (S k) = S (2 * power2m1 k)

この関数の重要な性質として S (power2m1 k) = power 2 k という等式があるわけだが、これは定義から直ちに明らかではないので、証明してやらないといけない。つまり、次の型を持つ関数を作る。

succPower2m1Power2 : (k : Nat) -> S (power2m1 k) = power 2 k

まず k がゼロの場合、S (power2m1 Z) = power 2 Z は計算すれば明らかなので（？）、

succPower2m1Power2 Z = Refl

と定める。（以前のIdrisでは反射律を表すタームは refl だったが、今は Refl となった）

次に \(k\) が \(k=m+1\) と書ける場合、帰納法の仮定は succPower2m1Power2 m : S (power2m1 m) = power 2 m である。これに inductiveHypothesis と名前を付けておく。

succPower2m1Power2 (S m) =
  let inductiveHypothesis = succPower2m1Power2 m
  in ?proof1

で、肝心の証明だが、「後回し」にする。証明の部分に ?[名前] と書いておくと、Idrisの証明支援機能でコマンドを打ちながら証明をつけられる。もちろん、以前の記事でやったように、直接ゴリゴリ証明を書いておくこともできる。

本題に戻ろう。finPower2 {n=S m} FZ の定義をしているのだった。

有界な自然数の「1」を表す FS FZ という項には Fin (S (S (ほにゃらら))) の型がつく。一方、必要なのは Fin (power 2 n) もとい Fin (power 2 (S m)) という型のついた項である。

そこで、S (S (ほにゃらら)) = power 2 (S m) となるほにゃららを与えてやれば良いが、それはさっき作った power2m1 関数を使って ほにゃらら = 2 * power2m1 m となる。つまり、次の等式が成り立つ。

S (S (2 * power2m1 m)) = power 2 (S m)

「成り立つ」と口で言ってもしょうがないので、Idrisのコンパイラに分かるように証明を書かないと行けない。まあ、これも後回しにしよう。

p : S (S (2 * power2m1 m)) = power 2 (S m)
p = ?proof2

この等式から、Fin (S (S (2 * power2m1 m))) -> Fin (power 2 (S m)) という関数を作るには、標準ライブラリにある

replace : {P : a -> Type} -> x = y -> P x -> P y

という関数を使って

f : Fin (S (S (2 * power2m1 m))) -> Fin (power 2 (S m))
f = replace {P=Fin} p

とすればよい。

まとめると、finPower2 の FZ の場合は

finPower {n = S m} FZ = f (FS FZ)
  where
    p : S (S (2 * power2m1 m)) = power 2 (S m)
    p = ?proof2
    f : Fin (S (S (2 * power2m1 m))) -> Fin (power 2 (S m))
    f = replace {P=Fin} p

と書ける。ただし、?proof2 には後で証明をつける。

次に、finPower2 (FS k) の場合を考える。素朴に考えれば、finPower2 k を2倍してやればよい。

finPower {n = S m} (FS k) = let x = finPower2 k
                            in x + x

ちなみに、有界な自然数に対する加法 + は、Data.Fin モジュールで

(+) : Fin n -> Fin m -> Fin (n + m)

と定義されている。

が、やはりというか、このままだと型が合わない。必要な型は Fin (power 2 n) もとい Fin (power 2 (S m)) だが、x + x の型は Fin (power 2 m + power 2 m) である。もちろん、我々は等式 power 2 (S m) = power 2 m + power 2 m が成り立つことを知っているので、これは正しい型だと分かるのだが、コンパイラはそうではない。

そこで、また、等式 power 2 (S m) = power 2 m + power 2 m の証明を与えてやって、replace 関数で型を合わせてやる。具体的には次のようなコードになる。

finPower2 {n = S m} (FS k) = let x = finPower2 k
                             in replace p (x + x)
  where
    p : (power 2 m) + (power 2 m) = power 2 (S m)
    p = ?proof3

肝心の証明は例によって後回しである。

ここまでで書いたコードをまとめると以下のようになる。FinPower2.idr という名前で保存しよう。

import Data.Fin

power2m1 : Nat -> Nat
power2m1 Z = Z
power2m1 (S k) = S (2 * power2m1 k)

succPower2m1Power2 : (k : Nat) -> S (power2m1 k) = power 2 k
succPower2m1Power2 Z = Refl
succPower2m1Power2 (S m) =
  let inductiveHypothesis = succPower2m1Power2 m
  in ?proof1

finPower2 : {n : Nat} -> Fin n -> Fin (power 2 n)
finPower2 {n = S m} FZ = f (FS FZ)
  where
    p : S (S (2 * power2m1 m)) = power 2 (S m)
    p = ?proof2
    f : Fin (S (S (2 * power2m1 m))) -> Fin (power 2 (S m))
    f = replace {P=Fin} p
finPower2 {n = S m} (FS k) = let x = finPower2 k
                             in replace p (x + x)
  where
    p : (power 2 m) + (power 2 m) = power 2 (S m)
    p = ?proof3

続き：Idrisの有界な自然数で遊んでみる(1) — 証明をつける