Қабаттасу (мерзімді қайта жазу) - Overlap (term rewriting)

Жылы математика, Информатика және логика, қабаттасу, қысқарту ережелерінің қасиеті ретінде мерзімді қайта жазу жүйесі, бірнеше түрлі қысқарту ережелерінде редекс ретінде белгілі азайтылатын өрнекті төмендетудің ықтимал қарама-қайшы тәсілдері көрсетілген жағдай сипатталады мерзім.^[1]

Дәлірек айтсақ, егер бірнеше кішірейту ережелері сол жақта функционалдық белгілерді бөліссе, қабаттасуы мүмкін. Көбінесе біз тривиальды редекспен және оның өзімен қабаттасуын қарастырмаймыз.

Мысалдар

Келесі қысқарту ережелерімен анықталған қайта жазу жүйесі терминін қарастырыңыз:

${displaystyle ho _ {1}: f (g (x), y) ightarrow y}$

${displaystyle ho _ {2}: g (x) ightarrow f (x, x)}$

Термин ${displaystyle f (g (x), y)}$ ρ арқылы азайтуға болады₁ өнім беру ж, бірақ оны ρ арқылы азайтуға болады₂ өнім беру ${displaystyle f (f (x, x), y).}$. Редекс қалай болатынына назар аударыңыз ${displaystyle g (x)}$ редекс құрамында болады ${displaystyle f (g (x), y)}$. Әртүрлі қызыл түстерді азайту нәтижесі а деп аталатын сипатталады сыни жұп; осы мерзімді қайта жазу жүйесінен туындайтын маңызды жұп ${displaystyle (f (f (x, x), y), y)}$.

Екіден кем қысқарту ережелерімен қабаттасуы мүмкін.

Келесі қысқарту ережесімен анықталған қайта жазу жүйесі терминін қарастырыңыз:

${displaystyle ho _ {1}: g (g (x)) ightarrow x}$

Термин ${displaystyle g (g (g (x)))}$ ішкі немесе сыртқы көріністеріне қолданылуы мүмкін қабаттасқан редекстерге ие ${displaystyle g (g (x))}$ мерзім.

Әдебиеттер тізімі

Бұл математикалық логика - қатысты мақала а бұта. Сіз Уикипедияға көмектесе аласыз оны кеңейту.