zkat’s diary

技術ブログ

CRLiteの仕組み:Bloom filterの偽陽性をなくす方法

はじめに

TLS証明書の失効情報を管理する新たな仕組みとして、CRLiteというものが考えられています。(以下の論文です) CRLiteの根幹部分は、偽陽性を排したBloom filterで成り立っています。
この記事では、どのようにしてそのような偽陽性のないBloom filterを作るのか記載します。

ieeexplore.ieee.org

まずは、Bloom Filterについて説明します。

Bloom filterについて

概要

Bloom filter(以下、BF)自体は1970年に考案されたデータ構造なだけあり、既に様々なウェブサイトにて解説がなされています。 このデータ構造の典型的な使い道の一つとして、ブラックリストがあります。あるデータが、許容されないリスト(ブラックリスト)に記載されているか否かを判別したいとき、これを用いることで高速に(どんなにブラックリストが大きくなっても定数時間で)判別を行うことができます。

但し、素のBFにはデメリットとして偽陽性(False Positive)があります。
偽陽性:本当はリストに含まれて いない データなのに、含まれて いる と判別してしまう。

なお、偽陰性はありません。
偽陰性:本当はリストに含まれて いる データなの、含まれて いない と判別してしまう。

言い換えると、「含まれている!」という判定をBFから得た時は、誤りである可能性があります*1が、「含まれていない!」という判定を得た時は、確実に正しいということです。

仕組み

適当なサイズの配列と、適当な個数のハッシュ関数*2を用意することでBFを構築することができます。たとえば、配列長8、ハッシュ関数2個(md4とmd5とします)の場合を考えます。

データの追加

appleという文字列を追加することにします。追加するデータに対して、先のハッシュ関数ハッシュ値を求めます。ハッシュ値(整数)は、配列のインデックスの為に使用します。ただ、ハッシュ値そのままでは長大ですから、配列長に収まる数となるように配列の長さで割った余りを求めます。

データ ハッシュアルゴリズム hash値 hash値を8で割った余り(インデックス)
apple md4 0x9443a56f029a293d8feff3c68d14b372 2
apple md5 0x1f3870be274f6c49b3e31a0c6728957f 7

求めたインデックスが指し示す配列の値を、1にしておきます。BFではこれでデータを追加したこととなります。

データの存在確認

先のBFに、データorangeが存在しているか確認してみます。まず、同様にハッシュ値を求めます。

データ ハッシュアルゴリズム hash値 hash値を8で割った余り
orange md4 0xb0e795cd4b8b3c8247a09cbcd6f4a76c 4
orange md5 0xfe01d67a002dfa0f3ac084298142eccd 5

求めたインデックスを用いて配列の値を確認し、全てが1である場合はデータが存在するということとなります。 そうでない場合、1つでも0の箇所があるなら、データorangeは存在しないこととなります。 今回の場合、配列[4]と配列[5]の値はどちらも0なので、orangeは存在しないこととなります。

性質

先の例のように、データを追加する時も検索するときも、必要なのは固定回数のハッシュ値の計算と配列参照だけです。そのため、どんなにデータが増えても処理時間に問題が生じることはありません。また、データの追加に伴って配列が長くなることもありません。これは、BFのメリットです。

一方で、orange以外のデータで偶然配列の番号が4,5となるようなものがあったとします。そうすると、誤ってBFにデータが含まれていると判断する原因になります。これは、データが追加され配列の中が埋まっていくほど発生しやすくなります。これは、BFのデメリットです。

改善

なお、配列長や用意するハッシュ関数の個数を調整することで、BFの偽陽性を減らすことはできます。ただし0にすることはできません。
BFで管理したいデータの見込み数や、偽陽性の確率を入力すると適切な配列長やハッシュ関数の数を計算してくれるサイトがありますので、こちらを参考にすると良さそうです。

hur.st

Filter Cascade Design

