07 - a helyettesítési algoritmus

previously on Heroes
Ugyan maga a "skolemizálás", aka zárt Skolem alakra hozás egy egyszerű algoritmusnak tűnik, formálisan bebizonyítani, hogy "helyes", mégsem olyan egyszerű.

Az outputja pl. nem lesz ekvivalens az eredeti formulával (vagy formulahalmazzal), hanem csak úgynevezett s-ekvivalens lesz (az "s" betű a "satisfiability"-ból, mint "kielégíthetőség" jön) :

Két formula, $F$ és $G$ $s$-ekvivalensek, jelben $F\equiv_s G$, ha

• vagy mindkettő kielégíthető,
• vagy mindkettő kielégíthetetlen.

A terv az, hogy megmutassuk: ha egy formulát skolemizálunk, akkor az eredmény az eredetivel $s$-ekvivalens lesz. 

Addig, hogy a nyilakat elimináltuk, nincs gond: ezt az ekvivalenciát már régről ismerjük, tetszőleges $\mathcal{A}$ struktúrára $\mathcal{A}(F\to G)=\mathcal{A}(\neg F\vee G)$, és mindkettő pontosan akkor lesz igaz, ha $\mathcal{A}(F)\leq\mathcal{A}(G)$.

A változóátnevezéssel gondok vannak: érzi az ember, hogy egy egyszerű refaktorral nem lehet gond... vagy mégis? Ha például a $\exists x(x<y)$ formulában az $x$ változót mondjuk épp $y$-ra akarjuk átnevezni, a kapott $\exists y(y<y)$ formula nem lesz vele ekvivalens, hiszen pl. az első igaz az egész számok struktúráján, bármi is $\varphi(y)$, bármilyen egész szánnál van kisebb, a második meg hamis ezen a struktúrán.Vagy egy eggyel összetettebb példa: a $\exists x(p(x)\wedge\exists y(x<y))$ formulában is ha az $x$ változót épp $y$-ra akarjuk átnevezni és csak átírjuk, akkor a kapott $\exists y(p(y)\wedge \exists y(y<y))$ formula megint csak nem lesz ekvivalens az eredetivel...viszont, ha mindenáron $y$-ra akarjuk átnevezni, és a másik $y$-t ezzel egyidőben mondjuk $z$-re átnevezzük, akkor a katpott $\exists y(p(y)\wedge\exists z(y<z))$ formula ekvivalens lesz az eredetivel.

A Skolem alakra hozáskor pedig egy változó helyére egy komplett termet írunk be, jó lenne, ha ezt a két dolgot (változóátnevezés + Skolem függvény bevezetése változó helyébe) egyben tudnánk bebizonyítani, hogy jó ötlet. Erről fog szólni a helyettesítés, aminek először megnézzük a (tádáááá felépítés szerinti indukciós) definícióját, és aztán kiderül, hogy miért is olyan jó. Persze mivel a formulákon belül termek vannak, először termekre nézzük meg, hogy mit is jelent egy termben egy változót egy termre helyettesíteni:

Ha $u$ egy term, $x$ egy változó és $t$ egy term, akkor $u[x/t]$ egy termet jelöl, melyet a következőképp kapunk ($u$ felépítése szerinti indukcióval): ha $u$ egy változó és $u=x$, akkor $u[x/t]:=t$. ha $u$ egy változó és $u\neq x$, akkor $u[x/t]:=u$. ha $u=f(t_1,\ldots,t_n)$ egy összetett term, akkor $u[x/t]:=f(t_1[x/t],\ldots,t_n[x/t])$.

Nézzük meg ezt egy példán: ha az $u=g(c,f(x,y),g(x))$  termen hajtjuk végre az $[x/h(z)]$ helyettesítést, akkor az $u[x/h(z)]$ termet így kapjuk: $\begin{align*}g(c,f(x,y),g(x))[x/h(z)]&=g(c[x/f(z)],f(x,y)[x/h(z)],g(x)[x/h(z)])&&\hbox{összetett term subst def}\\&=g(c,f(x[x/h(z)],y[x/h(z)]),g(x[x/h(z)]))&&\hbox{összetett term subst, note konstans: eltűnik}\\&=g(c,f(h(z),y),g(h(z)))&&\hbox{változó substok} \end{align*}$

