Abstrakt. Termen omskrivningssystem (TRS) utökas genom att tillåta att innehålla extra variabler i sina omskrivningsregler. Vi kallar de utökade systemen EV-TRS. De är illvilliga eftersom varje minskning i ett steg av deras regler med extra variabler är oändligt förgrenad och de inte upphör. För att lösa dessa problem sträcker sig detta dokument till att begränsa TRS till det på EV-TRS och visar att det simulerar reduktionssekvenserna för EV-TRS som de förträngningssekvenser som utgår från marktermer. Vi bevisar sundheten i markförträngningssekvenserna för reduktionssekvenserna. Vi bevisar fullständigheten för fallet med högerlinjära system, och även för fallet att ingen redex i termer ersätta extra variabler minskas i reduktionssekvenserna. Dessutom ger vi en metod för att bevisa avslutandet av simuleringen, utvidga avslutandet av TRS med hjälp av beroendepar, till att minska på EV-TRS från och med markvillkor.
Nishida, Sakai och Sakabe REF anpassade metoden för beroendepar för att bevisa att begränsningen för TRS med extra variabler upphörde.
Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables
{'venue': 'In Proc. of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP’05', 'journal': None, 'mag_field_of_study': ['Computer Science']}