BFの偽陽性なくす方法について説明します。
残念ながらいつでも偽陽性をなくすことができる、というわけではありません。
BFを作成する時点で、BFに追加するデータと 追加しないデータ の全て(これを、 $ U $ とします)が分かっている場合、BFを多段に構築(カスケード)することで偽陽性をなくすことができます。

ここでは追加するデータの集合を $A$ とし、追加しないデータの集合を $B$ とします。 $ A \cup B = U, A \cap B = \varnothing $ であるとして、構築手順の例を説明します。

データの追加

  1. $ A $を用いて通常通り、素のBFを構築します。これを、$ BF_1 $ とします。
  2. $ BF_1 $ が判断を誤ってしまうデータを見つけ(そのようなデータは、 $B$の要素として存在することとなります)、これを $ FP_1 $ とします。
  3. もし、$ FP_1 = \varnothing $ であるなら、偽陽性のないBFの完成です(1段)。そうでないなら、次の手順を続けます。
  4. $ FP_1 $を用いてBFを構築します。これを、$ BF_2 $ とします。
  5. $ BF_2 $ が判断を誤ってしまうデータを見つけ(そのようなデータは、 $A$の要素として存在することとなります)、これを $ FP_2 $ とします。
  6. もし、$ FP_2 = \varnothing $ であるなら、偽陽性のないBFの完成です(2段)。そうでないなら、次の手順を続けます。
  7. $ FP_2 $を用いてBFを構築します。これを、$ BF_3 $ とします。
  8. $ BF_3 $ が判断を誤ってしまうデータを見つけ(そのようなデータは、 $FP_1$の要素として存在することとなります)、これを $ FP_3 $ とします。
  9. もし、$ FP_3 = \varnothing $ であるなら、偽陽性のないBFの完成です(3段)。そうでないなら、次の手順を続けます。 (以下、省略)

このようにして、多段のBFを作成します。この例では、$ FP_3 = \varnothing $であったとして3段のBFを作成したものとします。

データの存在確認

上記で作成した多段のBFに順々に問い合わせを行うことで、確認します。

*1:BFを構築する際のパラメータを調整することで実用的なレベルまで誤りの可能性を減らすことができます

*2:必ずしもSHA-256などの暗号学的ハッシュ関数である必要はありません

Web Key DirectoryでPGPの公開鍵を配布する

概要

次のインターネットドラフト(以下、I-D)に基づいて、PGPの公開鍵を配布してみたので、そのメモを残します。

datatracker.ietf.org

WKDとは

Web Key Directoryの略で、PGPの公開鍵をHTTPSで公開する仕組みです。 PGPの公開鍵を公開する方法はすでに他のものが様々ありますが、それらがもつ課題の解決を目指しているようです。I-Dには、以下のようなことが記載されていました。

既存の方法 課題
DNSで配布する方法 必ずしもメールプロバイダがDNSの管理をしているわけではない
始めのメールに公開鍵を添付する方法 始めのメールが改ざんされる可能性がある
鍵配布サーバーを用いる方法 メールアドレスと鍵の対応性が正しく管理できない場合がある

公開用のURL

公開用のURLは、directとadvancedと呼ばれる2つの形式があるようですが、いずれかのURLでバイナリ形式の公開鍵を公開すればよいです。I-Dに倣い、メールアドレスがJoe.Doe@example.orgである場合のURLの例を以下に記載します。

direct method

https://example.org/.well-known/openpgpkey/hu/iy9q119eutrkn8s1mk4r39qejnbu3n5q?l=Joe.Doe

無作為に見える文字列、iy9q119eutrkn8s1mk4r39qejnbu3n5qは、メールアドレスのローカルパートであるJoe.Doeを変換することで作る文字列となります。 変換の方式ですが、以下で行うことができます。

  1. 小文字にする(Joe.Doe → joe.doe)
  2. sha1でハッシュをとる(joe.doe → a83ee94be89c48a11ed25ab44cfdc848833c8b6e)
  3. ハッシュした値(バイナリ)を、Z-Base32でエンコードする(a83ee94be89c48a11ed25ab44cfdc848833c8b6e → iy9q119eutrkn8s1mk4r39qejnbu3n5q)

