Begin Rust

Rustを勉強している。やはりライフタイムとか借用のあたりで苦労している。所有権やライフタイムはわかるのだが、借用の仕組みがイマイチわからない。特に可変な借用が同時に複数あってはならない、という規則で、同時にとは一体？という気持ちになる。同時の概念を理解させてくれる文書に出会えていない。これが原因で詰まった話をする。一応問題の回避はできたが、腑に落ちきっていない。

練習がてら、状態遷移系の各ノードで、与えられたCTL-formulaが成り立つかを調べるラベリングアルゴリズムを実装した。

labeling関数内でループを回す。考慮するすべてのCTL-formulaについて、条件が合えば add_label 関数を呼んでノードにその論理式への参照を追加する。ノード（State）につけるラベルはlabels: HashMap<State, HashSet<&Formula>>としている。

はじめ、add_labelはlabelsの可変参照をとるようにしていたのだが、借用チェッカに怒られてしまった。つまりadd_label : (..., labels: &mut HashMap<...>) -> ()。add_labelsの呼び出しが複数回あって、それぞれに参照で貸し出したのがまずいようだ。直感では関数呼び出しが終わると参照を捨てるから安全だし、型システムもそう思ってくれる気がしていたのだが…。

add_labelに所有権を一旦渡して、変更した上で返却するようにしたら、怒られがなくなった。つまりadd_label : (..., labels: HashMap<...>) -> HashMap<...>とした。呼び出し元でlabelsに再代入することで所望の追加を実現できる。

これはこれできれいだと思うけど、はじめのアイデアも悪くない気がしてしまう。きっと修行が足りないのだろう。