ドリコムのエンジニアの桂田です。
こちらの記事では、RubyKaigi2017の３日目に発表されたセッションの中で、
印象に残ったセッションを紹介したいと思います。
Pattern Matching in Ruby(en)
Rubyでパターンマッチングを行うために取り組んだ内容の講演です。
弊社のプロダクトでも採用されている関数型言語のElixirからアイデアを得たようで、HTTPステータスのチェックを例として
%p([:ok, x]) =~ [:ok,200]
の記法でRubyでパターンマッチが実行できるようことが紹介されていました。
%pでパターンリテラルを作って、独自に追加した=~演算子でパターンマッチを行います。
実装内容は構文解析器（パーサー）の拡張に関してはC言語で実装し、パターンマッチに関する部分をRubyで実装しております。
詳細に関しては、
https://github.com/yakitorii/pattern-match-ruby
を覗いてみてください。
Ruby Extension Library Verified using Coq Proof-assistant
証明支援系のCoqから生成されるコードをRubyで利用するために取り組んだ内容の講演です。
Coqは四色定理の証明にも利用されたことがある定理証明支援器です。
＊四色定理は、容疑者xの献身にも取り上げられた平面上隣接する領域を塗り分けるのは４色で十分という定理です。
Ruby, Opal and WebAssembly
証明支援系のCoqから生成されるコードをRubyで利用するために取り組んだ内容の講演です。
Coqは四色定理の証明にも利用されたことがある定理証明支援器です。
＊四色定理は、容疑者xの献身にも取り上げられた平面上隣接する領域を塗り分けるのは４色で十分という定理です。
Coqは標準で生成できるコードがOcaml、Haskell、Scheme の三つなのですが、
これではRubyで利用するのが難しいのでC言語で出力できるようにし、Rubyの拡張ライブラリとして利用するというものです。
講演内容は、自明だが遅いpow関数に対して、
自明ではないが末尾最適で計算量を最適化したfastpow関数をCoqでpow AB = fastpow ABであることを証明した上で、
C言語で出力し、Rubyで利用するまでの流れが話されました。
その後、カリー＝ハワード同型対応（「型=命題」「証明=プログラム」で知られるやつです）、
HTML Escapeを例にC言語でSIMDを利用した場合のものも含めた実装方法などが紹介されました。
最後にCoqを学習することでアルゴリズムとして正しさがあるかどうかを強く意識するようになるため、ぜひ勉強してほしいとのことでした。
