🔁

Netlify のリダイレクトの仕組みはチューリング完全

に公開
Netlify
Turing complete
tech

Web サイトのホスティングサービスの一つである Netlify には、柔軟にリダイレクトを設定可能な仕組みが備わっています。本稿では、この仕組みを一種の計算モデルとして捉え、その計算能力がチューリング完全であると示します。具体的には、この仕組みを用いて 2-タグシステムを模倣可能であると示します。非形式的な証明である点にはご注意ください。

背景

詳細は後述しますが、Netlify のリダイレクトの仕組み（以下、redirects）では、かなり柔軟なリダイレクトの設定が可能です。そのため、誤ってリダイレクトループが生じる危険性があります。怖いですね。
リダイレクトループが生じると困るので予めリダイレクトの設定を検査するわけですが、設定するリダイレクトの数が多いと人手による検査が大変になってきます。そこで検査を自動化したくなります。しかし、なかなか良い検査アルゴリズムが作れなかったので、redirects はチューリング完全ではないかと疑い始めました。もしチューリング完全ならば無限ループの検出は無理なので、つまりリダイレクトループの検出も無理と言えるわけです。

Netlify のリダイレクトの仕組み（redirects）

本節では、redirects のチューリング完全性の証明に必要な機能に絞り、redirects について簡単に説明します。

redirects の基本

Netlify では redirects を用いてリダイレクトのルール（以下、リダイレクトルール）を設定できます。リダイレクトルールは _redirects ファイルに記述します。

リダイレクト元のパスとリダイレクト先のパスを行ごとに記述します:

/foo  /
/bar  /hoge

上記のルールを記述している場合、例えば /foo というパスへのリクエストは / にリダイレクトされます。同様にして、/bar は /hoge にリダイレクトされます。なお、リダイレクトルールは上から順番に読まれ、最初にマッチしたルールが適用されます。

パスを展開する

redirects では、変数をリダイレクト元のパスの一部に束縛してリダイレクト先に展開できます。

:splat

以下のルールを記述している場合、:splat を /news 配下の任意のパス（* に相当する部分）に束縛し、リダイレクト先の :splat に展開できます。例えば /news/foo/bar にリクエストすると /blog/foo/bar にリダイレクトされます。

/news/*  /blog/:splat

注意点として、* はパスの末尾にのみ記述できます。つまり、例えば /news/*.html /blog/:splat は記述できません。

プレースホルダー

:splat を用いる方法は単一のディレクトリを束縛できませんが、プレースホルダーでは可能です。Netlify の公式ドキュメントより、例を以下に引用します:

/news/:month/:date/:year/:slug  /blog/:year/:month/:date/:slug

上記のルールを記述している場合、例えば /news/02/12/2004/my-story にリクエストすると /blog/2004/02/12/my-story にリダイレクトされます。

2-タグシステム

本節では 2-タグシステムについて簡単に説明します。

めちゃくちゃ雑に説明すると、2-タグシステムは何らかの規則に基づいて文字列を書き換えていくシステムです。例えば baa → acca → …… → Hcccccca という風に書き換えていきます。停止記号（先の例では H）から始まる文字列、または、長さが 2 未満の文字列に書き換えると停止します。

何らかの規則とは、例えば以下のような規則です。文字を文字列に写す関数だと考えてもらえばよいです。

  • a --> ccbaH
  • b --> cca
  • c --> cc

2-タグシステムは与えられた文字列を先頭 2 文字（s_1）と残りの文字列（s_2）に分け、上記の規則に基づき s_1 の先頭文字を写した文字列を s_2 の末尾につけます。その後 s_1 は捨てます。これを先述の停止条件を満たすまで繰り返します。例えば、baa が入力された場合、baa → acca → caccbaH → ccbaHcc → baHcccc → Hcccccca という風に書き換えていきます。

小さな体系の 2-タグシステムですが、その計算能力はチューリング完全であると知られています。つまり 2-タグシステムと Rust の計算能力は同じです。すごいですね。

ここまでの説明は Wikipedia での 2-タグシステムの説明を噛み砕いたものでした。Wikipedia ではより詳細に説明されているので、そちらもぜひ参照してください。

redirects による 2-タグシステムの模倣

前提知識の長い説明を終え、ここから redirects のチューリング完全性を示します。

redirects を用いた計算モデル

まずは redirects を用いた HTTP 通信の流れを一種の計算モデルとして捉えます。と言っても大層なものではなく、redirects は入力された URL を書き換えて出力する関数とし、URL が書き変わらなくなるまで繰り返し redirects に URL を入力するシステムを考えます。HTTP 通信のリダイレクトの流れを抽象化しているだけです。
システムの動作を疑似コードで表すとこんな感じでしょうか（Python 風のシンタックスです）:

  • 入力: URL u
  • アルゴリズム:
    1. \texttt{while} \ \texttt{True} \colon
    2. \quad u' \coloneqq \textit{redirects}(u)
    3. \quad \texttt{if} \ u = u' \colon
    4. \qquad \texttt{return} \ u
    5. \quad \texttt{else} \colon
    6. \qquad u \coloneqq u'

ただし、関数である redirects は、_redirects ファイルの定義に基づいて URL を書き換えるものとします。また、もしマッチするリダイレクトルールが存在しない場合は、入力された URL をそのまま返すものとします。

なお、実は本家の redirects ではリバースプロキシが可能なのですが、これを認めてしまうとリバプロ先で任意の計算が可能なので、今回は存在しないものとして扱います。

模倣方法

先の計算モデルを踏まえて、redirects の機能をグッと睨むとある存在が思い浮かびます。2-タグシステムです。
というわけで、この計算モデルはほとんど 2-タグシステムそのものです。例えば 2-タグシステムにおける

  • a --> ccbaH
  • b --> cca
  • c --> cc

という規則は、redirects では以下のようなリダイレクトルールの列として定義できます:

/a/:dummy/*  /:splat/c/c/b/a/H
/b/:dummy/*  /:splat/c/c/a
/c/:dummy/*  /:splat/c/c

例えば /b/a/a というパスの URL は上記の 2 つ目のリダイレクトルールにマッチし、:dummy が束縛する a は捨てられ、:splat が束縛する a はリダイレクト先に展開されて /a/c/c/a に書き換えられます。このように定義すると、入力 URL のパスの先頭ディレクトリ 2 つを削除し、先頭ディレクトリに合わせて残りのパスを加工できます。また、上記のリダイレクトルールではリダイレクト元の先頭ディレクトリとして a, b, c のみ存在するので、例えば /H/c/c/c/c/c/c/a はどのリダイレクトルールにもマッチせず停止します。

/b/a/a が停止するまでの流れを明示すると次の通りです: /b/a/a → /a/c/c/a → /c/a/c/c/b/a/H → /c/c/b/a/H/c/c → /b/a/H/c/c/c/c → /H/c/c/c/c/c/c/a
節「2-タグシステム」で見た例と同じ流れになっていますね。

まとめ

本稿では、Netlify のリダイレクトの仕組み（redirects）を用いて 2-タグシステムを模倣し、redirects のチューリング完全性を非形式的に示しました。

元々はリダイレクトループの検査アルゴリズムを作りたかったわけですが、無理だと分かったので早々に撤退できて良かったです。完璧なアルゴリズムは諦め、今では頻出パターンにのみ対応した検査アルゴリズムでお茶を濁しています。

GitHubで編集を提案

Discussion