新鮮な変動

形式的推論、特に数理論理学、コンピュータ代数、自動定理証明において、新しい変数とは、これまで検討してきた文脈では出現しなかった変数のことである。^{[ 1 ]} この概念はしばしば説明なしに使用される。^{[ 2 ]}

新しい変数は、他の変数を置き換えて、変数シャドウイングやキャプチャを解消するために使用できます。たとえば、ラムダ計算の項を名前を変更した変数を持つ同等の項に変換するアルファ変換では、変数を新しい変数に置き換えることで、本来自由であるべき変数を誤ってキャプチャしてしまうことを防ぐことができます。^{[ 3 ]}新しい変数のもう1つの用途は、形式的プログラム検証におけるループ不変条件の開発です。この場合、定数を新しく導入された新しい変数に置き換えることが役立つことがあります。^{[ 4 ]}

例えば、項の書き換えでは、ルールを適用する前に${\displaystyle l\to r}$特定の用語に${\displaystyle t}$、各変数${\displaystyle l\to r}$変数との衝突を避けるため、新しいものに置き換える必要があります。${\displaystyle t}$ ルールが与えられた 場合$${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))}$$ そしてその用語 $${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} )),}$$ 規則の左辺に一致する置換を見つけようと試み、${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)}$、 内で${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))}$失敗するだろう、なぜなら${\displaystyle y}$一致しません${\displaystyle \operatorname {cons} (y,\mathrm {nil} )}$ただし、ルールが新しいコピーに置き換えられた場合^{[ a ]}$${\displaystyle \operatorname {append} (\operatorname {cons} (v_{1},v_{2}),v_{3})\to \operatorname {cons} (v_{1},\operatorname {append} (v_{2},v_{3}))}$$ 以前は、解答の置換によってマッチングが成功していました $${\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}。$$