Fresh variable: Difference between revisions

Revision as of 17:40, 25 January 2024

Latest revision as of 12:44, 4 January 2025

(2 intermediate revisions by 2 users not shown)

Line 1:

<!-- Please do not remove or change this AfD message until the discussion has been closed. -->

{{Article for deletion/dated|page=Fresh variable|timestamp=20240119165803|year=2024|month=January|day=19|substed=yes|help=off}}

<!-- Once discussion is closed, please place on talk page: {{Old AfD multi|page=Fresh variable|date=19 January 2024|result='''keep'''}} -->

<!-- End of AfD message, feel free to edit beyond this point -->

{{Multiple issues|

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

Line 24 ⟶ 20:

| 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

| year = 1996}}</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

Line 46 ⟶ 43:

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}}

:<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 ==