@makenowjust の技術ブログです。
オートマトン理論や形式言語などの情報科学的なことや、JavaScript (フロントエンド) や Scala などのプログラミングの技術について書きます。
記事の正確さについては保証しません。間違っていたらごめんなさい。
記事
Immerman-Szelepcsényiの定理について
Immerman-Szelepcsényiの定理は の場合に (テープ長に上限のある非決定性チューリングマシンが受理できる言語のクラス) が、否定について閉じていることを示す定理です。 Neil ImmermanとRóbert Szelepcsényiが1987年にそれぞれ独立して示し、この成果により両者は1995年にGödel賞を受賞しました。 このように、Immerman-Szelepcsényiの定理は、計算量複雑性の理論上とても重要な定理となっています。
Immerman-Szelepcsényiの定理の証明は、テープ長に上限のある非決定性有限チューリングマシン (NTM) の様相 (configuration) の総数が入力の長さとそのNTMの大きさで抑えられることを活かして、次のようなNTMを構成することで実現されます。
- ある様相から到達可能な様相の総数を数え上げた上で、
- その総数のステップ中に、受理状態に到達可能かを判定する。
この記事ではImmerman-Szelepcsényiの定理を[Uezato, 2024]を参考に証明したいと思います。 方針は論文に書いてある通りで特に目新しい部分はありません。自分の備忘録として残しておきます。
想定読者: 情報科学の基本的な部分を理解しており、計算量複雑性の理論などに関心があることを想定しています。
時相論理 (Temporal Logic) のモニタリングの調査
時相論理 (Temporal Logic) は時間に関する作用素を追加した論理の体系です。 例えば、時相論理では「ボタンを押したら、3秒以内に明かりが点く」のような時間による状況の変化を含めた文を表現することができます。
時間に関する論理的な文は、プログラムやシステムの満たすべき性質を考える際に頻繁に現れます。 そのため、時相論理は形式検証 (Formal Verification) の分野で重要な道具の一つとなっています。
モニタリングとは、入力として与えられた時系列に沿ったイベント列が、時相論理などの形で与えられた仕様を満たすかどうか判定する問題です。 線形時相論理 (LTL) やMetric Temporal Logic (MTL)、Signal Temporal Logic (STL) といった時相論理では、このモニタリングを効率的に行う方法が知られています。 モニタリングは、システムが仕様通りのふるまいをしているかを実行時に確認する、実行時検証の実現方法の1つでもあります。
この記事では、時相論理のモニタリング実装や、その背景にあるアイディアについて整理します。
ブログにPagefindを導入しました
Pagefindとは静的サイトで動作する (バックエンドのサーバーを必要としない) 全文検索エンジンです。
このブログにPagefindによる全文検索機能を導入しました。 右上の虫眼鏡ボタンをクリックすると、検索用のダイアログが開くはずです。
この記事では、どのようにしてNext.js製のサイトにPagefindを導入したのかを説明します。
自然数の分割とその積の最大値について
自然数の分割とは、ある数と和が等しくなるような自然数の多重集合です。 例えば は なので の分割となります。
この記事では、自然数の分割の積の最大値について考えます。
ブログを App Router へ移行しました
このブログは現在 (2023年12月11日付) Next.jsで実装されています (移行の際の記事)。
これまでは実装にPages Routerを使っていました。
最近「カテゴリ機能」(現在は「タグ機能」) を追加したのですが、その際にカテゴリの一覧の取得をすべてのページのgetStaticProps
で行わなければならず、不便に感じていました。
そうした問題の解消のために、App Routerへと移行しました。
他にもOGP画像の生成にsatoriを使うようにしたり、GitHub PagesへのデプロイをGitHub Actionsで成果物をアップロードする形にしたり、色々と修正をしました。 それらの実装を通じて学んだことを、この記事では整理します。