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

В формальном рассуждении, в частности в математической логике , компьютерной алгебре и автоматизированном доказательстве теорем , новая переменная — это переменная, которая не встречалась в рассматриваемом до сих пор контексте. ^{[1] [ требуется цитирование ]} Это понятие часто используется без объяснения. ^{[2] [ требуется цитирование ]}

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

Пример

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

${\displaystyle append(cons(x,y),z)\to cons(x,append(y,z))}$

и термин

${\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))}$,

попытка найти соответствующую замену левой части правила, , внутри потерпит неудачу, так как не может соответствовать . Однако, если правило заменено новой копией ^[a] ${\displaystyle append(cons(x,y),z)}$ ${\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))}$ ${\displaystyle y}$ ${\displaystyle cons(y,nil)}$

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

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

Примечания

1. то есть копия, в которой каждая переменная последовательно заменена новой переменной

Ссылки

1. Кармен Бруни (2018). Предикатная логика: естественная дедукция (PDF) (слайды лекций). Univ. of Waterloo.Здесь: слайд 13/26.
2. Михаэль Фарбер (февраль 2023 г.). Денотационная семантика и быстрый интерпретатор для jq (технический отчет). Инсбрукский ун-т. arXiv : 2302.10576 .Здесь: стр.4.
3. Гордон, Эндрю Д.; Мелхэм, Томас Ф. (1996). «Пять аксиом альфа-преобразования». В фон Райт, Йоаким; Гранди, Джим; Харрисон, Джон (ред.). Доказательство теорем в логике высшего порядка, 9-я международная конференция, TPHOLs'96, Турку, Финляндия, 26-30 августа 1996 г., Труды . Заметки лекций по информатике. Том 1125. Springer. стр. 173–190. doi :10.1007/BFB0105404.
4. Коэн, Эдвард (1990). «Циклы B — О замене констант новыми переменными». Программирование в 1990-х годах . Монографии по информатике. Нью-Йорк: Springer. С. 149–194. doi :10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID  1509875.