【終わり】正規表現エンジンの実装と形式検証を手伝ってくれる方を募集します（報酬あり！）
そろそろ懐が寂しいので終わりです。ご協力ありがとうございました！
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までお願いします。
SQLiteは同時書き込みできるようにならないです（当面）
Publickeyの記事をきっかけに話題になっているようです。
ネタ元はHacker Newsなんですかね。
残念ながら、リンクされているページは開発中のブランチであり、まだSQLite本流にはマージされていません。
また、現状ではマージする予定もありません。
ちなみに、このブランチは楽観的ロックを実装しているので、マージされたとしても使うときにはアプリケーション側でちょっと気を付ける必要がありそうですね。リトライすればいいんですかね？
28000円分世界を変える
皆さん、こんにちは！
今回のブログでは、私が最近行った28000円の寄付についてお話しします。私は昨年から効果的利他主義に基づいて寄付を続けており、この記事が皆さんに善行を広めるきっかけになればと思っています。
効果的利他主義とは？
効果的利他主義(Effective Altruism, EA)とは、人々を助ける際に最大限効果のある方法を採用することを重視する考え方のことであり、効果的利他主義に従って慈善活動を行っている人々やプロジェクトが多数存在します。今回私は、その中でも次の2つのファンドにそれぞれ$100ずつ（PayPal経由で14000円ずつ）寄付しました。
funds.effectivealtruism.org
www.givewell.org
これらのファンドは、特に最貧国に住む人々の衛生環境や経済状況を直接改善するプロジェクトに寄付金を分配しています。
寄付プロジェクトの具体例
これらのファンドが寄付しているプロジェクトをいくつか見てみましょう*1。
マラリアコンソーシアム
マラリアコンソーシアムはアフリカやアジアの地域でマラリアやその他の感染症の対策を行っている団体です。例えば、子どもたちに抗マラリア薬を投与することによってマラリア感染を予防しています*2。このプロジェクトでは$5500で一人の命を救うことができるようです。すごいですね*3。
寄付をするメリット
あなたが寄付をすることには次のようなメリットがあります。
- 最貧国の人々を直接助けることができます。世界レベルで見たときの所得格差はとても大きく、一日数百円程度で生活せざるを得ない人が数億人居ます。）私達のように世界でも高所得の国々に住んでいる人々にとってはあまり大したことのない出費でも、これらの人々にとっては生活を一変させるほどの価値があるのです。
- あなたの人間としての道徳的地位を向上させることができます。寄付は善いことであり、それをする人は徳の高い素晴らしい人です。そして、その徳の高さは（この記事のように）他人に見せびらかすと気分の良いものです。皆さんも私の徳を羨ましく思うのであれば、ぜひ私に張り合って寄付してみてくださいね。
世界を良くしていきましょう。
*1:https://www.givewell.org/top-charities-fundを参照。EA Fundsの方もだいたい同じようなところに寄付しています。
状態の概念無しで表現できる計算も大事です
私が主張したいのは「私たちが計算*1と呼ぶもののモデル化には、必ずしも状態の概念が現れるとは限らない」です。これを立証するために、ブーリアン回路族という状態の概念を必要としないモデルが、計算をしていると言えるほど十分強力であることを前の記事で紹介しました。
一方、私は「全ての計算は状態の概念を利用せずにモデル化できる」と言いたいのではありません。なぜならば、状態の概念を必要とする計算はあるからです。
状態の概念を必要とする計算はあります
世の中には状態の概念が必要な問題領域が存在します。例えば、時計は現在の時間を状態として持つでしょうし、自動販売機はユーザが投入された金額を状態の形で追跡する必要があります。
当然、このような問題を解く計算機やそのモデルには状態の概念が存在します。ミーリ・マシンがこういった計算機の一つのモデルです。
例えば、きしださんの言う「1を無限に出力する」機械はミーリ・マシンを使って以下のように表現できます。
- 状態は1つです
- 単一の入力（例: 時間経過）に応じて状態が遷移します。状態が1つしかないので遷移先も同じ状態ですが。
- 状態遷移に伴って1を外部に出力します。
状態の概念無しで表現できる計算も大事です
ですが、計算が全てこのようなものであるとは限りません。例えば、コンパイラはソースコードを入力として受け取り機械語を出力するような計算機だと考えられます。
コンパイラが行うような計算はブーリアン回路族でシミュレートできます。つまり、コンパイラを表現するために状態概念は必要ありません。
コンパイラのような計算は私たちが計算と呼ぶもののうち重要な部分をなしていると私は考えます。実際、これらの計算は決定問題という部分に少しの工夫*2で対応します。回路族とチューリングマシンの等価性も決定問題の文脈において示されています*3。
この話題の大元はプログラミング教育についてでした。私たちがプログラミングを学ぶとき、決定問題に対応するような計算をたくさん扱うでしょう。例えば、入力を二つ受け取って足し算するようなプログラムもこの部分に入ります。
プログラミングの基本は順次処理と状態遷移なわけで、公教育ではそこを押さえればいい。
— きしだൠ(K1S) (@kis) 2023年2月27日
あと、オブジェクト指向の前に高階関数のほうが大事やろ。で、高校の授業としては難しすぎる。
話をずらしていくのはやめましょう
結局、きしださんは構文解析がブーリアン回路族で計算できることには合意されるのでしょうか？どんどん話題を変えられるとそもそも何の話をしているか分からなくなってしまいますし、不誠実です。
状態の概念が存在しない計算モデルはあります (例: ブーリアン回路)
きしださんは（チューリング完全な）計算モデルにはかならず状態の概念がある、と主張しています。文脈は次のツイートのあたりを見るとまあわかると思います。
いえ、チューリングマシンで見いだされた計算の性質は、ほかの計算モデルにも引き継がれます。互換性があるからほかの計算モデルを利用しているわけです。
— きしだൠ(K1S) (@kis) 2023年2月28日
単に状態が明示的ではないだけです。
この主張に対する反例として、ブーリアン回路による計算モデルを紹介します。
ブーリアン回路とチューリングマシンの等価性
ブーリアン回路*1とは、ANDやORといった組み合わせゲートを集めてできる回路のことです。
ブーリアン回路に対する入力をnビットのビット列、出力をmビットのビット列としましょう。
ブーリアン回路を構成するゲートとして{AND, OR, NOT}の三種*2を用いると、ブーリアン回路はnビットのビット列をmビットのビット列に移すどのような関数も表現することができます。
1つのブーリアン回路では入力サイズが固定されてしまっているので、代わりに各入力サイズnごとに異なる回路を利用することにしましょう。例えば、1ビット加算器、2ビット加算器、3ビット加算器…といったブーリアン回路の族（列）を考えると、この回路族全体で足し算という計算を表現していると考えることができます。
それぞれの入力サイズについてブーリアン回路はどのような関数も表現できたわけですから、それぞれの入力サイズに対応する回路に入力してあげることによって、ブーリアン回路族はチューリングマシンで表現可能などのような計算も再現することができます*3。
ブーリアン回路に状態は無い
上で書いた通り、ブーリアン回路は組み合わせ回路だけでできています。反対に言えば、ラッチ回路やフリップフロップのような状態回路は全く使っておらず、回路に対する入力を決めると出力はただ一つに決まります。従って、ブーリアン回路には状態の概念は（少なくとも陽に）存在しないと言えるでしょう。
ブーリアン回路に状態概念は暗に存在するか？→しないと思う
この意見に対する反論として、ブーリアン回路の実行には状態が暗黙的に存在するという主張が考えられます。
例えば、ANDゲートの出力に対してNOTゲートをくっつけることでNAND回路を構築したとしましょう。このNAND回路に対して[1, 0]というビット列を入力したとき、
- まず、ANDゲートが[1, 0]という入力に対して0を出力する。
- 次に、NOTゲートが0という入力に対して1を出力し、結果としてNAND回路が1を出力する。
というステップで回路の出力が分かります。そして、きしださんはこのステップをNAND回路に暗に存在する状態であると主張するかもしれません。
しかし、私はこの主張は成立しないと考えます。なぜならば、このステップはNAND回路をシミュレートする私たちの頭の中に存在するのであり、NAND回路の本質ではないと考えているからです。やはり、NAND回路自体は状態の無いブーリアン回路でしかないと考えます。
同様の再反論がラムダ計算についても言えるでしょう。確かに、私たちはラムダ項の書き換えプロセスに状態を見出すことはできます。しかし、その状態は項書き換えプロセスをシミュレートする私たちの頭（もしくはラムダ計算をシミュレートするチューリングマシン）の方にあるのであって、ラムダ計算自体には無いのでは無いでしょうか。
*1:https://en.wikipedia.org/wiki/Logic_gate
*2:NANDだけでもOKです。
*3:本当はほかにも色々と考えることがあります。例えばhttps://cs.stackexchange.com/a/96618を見てください
トゥイッター休止します
最近のゴタゴタは流石に目に余るので一時離れておきたいと思います。
アプリのアンインストールはしてないので連絡来たら通知は届くはず。
目標は一週間だけどそんなに長く離れられるかな。。。
本『実力も運のうち』第2章
サンデルは第2章の冒頭で次のように述べている。
能力に基づいて人を雇うのは悪いことではない。それどころか、正しい行為であるのが普通だ。 （中略）
仕事をあてがう際に能力が重要な理由は、少なくとも二つある。一つ目は有効性。配管工や歯科医が無能であるよりも有能であるほうが、私の置かれた状況は改善するだろう。二つ目は公正さ。人種的・宗教的・性差別的偏見から、その仕事に最もふさわしい応募者を差別し、ふさわしくない人物を代わりに雇うのは間違いだ。自分の偏見のおもむくままに、私が粗雑な配管修理や歯根管治療を進んで受け入れたとしても、差別が不公正であることに変わりはない。その仕事によりふさわしい候補者が、自分は不正の犠牲者だと不平を言うのは当然である。
これはその通りであり、能力主義には良い点がある。それでまあ「一体全体、能力主義の何が悪いというのだろうか？」ということを歴史の視点から扱っていくのだが、何の話をするかというとキリスト教の話なんだよね。
正直あまり興味が無くてちゃんと読んでない…
