ディレクターストリング

数学、特にラムダ計算と計算の分野では、ディレクターまたはディレクター ストリングは、項内の自由変数を追跡するためのメカニズムです。大まかに言えば、自由変数のメモ化の一種、つまり項代数またはラムダ式内の自由変数を迅速に特定するための最適化手法として理解できます。ディレクター ストリングは、1982 年に Kennaway と Sleep によって導入され、ベータ削減の計算複雑性コストを理解し制御するためのメカニズムとしてSinot、Fernández、および Mackie ^{[ 1 ]}によってさらに発展しました。

ベータ簡約では、左辺の式の値を右辺の値として定義します。

${\displaystyle (\lambda xE)y\equiv E[x:=y]\,}$または${\displaystyle (\lambda xE)y\equiv E[y/x]}$（ E（本体）中のすべてのxをyに 置き換える）

これは概念的には単純な操作ですが、このステップの計算複雑度は無視できないほど高くなる可能性があります。単純なアルゴリズムでは、式Eをスキャンして自由変数xのすべての出現箇所を探します。このようなアルゴリズムは、式Eの長さに対して明らかにO ( n ) です。したがって、式中の自由変数の出現箇所を何らかの方法で追跡する動機が生まれます。式中のどこに出現するかに関わらず、すべての自由変数の位置を追跡しようと試みることもできますが、これは明らかにストレージの面で非常にコストがかかる可能性があります。さらに、実際には必要のないレベルの詳細情報を提供してしまいます。ディレクター ストリングは、構成要素の項での使用を追跡することによって、自由変数を階層的に追跡することが正しいモデルであることを示唆しています。

簡単にするために、項代数、つまり自由に組み合わせることができる自由変数、定数、演算子の集合を考えます。項tが次の形式をとると仮定します。

${\displaystyle t::=f(t_{1},t_{2},\dots ,t_{n})}$

ここで、fはn のアリティを持つ関数であり、自由変数はなく、$t_i$は、自由変数を含む場合と含まない場合がある項です。Vを、すべての項の集合に現れる可能性のあるすべての自由変数の集合とします。ディレクターは、次のマップです。

${\displaystyle \sigma _{t}:V\to P(\lbrace 1,2,\dots ,n\rbrace )}$

自由変数から冪集合へ${\displaystyle P(X)}$セットの${\displaystyle X=\lbrace 1,2,\dots ,n\rbrace }$. 値$\displaystyle \sigma _{t}}$は単にインデックスのリストです$t_i$特定の自由変数が出現する場合。したがって、たとえば、自由変数が${\displaystyle x\in V}$発生する$t3$そして$t5$しかし、それ以外の言い方では、$\displaystyle \sigma _{t}(x)=\lbrace 3,5\rbrace }$。

したがって、すべての項について$t ∈ T$すべての項の集合Tにおいて、関数を維持する$\displaystyle \sigma _{t}}$、そして項tだけを扱うのではなく、ペアを扱う${\displaystyle (t,\sigma _{t})}$したがって、 t内の自由変数を見つけるための時間計算量は、変数が出現する項のリストを維持するための空間計算量と交換されます。

上記の定義は項代数の観点から定式化されているが、一般的な概念はより一般的に適用され、組み合わせ代数とラムダ計算そのものの両方について、特に明示的置換の枠組みの中で定義することができる。

• 用語書き換えシステム
• 明示的な置換
• メモ化

• F.-R. Sinot.「ディレクター文字列の再考：高階書き換えにおける自由変数の効率的な表現への汎用的アプローチ」 Journal of Logic and Computation 15 (2)、201-218ページ、2005年。