fresh variable

{{Multiple issues|

}}

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.{{cite report | url=https://cs.uwaterloo.ca/~cbruni/CS245Resources/lectures/2018_Fall/13_Predicate_Logic_Natural_Deduction_post.pdf | author=Carmen Bruni | title=Predicate Logic: Natural Deduction | institution=Univ. of Waterloo | type=Lecture Slides | number=CS245 / 13 | year=2018 }} Here: slide 13/26.{{cn|reason=Find more citations like the former one, where it is explained ad hoc, or a proper definition in a textbook.|date=September 2023}}

The concept is often used without explanation.{{cite report | arxiv=2302.10576 | author=Michael Färber | title=Denotational Semantics and a Fast Interpreter for jq | institution=Univ. of Innsbruck | type=Technical Report | number= | date=Feb 2023 }} Here: p.4.{{cn|reason=Find a few more citations where it is used without further explanation.|date=September 2023}}

Fresh variables may be used to replace other variables, to eliminate variable shadowing or capture. For instance, in alpha-conversion, the processing of terms in the lambda calculus into equivalent terms with renamed variables, replacing variables with fresh variables can be helpful as a way to avoid accidentally capturing variables that should be free.{{cite book

| last1 = Gordon | first1 = Andrew D.

| last2 = Melham | first2 = Thomas F.

| editor1-last = von Wright | editor1-first = Joakim

| editor2-last = Grundy | editor2-first = Jim

| editor3-last = Harrison | editor3-first = John

| contribution = Five axioms of alpha-conversion

| doi = 10.1007/BFB0105404

| pages = 173–190

| publisher = Springer

| series = Lecture Notes in Computer Science

| title = Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings

| volume = 1125

| year = 1996| isbn = 978-3-540-61587-3

}} Another use for fresh variables involves the development of loop invariants in formal program verification, where it is sometimes useful to replace constants by newly introduced fresh variables.{{cite book

| last = Cohen | first = Edward

| contribution = Loops B — On replacing constants by fresh variables

| doi = 10.1007/978-1-4613-9706-9

| isbn = 9781461397069

| location = New York

| pages = 149–194

| publisher = Springer

| series = Monographs in Computer Science

| title = Programming in the 1990s

| year = 1990| s2cid = 1509875

}}

Example

For example, in term rewriting, before applying a rule $l \to r$ to a given term $t$ , each variable in $l \to r$ should be replaced by a fresh one to avoid clashes with variables occurring in $t$ .{{cn|date=June 2023}}

Given the rule

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

and the term

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

attempting to find a matching substitution of the rule's left-hand side, $append(cons(x,y),z)$ , within $append(cons(x,cons(y,nil)),cons(3,nil))$ will fail, since $y$ cannot match $cons(y,nil)$ .

However, if the rule is replaced by a fresh copy{{efn|name=copy|that is, a copy with each variable consistently replaced by a fresh variable}}

: $append(cons(v_1,v_2),v_3) \to cons(v_1,append(v_2,v_3))$

before, matching will succeed with the answer substitution $\{ v_1 \mapsto x, \; v_2 \mapsto cons(y,nil), \; v_3 \mapsto cons(3,nil) \}$ .

Notes

References

Category:Rewriting systems

Category:Automated theorem proving

Category:Computer algebra

Category:Variables (mathematics)