ez általában is igaz: ha egy $u$ termen egy $[x/t]$ helyettesítést hajtunk végre, akkor az eredmény $u\cdot[x/t]$ termet úgy kapjuk, hogy simán kicseréljük az összes $u$-beli $x$-et $t$-re.
Más lesz a helyzet a formuláknál:

Ha $F$ egy formula, $x$ egy változó és $t$ egy term, akkor $F[x/t]$ egy formulát jelöl, melyet a következőképp kapunk $F$ felépítése szerinti indukcióval: ha $F=p(t_1,\ldots,t_n)$ atomi formula, akor $F[x/t]:=p(t_1[x/t],\ldots,t_n[x/t])$. tehát: atomi formulában ha az $x$-et $t$-re helyettesítjük, akkor csak kicseréljük az összes $x$-et $t$-re ha $F=\neg G$, akkor $F[x/t]:=\neg(G[x/t])$ ha $F=(G\bullet H)$, ahol $\bullet\in\{\vee,\wedge,\to,\leftrightarrow\}$, akkor $F[x/t]:=(G[x/t])\bullet(H[x/t])$ tehát: a logikai konnektívákon keresztül simán csak "migráljuk lefelé" a helyettesítést ha $F=\uparrow$ vagy $F=\downarrow$, akkor $F[x/t]:=F$ tehát: a logikai konstansok nem változnak meg attól, hogy egy változót helyettesítünk ha $F=Q xG$, $Q\in\{\exists,\forall\}$ (tehát: a kötött változó épp az, amit most helyettesítünk), akkor $F[x/t]:=F$ tehát: kötött változóelőfordulást nem helyettesítünk le ha $F=Q yG$, $Q\in\{\exists, \forall\}$, $y\neq x$ és $y$ nem fordul elő $t$-ben, akkor $F[x/t]:=\exists yG[x/t]$ tehát: ha más változót kötünk, akinek köze nincs $t$-hez, akkor nem kell semmi extrát csinálni ha $F=QyG$, $Q\in\{\exists,\forall\}$, $y\neq x$ és $y$ előfordul $t$-ben, akkor legyen $z$ egy új változó, aki nem $x$, nem $y$ és nem szerepel $G$-ben sem és $F[x/t]:=Qz(G[y/z][x/t])$. tehát, ha olyan kötött változón belül helyettesítjük $x$-et, aki szerepel a $t$ termben, akire helyettesítjük épp $x$-et, akkor át kell nevezzük a kötő kvantor változóját valami zsír újra.

Nézzük csak meg ezt egy példán:

$\begin{align*}&\Bigl(\exists x p(x,y)~\wedge~\forall y q(x,y)~\wedge~\exists z r(x,y)\Bigr)[x/f(y)]\\&=(\exists xp(x,y))[x/f(y)]~\wedge~(\forall yq(x,y))[x/f(y)]~\wedge~(\exists z r(x,y))[x/f(y)]&&\hbox{éselésen átmegy}\\&=(\exists xp(x,y))~\wedge~(\forall yq(x,y))[x/f(y)]~\wedge~(\exists z r(x,y))[x/f(y)]&&\hbox{a kötött előfordulások békén maradnak}\\&=(\exists xp(x,y))~\wedge~(\forall z(q(x,y)[y/z][x/f(y)]))~\wedge~(\exists z r(x,y)[x/f(y)])&&\hbox{kötő $t$-beli kvantor változóját átnevezzük, másikon átmegyünk}\\&=(\exists xp(x,y))~\wedge~(\forall z(q(x,z)[x/f(y)]))~\wedge~(\exists z r(x[x/f(y)],y[x/f(y)]))\\&=(\exists xp(x,y))~\wedge~(\forall z(q(f(y),z)))~\wedge~(\exists z r(f(y),y))\end{align*}$

Ez ugyanazt eredményezi, mint ha:

• a szabad $x$ előfordulásokat mindet $t$-re cseréljük,
• és ha így egy "lecserélt" $t$-ben egy változó "lekötődne", akkor az őt "véletlenül" lekötő kvantor változóját (ilyen több is lehet, ha $t$-ben van több változó is) átnevezzük valami egészen újra.

A kövi posztban megnézzük, hogy ez a helyettesítési értékadás tulajdonképpen ugyanaz, mint egy értékadás, de szemantikai helyett a szintaktikai szinten.

folytköv