停止することの証明

ウィキペディア小見出し辞書

停止することの証明

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/22 09:08 UTC 版)

「ユニフィケーション」の記事における「停止することの証明」の解説

停止性の証明においては という3タプルを考察する。NVUN は一意でない変数の数、NLHS は潜在的等式の左辺にある関数記号と定数の数、EQN は等式の数である。書き換え規則をどのような順序で適用しても、書き換えの度にNUVNは減るか、減らずに現状維持するかのどちらかなので、最終的に停止する。NUVNが現状維持した場合、NLHSが書き換えによって減るか、減らずに現状維持するかのどちらかである。NUVNとNLHSがどちらも現状維持した場合、EQNが書き換えによって減る。