Ortogonalitet (termomskrivning)

Ortogonalitet som en egenskap hos termomskrivningssystem (TRS) beskriver där reduktionsreglerna för systemet alla är vänsterlinjära, det vill säga varje variabel förekommer endast en gång på vänster sida av varje reduktionsregel, och det finns ingen överlappning mellan dem , dvs TRS har inga kritiska par . Till exempel $D(x,x)\to E$ inte vänsterlinjär.

Ortogonala TRS:er har den konsekventa egenskapen att alla reducerbara uttryck (redexer) inom en term är helt osammanhängande -- det vill säga redoxerna delar ingen gemensam funktionssymbol.

Till exempel TRS med reduktionsregler

$${\begin{array}{lrcl}\rho _{1}: \ &f(x,y)&\högerpil &g(y)\\\rho _{2}:\ &h(y)&\högerpil &f(g(y),y)\end{array}}$$

är ortogonal -- det är lätt att observera att varje reduktionsregel är vänsterlinjär, och den vänstra sidan av varje reduktionsregel har ingen funktionssymbol gemensam, så det finns ingen överlappning.

Ortogonala TRS är konfluenta .

Svag ortogonalitet

En TRS är svagt ortogonal om den är vänsterlinjär och endast innehåller triviala kritiska par, dvs om $(t,s)$ är ett kritiskt par så är $t=s$ . Svagt ortogonala TRS är konfluenta.

En TRS är nästan ortogonal om den är svagt ortogonal och har den ytterligare egenskapen att överlappning mellan redex-förekomster endast sker vid roten av redex-förekomsterna.