新鮮な変数

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

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

例

例えば、項の書き換えでは、与えられた項に規則を適用する前に、項の各変数を新しいものに置き換えて、項に現れる変数との衝突を避けるべきである。^[^要出典^]規則と項が与えられ、規則の左側の置換を見つけようとすると、項は一致しないため、一致しない。しかし、規則が^[a]の前に新しいコピーに置き換えられると、答えの置換で一致が成功する。 $l\to r$ $t$ $l\to r$ $t$ $\operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))$ $\operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} )),$ $\operatorname {append} (\operatorname {cons} (x,y),z)$ $\operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))$ $y$ $\operatorname {cons} (y,\mathrm {nil} )$ $\operatorname {append} (\operatorname {cons} (v_{1},v_{2}),v_{3})\to \operatorname {cons} (v_{1},\operatorname {append} (v_{2},v_{3}))$ $\{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.$

注記

^ つまり、各変数が常に新しい変数に置き換えられたコピー

参考文献

^ Carmen Bruni (2018). 述語論理：自然演繹(PDF) (講義スライド). ウォータールー大学.こちら: スライド 13/26。
^ Michael Färber (2023年2月). 「jqのための表示的意味論と高速インタープリタ（技術レポート）」インスブルック大学. arXiv : 2302.10576 .こちら：p.4。
^ Gordon, Andrew D.; Melham, Thomas F. (1996). 「アルファ変換の5つの公理」. von Wright, Joakim, Grundy, Jim, Harrison, John (編). Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings . Lecture Notes in Computer Science. Vol. 1125. Springer. pp. 173– 190. doi :10.1007/BFB0105404. ISBN 978-3-540-61587-3。
^ コーエン、エドワード (1990). 「ループB — 定数を新しい変数に置き換えることについて」. 1990年代のプログラミング. コンピュータサイエンスのモノグラフ. ニューヨーク: シュプリンガー. pp. 149– 194. doi :10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID 1509875。

この論理関連の記事はスタブです。記事を拡張することでWikipediaに貢献できます。

[copy-5] つまり、各変数が常に新しい変数に置き換えられたコピー

[1] Carmen Bruni (2018). 述語論理：自然演繹(PDF) (講義スライド). ウォータールー大学.こちら: スライド 13/26。

[2] Michael Färber (2023年2月). 「jqのための表示的意味論と高速インタープリタ（技術レポート）」インスブルック大学. arXiv : 2302.10576 .こちら：p.4。

[3] Gordon, Andrew D.; Melham, Thomas F. (1996). 「アルファ変換の5つの公理」. von Wright, Joakim, Grundy, Jim, Harrison, John (編). Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings . Lecture Notes in Computer Science. Vol. 1125. Springer. pp. 173– 190. doi :10.1007/BFB0105404. ISBN 978-3-540-61587-3。

[4] コーエン、エドワード (1990). 「ループB — 定数を新しい変数に置き換えることについて」. 1990年代のプログラミング. コンピュータサイエンスのモノグラフ. ニューヨーク: シュプリンガー. pp. 149– 194. doi :10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID 1509875。