انجمن کامپیوتر ایران

سيستم¬ بازنويسي ترم (TRS) مدلي انتزاعي از زبان¬هاي تابعي ارائه مي¬دهد.اثبات پايان¬پذيرييکTRSبراي تاييد درستي عملکرد زبانهاي تابعيضروري است.روش برچسب¬گذاري معنايي(SL) روشي کامل براي اثبات پايان¬پذيري به شمار مي¬رود. بخش معنايياين روش توسط يک شبه-مدلاز تفسير تابع¬نشانه¬ها ايجاد مي¬شود. بيشتر توان روش SLبه استفاده از مدل¬هاي نامتناهي مربوط مي¬شود کهارائه آنها در ابزارهاي آزمون خودکار پايان¬پذيري دشوار است. در اين مقاله روش SL با دامنه تفسيراعداد طبيعي به شکلي با ترتيب کُنت-بنديکس (KBO) ترکيب شده تا بتوان اثبات پايان¬پذيري با مدل¬هاي نامتناهي را به طور خودکار انجام داد. ابتدا تعميمي از KBO به نام ترتيب کُنت-بنديکس برچسب¬گذاري(ℓKBO) ارائه، سپس توانايي آن را در اثبات پايان-پذيري TRS نشان داده¬ايم. الگوريتم جستجوي خودکار يک ℓKBO براي يک TRSمعرفيشده و عملکرد آن روي کتابخانه TPDB 3.1 با موفقيت مورد آزمون قرار گرفته است.