Fresh variable: Difference between revisions

Revision as of 03:20, 3 September 2023

Latest revision as of 12:44, 4 January 2025

(9 intermediate revisions by 8 users not shown)

Line 1:

{{Multiple issues|

{{unreferencedMore citations needed|date=September 2023}}

{{notability|date=September 2023}}

}}

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.<ref>{{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.</ref>{{cn|reason=Find more citations like the former one, where it is explained ad hoc, or a proper definition in a textbook.|date=JuneSeptember 2023}}

The concept is often used without explanation.<ref>{{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.</ref>{{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 variable|free]].<ref>{{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

}}</ref> Another use for fresh variables involves the development of [[loop invariant]]s in [[formal verification|formal program verification]], where it is sometimes useful to replace constants by newly introduced fresh variables.<ref>{{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

}}</ref>

== Example ==

Line 13 ⟶ 41:

:<math>append(cons(x,cons(y,nil)),cons(3,nil))</math>,

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

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

:<math>append(cons(v_1,v_2),v_3) \to cons(v_1,append(v_2,v_3))</math>

before, matching will succeed with the answer substitution <math>\{ v_2v_1 \mapsto x, \; v_2 \mapsto cons(y,nil), \; v_3 \mapsto cons(3,nil) \}</math>.

== Notes ==

{{notelist}}

== References ==

Line 25 ⟶ 56:

[[Category:Automated theorem proving]]

[[Category:Computer algebra]]

[[Category:Variables (mathematics)]]