makenowjust-labs/blog

時相論理 (Temporal Logic) は時間に関する作用素を追加した論理の体系です。 例えば、時相論理では「ボタンを押したら、3秒以内に明かりが点く」のような時間による状況の変化を含めた文を表現することができます。

時間に関する論理的な文は、プログラムやシステムの満たすべき性質を考える際に頻繁に現れます。 そのため、時相論理は形式検証 (Formal Verification) の分野で重要な道具の一つとなっています。

モニタリングとは、入力として与えられた時系列に沿ったイベント列が、時相論理などの形で与えられた仕様を満たすかどうか判定する問題です。 線形時相論理 (LTL) やMetric Temporal Logic (MTL)、Signal Temporal Logic (STL) といった時相論理では、このモニタリングを効率的に行う方法が知られています。 モニタリングは、システムが仕様通りのふるまいをしているかを実行時に確認する、実行時検証の実現方法の1つでもあります。

この記事では、時相論理のモニタリング実装や、その背景にあるアイディアについて整理します。

Pagefindとは静的サイトで動作する (バックエンドのサーバーを必要としない) 全文検索エンジンです。

このブログにPagefindによる全文検索機能を導入しました。 右上の虫眼鏡ボタンをクリックすると、検索用のダイアログが開くはずです。

この記事では、どのようにしてNext.js製のサイトにPagefindを導入したのかを説明します。

自然数の分割とは、ある数と和が等しくなるような自然数の多重集合です。 例えば $\{\!| 3, 2, 2, 1 |\!\}$ は $3 + 2 + 2 + 1 = 8$ なので $8$ の分割となります。

この記事では、自然数の分割の積の最大値について考えます。

このブログは現在 (2023年12月11日付) Next.jsで実装されています (移行の際の記事)。

これまでは実装にPages Routerを使っていました。 最近「カテゴリ機能」(現在は「タグ機能」) を追加したのですが、その際にカテゴリの一覧の取得をすべてのページのgetStaticPropsで行わなければならず、不便に感じていました。 そうした問題の解消のために、App Routerへと移行しました。

他にもOGP画像の生成にsatoriを使うようにしたり、GitHub PagesへのデプロイをGitHub Actionsで成果物をアップロードする形にしたり、色々と修正をしました。 それらの実装を通じて学んだことを、この記事では整理します。

最近RPrecという演算子の優先順位に基づいて構文解析を行うRubyのライブラリを実装しました。 その中で、演算子の優先順位と結合順位についての理解が深まりました。

演算子の優先順位 (precedence) というのは、1 + 2 * 3が1 + (2 * 3)と解釈されて「*は+よりもつよく結合する」というように言われるものです。 この優先順位はJavaScriptであればこの辺りに、Rubyであればこの辺りにまとまっています。

そして、演算子の結合規則 (associativity) というのは、左結合とか右結合とか言われるものです。 1 + 2 + 3は(1 + 2) + 3と解釈されるので+は左結合であったり、a = b = 1がa = (b = 1)と解釈されるので=は右結合というようなものです。

今回は、この演算子の結合規則のバリエーションについて考察したことについて、まとめたいと思います。

想定読者: 構文解析やプログラミング言語の構文に興味があり、これらについて多少の知識があることを想定しています。