التعامد (إعادة صياغة المصطلح)

تُشير خاصية التعامد في أنظمة إعادة كتابة المصطلحات (TRSs) إلى أن قواعد الاختزال في النظام تكون جميعها خطية من اليسار، أي أن كل متغير يظهر مرة واحدة فقط على الجانب الأيسر من كل قاعدة اختزال، ولا يوجد تداخل بينها، أي أن نظام إعادة كتابة المصطلحات لا يحتوي على أزواج حرجة . على سبيل المثال${\displaystyle D(x,x)\to E}$ليست خطية من اليسار. ^{[ 1 ]}

تتمتع مقاييس TRS المتعامدة بالخاصية المترتبة على ذلك وهي أن جميع التعبيرات القابلة للاختزال (redexes) داخل مصطلح ما تكون منفصلة تمامًا - أي أن التعبيرات القابلة للاختزال لا تشترك في رمز دالة مشترك.

على سبيل المثال، نظام TRS مع قواعد التخفيض $${\displaystyle {\begin{array}{lrcl}\rho _{1}:\ &f(x,y)&\rightarrow &g(y)\\\rho _{2}:\ &h(y)&\rightarrow &f(g(y),y)\end{array}}}$$ متعامد - من السهل ملاحظة أن كل قاعدة اختزال خطية يسارية، والجانب الأيسر من كل قاعدة اختزال لا يشترك في أي رمز دالة مشترك، لذلك لا يوجد تداخل.

تتحد أنظمة TRS المتعامدة .

تكون عملية إعادة ترتيب المعاملات (TRS) متعامدة بشكل ضعيف إذا كانت خطية من اليسار وتحتوي فقط على أزواج حرجة تافهة، أي إذا${\displaystyle (t,s)}$إذا كان هذا زوجًا حرجًا${\displaystyle t=s}$[ ^{1 ]} تتحد أنظمة TRS المتعامدة بشكل ضعيف ^{. [ 2 ]}

تكون بنية TRS شبه متعامدة إذا كانت متعامدة بشكل ضعيف، ولها خاصية إضافية تتمثل في أن التداخل بين ظهورات redex يحدث فقط عند جذر ظهورات redex. ^{[ 3 ]}