advanced method

direct methodとほとんど一緒ですが、openpgpkeyというサブドメインをつくる必要が生じます。

https://openpgpkey.example.org/.well-known/openpgpkey/example.org/hu/iy9q119eutrkn8s1mk4r39qejnbu3n5q?l=Joe.Doe

公開の仕方

I-Dでは、上記のURLに公開鍵を配置するまでの仕組みが、Web Key Directory Update Protocolとして記載されています。

draft-koch-openpgp-webkey-service-14

ただ、お手軽に試すには少々時間が掛かりそうな内容ですので、手動で公開することにしました。 まずは、公開するためのPGPの鍵ペアをThunderbirdで作り、適当なファイルにエクスポートします。

thunderbird-pgp-key-export

エクスポートしたファイルの中には、-----BEGIN PGP PUBLIC KEY BLOCK----------END PGP PUBLIC KEY BLOCK-----で囲まれたデータが記載されています。 このデータの形式はASCII Armoredであり、以下で述べられている通りバイナリに変換する必要があります。

The HTTP GET method MUST return the binary representation of the OpenPGP key for the given mail address.

フッターとヘッダーを取り除き、そのまま変換したくなりますが、データの末尾にはCRCを示す情報が付加されているのでそれを削除してからbase64 -dなどでバイナリにします。 そのファイルをサーバーにアップロードすればよいです。

正しく公開できたか確認する

こちらのツールを利用することで、正しい形式の鍵が公開できているか確認することができました。

metacode.biz

メールソフトで利用する

このあたりに記載されているメールソフトを利用することで、WKDで公開鍵を取得し検証等に利用してくれるはずですが、確認はできていません。

https://wiki.gnupg.org/WKD#Implementations

ThunderbirdはEnigmailなどのアドオンを用いることなく内蔵の機能でpgpメールを送れるようにりましたが、WKDについてはまだアドオン使わないといけない感じでしょうかね。

Chromeの履歴はSQLiteらしいのでいじってみる

概要

  • Chromeの履歴はSQLiteで管理されているらしく、容易に中身を見れそうなので試してみました。
  • 自分のChromeの履歴を用いて、どのウェブサイトに頻繁にアクセス(回数、滞在時間)しているか見てみます。

おことわり

  • SQLiteの.schemaコマンドを用いることで、どのようなテーブルが定義されているかは分かりますが、その使われ方(どのようなイベントが起きた時に、レコードが積まれるのか・レコードが更新されるのか)について明確に説明している公式情報を見つけられませんでした。
  • そのため、今回実行したSQLが目的の情報を正しく取得するものとなっているかは微妙なところがあります。

テーブル定義を見てみる

Historyファイル*1をsqlite3コマンドがある環境にコピーして開きます。.schemaコマンドで、定義されているテーブルを確認すると 以下、17のテーブルが定義されていました。

urlsvisitskeyword_search_termsあたりに面白そうなデータが入っていそうです。

CREATE TABLE meta(
    key LONGVARCHAR NOT NULL UNIQUE PRIMARY KEY,
     value LONGVARCHAR);

CREATE TABLE downloads (
    id INTEGER PRIMARY KEY,
    guid VARCHAR NOT NULL,
    current_path LONGVARCHAR NOT NULL,
    target_path LONGVARCHAR NOT NULL,
    start_time INTEGER NOT NULL,
    received_bytes INTEGER NOT NULL,
    total_bytes INTEGER NOT NULL,
    state INTEGER NOT NULL,
    danger_type INTEGER NOT NULL,
    interrupt_reason INTEGER NOT NULL,
    hash BLOB NOT NULL,
    end_time INTEGER NOT NULL,
    opened INTEGER NOT NULL,
    last_access_time INTEGER NOT NULL,
    transient INTEGER NOT NULL,
    referrer VARCHAR NOT NULL,
    site_url VARCHAR NOT NULL,
    tab_url VARCHAR NOT NULL,
    tab_referrer_url VARCHAR NOT NULL,
    http_method VARCHAR NOT NULL,
    by_ext_id VARCHAR NOT NULL,
    by_ext_name VARCHAR NOT NULL,
    etag VARCHAR NOT NULL,
    last_modified VARCHAR NOT NULL,
    mime_type VARCHAR(
    255) NOT NULL,
    original_mime_type VARCHAR(
    255) NOT NULL,
     embedder_download_data VARCHAR NOT NULL DEFAULT '');

