Свежая переменная

В формальных рассуждениях, в частности в математической логике , компьютерной алгебре и автоматизированном доказательстве теорем , новая переменная — это переменная, которая не встречалась в контексте, рассмотренном до сих пор. Это понятие часто используется без объяснения.

Новые переменные могут использоваться для замены других переменных, чтобы исключить затенение или захват переменных. Например, при альфа-конверсии обработка термов лямбда-исчисления в эквивалентные термы с переименованными переменными, замена переменных свежими переменными может быть полезна как способ избежать случайного захвата переменных, которые должны быть свободными . Другое использование новых переменных включает разработку инвариантов цикла при формальной верификации программ , где иногда бывает полезно заменить константы вновь введенными свежими переменными.

Пример

Например, при переписывании терминов перед применением правила $l\to r$ на определенный срок $t$, каждая переменная в $l\to r$ должен быть заменен новым, чтобы избежать конфликтов с переменными, возникающими в $t$. Учитывая правило

$append(cons(x,y),z)\to cons(x,append(y,z))$

и термин

$append(cons(x,cons(y,nil)),cons(3,nil))$,

пытаясь найти подходящую замену левой части правила, $append(cons(x,y),z)$, в пределах $append(cons(x,cons(y,nil)),cons(3,nil))$ потерпит неудачу, поскольку $y$ не может соответствовать $cons(y,nil)$.Однако если правило заменяется новой копией

$append(cons(v_{1},v_{2}),v_{3})\to cons(v_{1},append(v_{2},v_{3}))$

раньше сопоставление будет успешным с заменой ответа $\{v_{2}\mapsto x,\;v_{2}\mapsto cons(y,nil),\;v_{3}\mapsto cons(3,nil)\}$.