数学の勉強が必要だと思った話

Rust プログラミング 数学 記号論理学 Haskell

人生何度目かわからないが、今日、数学の勉強をする必要があると再認識した。

シチュエーション

僕は今、初心者ながらRustで編集のヒストリー機能を実装している。他の言語では幾度となく実装してきたような機能だが、Rustでやるとなると、どのように実装してよいかよくわからなくなってしまった。僕はデザインパターンには明るくないが、おそらく「コマンドパターン」と呼ばれるものを実装しようとしていた*1。また、現在実装しているRustのコードはCとしてのAPIを持ち、外から呼び出せるようになっていて、そのために現在の状態が全てContextと呼ばれる構造体に押し込められている*2。アンドゥ操作はこのContextに対して行われるものであると見ることができる。そこで、普通に実装しようと思うと以下のようなコードになる。

struct Context {
    ...
    history_manager: HistoryManager,
    ...
}

trait Action {
    fn do_undo(context: &mut Context);
}

struct HistoryManager {
    ...
    undo_list: Vec<Box<Action>>,
    ...
}

impl HistoryManager {
    pub fn do_undo(context: &mut Context) {
        if let Some(mut action) = self.undo_list.pop() {
            action.do_undo(context);
        }
    }
}

fn do_undo(context: &mut Context) {
    let mut history_manager = &mut context.history_manager;
    history_manager.do_undo(context); // ERROR!!
}

#[no_mangle]
pub unsafe fn c_do_undo(context: *mut Context) {
    do_undo(&mut *context);
}

しかし（当然ながら？）、このコードはコンパイルが通らない。// ERROR!!とコメントを付けた行で二回目の&mutの借用が生じるからだ。

解決策として、ぱっと思いつくものには次のようなものがある。

  • ContextをRc<RefCell<Context>>とする
  • Box<Action>をRc<RefCell<Action>>とする
  • 「コマンドパターン」を使うことをやめる

ここまで考えると、これ以上考えが進まなくなってしまった。本当に「コマンドパターン」を実装するためにはRc<RefCell<T>>は必要なのか？僕の実装が「ヘタクソ」なだけで、本当は素朴な借用のみで実装できてしまうのではないだろうか？という疑問が生じてしまったのだ。

素朴な借用のみを用いて「コマンドパターン」を実装することはできるのか。しばらく考えたが、出た答えは「多分出来ない」だった。「コマンドパターン」を実装する際には、どこかしらに同一オブジェクトに対する複数の参照が同時に存在してしまうような「気がした」

しかし、安易にRefCellを使うのは、ただごまかしているだけだ。理屈ではよくわからないから、実行時に本当に借用できるかどうか、サイコロを振っているようなものだ。なるべくRefCellを使わないほうが「Rustっぽい」やりかたなのではないだろうか。

もやもやして非常に気持ちが悪い。「Rustの借用を用いるという枠組みの中でコマンドパターンを実装することができるかどうか」証明できれば良いのだが。

デジャヴ

直観主義論理

大学の教養の授業の中で直観主義論理に触れる機会があった。ちょっと練習問題を解き、簡単な証明図を書くことができるようになった。この練習問題の中には「古典論理を用いないと証明できないものであるので帰結の二重否定を証明せよ」というものもあった。

ここで、今回と同じような疑問が生じた。直観主義論理で証明できないのはなぜか？本当に古典論理が必要なのだろうか？もやもやする。でも、証明図を考えてみると「多分できない」と思った。なんだか、うまく否定をキャンセルすることができないのだ。

ポイントフリースタイル

Haskellというプログラミング言語があるが、プログラムの書き方の流儀（？）にポイントフリースタイルというものがある。「一般的な」書き方からポイントフリースタイルに書き換えるのはパズルのようなもので、解説を追い、少しだけ練習してみたことがある。この練習中にまた疑問が生じた、ポイントフリースタイルへの書き換えにおいてflipがよく用いられているが、flipを用いずに、練習問題の題材となっていた関数をポイントフリースタイルへ書き換えることは不可能なのだろうか？ほかに用いられている「もっと単純そうな」関数(.)、($)、idでflipを表現することは出来ないのだろうか？というものだ。

これについてもちょっと考えてみたのだが、どうにもこれらの関数では実現することが出来ないように思えた。引数を「ひっくり返す」ことを表現する能力は、これらの関数とカリー化と部分適用の組み合わせには「なさそう」だ。でも、本当に表現できないのだろうか？自分が十分に頭が良ければ、これらの関数の組み合わせでflipを表現できたのではないだろうか？もやもやする。Googleで検索しても、みんな当たり前のようにflipを使っている。機械的にポイントフリースタイルに変換するプログラムも当たり前のようにflipを出力する。これらは簡潔に表現するために用いられているのだろうか？それとも「ほんとうに必要」だから用いられてるのだろうか？もやもやする。うう。

結局

これらの３つのケースは自分の数学力の欠如が現れた似たようなケースであったように思う。こういう状況を解決することができれば、何もかもスッキリして最高なのだが。

一番手をつけやすいのは２番めの論理の例かなと思っている。記号論理学には教科書があるし、確実な「解答」がありそうで、きちんと勉強しなおせばきっと理解できるはずだ。

ヒマと本を買うお金と理解する能力とモチベがあれば勉強したい。できるかな？つらそう。

*1:https://crates.io/crates/undoというcrateがあったが、あまり参考にならなかった

*2:このようなAPIを持つ一例としてDuktapeなど