CREATE TABLE downloads_url_chains (
    id INTEGER NOT NULL,
    chain_index INTEGER NOT NULL,
    url LONGVARCHAR NOT NULL,
    PRIMARY KEY (id, chain_index) );

CREATE TABLE downloads_slices (
    download_id INTEGER NOT NULL,
    offset INTEGER NOT NULL,
    received_bytes INTEGER NOT NULL,
     finished INTEGER NOT NULL DEFAULT 0,
    PRIMARY KEY (download_id, offset) );

CREATE TABLE typed_url_sync_metadata (
    storage_key INTEGER PRIMARY KEY NOT NULL,
    value BLOB);

CREATE TABLE IF NOT EXISTS "urls"(
    id INTEGER PRIMARY KEY AUTOINCREMENT,
    url LONGVARCHAR,
    title LONGVARCHAR,
    visit_count INTEGER DEFAULT 0 NOT NULL,
    typed_count INTEGER DEFAULT 0 NOT NULL,
    last_visit_time INTEGER NOT NULL,
    hidden INTEGER DEFAULT 0 NOT NULL);

CREATE TABLE sqlite_sequence(
    name,
    seq);

CREATE TABLE visit_source(
    id INTEGER PRIMARY KEY,
    source INTEGER NOT NULL);

CREATE TABLE keyword_search_terms (
    keyword_id INTEGER NOT NULL,
    url_id INTEGER NOT NULL,
    term LONGVARCHAR NOT NULL,
    normalized_term LONGVARCHAR NOT NULL);

CREATE TABLE segments (
    id INTEGER PRIMARY KEY,
    name VARCHAR,
    url_id INTEGER NON NULL);

CREATE TABLE segment_usage (
    id INTEGER PRIMARY KEY,
    segment_id INTEGER NOT NULL,
    time_slot INTEGER NOT NULL,
    visit_count INTEGER DEFAULT 0 NOT NULL);

CREATE TABLE content_annotations (
    visit_id INTEGER PRIMARY KEY,
    floc_protected_score DECIMAL(
    3,
     2),
    categories VARCHAR,
    page_topics_model_version INTEGER,
    annotation_flags INTEGER DEFAULT 0 NOT NULL,
     entities VARCHAR,
     related_searches VARCHAR,
     visibility_score NUMERIC DEFAULT -1,
     search_normalized_url,
     search_terms LONGVARCHAR,
     alternative_title);

CREATE TABLE context_annotations(
    visit_id INTEGER PRIMARY KEY,
    context_annotation_flags INTEGER DEFAULT 0 NOT NULL,
    duration_since_last_visit INTEGER,
    page_end_reason INTEGER,
     total_foreground_duration NUMERIC DEFAULT -1000000);

CREATE TABLE clusters(
    cluster_id INTEGER PRIMARY KEY,
    score NUMERIC NOT NULL);

CREATE TABLE clusters_and_visits(
    cluster_id INTEGER NOT NULL,
    visit_id INTEGER NOT NULL,
    score NUMERIC NOT NULL,
    PRIMARY KEY(cluster_id, visit_id))WITHOUT ROWID;

CREATE TABLE downloads_reroute_info (
    download_id INTEGER NOT NULL,
    reroute_info_serialized  VARCHAR NOT NULL,
    PRIMARY KEY (download_id) );

