みなさん、自然数というと、何を思い浮かべますか?
まずは、ゼロですよね。(本記事では自然数はゼロを含むものとします。異論は認めません)
他にどんな自然数があるのか、よく分からないんですが、ゼロの次にくる自然数があるような気がします。その次にくる自然数もあるような気がします。
もっと言うと、どんな自然数に対しても、それの次の自然数があるような気がします。
これを、Rustのenum型で表すと次のようになります。
#![allow(dead_code)]
use std::rc::Rc;
#[derive(Clone, Debug)]
enum Nat {
O,
S(Rc<Nat>),
}
ここで、ゼロをO, なにかの次の自然数をSで表しました。
つまり、
| アラビア数字 | Nat |
|---|---|
| 0 | Nat::O |
| 1 | Nat::S(Rc::new(Nat::O)) |
| 2 | Nat::S(Rc::new(Nat::S(Rc::new(Nat::O)))) |
| ... | ... |
と表せています。
Nat::S(Rc::new(...)) はめんどくさいので、succというメソッドを生やしましょう。
impl Nat {
fn succ(n: Nat) -> Nat {
Nat::S(Rc::new(n))
}
}
| アラビア数字 | Nat |
|---|---|
| 0 | Nat::O |
| 1 | Nat::succ(Nat::O) |
| 2 | Nat::succ(Nat::succ(Nat::O)) |
| ... | ... |
と書けるようになりました。Nat::も外せるようにimplの外に書きたい、とか、いろいろ思うところはあるかもしれませんが。とりあえずこれでいきましょう。
さらに、succをいっぱい書くのもめんどくさいので、もっとメソッドを生やしてみましょう。
impl Nat {
fn from_u32(n: u32) -> Nat {
if n == 0 {
Nat::O
} else {
Nat::succ(Nat::from_u32(n - 1))
}
}
}
再帰的にsuccをする関数です。
我々はu32型には詳しいので、u32型でこうやれば再帰ができることを知っていて、こういうコードが書けました。
Natでも再帰ができる気がするので、ちょっと考えてみます。
- u32での再帰と同様、Natでも、再帰をどこかで止めたいです。具体的には
Nat::Oのとき、何かを返すようにしたいです -
Nat::Oじゃないとき、先ほどのelse節Nat::succ(Nat::from_u32(n - 1))のような雰囲気の形にしたいです -
n - 1←こんな計算しらない。けど、Natでは、Nat::S(m)のmの部分を使えばよさそうです。
これらを考えたとき、例えば次のような実装ができます。
impl Nat {
fn rec<T>(c0: T, cs: &dyn Fn(&Nat, T) -> T, n: &Nat) -> T {
match n {
Nat::O => c0,
Nat::S(m) => cs(m, Nat::rec(c0, &cs, m)),
}
}
}
これで、再帰ができるようになりました。
再帰によって、Natをu32に戻すには、次のようにすればいいですね。
impl Nat {
fn to_u32(&self) -> u32 {
Nat::rec(0, &|_, cnt: u32| cnt + 1, self)
}
}
以下を動かすと、動作が確認できます。
fn main() {
println!("Except: 100, Actual: {}", Nat::to_u32(&Nat::from_u32(100)));
}
最後に、足し算を定義してみます。
use std::ops::Add;
impl Add for Nat {
type Output = Self;
fn add(self, other: Self) -> Self {
Self::rec(other.clone(), &|_, n: Nat| Nat::succ(n), &self)
}
}
これは、u32での再帰風に書くと
fn add(this: u32, other: u32) -> u32 {
if this == 0 {
other
} else {
1 + add(this - 1, other)
}
}
です。とても愚直ですが、確かに、足し算になっていることが分かります。
以下のコードで動作確認してみましょう。
fn main() {
println!("Except: 7, Actual: {}",
Nat::to_u32(&(Nat::from_u32(3) + Nat::from_u32(4))));
println!("Except: 100, Actual: {}",
Nat::to_u32(&(Nat::from_u32(43) + Nat::from_u32(57))));
}
続く……のか?
続けたいのですが、Rustだと、高階関数を作ろうと思うと、関数自体の置き場所、クロージャに渡すものの所有権やライフタイムなどが問題になってきて、非常につらいです。
余力のある方は、例えば、recの定義に適当に参照をつけたりとったり、あるいはrecの定義をCurry化してもコンパイルが通るかどうか、試してみて下さい。非常に苦労されると思います。
そのため「進捗が出たら続きを書く」という方式を取ります。
参考文献
HoTT bookの最初の方