Fresh variable

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]

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.[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.[4]

Example

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[a]

before, matching will succeed with the answer substitution .

Notes

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

References

  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.
  3. ^ Gordon, Andrew D.; Melham, Thomas F. (1996). "Five axioms of alpha-conversion". In von Wright, Joakim; Grundy, Jim; Harrison, John (eds.). Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings. Lecture Notes in Computer Science. Vol. 1125. Springer. pp. 173–190. doi:10.1007/BFB0105404.
  4. ^ Cohen, Edward (1990). "Loops B — On replacing constants by fresh variables". Programming in the 1990s. Monographs in Computer Science. New York: Springer. pp. 149–194. doi:10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID 1509875.
Stub icon

This logic-related article is a stub. You can help Wikipedia by expanding it.

Read other articles:

Keamanan laser

Simbol peringatan laser Keamanan radiasi laser adalah desain, penggunaan, dan implementasi laser yang aman untuk meminimalkan risiko kecelakaan laser, terutama yang melibatkan cedera mata. Karena sinar laser dalam jumlah yang relatif kecil dapat menyebabkan cedera mata permanen, penjualan dan penggunaan laser biasanya tunduk pada peraturan pemerintah. Laser berdaya sedang dan tinggi berpotensi berbahaya karena dapat membakar retina, atau bahkan kulit. Untuk mengontrol risiko cedera, berbagai ...

 

Charlie Villanueva

Charlie Villanueva Villanueva con la maglia dei Dallas Mavericks Nazionalità  Stati Uniti Rep. Dominicana Altezza 211 cm Peso 109 kg Pallacanestro Ruolo Ala grande Termine carriera 2016 Carriera Giovanili Blair Academy2003-2005 UConn Huskies63 (707) Squadre di club 2005-2006 Toronto Raptors81 (1.053)2006-2009 Milwaukee Bucks193 (2.612)2009-2014 Detroit Pistons256 (2.421)2014-2016 Dallas Mavericks126 (722) Nazionale 2009-2011 Rep. Dominicana Palmarès  ...

 

Fedotozine

Chemical compound FedotozineClinical dataRoutes ofadministrationOralATC codeNoneLegal statusLegal status In general: non-regulated Identifiers IUPAC name (2R)-N,N-dimethyl-2-phenyl-1-[(3,4,5-trimethoxybenzyl)oxy]-2-butanamine CAS Number123618-00-8 133267-27-3 (tartrate)PubChem CID6918160ChemSpider5293373UNIIF45VW2087WChEMBLChEMBL2106275Chemical and physical dataFormulaC22H31NO4Molar mass373.493 g·mol−13D model (JSmol)Interactive image SMILES O(c1cc(cc(OC)c1OC)COC[C@@](c2ccccc2)(N...

Papakura

This article is about the suburb. For the past territorial authority, see Papakura District. For the current local board area, see Papakura (local board area). For the local board, see Papakura Local Board. Suburb in Auckland, New ZealandPapakuraSuburbAerial view of Papakura and the Auckland Southern MotorwayCoordinates: 37°3′45″S 174°56′31″E / 37.06250°S 174.94194°E / -37.06250; 174.94194CountryNew ZealandCityAucklandLocal authorityAuckland CouncilElectora...

 

Синелобый амазон

Синелобый амазон Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:ЗавропсидыКласс:Пт�...

 

Suisse au Concours Eurovision de la chanson 1966

Suisseau Concours Eurovision 1966 Données clés Pays  Suisse Chanson Ne vois-tu pas ? Interprète Madeleine Pascal Langue Français Sélection nationale Radiodiffuseur SRG SSR Type de sélection Finale nationaleÉmission télévisée : Concours Eurovision 1966 Date 5 février 1966 Concours Eurovision de la chanson 1966 Position en finale 6e (12 points) 1965 1967 modifier La Suisse a participé au Concours Eurovision de la chanson 1966 le 5 mars à Luxembourg. C'est la 11e par...

Grèce au Concours Eurovision de la chanson 2010

Cet article est une ébauche concernant le Concours Eurovision de la chanson et la Grèce. Vous pouvez partager vos connaissances en l’améliorant (comment ?) ; pour plus d’indications, visitez le projet Eurovision. Grèceau Concours Eurovision 2010 Données clés Pays  Grèce Chanson Opa Interprète Yórgos Alkéos & Friends Compositeur Yórgos Alkéos Parolier Giannis Antoniou Langue Grec Sélection nationale Date 12 mars 2010 Concours Eurovision de la chanson 2010 P...

 

Kau Masih Kekasihku

Kau Masih KekasihkuGenre Drama Roman PembuatSinemArtBerdasarkanAt Dolphin BaySutradaraSridhar JettyPemeran Arifin Putra Asmirandah Baim Wong Slamet Rahardjo Marini Burhan Penggubah lagu temaNaffLagu pembukaKau Masih Kekasihku oleh NaffLagu penutupKau Masih Kekasihku oleh NaffPenata musikPongky PrasetyoNegara asalIndonesiaBahasa asliBahasa IndonesiaJmlh. musim1Jmlh. episode29ProduksiProduserLeo SusantoPengaturan kameraMulti-kameraDurasi60 menitRumah produksiSinemArtDistributorSurya Citr...

 

Данио-рерио

Данио-рерио Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеГруппа:Костные рыбыКласс:Лучепёрые рыбыПодкласс:Новопёрые рыбыИн�...

SMK Negeri 7 Bandung

SMK Negeri 7 BandungSekolah Menengah Kejuruan Negeri 7 Kota BandungInformasiDidirikan1965JenisNegeriAkreditasi Teknik Penyempurnaan Tekstil (A) Analisis Pengujian Laboratorium (A) Kimia Industri (A) Farmasi (A) Nomor Statistik Sekolah511026025003Nomor Pokok Sekolah Nasional20219141Jurusan atau peminatan Teknik Penyempurnaan Tekstil Analisis Pengujian Laboratorium (APL) Kimia Industri Farmasi Rentang kelasX, XI, XIIKurikulumKurikulum Tingkat Satuan PendidikanJumlah siswa1.727 siswa/iStatu...

 

Trijodtyronin

Den kemiska strukturen för L-trijodtyronin Den kemiska strukturen för trijodtyronin, notera de tre lila jodatomerna. Trijodtyronin, liotyronin, eller 3,3',5-trijod-L-tyronin (T3) (C15H12I3NO4) är ett tyroideahormon. Det påverkar nästan alla fysiologiska processer i kroppen, däribland tillväxt och utveckling, ämnesomsättning, kroppstemperatur och hjärtfrekvens.[1] Produktionen av T3 och dess prohormon tyroxin (T4) i sköldkörteln (tyreoidea) aktiveras av hormonet tyreoideastimuleran...

 

西遊記大結局之仙履奇緣

本條目存在以下問題，請協助改善本條目或在討論頁針對議題發表看法。 此條目需要編修，以確保文法、用詞、语气、格式、標點等使用恰当。 (2013年8月6日)請按照校對指引，幫助编辑這個條目。（幫助、討論） 此條目剧情、虛構用語或人物介紹过长过细，需清理无关故事主轴的细节、用語和角色介紹。 (2020年10月6日)劇情、用語和人物介紹都只是用於了解故事主軸，輔助�...

Байдибекский район

районрайон БайдибекаБәйдібек ауданы Герб 43°02′07″ с. ш. 69°22′33″ в. д.HGЯO Страна  Казахстан Входит в Туркестанская область Адм. центр Шаян Аким Нурмаханов Ерлан Заипович История и география Дата образования 1928 Площадь 7200 км² Часовой пояс UTC+6 Население Насел�...

 

Brown dwarf

Type of substellar object larger than a planet Artist's concept of a T-type brown dwarfComparison: most brown dwarfs are slightly larger in volume than Jupiter (15–20%),[1] but are still up to 80 times more massive due to greater density. Image is to scale, with Jupiter's radius being 11 times that of Earth, and the Sun's radius 10 times that of Jupiter. Brown dwarfs are substellar objects that have more mass than the biggest gas giant planets, but less than the least massive main-s...

 

Nagahama Station

Railway station in Nagahama, Shiga Prefecture, Japan Nagahama Station長浜駅The east entrance of Nagahama Station, October 2010General informationLocation1 Kitafunachō, Nagahama-shi, Shiga-ken 526-0057JapanCoordinates35°22′43″N 136°15′55″E / 35.378483°N 136.265262°E / 35.378483; 136.265262Operated by JR WestLine(s) Hokuriku Main LineDistance7.7 km from MaibaraPlatforms1 side + 1 island platformConstructionStructure typeGround levelOther informationS...

Repubblica Autonoma di Naxçıvan

Questa voce o sezione sull'argomento Azerbaigian non cita le fonti necessarie o quelle presenti sono insufficienti. Puoi migliorare questa voce aggiungendo citazioni da fonti attendibili secondo le linee guida sull'uso delle fonti. Repubblica Autonoma di Naxçıvanrepubblica autonomaNaxçıvan Muxtar Respublikası Repubblica Autonoma di Naxçıvan – Veduta LocalizzazioneStato Azerbaigian AmministrazioneCapoluogoNaxçıvan GovernatoreVasif Talibov Lingue ufficialiazero TerritorioC...

 

Hangiri

Japanese wooden rice tub A hangiri. This example is 41 cm (16 in) in diameter. In Japanese cuisine, a sushi oke (寿司桶), also known as a hangiri, is a round, flat-bottomed wooden tub or barrel used in the final steps of preparing rice for sushi.[1] Traditional hangiri are made from cypress[citation needed] wood bound with two copper bands. They range in diameter from about 30 cm (12 in) for use at home, to 1 m (3 ft 3 in) for use in a res...

 

Morpheme

Smallest lexical item in a language Some of this article's listed sources may not be reliable. Please help improve this article by looking for better, more reliable sources. Unreliable citations may be challenged and removed. (January 2023) (Learn how and when to remove this message) Part of a series onLinguistics OutlineHistoryIndex General linguistics Diachronic Lexicography Morphology Phonology Pragmatics Semantics Syntax Syntax–semantics interface Typology Applied linguistics Acquisitio...

2002 New England 300

19th race of the 2002 NASCAR Winston Cup Series 2002 New England 300 Race details Race 19 of 36 in the 2002 NASCAR Winston Cup Series The 2002 New England 300 program coverDate July 21, 2002Official name 10th Annual New England 300Location Loudon, New Hampshire,New Hampshire International SpeedwayCourse Permanent racing facility1.058 mi (1.703 km)Distance 300 laps, 317.4 mi (510.805 km)Scheduled Distance 300 laps, 317.4 mi (510.805 km)Average speed 92.342 miles per hour (148.610 km/h)Pol...

 

لويس إيسلاس

لويس إيسلاس (بالإسبانية: Luis Islas)‏    معلومات شخصية الميلاد 22 ديسمبر 1965 (العمر 58 سنة)بوينس آيرس الطول 1.85 م (6 قدم 1 بوصة) مركز اللعب حارس مرمى الجنسية الأرجنتين  المسيرة الاحترافية1 سنوات فريق م. (هـ.) 1982 تشاكاريتا جيونيورز 21 (0) 1983–1986 إستوديانتيس دي لا بلاتا 107 (0) 1986...