CREATE TABLE IF NOT EXISTS "visits"(
    id INTEGER PRIMARY KEY AUTOINCREMENT,
    url INTEGER NOT NULL,
    visit_time INTEGER NOT NULL,
    from_visit INTEGER,
    transition INTEGER DEFAULT 0 NOT NULL,
    segment_id INTEGER,
    visit_duration INTEGER DEFAULT 0 NOT NULL,
    incremented_omnibox_typed_score BOOLEAN DEFAULT FALSE NOT NULL,
    opener_visit INTEGER,
     originator_cache_guid TEXT,
     originator_visit_id INTEGER);

集計してみる

どれくらい頻繁にウェブサイトにアクセスしているか確認したいので、urlsvisitsのテーブルを用いれば良さそうです。 ドメイン単位に、どれくらいの時間閲覧していたか、どれくらいの回数アクセスしたかを集計するSQLを書いてみます。

閲覧時間について

閲覧時間が長いドメイン順にソートして、上位5件を取得しました。

sqlite> WITH joined_http_url AS (
   ...> SELECT replace(replace(urls.url, 'https://', ''), 'http://', '') AS replaced,
   ...>        visits.visit_duration AS duration
   ...> FROM visits
   ...> LEFT JOIN urls
   ...> ON visits.url = urls.id
   ...> WHERE urls.url LIKE 'https://%' or urls.url LIKE 'http://%'
   ...> ), per_domain AS (
   ...> SELECT CASE
   ...>            WHEN instr(replaced, '/') > 0 THEN substr(replaced, 1, instr(replaced, '/') -1)
   ...>            ELSE replaced
   ...>        END AS domain,
   ...>        duration
   ...>     FROM joined_http_url
   ...> ), aggregation AS (
   ...> SELECT domain,
   ...>        sum(duration) AS total
   ...> FROM per_domain
   ...> GROUP BY domain
   ...> )
   ...> SELECT (total / 3600 / 1000000) || ' hours ' || strftime('%M minutes %S seconds', total / 1000000 / 86400.0) as total_duration,
   ...>        domain
   ...> FROM aggregation
   ...> ORDER BY total DESC
   ...> LIMIT 5
   ...> ;
total_duration  domain
107 hours 44 minutes 31 seconds www.google.com
99 hours 44 minutes 21 seconds  docs.python.org
82 hours 56 minutes 20 seconds  github.com
64 hours 38 minutes 15 seconds  www.rfc-editor.org
64 hours 36 minutes 36 seconds  www.ietf.org

アクセス回数について

アクセス回数が多いドメイン順にソートして、上位5件を取得しました。

sqlite> WITH http_url AS (
   ...> SELECT replace(replace(urls.url, 'https://', ''), 'http://', '') AS replaced,
   ...>            urls.visit_count
   ...> FROM urls
   ...> WHERE urls.url LIKE 'https://%' or urls.url LIKE 'http://%'
   ...> ), per_domain AS (
   ...> SELECT CASE
   ...>            WHEN instr(replaced, '/') > 0 THEN substr(replaced, 1, instr(replaced, '/') -1)
   ...>            ELSE replaced
   ...>        END AS domain,
   ...>        visit_count
   ...>     FROM http_url
   ...> ), aggregation AS (
   ...> SELECT domain,
   ...>        sum(visit_count) AS total
   ...> FROM per_domain
   ...> GROUP BY domain
   ...> )
   ...> SELECT total,
   ...>        domain
   ...> FROM aggregation
   ...> ORDER BY total DESC
   ...> LIMIT 5
   ...> ;
total   domain
3240    www.google.com
1340    github.com
1326    docs.google.com
872     twitter.com
395     www.cambly.com

それらしいデータを得ることはできましたが、どうも閲覧時間の方の集計について 主観よりも長い時間になっているように思えます。ページを開きっぱなしにして、別のタブに移動していたとしても、アクセス時間として計上される仕様なのかもしれません。(そのあたりは十分に調べられていません)

*1:windowsであれば、C:\Users\ユーザー名\AppData\Local\Google\Chrome\User Data\Default配下に存在する模様

what3wordsをDNSで引けるようにした

概要

what3wordsというサービスを使うと、地球上のあらゆる場所を3つの単語で表せます。

