【終わり】正規表現エンジンの実装と形式検証を手伝ってくれる方を募集します（報酬あり！）

そろそろ懐が寂しいので終わりです。ご協力ありがとうございました！

Lean 4で作っている正規表現エンジンを、もっと便利で実用的なライブラリにするために、一緒に開発・証明してくれる仲間を募集しています。せっかくなので、今回はいくつかのIssueにバウンティを設定してみることにしました。

Leanや形式検証に興味がある方、Unicode周りが好きな方、正規表現エンジンの内部に触れてみたい方ならどなたでも歓迎です。
取り組む Issue は自由に選べますし、実装方針の相談やレビューは気軽にどうぞ。必要なら背景説明や資料も用意します。

報酬について

対象 Issue を解決して PR がマージされたら1件につき10万円〜のバウンティをお支払いします。重めのタスクはマイルストーンに分けて途中支払いもできますし、難しい部分を突破したときの追加ボーナスもあります。

こんな方に向いています

形式検証やLeanを実際のプロジェクトで使ってみたい方（学生の方も歓迎です）
計算機科学の基礎（形式言語など）に興味がある方
正規表現エンジンの内部構造やパーサ、Unicodeの実装に興味がある方
実装、証明をどちらもやってみたい方
ちょっと変わったOSSに貢献してみたい方

サポート内容

GitHub/Discordでいつでも質問OK
タスクの難易度調整や着手前のスコープ相談
実装の方針相談、PR のドラフトレビュー
Unicodeの仕様や正規表現実装周りのナビゲート
Leanの書き方や証明のコツの共有
- 基本的なプログラムの書き方自体は自走して学べる方を想定しています

今回募集しているタスク

Unicode対応

正規表現におけるUnicode対応を改善してくれる方を募集します。目標はUTS 18のレベル1サポートを完了することです。

~~RL1.1: \u{...}形式のリテラル~~ 終了しました
- 正規表現リテラルのパーサを拡張し、すべてのコードポイントを表現できるようにします
- この中だと一番かんたんかも
RL1.2: Unicodeプロパティ
- \p{Uppercase Letter}といったプロパティに対するマッチを実装します
- エンジンの正当性証明も拡張します
- UnicodeプロパティのLean実装の調査からお願いする可能性があります
- 規模が大きいのでマイルストーンごとに追加報酬を支払い可能です
RL 1.3: 文字クラスの集合演算
- [[a-z]--[aeiou]]のような正規表現を書けるようにデータ構造やマッチングを拡張します
- そこそこの難しさです
- 集合演算の木構造をマッチング用に最適化し、その正しさの証明までできたらボーナスあり
RL 1.4: 単語境界のUnicode対応
- \bや\B演算子をUnicode文字プロパティベースの実装に変更します
- RL1.2が前提
- Unicodeの理解が必要で、そこそこの難易度です
RL 1.5: Case-insensitiveマッチモードの実装
- 大文字小文字を区別しないマッチモードを実装します
  - そのために必要なUnicodeデータベースの処理も実装します
- 正規表現中でモードを切り替える構文も導入します
- 正当性定理をマッチモード対応に拡張できたらボーナスあり
  - 後述の「ASTレベルの意味論」を先に終わらせる必要があります

形式検証

ASTレベルの意味論
- 正規表現コンパイルには脱糖 → オートマトン変換という2段階の処理があります
- 現在は脱糖後の部分のみ形式検証されていますが、脱糖自体の正当性は未証明です
- 脱糖前 AST のマッチング意味論を定義し、脱糖が正しいことを証明します
- そこそこ難しいと思います
正規表現リテラルの形式文法
- 現状、正規表現の文法はパーサ実装が事実上の定義になっています
- 正規表現そのものを形式的に文法化します
- 目標は「文脈自由文法で定義できること」を示すこと
- おそらく LL(k) に収まると思われ、パーサを書き直して文法どおりであることを証明できたら大変素晴らしいので追加報酬
- 文法定義はそこそこの難しさ、パーサと証明は難しいと思います

興味があれば、まずは気軽にIssueでコメントするかTwitterまでお願いします。