You can edit almost every page by Creating an account. Otherwise, see the FAQ.

Fresh variable

From EverybodyWiki Bios & Wiki


In formal reasoning, in particular in mathematical logic, computer algebra, and automated theorem proving, a fresh variable is a variable that did not occur in the context considered so far.[1][citation needed] The concept is often used without explanation.[2][citation needed]

Example[edit]

For example, in term rewriting, before applying a rule to a given term , each variable in should be replaced by a fresh one to avoid clashes with variables occurring in .[citation needed] Given the rule

and the term

,

attempting to find a matching substitution of the rule's left-hand side, , within will fail, since cannot match . However, if the rule is replaced by a fresh copy[lower-alpha 1]

before, matching will succeed with the answer substitution .

Notes[edit]

  1. that is, a copy with each variable consistently replaced by a fresh variable

References[edit]

  1. Carmen Bruni (2018). Predicate Logic: Natural Deduction (PDF) (Lecture Slides). Univ. of Waterloo. Here: slide 13/26.
  2. Michael Färber (Feb 2023). Denotational Semantics and a Fast Interpreter for jq (Technical Report). Univ. of Innsbruck. arXiv:2302.10576. Here: p.4.


This article "Fresh variable" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Fresh variable. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.