例えば自由の女神の松明の場所はtoned.melt.shipで表せます。

https://w3w.co/toned.melt.ship

これを次のように、ドメイン名部分に単語を含ませる形でアクセスできるようにしてみました。

http://toned.melt.ship.point.place

仕組み

上記のpoint.placeドメインにアクセスすると、w3w.coが提供する本来のurlへリダイレクトするようにしています。

IDN対応

what3wordsでは、英単語のみならず日本語の単語でも場所を表すことができます。

例えば、次の単語も自由の女神の場所を表します。

あかり。ふえた。くねくね

ドメイン名は、英単語(ascii文字)のみならず日本語等も表現することができます。

そのため、以下を用いても同様にアクセスすることができます。

http://あかり。ふえた。くねくね.point.place

完備化の問題をいくつか解いてみたーその2

概要

拙作の完備化ツールをいろいろ使ってみたメモのその2です。 今回は、簡単な状態遷移図に対して用いてみます。 その1はこちらです。115個の完備化の問題を解いています。

zkat.hatenablog.com

やってみた

今回ツールに与える状態遷移図は以下のようにします。 これは、RFC 8555に出てくるとある状態遷移図をアレンジしたものです。

state-transition

ツールに入力できる形式で表すと以下の通りです。 trnという関数が、状態遷移を示しています。第二引数の状態に於いて、第一引数で示すトリガーが生じると、次の状態に遷移するということを表しています。

$ cat data
(VAR x y z)
(RULES

 trn(INIT, INIT)                      -> PENDING
 trn(ERROR, PENDING)                  -> INVALID
 trn(RECEIVEREQUEST, PENDING)         -> READY
 trn(ERROR, READY)                    -> INVALID
 trn(RECEIVEDATA, READY)              -> PROCESSING
 trn(ERROR, PROCESSING)               -> INVALID
 trn(FINISHCREATION, PROCESSING)      -> VALID

 car(cons(x,y)) -> x
 cdr(cons(x,y)) -> y
 cdr(NIL) -> NIL
 apply(NIL, x) -> x
 apply(x, y) -> apply(cdr(x), trn(car(x),y))
 trace(x) -> apply(x, INIT)
)

状態遷移図を辿る際に便利な関数traceを定義する為に、trn以外の諸々の関数を定義しています。 traceは、引数に1つのリストをとります。リストは状態遷移の為のトリガーを並べたものです。 traceは、リスト内のトリガー(操作)を全て実行した際の状態を返す関数です。

上記を完備化した書き換え系の下で、次の2つの項が何になるか確認してみたいと思います。 \begin{align} trace([INIT, RECEIVEREQUEST, RECEIVEDATA])\\ trace([INIT, ERROR]) \end{align}

$ wget https://github.com/moratori/clover/releases/download/v2.4.2/clover-linux-x86_64_v2.4.2 && chmod +x clover-linux-x86_64_v2.4.2
$ ./clover-linux-x86_64_v2.4.2 rewrite data 'trace([INIT, RECEIVEREQUEST, RECEIVEDATA])' 'trace([INIT, ERROR])'
YES

(VAR z x y)
(RULES
 trn(car(NIL),x) -> x
 apply(cons(y,x),z) -> apply(x,trn(y,z))
 apply(cdr(x),trn(car(x),y)) -> apply(x,y)
 trace(x) -> apply(x,INIT)
 apply(NIL,x) -> x
 cdr(NIL) -> NIL
 cdr(cons(x,y)) -> y
 car(cons(y,x)) -> y
 trn(FINISHCREATION,PROCESSING) -> VALID
 trn(ERROR,PROCESSING) -> INVALID
 trn(RECEIVEDATA,READY) -> PROCESSING
 trn(ERROR,READY) -> INVALID
 trn(RECEIVEREQUEST,PENDING) -> READY
 trn(ERROR,PENDING) -> INVALID
 trn(INIT,INIT) -> PENDING
)
(COMMENT
 ERROR < FINISHCREATION < INIT < INVALID < NIL < PENDING < PROCESSING < READY < RECEIVEDATA < RECEIVEREQUEST < VALID < TRN < APPLY < TRACE < CAR < CDR < CONS
)
(COMMENT
 trace([INIT, RECEIVEREQUEST, RECEIVEDATA]) reduced PROCESSING
 trace([INIT, ERROR]) reduced INVALID
)

最後に出力されている通り、 $trace([INIT, RECEIVEREQUEST, RECEIVEDATA])$は、$PROCESSING$となることが分かりました。 また、$trace([INIT, ERROR])$は、$INVALID$となることが分かりました。

完備化の問題をいくつか解いてみた

概要

先の記事に書きましたとおり、等式の完備化ツールをCommon Lispで作ってみています。

zkat.hatenablog.com

このツールを使って、いくつかの問題を実際に完備化してみたいと思いました。

試してみる

とは言っても、いい感じの入力となる問題を自分で作るのは難しいなと思っていたところ、以下を見つけました。

https://www.jaist.ac.jp/project/maxcomp/experiments/eq_systems.tar.gz

こちらは、JAISTの廣川研究室で開発されているツールMaxcomp(Maximal Completion)の 評価に用いられている問題のようです。

こちらの問題(合計115個)を利用させていただき、実行してみたところ以下の通りの結果となりました。

項目
実行環境(CPU) Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz
実行環境(メモリ) 6GB
実行環境(OS) Ubuntu 20.04.1 LTS on WSL2
完備化できた問題の数 65
完備化に失敗した問題の数 6
タイムアウトした問題の数 44
合計問題数 115

一つの問題ごとに、タイムアウトは30秒を設定しています。 だいたい、半分程度の問題を完備化するにとどまりました。

結果の詳細

Results of the Knuth-Bendix completion algorithm implemented in the tool Clover https://github.com/moratori/clover · GitHub

補足

以下のように実行しています。

$ wget https://github.com/moratori/clover/releases/download/v2.2.1/clover-linux-x86_64_ver2.2.1
$ chmod +x clover-linux-x86_64_ver2.2.1
$ time timeout -k 3 30 ./clover-linux-x86_64_ver2.2.1 complete slothrop_ackermann.trs
a(s(x),s(y))=>a(x,a(s(x),y))
a(s(x),Z)=>a(x,s(Z))
a(Z,x)=>s(x)

real    0m0.170s
user    0m0.227s
sys     0m0.042s
$ 

Common LispでKnuth-Bendixの完備化アルゴリズムを実装した

概要

Knuth-Bendixの完備化アルゴリズムを実装したツールを作ってみました。いくつかの簡単な問題に対して使ってみながら紹介します。

github.com

なお、Knuth-Bendixの完備化アルゴリズムの詳細自体については、こちらのページが分かりやすいです。

www.nue.ie.niigata-u.ac.jp

インストールの仕方

Linux/Windowsのそれぞれ用に、実行可能バイナリをビルドしました。 こちらからダウンロードできます。

Releases · moratori/clover · GitHub

Common Lisp(と、roswell)の実行環境がある場合は、リポジトリをクローンしてコードを取得しても大丈夫です。

実行してみる(その1)

実行権限を確認して、ダブルクリックなりで起動します。 コードを取得しroswell経由で実行する場合は以下の通り、起動スクリプトを叩いてください。

$ ./roswell/clover.ros

実行するとREPLに入るので、そこに完備化したい等式を入力していきます。 例えば、群の公理を示す以下の3つの等式を入力します。

\begin{align} plus(ZERO, x)& = x\\ plus(plus(x,y),z)& = plus(x, plus(y,z))\\ plus(i(x),x)& = ZERO \end{align}

(NIL)>>> :def-axiom group
input . to finish definition
axiom[1]>>> plus(ZERO,x) = x
axiom[2]>>> plus(plus(x,y),z) = plus(x, plus(y,z))
axiom[3]>>> plus(i(x),x) = ZERO
axiom[4]>>> .
Detected that a set of equations has been inputted.
Do you want to execute completion algorithm?  (yes or no) yes

The completion process was successful:
i(plus(y,x))=>plus(i(x),i(y))
i(i(x))=>x
i(ZERO)=>ZERO
plus(x,ZERO)=>x
plus(x,i(x))=>ZERO
plus(x,plus(i(x),y))=>y
plus(i(x),plus(x,y))=>y
plus(ZERO,x)=>x
plus(plus(x,y),z)=>plus(x,plus(y,z))
plus(i(x),x)=>ZERO
(group)>>>

完備化が成功し、10個の項書き換え規則が出力されたことが分かります。 この状態で証明したい等式、例えば $plus(plus(x,y),plus(z,w)) = plus(x, plus(y, plus(z, w)))$ を入力してみます。

すると、想定通り証明することができます。

(group)>>> plus(plus(x,y),plus(z,w)) = plus(x, plus(y, plus(z, w)))
The equation can be PROVED under the axiom group

irreducible form under the group:
plus(x,plus(y,plus(z,w))) = plus(x,plus(y,plus(z,w)))

(group)>>>

先ほどの項書き換え規則の下で両辺の既約形が同じになった為、等式が成り立つことが分かります。

実行してみる(その2)

続いて別の問題として、以下リンクに記載のある「グラス置き換えパズル」を解いてみようと思います。

http://www.nue.ie.niigata-u.ac.jp/toyama/lab-intro/TRS-intro/index.html#glass

グラスの列の置き換えを、以下の等式で表してみます。列は $cons$ を用いたリストで表すこととしてます。

\begin{align} cons(S, cons(W, x))& = cons(W, x)\\ cons(x, cons(S, cons(W, y)))& = cons(x, cons(W, y))\\ cons(W, cons(B, x))& = cons(S, x)\\ cons(x, cons(W, cons(B, y)))& = cons(x, cons(S, y)) \end{align}

上2つは、列 $SW$ が列 $W$ と等しいことを示しています。

1つは、列の先頭に $SW$ が存在した場合、1つは、列の途中又は最後に存在した場合を示しています。 下2つも同様です。

この等式を完備化してみますと、3つの書き換え規則に変換されます。

(NIL)>>> :def-axiom glass
input . to finish definition
axiom[1]>>> cons(S, cons(W, x)) = cons(W, x)
axiom[2]>>> cons(x, cons(S, cons(W, y))) = cons(x, cons(W, y))
axiom[3]>>> cons(W, cons(B, x)) = cons(S, x)
axiom[4]>>> cons(x, cons(W, cons(B, y))) = cons(x, cons(S, y))
axiom[5]>>> .
Detected that a set of equations has been inputted.
Do you want to execute completion algorithm?  (yes or no) yes

The completion process was successful:
cons(S,cons(S,x))=>cons(S,x)
cons(S,cons(W,x))=>cons(W,x)
cons(W,cons(B,x))=>cons(S,x)
(glass)>>>

この状態で、次の2つの等式 $[S,S,W,B] = [W,B,W,B]$ と $[S,S,S,W] \neq [W,B,W,B]$ を証明してみます。

(glass)>>> [S,S,W,B] = [W,B,W,B]
The equation can be PROVED under the axiom glass

irreducible form under the glass:
cons(S,NIL) = cons(S,NIL)

(glass)>>> [S,S,S,W] != [W,B,W,B]
The equation can be PROVED under the axiom glass

irreducible form under the glass:
cons(W,NIL) ≠ cons(S,NIL)

想定通り証明することができました。

実装の為に参考にした情報

資料

  • Knuth-Bendixの完備化手続きとその応用

www.jstage.jst.go.jp

https://lat.inf.tu-dresden.de/webcms/studium/lehrveranstaltungen/sommersemester-2018/term-rewriting-systems/trs1Handout.pdf

実装関連

Maxcomp

JAISTの以下のページで公開されているHaskell実装を確認させていただきました。

www.jaist.ac.jp

egison-trs

EgisonおよびHaskellで実装されているコードを確認させていただきました。

github.com