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

06 - Elsőrendű normálformák

previously on Heroes

Tehát most a célunk az, hogy egy következtető rendszert adjunk meg, ami elsőrendű logikai formulák egy $\Sigma$ halmazára és egy $F$ célformulára ha $\Sigma\vDash F$ igaz, akkor arra előbb-utóbb rájön, ha meg nem következmény, akkor nem jön ki azzal a válasszal, hogy "következménye".

(Olyan algoritmus matematikailag igazoltan nincs, ami arra is garantáltan rájönne, hogy nem következménye egy formula egy másiknak, itt a legjobb amit remélhetünk, az az, hogy vagy rájön az algoritmus, hogy nem következmény, vagy végtelen ciklusba esik.)

Erre a problémára (ezen a kurzuson) kétféle rezolúciós algoritmust fogunk nézni: az egyiknek a neve "alap rezolúció" lesz, a másiké meg (ravasz módon) "elsőrendű rezolúció". Mindkettő, hasonlóan az ítéletkalkulus-beli változatukhoz, arra lesz jó, hogy egy input formulahalmazról megmutassa, hogy kielégíthetetlen, azzal, hogy levezeti belőle az üres klózt.

Ugyanúgy, ahogy a ítéletkalkulus rezolúciós algoritmusához is egy ottani normálformára (CNF-re) kellett hozni az inputot, itt is: ezt a normálformát zárt Skolem (ejtsd: Szkólem) alaknak hívják.

Ebben a posztban megnézzük, hogy hogyan hozunk egy formulát zárt Skolem alakúra, az eredmény "magját" pedig CNF-re, a következőben pedig bebizonyítjuk, hogy amit csinálunk, az jó lesz, ha az input kielégíthetetlenségét akarjuk bizonyítani. (Ez most nem lesz ekvivalens az inputtal, amit gyártunk, de "majdnem". Ezt a következőből megértjük.)

Tehát, induljunk ki egy formulából, az algoritmust példán keresztül is visszük végig. Legyen mondjuk ez: $\forall x(\exists yp(f(x),y)~\to r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg r(z)$.

1. Elimináljuk a $\to$ és $\leftrightarrow$ konnektívákat a szokásos $\begin{align*}F\to G&\equiv\neg F\vee G&F\leftrightarrow G&\equiv(\neg F\vee G)\wedge(F\vee\neg G)\end{align*}$ azonosságokkal.

   
   

   Most ennek az eredménye ezen a formulán  az egyetlen $\to$ konnektíva kiütése után: $\forall x(\neg\exists yp(f(x),y)~\vee r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg r(z)$

2. Kiigazítás: Átnevezzük a változókat, hogy különböző kvantor előfordulások különböző változókat kössenek le, és ne legyen olyan változó sem, ami szabadon is és kötötten is előfordul. A szabad változókat nem nevezhetjük át. Ennek egy módja pl (ha az input formulánkban amúgy nincsenek indexelve a változók), hogy indexeljük az összes kötött változót, akár $1$-től kezdve sorfolytonosan, minden egyes kvantornál növelve az indexet, akár változónként külön-külön indexet vinni, mindegy, csak ne legyen névütközés. Arra persze figyeljünk oda, hogy ha egy kvantor mellett álló változót átnevezünk valamire, akkor pontosan azokat a változóelőfordulásokat kell átneveznünk ugyanerre, melyeket ez a kvantorelőfordulás köt.

   
   

   A munkaformulánkon ennek a lépésnek ez lesz (pl) az eredménye: $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$ Itt most minden kvantorelőfordulás egy közös indexet növelt. Látszik, hogy a $z$ az egyetlen változó, mely előfordul szabadon is, de azt kétszer teszi. Nem baj.

3. Prenex alakra hozás: ennek a lépésnek az a célja, hogy az összes kvantor a formula elejére kerüljön. Ezt tehetjük pl. a következő kvantorkihúzási azonosságokkal, amik akkor igazak, ha a formula kiigazított: $\begin{align*}(Qx F)\bullet G&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\F\bullet(QxG)&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\\neg\exists xF&\equiv\forall x\neg F\\\neg\forall xF&\equiv \exists x\neg F\end{align*}$

   Ha ezeket a szabályokat alkalmazgatjuk a munkaformulánkon, akkor ilyesmi lépéseket kapunk: $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$  $\forall x_1(\forall y_2\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$  $\forall x_1\forall y_2(\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$ és ezen a ponton van négy formulánk éselve, mindnek az elején kvantorok, kihozzuk mindet:  $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$

   
   
   Egy másik módszer, ami kézzel végrehajtva gyorsabb kicsit, ha az ember átlátja a formulát (programmal mindenképp gyorsabb, ha a formulánkat fában reprezentáljuk):
   

   • fogjuk az eredeti kigazított, nyílmentesített formulát
   • a benne levő kvantált változókat balról jobbra, az eredeti deklarációs sorrendben kötjük le
   • egy változót lekötő kvantor "megfordul" ($\exists$-ből $\forall$ lesz és fordítva), ha páratlan sok $\neg$ jel hatáskörébe esik; ha pároséba, akkor nem fordul meg
   • végül, a formula magját (így hívják a prenex formuláknak azt a részformuláját, amelyikben már épp nincs kvantor) úgy kapjuk, hogy az eredeti formulából kitöröljük a kvantorokat.

   Ezt végrehajtva az előzőre: kiindulunk ebből
   

   $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$

   a sorrend $x_1$, $y_2$, $x_3$, $y_4$, $z_5$ lesz; három negálás van a formulában, nincsenek egymásba ágyazva, így ezt most egyszerű látni, hogy csak az $\exists y_2$ az egyetlen kvantált változó, aki páratlan sok (egy) negálás belsejében van, így ő az egyetlen, aki megfordul. A kvantor prefix tehát $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5$ lesz. Utánaírjuk a formulánkat úgy, hogy kitöröljük a kvantorokat éééés:
   

   $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$

   yep, ugyanaz lett, mint az előbb.

4. Skolem alakra hozás: ennek a lépésnek a célja, hogy csak $\forall$-kvantorok maradjanak a formulában (és persze maradjon prenex alakban). Az előző lépések ekvivalens átalakítások voltak, ez már nem lesz az. Ahogy csináljuk: kiindulunk a prenex, kiigazított alakból minden egyes $\exists y$-ra kitöröljük az $\exists y$-t a formula elejéről és $y$ minden előfordulásának helyébe a magban egy $f(x_1,\ldots,x_n)$ termet írunk ahol is $f$ egy teljesen új függvényjel (amit Skolem függvénynek is hívnak), amit most generáltunk -- ha egyszerre több formulát hozunk Skolem alakra, akkor meg kell nézni, hogy egyikben sem szerepelhet! Ha több Skolem függvényjelet generálunk, akkor mind egymástól is különböző kell legyen! az $x_1,\ldots,x_n$ változók pedig azok, akik az $y$ előtt (attól balra) vannak $\forall$ kvantorral kötve a formulában.

   nézzük ezt a munkaformulánkon, itt tartunk: $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$ sok dolgunk nincs ezzel most, egyetlen $\exists$ kvantor van benne, ami $x_3$-at köti. Keresünk egy új függvényjelet, amit még nem használunk, ez pl most lehet $g$ ($f$ viszont nem), és függni fog $x_1$-től és $y_2$-től, mert azok vannak $x_3$ előtt univerzálisan deklarálva. Tehát, töröljük a $\exists x_3$ részt és a formulában $x_3$ minden előfordulása helyébe $g(x_1,y_2)$-t írunk: $\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$ ez így most kész is, a formula Skolem alakú.

5. Lezárás: ennek a lépésnek a célja, hogy ne legyen szabad változónk. Ezt úgy érjük el, hogy minden $x$ szabad változóelőfordulás helyébe egy új, $x$-től függő konstanst, pl. $c_x$-et írunk. Szintén fontos, hogy a konstans új legyen, itt viszont ha több formulában is szerepel szabadon ugyanaz az $x$, akkor mindegyikben ugyanazt a $c_x$-et kell írjuk a helyébe!

   
   

   Folytatva az előző példánkat: $z$ az egyetlen szabadon előforduló változó, ő kétszer is szerepel, helyére bekerül a $c_z$ konstans: $\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(c_z))~\wedge~\neg q(c_z)~\wedge~\neg r(z_5)\Bigr)$

6. A mag CNF-re hozása: teljesen ugyanazzal a módszerrel, mint ítéletkalkulusban, a zárt Skolem alakú formulánk magját CNF-re hozzuk. Most literál minden atomi formula (ők pozitívak) és azok negáltjai (ők negatívak), vagyis a predikátumjellel kezdődő, vagy esetlegesen negált predikátumjellel kezdődő részek klóz továbbra is véges sok literál vagyolása a CNF pedig továbbra is klózok éselése

Ha megnézzük, a mostani munkaformulánkban literálok pl. a $\neg p(f(x_1),y_2)$, az $r(x_1)$, a $p(y_4,f(g(x_1,y_2)))$, a $q(c_z)$, a $\neg q(c_z)$ és a $\neg r(z_5)$, de most teljesen jól vannak, literálok vannak vagyolva egy- vagy kéttagú klózokká, és ilyen klózból van négy. Akár le is írthatjuk őket egy $\Sigma$ klózhalmazba, ugyanúgy halmazként reprezentálva mindent, mint ítéletkalkulusban tettük: $\left\{\{\neg p(f(x_1),y_2),r(x_1)\},~\{p(y_4,f(g(x_1,y_2))),q(c_z)\},~\{\neg q(c_z)\},~\{\neg r(z_5)\}\right\}$.

Ez minden; mindkét rezolúciós algoritmus ebben a formátumban, zárt Skolem alakú formulákként, melyeknek a magját CNF-re hoztuk és az összes klózt egy $\Sigma$ halmazba tesszük. Hogy mit tesznek vele, azt meglátjuk, miután megnézzük, hogy ezek az átalakítások tényleg jók lesznek nekünk.

A kapcsolódó gyakanyag a hetedik és a nyolcadik és érdemes lehet nyomkodni itt a "Generálj Skolemest!" gombot, hogy biztos értsük a zárt Skolem normálformára hozás minden részletét. (Itt nem kell CNF-re hozni a magot.)

folytköv

05 - a Peano axiómák

previously on Heroes

Addig tehát megvagyunk, hogy hiába tűnnek faék egyszerűnek a természetes számok a szorzással meg az összeadással, már erre a struktúrára sincs algoritmus, ami ki tudna benne értékelni egy input formulát.

Olyan algoritmus viszont lesz, ami arra alkalmas, hogy egy input elsőrendű $\Sigma$ formulahalmazra és egy elsőrendű $F$ formulára igaz, hogy $\Sigma\vDash F$, akkor erre véges idő alatt rá is jöjjön.

Persze ezek a jelek itt is ugyanazt jelentik, mint ítéletkalkulusban:

hogy az $\mathcal{A}$ struktúrában az $F$ formula értéke $1$, azt írjuk úgy is, hogy $\mathcal{A}(F)=1$, úgy is, hogy $\mathcal{A}\vDash F$, úgy is, hogy $\mathcal{A}\in\mathrm{Mod}(F)$, úgy is mondjuk, hogy $\mathcal{A}$ kielégíti $F$-et és úgy is, hogy $\mathcal{A}$ egy modellje az $F$-nek ha $F$ formula, akkor $\mathrm{Mod}(F)$ az összes olyan struktúra osztálya (note: az osztály olyan, mint egy halmaz, csak lehet nagyobb is; struktúrákból simán lehet olyan sok, hogy nem férnek bele egy halmazba, ezért $\mathrm{Mod}(F)$ officially "osztály", nem "halmaz" de a mi szempontunkból nem lesz különbség), amik kielégítik $F$-et: $\mathrm{Mod}(F)~:=~\{\mathcal{A}:~\mathcal{A}\vDash F\}$ ha $F$ és $G$ formulák, akkor $F\vDash G$ azt jelöli, hogy $\mathrm{Mod}(F)\subseteq\mathrm{Mod}(G)$, úgy mondjuk, hogy $F$-nek következménye $G$ (és továbbra is azt jelenti tehát, hogy ha egy $\mathcal{A}$ struktúrában $F$ igaz, akkor $G$ is) formulák helyett föntebb mindenhol írhatunk formulahalmazt is: $\mathcal{A}\vDash\Sigma$ akkor igaz, ha $\mathcal{A}$ modellje $\Sigma$ összes elemének $\mathrm{Mod}(\Sigma)$-ban azok a struktúrák vannak benne, melyek modelljei $\Sigma$ összes elemének $\Sigma\vDash F$ azt rövidíti, hogy $\mathrm{Mod}(\Sigma)\subseteq\mathrm{Mod}(F)$, azaz hogy $\Sigma$-nak $F$ következménye $\Sigma\vDash\Gamma$ azt, hogy $\mathrm{Mod}(\Sigma)\vDash F$ minden $F\in\Gamma$-ra

Mivel itt megint a $\vDash$ által meghatározott Galois-kapcsolatról beszélünk, így az abból kijövő dolgok, amiket néztünk ítéletkalkulusban, itt is megmaradnak, majd amikor szükség lesz rájuk, listázom őket.

Tehát, ha az ember a számokról akar bizonyítani egy formulát, azaz a természetes számok szokásos $\mathcal{N}=(\mathbb{N}_0,I)$ struktúrájában akarja megmutatni egy $F$ mondatra, hogy $\mathcal{N}\vDash F$, akkor erre egy módszer az, hogy felírunk egy csomó formulát egy $\Sigma$ halmazba, melyekről tudjuk, hogy igazak a természetes számokra, és eztán az $F$ formulánkra megpróbáljuk bebizonyítani, hogy $\Sigma\vDash F$. A logikai következmény fogalma miatt ha ez sikerül, akkor mivel $\mathcal{N}\vDash\Sigma$, ezért ekkor $\mathcal{N}\vDash F$ is igaz lesz és a formula tényleg igaz ebben a struktúrában.

(Ilyen bizonyítást majd a Floyd-Hoare kalkulusban fogunk látni, ott visszatérünk erre még.)

A természetes számokra nagyon gyakran használt ilyen $\Sigma$ formulahalmaz a Peano-féle axiómarendszer. Ebben a struktúrában használjuk a $+/2$, $\times/2$ és $'/1$ függvényjeleket, előbbieket infix, utóbbit posztfix szoktuk írni, interpretációjuk rendre az összeadás, szorzás és növelés eggyel, a $0/0$ konstansjelet, aki a $0$ számot jelöli és a $\leq/2$ predikátumjelet (az $=/2$ mellett), ami pedig a szokásos kisebb-egyenlő relációt. Az axiómák:

$\forall x(\neg(x'=0))$. ez igaz, hiszen azt állítja, hogy minden $n\in\mathbb{N}_0$ természetes számra $n+1\neq 0$. $\forall x\forall y(x'=y'~\to~x=y)$ ez meg azt, hogy ha $n+1=m+1$, akkor $n=m$. Persze, az eggyel növelés függvény injektív. $\forall x(x+0=x)$ hát igen, ha valamihez nullát adunk, nem változik $\forall x\forall y(x+y'=(x+y)')$ eszerint meg $n+(m+1)=(n+m)+1$, ez is stimmel $\forall x(x\times 0=0)$ yep, bármit nullával szorozva nullát kapok $\forall x\forall y(x\times y'=x\times y+x)$ disztributivitás: tetszőleges $n,m$ természetes számokra $n\times(m+1)=n\times m+n$, oké $\forall x(x\leq 0~\to~x=0)$ ez is stimmel, ha egy természetes szám legfeljebb nulla, akkor az nulla $\forall x\forall y(x\leq y'~\to~(x\leq y\vee x=y'))$ ez azt mondja, hogy ha $n\leq m+1$, akkor vagy $n\leq m$, vagy pedig $n=m+1$. Stimmel, hiszen ha $n>m$, és $n\leq m+1$, akkor $n$ csak $m+1$ lehet. Ez az axióma lényegében azt állítja, hogy $n$ és $n+1$ között nincs több természetes szám. $\forall x\forall y(x\leq y\vee y\leq x) stimmel ez is, ezpz és az indukciós axióma séma: $(F(0)\wedge(\forall x(F(x)\to F(x'))))\to\forall x F(x)$  ahol $F=F(x)$ egy olyan formula, amiben csak az $x$ változó szerepel szabadon, az $F(0)$ az $F$-ből úgy áll elő, hogy a szabad $x$-ek helyére $0$-t írunk mindenhol, az $F(x')$ meg úgy, hogy $x'$-t. ez azt állítja, hogy ha egy formula igaz $0$-ra és az is igaz, hogy tetszőleges $n$ esetén ha a formula igaz $n$-re, akkor igaz $n+1$-re is, akkor a formula igaz minden természetes számra. Ez is igaz, ezen alapszik a teljes indukció.

Tehát azt, hogy valami igaz a természetes számok struktúrájában, sokszor úgy szoktuk megmutatni, hogy "mert következménye a Peano axiómáknak". Egyelőre következtető algoritmusunk nincs az elsőrendű logikában, de nézünk egyet, amit ha valaki nem ért meg elsőre, nem baj:

Meg akarjuk mondjuk mutatni, hogy $\forall x\forall y\forall z(z\times(y+x)=z\times y+z\times x)$. Ez a teljes disztributivitás, az ilyesmiről szóló Peano axióma az csak $x=1$-re mondja, hogy teljesül.  Ha levágjuk a formula elejéről az első kvantort: $F=\forall y\forall z(z\times(y+x)=z\times y+z\times x)$ pont egy olyan formulát kapunk, amiben egy szabad változó szerepel, ez történetesen most épp $x$, de lehetne más is. Ha ezzel az $F=F(x)$-szel az indukciós axióma sémát akarjuk powerelni, akkor először is meg kell néznünk, hogy $F(0)$ következik-e e a Peano axiómákból: $F(0)=\forall y\forall z(z\times(y+0)=z\times y+z\times 0)$ ez kéne következzen belőlük. Ugyan még nem ismerünk következtetési szabályt, de a következők elég validnak tűnnek: $\begin{align*}\forall x(x+0=x)&\vDash\forall y(y+0=y)\tag{változó átnevezés}\\\forall x(x\times 0=0)&\vDash\forall z(z\times 0=0)\tag{változó átnevezés}\\\forall y(y+0=y)&\vDash\forall y\forall z(z\times(y+0)=z\times y)\\\forall x(x+0=x)&\vDash\forall y\forall z(z\times y=z\times y+0)\\\{\forall y\forall z(z\times (y+0)=z\times y),~\forall y\forall z(z\times y=z\times y+0)\}&\vDash\forall y\forall z(z\times(y+0)=z\times y+0)&\tag{az egyenlőség tranzitív}\\\forall z(z\times 0=0)&\vDash\forall y\forall z(z\times y+0=z\times y+z\times 0)\\\{\forall y\forall z(z\times(y+0)=z\times y+0), \forall y\forall z(z\times y+0=z\times y+z\times 0)\}&\vDash\forall y\forall z(z\times(y+0)=z\times y+z\times 0)&\tag{az egyenlőség tranzitív}\end{align*}$ ami épp $F(0)$. Tehát ez seems kijön a Peano axiómákból. Vajon az indukciós axióma séma középső része, $\forall x(F(x)\to F(x'))$ is következik belőlük? Írjuk ki: $\forall x\Bigl(\forall y\forall z(z\times (y+x)=z\times y+z\times x)\to\forall y\forall z(z\times (y+x')=z\times y+z\times x')\Bigr)$ hm. Ezt már az olvashatóság kedvéért informálisabban írom, hogy hogy megy: $z\times (y+x)=z\times y+z\times x$-ből indulunk. Az $x\times y'=x\times y+x$ axiómát használva kapjuk, hogy $z\times(y+x)'=z\times (y+x)+z$, majd ezen a jobb oldali $z\times (y+z)=z\times y+z\times x$-et átírva kapjuk, hogy $z\times(y+x)'=z\times y+z\times x+z$. Ennek a jobb oldalán a $x\times y'=x\times y+x$ axiómát "alkalmazva" "jobbról balra" kapjuk, hogy$z\times(y+x)'=z\times y+z\times x'$. A bal oldalán még alkalmazzuk az $(x+y)'=x+y'$ axiómát is, és kapjuk, hogy $z\times(y+x')=z\times y+z\times x'$. És pont ezt akartuk kihozni, ez a $F(x)\to F(x')$ implikáció jobb oldala erre az $F$-re! Ezért mivel az indukciós axióma séma bal oldalán lévő éselés mindkét tagja kijön a Peano axiómákból, így le tudjuk vezetni a jobb oldalát is és kapjuk, hogy következményük a $\forall x\forall y\forall z(z\times(y+x)=z\times y+z\times x)$ formula is. weeee.

Érdemes észrevenni, hogy a levezetés közben semmilyen plusz tudást nem vetettünk be a számokról, kizárólag az axiómákat használtuk és (valamiféle) logikai követktetéseket, amik a formulák szintaktikus átirkálásával készültek, azok jelentésének ismerete nélkül!
Ez pedig azért lesz jó, mert így van rá esély, hogy algoritmizálható.
Mindenesetre, levezettük, hogy a természetes számok struktúrájában az $x\times(y+z)=(x\times y)+(x\times z)$ azonosság teljesül, hiszen következménye a Peano axiómáknak.
Felmerül a kérdés, hogy mit lehet tenni, ha nem sikerül levezetnünk, hát, ilyenkor vagy az van, hogy nem is igaz a mondat a természetes számokra és meg lehet próbálni levezetni az ellentétét; ha ez se jön össze, akkor vagy csak nem vártunk eleget, hogy kijöjjön a következtetés, vagy fel kell venni még axiómát, ami garantáltan igaz a természetes számokra, hátha azzal együtt már ki tudja hozni a következtető rendszer...

folytköv

04 - elég a szabad változók értékét megadni - bizonyítás

previously on Heroes

Tehát, most nézzük meg formálisan, hogy tényleg kijön a "formula értékét egy struktúrában csak a benne szabadon elődorduló változók alapértéke befolyásolja, a többié nem" állítás.

Mivel a szokásos módon indukcióval látjuk be, ezért előbb a termekkel kezdjük. Ott minden változó "szabad", aki csak előfordul, hiszen termben nincs kvantor. Másrészt, azt, hogy "nem befolyásolja", azt úgy mondhatjuk matekul, hogy "ha két struktúra megegyezik mindenben, kivéve esetleg olyan változók alapértékét, ami nincs is a termben, akkor bennük a term értéke ugyanaz lesz", hiszen ez jelenti azt, hogy tkp mindegy, milyen alapértéket adunk ezeknek a változóknak.

Formálisan:

Legyen $t$ term, $\mathcal{A}=(A,I,\varphi)$ és $\mathcal{A}'=(A,I,\varphi')$ pedig két struktúra, melyekben minden $t$-ben előforduló $x$ változó esetén $\varphi(x)=\varphi'(x)$.  Akkor $\mathcal{A}(t)=\mathcal{A}'(t)$.

A bizonyítás $t$ felépítése szerinti indukcióval zajlik ofc:

ha a $t$ term egy $x$ változó, akkor $t$-ben persze hogy előfordul $x$, ezért a feltétel szerint $\varphi(x)=\varphi'(x)$. Másrészt az $\mathcal{A}$ struktúrában a term kiértékelés definíciója szerint $\mathcal{A}(t)=\varphi(x)$, a másikban pedig $\mathcal{A}'(t)=\varphi'(x)$. Összerakva kijön az egyenlőség: $\mathcal{A}(t)=\varphi(x)=\varphi'(x)=\mathcal{A}'(t)$ . ha pedig $t=f(t_1,\ldots,t_n)$ egy összetett term, akkor ugye tudjuk az állítás feltételéből, hogy minden $x$-re, aki $t$-ben bárhol szerepel, igaz, hogy $\varphi(x)=\varphi'(x)$. Persze aki bármelyik $t_i$-ben szerepel, az $t$-ben is, ezért az is igaz, hogy minden $i$-re minden $t_i$-beli $x$ változóra $\varphi(x)=\varphi'(x)$. Ezért a $t_i$-kre, akik egyszerűbb termek, mint $t$, alkalmazhatjuk az indukciós feltevést, ebből azt kapjuk, hogy minden $i$-re $\mathcal{A}(t_i)=\mathcal{A}'(t_i)$. Összerakva az összetett term kiértékelésének definíciójával a két struktúrában kijön az egyenlőség: $\begin{align*}\mathcal{A}(f(t_1,\ldots,t_n))&=I(f)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))\tag{term kiértékelés def}\\&=I(f)(\mathcal{A}'(t_1),\ldots,\mathcal{A}'(t_n))\tag{indukció}\\&=\mathcal{A}'(f(t_1,\ldots,t_n)).\tag{term kiértékelés def}\end{align*}$

Ez nem volt nehéz, de csak azért csináltuk, hogy a formulákra vonatkozó ugyanilyen állítás (ami viszont fontos, hogy csak a szabad változókra vonatkozzon!) atomi formulákra vonatkozó részét be tudjuk látni. Lássunk neki:

Legyen $F$ formula, $\mathcal{A}=(A,I,\varphi)$ és $\mathcal{A}'=(A,I,\varphi')$ pedig két struktúra, melyekben minden, $F$-ben szabadon előforduló $x$ változóra $\varphi(x)=\varphi'(x)$. Akkor $\mathcal{A}(F)=\mathcal{A}(F)$.

A bizonyítás (surprise) $F$ felépítése szerinti indukcióval zajlik, sok eset van:

ha az $F$ formula egy $p(t_1,\ldots,t_n)$ atomi formula, akkor benne minden változóelőfordulás szabad. Tehát a feltétel azt mondja, hogy minden $F$-beli $x$ változóra $\varphi(x)=\varphi'(x)$. Persze ami egy $t_i$ termben előfordul, az az őt tartalmazó $F$-ben is, ezért az is igaz az állítás feltétele szerint, hogy minden $i$-re igaz, hogy minden, a $t_i$-ben előforduló $x$ változóra $\varphi(x)=\varphi'(x)$. Ezért, alkalmazhatjuk a termekre vonatkozó, az imént belátott állításunkat és azt kapjuk, hogy minden $i$-re $\mathcal{A}(t_i)=\mathcal{A}'(t_i)$. Ezt kombinálva az atomi formula kiértékelésének definíciójával a két struktúrában, kijön az egyenlőség: $\begin{align*}\mathcal{A}(p(t_1,\ldots,t_n))&=I(p)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))\tag{atomi szemantika def}\\&=I(p)(\mathcal{A}'(t_1),\ldots,\mathcal{A}'(t_n))\tag{indukció}\\&=\mathcal{A}'(p(t_1,\ldots,t_n)).\tag{atomi szemantika def}\end{align*}$ Nyilván ha $F=\uparrow$ vagy $F=\downarrow$, akkor $\mathcal{A}(F)=\mathcal{A}'(F)$, bármi is van. Konstans $1$ vagy konstans $0$. (most jönnek az unalmas részek) Ha $F=(\neg G)$, akkor ami $G$-ben szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben szabadon előfordul, $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a negálás szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(\neg G)&=\neg\mathcal{A}(G)\tag{$\neg$ kiértékelés def}\\&=\neg\mathcal{A}'(G)\tag{indukció}\\&=\mathcal{A}'(G)\tag{$\neg$ kiértékelés def}\end{align*}$ Ha $F=(G\vee H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a vagyolás szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\vee H)&=\mathcal{A}(G)\vee\mathcal{A}(H)&\tag{$\vee$ kiértékelés def}\\&=\mathcal{A}'(G)\vee\mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\vee H)\tag{$\vee$ kiértékelés def}\end{align*}$ Ha $F=(G\wedge H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit az éselés szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\wedge H)&=\mathcal{A}(G)\wedge \mathcal{A}(H)&\tag{$\wedge $ kiértékelés def}\\&=\mathcal{A}'(G)\wedge \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\wedge H)\tag{$\wedge $ kiértékelés def}\end{align*}$ Ha $F=(G\to H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit az implikáció szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\to H)&=\mathcal{A}(G)\to \mathcal{A}(H)&\tag{$\to $ kiértékelés def}\\&=\mathcal{A}'(G)\to \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\to H)\tag{$\to $ kiértékelés def}\end{align*}$ Ha $F=(G\leftrightarrow H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a kettősnyíl szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\leftrightarrow H)&=\mathcal{A}(G)\leftrightarrow \mathcal{A}(H)&\tag{$\leftrightarrow $ kiértékelés def}\\&=\mathcal{A}'(G)\leftrightarrow \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\leftrightarrow H)\tag{$\leftrightarrow $ kiértékelés def}\end{align*}$ Ha $F=\exists xG$ vagy $F=\forall xG$ alakú formula, akkor elég azt belátnunk, hogy minden $a\in A$ objektum esetén $\mathcal{A}_{[x\mapsto a]}(G)=\mathcal{A}'_{[x\mapsto a]}(G)$, hiszen ezekből az értékekből számítjuk ki $\mathcal{A}(F)$-et és $\mathcal{A}'(F)$-et. A $G$ formulában kik fordulhatnak elő szabadon? Ugyanazok, mint akik $F$-ben, plusz esetleg $x$. (Ha $G$-ben nincs szabadon $x$, azaz ha a kvantor le se kötött senkit, akkor csak azok, akik $F$-ben, egyébként még $x$ is pluszban.) No de akkor a $G$-beli szabadon előforduló összes (mondjuk) $y$ változóra vagy $y$ szabadon előfordult $F$-ben is, ezért az állítás feltétele miatt $\varphi(y)=\varphi'(y)$ volt és mivel $x\neq y$ (az $x$ mindenhol kötve van $F$-ben, hiszen kvantált $x$-szel kezdődik), ezért a két $[x\mapsto a]$-val származtatott struktúrában nem írtuk át az értékeiket, így azokban is megegyezik a default értékük; vagy $y=x$, de annak meg a default értéke $\mathcal{A}_{[x\mapsto a]}$-ban is és $\mathcal{A}'_{[x\mapsto a]}$-ban is $a$, tehát megegyezik. Ezért az indukciós feltevést alkalmazhatjuk $G$-re a két származtatott struktúrában és kapjuk, hogy minden $a\in A$-ra $\mathcal{A}_{[x\mapsto a]}(G)=\mathcal{A}'_{[x\mapsto a]}(G)$. Ami miatt persze $\begin{align*}\mathcal{A}(\exists G)=1&\Leftrightarrow\hbox{van olyan }a\in A\hbox{, melyre }\mathcal{A}_{[x\mapsto a]}(G)=1&\tag{$\exists$ def}\\&\Leftrightarrow\hbox{van olyan }a\in A\hbox{, melyre }\mathcal{A}'_{[x\mapsto a]}(G)=1\tag{ezt láttuk be az előbb}\\&\Leftrightarrow\mathcal{A}'(\exists G)=1\tag{$\exists$ def}\end{align*}$ és $\begin{align*}\mathcal{A}(\forall G)=1&\Leftrightarrow\hbox{minden }a\in A\hbox{-ra }\mathcal{A}_{[x\mapsto a]}(G)=1&\tag{$\forall$ def}\\&\Leftrightarrow\hbox{minden }a\in A\hbox{-ra }\mathcal{A}'_{[x\mapsto a]}(G)=1\tag{ezt láttuk be az előbb}\\&\Leftrightarrow\mathcal{A}'(\forall G)=1\tag{$\forall$ def}\end{align*}$.

Látszik, hogy a bináris konnektívákra vonatkozó esetek tényleg copypaste készíthetőek, meg a két kvantor esete is nagyon hasonló: legközelebb már az ilyeneket összevonjuk úgy, hogy "ha $\bullet\in\{\vee,\wedge,\to,\leftrightarrow\}$, akkor$\ldots$".

Mindenesetre, kijött, hogy a formula értéke tényleg csak a benne szabadon előforduló változók default értékétől függ, a többitől nem.

Ezért:

Egy mondat értéke egy $\mathcal{A}=(A,I,\varphi)$ struktúrában a $\varphi$-től nem függ. Ezért ha mondatok értékéről beszélünk, úgy $\varphi$-t elhagyhatjuk és egy struktúrára úgy tekintünk, mint egy $\mathcal{A}=(A,I)$ párra.

folytköv

03 - elsőrendű logika - még pár jelölés

previously on Heroes

Nézzünk pár fogalmat, aztán megpróbálunk kiértékelni egy "egyszerű"(nek tűnő) struktúrában formulákat.

Az előző postban a kvantoros formula kiértékelésekor érezhettük, hogy a "kvantoron belül" a változó már a "kvantortól kapja" az értéket legalábbis abban az értelemben, hogy mire odajut a kiértékelés, már nem számít, hogy mit adott neki eredetileg a struktúrában a $\varphi$ függvény. Most ezt formalizáljuk le egy kicsit (főleg azért, mert később a bizonyításokban szükség lesz ezekre a fogalmakra és állításokra).

Egy formulában minden változó minden egyes előfordulása vagy szabad lesz, vagy egy kvantorelőfordulás fogja kötni (az "előfordulás" tkp azt jelenti, hogy nem "az $x$ változó" lesz szabad a formulában, hanem a "hatodik karakteren álló $x$ változó", és lehet, hogy a formulában egy máshol levő $x$ meg nem lesz szabad. Kvantorokra ugyanez: fontos lesz, hogy melyik kötött változóelőfordulást melyik kvantor köti le). Informálisan (avagy konyhanyelven): ha egy $x$ változóelőfordulás egy $\exists x$ vagy egy $\forall x$ kvantor hatáskörén belülre (azaz a mögötte álló formulába, amivel konstruáltuk) esik, akkor az az $x$ kötve van; mégpedig, ha több ilyen kvantorelőfordulásnak is beleesik a hatáskörébe, akkor a legbelső ilyen fogja kötni.

Például: $\color{blue}{\exists x}\Bigl(~p(y)~\wedge~\color{red}{\exists y}(q(\color{blue}{x},\color{blue}{x}))~\wedge~\color{brown}{\exists x}(p(\color{brown}{x}))~\Bigr)$ a formulában az egyes kvantor-előfordulások az ő színükre színezett változóelőfordulásokat kötik. A fekete változóelőfordulás szabad. Note: a kvantor mellett álló változó nem "változóelőfordulás"!

Formálisan: az $F$ formula szabad előfordulásai (persze, hogy $F$ felépítése szerinti indukcióval):

ha $F$ atomi formula, akkor benne minden változóelőfordulás szabad; ha $F=\uparrow$ vagy $F=\downarrow$ alakú formula, akkor benne nincs szabad változóelőfordulás; ha $F=(\neg G)$ alakú formula, akkor benne $G$ összes szabad változóelőfordulása szabad; a kötött változóelőfordulásokat ugyanazok a kvantorok kötik $F$-ben, mint akik $G$-ben kötötték őket ha $F=(G\vee H)$,  $(G\wedge H)$, $(G\to H)$ vagy $(G\leftrightarrow H)$ alakú, akkor benne mind a $G$, mind a $H$ összes szabad változóelőfordulása szabad; a kötött változóelőfordulásokat ugyanazok a kvantorok kötik $F$-ben, mint akik $F$-ben / $G$-ben kötötték őket; ha $F=(\exists xG)$ vagy $F=(\forall xG)$ alakú, akkor a $G$-beli kötött változóelőfordulások $F$-ben is kötöttek, ugyanazon kvantor által; a $G$-beli szabad $x$ változóelőfordulások $F$-ben kötöttek, az $F$ elején álló kvantor által; a többi változó $G$-beli előfordulásai $F$-ben is szabadok.

Ha ezt így végigjátsszuk a fönti formulára: $p(y)$-ban az $y$ szabadon fordul elő, $q(x,x)$-ben az $x$ szintén mind a két helyen, $p(x)$-ben az $x$ szabad, mert ezek atomi formulák. $\color{red}{\exists y}(q(x,x))$-ben a két $x$ előfordulás szabad, más változó nem fordul elő benne (így, mivel $y$ nincs szabadon $q(x,x)$-ben, a $\exists y$ kvantor nem köt le semmit). $\color{brown}{\exists x}(p(\color{brown}(x))$-ben $p(x)$-ben az $x$ eredetileg szabad előfordulás volt, most pont az $x$ változót kötöttük le, így ezt a szabad előfordulást ez az (ebben a formulában) legkülső kvantor leköti. Ebben a formulában nincs szabad változóelőfordulás. $p(y)~\wedge~\color{red}{\exists y}(q(x,x))~\wedge~\color{brown}{\exists x}(p(\color{brown}(x))$-ben, mivel ez egy éselés, az marad szabad, aki eredetileg is az volt: az első $y$ előfordulás, és a középső részformula két $x$-e. (A fekete változóelőfordulások.) A többieket az a kvantor köti, aki eddig is. végül, $\color{blue}{\exists x}\Bigl(~p(y)~\wedge~\color{red}{\exists y}(q(\color{blue}{x},\color{blue}{x}))~\wedge~\color{brown}{\exists x}(p(\color{brown}{x}))~\Bigr)$ az előzőhöz képest még leköti a szabad $x$ előfordulásokat, vagyis a középső részformula két $x$-ét. Az $y$ szabad marad. És tényleg pont azt kaptuk vissza, mint amit az előbb az informális def alapján színeztünk, great.

Az éselés harmadik tagjában nem volt szabad változóelőfordulás, az ilyeneket mondatnak nevezzük.

Egy formula mondat, ha nincs benne szabad változóelőfordulás.

Ha egy $F$ formulában az  $x_1,\ldots,x_n$ változók fordulnak elő szabadon, azt úgy is jelezzük, hogy $F=F(x_1,\ldots,x_n)$. Például az előző formulára $F=F(y)$, mert benne $y$-nak volt szabad előfordulása.

A szabad változóelőfordulások például azért érdekesek, mert egy $\mathcal{A}=(A,I,\varphi)$ struktúrában ha egy $F=F(x_1,\ldots,x_n)$ formulát akarunk kiértékelni, akkor $\mathcal{A}(F)$ értéke $\varphi$-nek csak a $\varphi(x_1),\ldots,\varphi(x_n)$ részétől függ, az $F$-ben szabadon nem szereplő változóknak mindegy, mi az értéke, ezért azt nem is kell megadni. Ezt a következő posztban be is bizonyítjuk, egyelőre fogadjuk el és nézzük a megígért kiértékelés példát, hosszú lesz:

A jelkészlet, amink van: vannak a $+/2$ és $\times/2$ függvényjelek, az $1$ konstansjel, az $=/2$ predikátumjel. A struktúra, amiben ki akarunk értékelni: $\mathbb{N}=(\mathbb{N}_0,I,\varphi)$, azaz az alaphalmaz a természetes számok, $I(+)$ és $I(\times)$ a szokásos összeadás és szorzás, $I(1)=1$ (azaz az $1$-es jel tényleg az $1$-es számot jelöli) $I(=)$ az egyenlőség (más nem is lehet). A formulák, amiknek megnézzük a szemantikáját ebben a struktúrában (infix írva a bináris függvény- és predikátumjeleket): $\exists z(x\times z=y)$. Ez a formula pontosan akkor igaz, ha létezik olyan $c$ természetes szám, melyre $\varphi(x)\times c=\varphi(y)$, azaz pontosan akkor, ha $\varphi(x)$ osztója $\varphi(y)$-nak. Ezt a formulát rövidítsük úgy, hogy $x|y$. $\exists z(x+z=y)$. Ez a formula pontosan akkor igaz, ha létezik olyan $c$ természetes szám, melyre $\varphi(x)+c=\varphi(y)$, azaz pontosan akkor, ha $\varphi(x)\leq\varphi(y)$. Ezt a formulát rövidítsük úgy, hogy $x\leq y$. Az $(x\leq y)\wedge\neg(x=y)$ formulát pedig úgy, hogy $x<y$. $1<x~\wedge~\neg\exists z(1<z~\wedge~z<x~\wedge~z|x)$ akkor igaz, ha $\varphi(x)$ egy $1$-nél nagyobb természetes szám, melynek nem létezik olyan osztója, aki szigorúan $1$ és $x$ közé esne -- tehát pontosan akkor, ha $\varphi(x)$ prímszám. Jelölje ezt a formulát $\mathrm{prime}(x)$. $\exists x( y<x~\wedge~\mathrm{prime}(y)~\wedge~\mathrm{prime}(y+1+1) )$ pontosan akkor igaz, ha $\varphi(y)$-nél létezik egy olyan nagyobb $a$ természetes szám, aki prímszám és a nála kettővel nagyobb szám is prímszám. Itt a $\mathrm{prime}(y+1+1)$ formula azt jelenti, hogy a $\mathrm{prime}$ formulába, aminek eredetileg $x$ volt a szabad változója, a szabad változója helyébe mindenhová az $y+1+1$ termet írjuk be és átnevezzük a belső kvantált változókat úgy, hogy ne ütközzön a nevük az $y$-nal. Ahogy a $\mathrm{prime}(y)$ is azt, hogy $y$-t írjunk a szabad változó, $x$ helyébe. Ezért paraméterezzük fel a szabad változókkal a formulákat, mint $\mathrm{prime}(x)$: általában ezeket mint "shorthand"eket használjuk és a szabad $x$-ek helyére valami más termet írunk. $\forall y\exists x( y<x~\wedge~\mathrm{prime}(y)~\wedge~\mathrm{prime}(y+1+1) )$ ezek szerint pontosan akkor igaz, ha minden természetes számnál van nagyobb prímszám, akinél a kettővel nagyobb szám is prímszám. Ez a legutolsó pedig egy mondat, tehát a $\varphi$ nem is kell hozzá, azaz neki "a" természetes számok struktúrájában van egy igazságértéke: igaz akkor, ha végtelen sok "ikerprím" (a $2$ különbségű prímeket így hívják) van és hamis, ha csak véges sok. Pl. ikerprímek az $(5,7)$, $(11,13)$, $(17,19)$, $(101,103)$. Ha megpróbáljuk kiértékelni, hogy ez vajon igaz vagy hamis, akkor (vélhetően) falba ütközünk: a mai napig senki nem tudja, hogy ez az állítás vajon igaz-e.

A rövidítés jó dolog: ha kiírjuk ezt az előző formulát fullosan, rövidítés nélkül az eredeti jelekkel, akkor ezt kapjuk kb:

$\begin{align*}\forall y\exists x( \exists z(y+z=x)&~\wedge~\neg\exists z(\exists w(1+1+w=z)\wedge\exists w(z+1+w=x)\wedge\exists w(z\times w=x))\\&\wedge\neg\exists z(\exists w(1+1+w=z)\wedge\exists w(z+1+w=x+1+1)\wedge\exists w(z\times w=x+1+1)))\end{align*}$

Rövidítéseket használva azért eggyel olvashatóbb volt.
De miért nem adja oda senki egy kiértékelő algoritmusnak ezt a formulát akkor és várja ki a választ? Azért, mert matematikailag be van bizonyítva, hogy ilyen kiértékelő algoritmus nem létezik. Ha ebben a struktúrában (természetes számok, összeadás, szorzás) akarunk kiértékelni egy formulát, arra nem lehet programot írni, ami mindig helyes válasszal jönne vissza és minden formulára megállna.

Ez pedig nagyon függ a struktúrától, amiben számolni akarunk:

• a valós számok struktúráján az összeadással és a szorzással van ilyen algoritmus. Lassú, de van.
• a természetes számok struktúráján csak az összeadással, szorzás nélkül, szintén van ilyen algoritmus.
• a valós számok struktúráján az összeadással, a szorzással és az $x\mapsto e^x$ függvénnyel nem tudjuk, hogy van-e ilyen algoritmus.

Ezért, mivel a kiértékelés nagyon könnyen kiszámíthatatlanul bonyolulttá válik, ahelyett, hogy egy formulát megpróbálnánk kiértékelni, inkább azt próbáljuk automatikusan bebizonyítani, hogy a formula kielégíthetetlen. Erre érdekes módon több esélyünk van: van olyan algoritmus, ami

• ha az input $F$ formula kielégíthetetlen, akkor arra véges sok idő alatt rájön;
• ha meg kielégíthető, akkor vagy arra jön rá véges sok idő alatt, vagy végtelen ciklusba esik.

 Ez ugyan nem hangzik annyira fényesen, de a helyzet az, hogy ennél jobbat nem lehet csinálni: nincs olyan algoritmus (read as: matematikailag be van bizonyítva, hogy ilyen algoritmus nem létezik), ami véges idő alatt garantáltan megáll és mindig helyes választ adna arra a kérdésre, hogy az input $F$ formula kielégíthetetlen-e vagy kielégíthető.
A kapcsolódó gyakanyag a hetedik, érdemes hozzáolvasni.

folytköv

02 - Elsőrendű logika - szemantika

previously on Heroes
Ítéletkalkulusban ha volt egy formulánk, könnyedén kiértékelhettük: csak adnunk kellett egy változó-értékadást, ami a változóknak beállította az értékét 0-ra vagy 1-re, és ezeket az értékeket alulról felfelé terjesztettük, a végén megkapva az egész formula értékét.

Az alulról felfelé értékelés továbbra is megmarad, de a "változóértékadás" helyett egy sokkal komplexebb dolgot kell megadjunk, ha formulát akarunk kiértékelni: egy struktúrát. ami egy

$\mathcal{A}~=~(A,I,\varphi)$

hármas. (Ez csak annyit jelent, hogy három dolgot kell megadjunk, az elsőnek a neve $A$ lesz, a másodiké $I$, a harmadiké $\varphi$, mindjárt mondom, hogy minek mi a "típusa" és ezt a hármat együtt elnevezhetjük $\mathcal{A}$-nak is. Általában egy struktúrát nagy "írott" betűvel jelölünk, az első komponensét ugyanannak a betűnek a sima nagybetűs változatával.)

Egy ilyen hármasban

$A$ egy nemüres halmaz, az objektumok halmaza, hívják alaphalmaznak vagy univerzumnak is. (őket veszik majd fel értékül a termek.) $\varphi$ a változóknak egy "default" értékadása, azaz egy olyan függvény, ami minden $x$ változóhoz egy $\varphi(x)\in A$ objektumot rendel. $I$ pedig az interpretációs függvény, ami a függvény- és predikátumjeleknek ad "jelentést": az $f$ függvényjelhez az $I(f)$-fel jelölt függvényt, a $p$ predikátumjelhez az $I(p)$-vel jelölt predikátumot rendeli. Konkrétan: ha $f/n$ egy ($n$-változós) függvényjel, akkor $I(f)$ egy $A^n\to A$ függvény ha $p/n$ egy ($n$-változós) predikátumjel, akkor $I(p)$ egy $A^n\to\{0,1\}$ predikátum. itt van egy megkötés: ha van $=/2$ predikátumjel, akkor $I(=)$ mindenképp tényleg az egyenlőség predikátum kell legyen.

Például ha a függvényjeleink $f/1$, $g/2$ és $c/0$, predikátumjeleink pedig $p/1$ és $q/2$, akkor egy struktúra lehet pl. az az $\mathcal{A}=(A,I,\varphi)$, ahol $A=\mathbb{N}_0=\{0,1,2,\ldots\}$ a természetes számok ($0$-t is tartalmazó) halmaza; $\varphi(x)=2$, $\varphi(y)=3$, $\varphi(z)=7$, \ldots (nem adom meg az egészet, de mind a végtelen sok változónak van valami alap értéke) az $I$ interpretációs függvényünk pedig $f$-hez egy $\mathbb{N}_0\to\mathbb{N}_0$ függvényt, $g$-hez egy $\mathbb{N_0}^2\to\mathbb{N_0}$ függvényt, $c$-hez egy $\to\mathbb{N}_0$ függvényt, azaz egy $\mathbb{N}_0$-beli értéket kell rendeljen, $p$-hez egy egyváltozós $\mathbb{N}_0\to\{0,1\}$ predikátumot, $q$-hoz pedig egy $\mathbb{N}_0\times\mathbb{N}_0\to\{0,1\}$ predikátumot. Akár így:  $\begin{align*}I(f)(n)&:=n+1&&\hbox{tehát $f$ az ,,adj hozzá egyet'' függvény}\\I(g)(n,m)&:=n+2m&&\hbox{why not, függvény ez is}\\I(c)&=7&&\hbox{konstans, egy eleme az alaphalmaznak}\\I(p)(n)=1&\Leftrightarrow n\hbox{ prímszám}&&\hbox{predikátumról azt adjuk meg pl, hogy mikor igaz}\\I(q)(n,m)=1&\Leftrightarrow n<m\end{align*}$

(note to self: a $\LaTeX$ben lévő text fonttal kezdenem kell valamit.)

Egy ilyen struktúra már elegendő információt szolgáltat ahhoz, hogy minden termnek legyen egy értéke benne és minden formulának is (bár ezt az értéket nem biztos, hogy ki is lehet számítani!). Kezdjük a termekkel, hiszen alulról kifelé akarunk kiértékelni és a termek vannak "belül". Ez lesz az egyszerűbb is, hiszen a termeknek összesen két konstruktora volt:

Ha $t$ egy term és $\mathcal{A}=(A,I,\varphi)$ egy struktúra, akkor $t$ értéke $\mathcal{A}$-ban egy $A$-beli objektum lesz, amit $\mathcal{A}(t)$-vel jelölünk (tehát mintha a termet behelyettesítenénk $\mathcal{A}$-be, mint függvénybe) és felépítés szerinti indukcióval definiálunk (ami még mindig annyit jelent, hogy minden képzési szabályra felírunk egy "ha a termet így építettük fel, akkor ez legyen az értéke, ha úgy, akkor az" szabályt úgy, hogy használhatjuk a "kisebb" termek értékét is. Mégpedig így:

ha a $t$ term egy $x$ változó, akkor $\mathcal{A}(t)~:=~\varphi(x)$ azaz: a változók értékét $\varphi$ mondja meg ha pedig a $t$ term egy $f(t_1,\ldots,t_n)$ alakú összetett term, akkor $\mathcal{A}(t)~:=~I(f)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))$. azaz: ha egy összetett termet kell kiértékelnünk, akkor rekurzívan értékeljük ki az "argumentumait", majd ezt a kapott $n$ objektumot helyettesítsük be abba a függvénybe, amit $\mathcal{A}$-ban jelöl a term gyökérszimbóluma (a képen ez az $f$, ami jelöli az $I(f)$ függvényt).

és ez minden, mert ez a két konstruktorunk volt.

Például az előző struktúrában a természetes számok fölött: $\mathcal{A}(x)=\varphi(x)=2$, ez volt $x$ alapértéke a példa struktúra $\varphi$-jében $\mathcal{A}(f(x))=I(f)(\mathcal{A}(x))=I(f)(2)=2+1=3$, mert az $f$ ebben a struktúrában az "adj hozzá $1$-et" függvény volt, az argumentum értéke pedig $2$ $\mathcal{A}(g(f(x),y))=I(g)(3,3)=3+2\cdot 3=9$, mert $g$ volt az "add össze az első argumentumot és a második dupláját" függvény, az első argumentumának az értéke $3$, a másodiké pedig $\varphi(y)=3$ szintén

A formulák kiértékelése eggyel komplikáltabb és kell hozzá még egy jelölés, mert a kvantorok megváltoztatják a változók értékét (ha informatikusul akarjuk elképzelni, akkor kb "végighúznak egy ciklust a változó összes lehetséges értékével"):

Ha $\mathcal{A}=(A,I,\varphi)$ egy struktúra, $x$ egy változó, $a\in A$ pedig egy objektum, akkor $\mathcal{A}_{[x\mapsto a]}$ azt a struktúrát jelöli, ami összesen annyiban tér el $\mathcal{A}$-tól, hogy benne $x$ default értéke $a$, minden más ugyanaz. Vagyis: $\mathcal{A}_{[x\mapsto a]}=(A,I,\varphi')$, tehát ugyanaz marad az objektumok halmaza és minden függvény- és predikátumjel is ugyanazt jelenti, csak a változók default értékadása változik $\varphi'$-vé, ahol  $\varphi'(x)=a$ (erre változott) és minden másik $y\neq x$-re $\varphi'(y)=\varphi(y)$ (a többi változó értéke nem változik).

Most, hogy ez a jelünk megvan, definiálhatunk: ha $F$ egy formula és $\mathcal{A}$ egy struktúra, akkor $F$ értéke $\mathcal{A}$-ban egy $\{0,1\}$-beli igazságérték lesz, amit $\mathcal{A}(F)$-fel jelölünk és $F$ felépítése szerinti indukcióval definiálunk. Csak most sok eset van, mert formulákat szintaktikailag is sokféleképp építhettünk fel. Mégpedig:

Ha $F=p(t_1,\ldots,t_n)$, akkor $\mathcal{A}(F)~:=~I(p)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n)).$ azaz: ha atomi formulát kell kiértékelnünk, akkor először is kiértékeljük benne a termeket, aztán megnézzük, hogy milyen predikátumot jelöl ebben a struktúrában a gyökérszimbólum (ami itt most $p$), és ebbe a predikátumba behelyettesítjük az $n$ darab termünk értékeit a megfelelő sorrendben. Ha $F=\uparrow$, akkor $\mathcal{A}(F)~:=~1$ (az $\uparrow$ formula igaz, ok) Ha $F=\downarrow$, akkor $\mathcal{A}(F)~:=~0$ (a $\downarrow$ formula hamis, ok) Ha $F=(\neg G)$, akkor $\mathcal{A}(F)~:=~\neg\mathcal{A}(G)$ (ha egy $\neg G$ alakú formulát kell kiértékelnünk, akkor értékeljük ki a $G$-t és negáljuk az eredményt, ok) Ha $F=(G\vee H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\vee\mathcal{A}(H)$ (ha egy vagyolást, akkor értékeljük ki a két közvetlen részformulát és vagyoljuk az eredményeket) Ha $F=(G\wedge H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\wedge\mathcal{A}(H)$ (éselésre ugyanez) Ha $F=(G\to H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\to\mathcal{A}(H)$ (implikációra ugyanez) Ha $F=(G\leftrightarrow H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\leftrightarrow\mathcal{A}(H)$ (duplanyílra ugyanez, eddig semmi meglepetés nem történt) Ha $F=\exists xG$, akkor $\mathcal{A}(F):=\begin{cases}1&\hbox{ha van olyan }a\in A\hbox{, melyre }\mathcal{A}_{[x\mapsto a]}(G)=1\\0&\hbox{ha nincs}\end{cases}$ azaz: mintha végigmennénk egy "ciklussal" az $x$ összes lehetséges értékén, és ha találunk egyet is, melyre beállítva $x$-et a formula "magja" igaz lesz, akkor ez a formula is igaz, ha meg mindenre hamis lesz, akkor hamis. Ha $F=\forall xG$, akkor $\mathcal{A}(F):=\begin{cases}1&\hbox{ha minden }a\in A\hbox{-ra }\mathcal{A}_{[x\mapsto a]}(G)=1\\0&\hbox{ha nem}\end{cases}$ azaz: mintha végigmennénk egy "ciklussal" az $x$ összes lehetséges értékén, és ha találunk egyet is, melyre beállítva $x$-et a formula "magja" hamis lesz, akkor ez a formula is hamis ha meg mindenre igaz lesz, akkor igaz.

Például ebben az előző struktúrában $\mathcal{A}(p(f(x)))=I(p)(\mathcal{A}(f(x)))=I(p)(3)=1$, mert $I(p)(n)$ akkor volt $1$, ha $n$ prímszám és a $3$ egy prímszám. $\mathcal{A}(\forall xp(f(x)))$ akkor igaz, ha minden $a\in\mathbb{N}_0$-ra $\mathcal{A}_{[x\mapsto a]}(p(f(x))=1$. De mivel pl. az $a=3$-ra $\mathcal{A}_{[x\mapsto 3]}(p(f(x)))=I(p)(I(f)(3))=I(p)(4)=0$, mert ebben a struktúrában $x$ értéke $3$, $3+1$ az $4$ és a $4$ nem prímszám, ezért van olyan $a$, melyre a mag hamis lesz, ha erre állítjuk $x$ értékét, ezért $\mathcal{A}(\forall x p(f(x)))=0$.

A következő posztban majd látjuk, hogy ez azért nem megy mindig ilyen könnyen.
A kapcsolódó gyakanyag a hetedik, érdemes hozzáolvasni.

folytköv

01 - Elsőrendű logika - szintaxis

Ítéletkalkulusban egyszerű volt a dolgunk: voltak a $p_1,p_2,\ldots$ ítéletváltozóink, amiket lehetett összekötni a szokásos konnektívákkal, és ennyi: ami így felépült, az formula volt, ami meg nem, az nem, ennyi volt a szintaxis.

Elsőrendű logikában viszont a változók (amiket "individuum"változóknak nevezünk teljes néven, de mostantól őket illeti a default "változó" kifejezés) nem egy szimpla 1/0 (avagy igaz/hamis) értéket vesznek fel kiértékeléskor, hanem egy objektumot valamiféle alaphalmazból. Adja magát, hogy máris kétféle "szintaktikus kategóriára" lesz szükségünk: egy olyanra, ami objektumot vesz majd fel értékül (ők lesznek majd a "term"-ek), és egy olyanra, ami egy 1/0 bitet, igazságértéket (ők meg a "formulák").

Sőt, lesznek függvényjeleink és predikátumjeleink is: amikor aláteszünk egy "melyik jel mit is jelent"-et (egy struktúrát, ez lesz a szemantika része), akkor mindkettő objektumokat vár majd inputként, nullát, egyet, kettőt vagy többet, a különbség az output lesz: a függvényjelhez rendelt tényleges függvény objektumot ad vissza, a predikátumjelhez rendelt predikátum pedig igazságértéket.

Egyelőre amíg a szintaxist adjuk meg, addig csak azt mondjuk meg, hogy milyen stringeket fogadunk el valamilyen típusú kifejezésnek (termnek vagy formulának), addig persze a jelentésükkel nem foglalkozunk, ez a szemantika része lesz (de azért valami intuíció nem árthat).

Szóval, elsőrendű logikában ami féle jeleket használunk:

• (individuum)változókat: nekik "hivatalosan" $\{x_1,x_2,x_3,\ldots \}$ a halmazuk, de azért, hogy a példák könnyebben parsolhatóak legyenek, fogunk használni betűket az ábécé környékéről is változónak, pl $x$, $y$, $z$, $w$, vesszőzve, indexelve ízlés szerint.
• függvényjeleket: az ő halmazuk az $\{f_1,f_2,f_3,\ldots\}$, de az ábécé elejét kb. $h$-ig megint csak függvényjeleknek fogjuk lefoglalni a példákban. Minden függvényjelnek van egy aritása, ami "változószámot" jelent, természetes szám (lehet $0$ is), azt adja meg, hogy hány változós ez a függvény; ha az $f$ függvényjel $n$-változós, azt $f/n$ fogja jelölni.
• például a jól ismert "összeadás" az egy kétváltozós függvény, a "szorzás kettővel" meg egyváltozós függvény, így az őket jelölő függvényjelek aritása 2, ill. 1 lesz. 
• Nullaváltozós függvény egy konstans: nem kap semmi inputot és kiad egy objektumot, az tkp maga az objektum lesz. A nulla aritású függvényjeleket konstansjelnek hívjuk.
• A példákban  $a$-tól $d$-ig fogjuk általában a konstansjeleket, $f$-től $h$-ig a nem-konstans függvényjeleket jelölni. $e$-t nem használunk :D
• predikátumjeleket: az ő halmazuk a $\{p_1,p_2,p_3,\ldots\}$ (pont úgy, mint eddig az ítéletváltozóké volt; ez nem véletlen), de az ábécénak a $p,q,r$ betűit erre fogjuk használni. A predikátumjeleknek is van aritásuk, ha $p$ egy $n$-változós predikátumjel, azt $p/n$ jelöli.
• például az "egyenlőség" az egy bináris predikátum lesz: bejön két objektum, eredmény akkor igaz, ha ugyanaz a két objektum, egyébként hamis. Ennek a predikátumnak a jele = lesz. A (valós, mondjuk) számok közt a "kisebb" szintén egy bináris predikátum: bejön két szám, igaz, ha a bal oldali kisebb, mint a jobb oldali, ezt a predikátumot jelölheti például a $</2$  predikátumjel.
• Nullaváltozós predikátum is lehet: nem kap semmi inputot és kiad egy igazságértéket.. ilyet már láttunk, a nulla aritású predikátumjeleket ítéletváltozóknak hívjuk majd.
• logikai konnektívákat: $\neg$, $\vee$, $\wedge$, $\to$, $\leftrightarrow$, $\uparrow$, $\downarrow$, az utolsó kettőt "logikai konstansjelnek" is hívjuk.
• nyitójelet $($, csukójelet $)$, vesszőt $,$ szeparátornak.

Ezekből a jelekből megint csak szintaktikai szabályokkal építhetünk fel valid stringeket, csak most kétfélét:  az első a termek szintaktikus kategóriája, aminek a képzési szabályai:

minden változó term ha $f/n$ függvényjel és $t_1,\ldots,t_n$ termek, akkor $f(t_1,\ldots,t_n)$ is term más term nincs.

Például ezek szerint ha $x$ és $y$ változók, $c/0$ konstansjel, $f/1$ (egyváltozós) függvényjel és $g/2$ (kétváltozós) függvényjel, akkor $x$ term, mert változó. $y$ is term, mert változó. $f(x)$ is term, mert $f$ egyváltozós függvényjel és belehelyettesítettünk egy termet, $x$-et. $g(y,f(x))$ is term, mert $g/2$ függvényjel, amibe behelyettesítettünk két termet, $y$-t és $f(x)$-et. $c()$ is term, mert $c/0$ függvényjel (konstansjel) és belehelyettesítettünk nulla termet. $g(c(),c())$ is term, mert $g/2$ függvényjel és belehelyettesítettünk két termet, $c()$-t és aztán megint $c()$-t.

A könnyebb olvashatóság kedvéért

• a konstansjeleknél $c()$ helyett csak $c$-t írunk (fontos, hogy így "külsőre" úgy néznek ki, mint a változók! ezért fontos, hogy lássuk, hogy az ábécé elején van a betű - akkor konstans -, vagy a végén - akkor változó -, ha élünk ezzel az egyszerűsítéssel)
• "megszokott" függvényjeleknél, mint pl a $+/2$, infix is írjuk a függvényt: $+(x,y)$ helyett $x+y$ alakban.

 A formuláknak több képzési szabálya van:

ha $p/n$ predikátumjel és $t_1,\ldots,t_n$ termek, akkor $p(t_1,\ldots,t_n)$ egy formula. Ezeket atomi formulának is nevezzük. ha $F$ és $G$ formulák, akkor formulák még $(F\vee G)$, $(F\wedge G)$, $(F\to G)$, $(F\leftrightarrow G)$, $(\neg F)$ is. $\uparrow$ és $\downarrow$ is formulák. ha $x$ változó és $F$ formula, akkor $(\exists x F)$ és $(\forall x F)$ is formulák. más formula nincs.

Például ezek szerint ha $x$ és $y$ változók, $c/0$ konstansjel, $f/1$ és $g/2$ függvényjelek, $p/1$ (egyváltozós) predikátumjel, $r/2$ (kétváltozós, bináris) predikátumjel és $q/0$ nulla változós predikátumjel, azaz konstans, akkor  $p(x,f(y))$ egy (atomi) formula, mert $p/2$ predikátumjel, amibe behelyettesítettünk két termet, $x$-et és $f(y)$-t. $q()$ is atomi formula: $q/0$ predikátumjel, amibe behelyettesítettünk nulla darab termet. A zárójelet itt is elhagyhatjuk és maradhat csak $q$ is. $r(g(c,x))$ is atomi formula: $r/1$ predikátumjel, amibe behelyettesítettünk egy darab termet, $g(c,x)$-et. $(p(x,f(y))\wedge r(g(c,x)))$ két formula éselése, ez is formula. $\exists x(p(x,f(y))\wedge r(g(c,x)))$ egy formula elé betett kvantált változó, ez is formula. $\exists x(p(x,f(y))\wedge r(g(c,x)))\to q$ is formula, két formula van összekötve egy implikációval. (note: elhagytuk a kvantált rész körüli zárójelet, megint elhagyhatunk zárójeleket precedencia alapon. A kvantorok kötnek erősebben, mint a logikai konnektívák!) $\forall x(\exists x(p(x,f(y))\wedge r(g(c,x)))\to q)$ is formula, egy formula elé tettünk egy kvantált változót. (igen, ugyanazt, ami már le volt kötve. ez nem baj, szabadnak szabad, csak ritkán van értelme.) Nem valid string viszont például $x\vee\neg x$, mert negálni-vagyolni formulát lehet, de az $x$ az változó, tehát term  $\exists x(f(x))$, mert kvantálni formulát lehet, de az $f(x)$ term. $g(c)$ (az előző jelkészlet mellett), mert $g/2$-be két termet kéne helyettesíteni, nem csak egyet. $f(p(x))$, mert $x$ term, $p(x)$ formula, de $f/1$-be aki függvényjel, formulát nem helyettesíthetünk, csak termet.

Ennyi az elsőrendű logika szintaxisa. A következő a szemantika lesz, amiben megmondjuk, hogy ha az alap jeleknek adunk egy jelentést, hogy lesz abból értéke egy egész termnek, vagy egy egész formuláknak.
Önellenőrzésként érdemes lehet nyomkodni itt párszor a "Generálj Szintaktikus Elemzőset!" gombot, és megpróbálni eltalálni, hogy a string valid-e vagy sem, és ha nem, akkor hol is hibás, hogy biztos értünk-e minden képzési szabályt :)
A kapcsolódó gyakanyag a hatodik, érdemes hozzáolvasni.

folytköv

14 - az immutable generic List osztály

Természetesen a lista mint adatszerkezet annyira alap komponense a funkcionális programozás eszköztárának, hogy van belőle built-in, nem kell újra írnunk mindig egyet. Nagyon sokrétű, a funkcionalitásai egy részével össze fogunk ismerkedni a félév során, mindenesetre:

• A típus neve $\mathrm{List}$ (teljes neve $\mathrm{scala.collection.immutable.List}$, de a Scala $\mathrm{Predef}$ objektumában szerepel mint type alias, ezért látszik a rövid neve is.
• Generic típus, a lista elemeinek típusát kapja paraméterként. Pl. az eddigi $(1,4,2,8,5,7)$ példánk $\mathrm{List}[\mathrm{Int}]$ típusúnak felel meg.
• Az eddigi $\mathrm{Ures}$ objektumunknak (amit genericként egyelőre csak mint case classt tudtunk összehozni) megfelelő üres lista a $\mathrm{Nil}$ nevű objektum. Igen, objektum, és mindenféle típusú generic listának megfelel, ezt később jobban meg fogjuk érteni.
• Az eddigi $\mathrm{Nemures}$ lista objektumunknak megfelelő osztály neve $\mathrm{::}$. Két kettőspont. Tehát akár így is létrehozhatunk egy $(1,4,2)$ értéket a mostani tudásunk alapján:
  

  
  val list: List[Int] = ::(1,::(4,::(2,Nil)))
  

• A $\mathrm{::}$ osztály nevét a fenti prefix (avagy lengyel) jelölés helyett infix is használhatjuk konstruáláskor, így szokás (és figyeljük meg, hogy ennek is ki tudja következtetni a type inference, hogy $\mathrm{List}[\mathrm{Int}]$ lesz:
  

  
  val list = 1 :: 4 :: 2 :: Nil
  

• A companion object apply metódusának köszönhetően így is létrehozhatjuk ugyanezt:
  

  
  val list = List(1,4,2,8,5,7)
  

• A $\mathrm{List}[T]$-ben egyebek mellett szerepelnek a $\mathrm{filter}(p:T\Rightarrow\mathrm{Boolean}):\mathrm{List}[T]$ és a $\mathrm{map}[U](f:T\Rightarrow U):\mathrm{List}[U]$ függvények, pontosan ugyanazzal a viselkedéssel, mint amit az előző posztokban láttunk.
• A $\mathrm{toString}$ metódusa visszaadja a $\mathrm{List}$ szót, majd zárójelek közé zárva vesszővel elválasztva a lista elemeit.
• Lehet rá mintailleszteni, az elv ugyanúgy megy, mint a saját korábbi implementációnkban: a nemüres listának van egy feje és egy farka, $\mathrm{head :: tail}$-ként is illeszthető rá a minta, így szoktuk kiírni, de persze fordul a $\mathrm{::(head,tail)}$ minta is.
• Egy hasznos metódusa a $\mathrm{zip}$, ami egy másik listával "pároztatja össze" úgy, hogy egy $\mathrm{List}[T]$ zipje egy $\mathrm{List}[U]$ zipjével egy $(T,U)$ párokat tartalmazó lista, vagyis egy $\mathrm{List}[(T,U)]$ lesz: az első elemek párja fogja alkotni a zipelt lista első elemét, a másodikoké a másodikat, stb, azaz pl. $\mathrm{List}(1,2,3)\mathrm{.zip~List}(\textrm{"dinnye"},\textrm{"szilva"},\textrm{"narancs"})$ értéke $\mathrm{List}((1,\textrm{"dinnye"}),(2,\textrm{"szilva"}),(3,\textrm{"narancs"}))$. Az ilyen pároknak, melyekből az eredménylista áll, egyébként az első mezőjét a $\_1$, a második mezőjét a $\_2$ adattagjukkal érjük el. Ha a zipelt listák hossza nem azonos, akkor a rövidebb lista hossza lesz az eredmény hossza, a hosszabb lista "leeső" farka nem számít az eredménybe.
• Amiért a $\mathrm{zip}$ pl. hasznos tud lenni: ha egy $\mathrm{list}$ nemüres listát zipelünk a farkával: $\mathrm{list}.\mathrm{zip}(\mathrm{list.tail})$, az, ha belegondolunk, a szomszédos elemeket teszi egy cellába, pl. $\mathrm{List}(1,4,2,8).\mathrm{zip}(\mathrm{List}(4,2,8))=\mathrm{List}((1,4),(4,2),(2,8))$. Ez hasznos lehet akkor, ha ez alapján akarunk $\mathrm{map}$ni vagy $\mathrm{filter}$ezni.

13 - generic

Hogy csak $\mathrm{Int}$eket tároló listákkal kelljen dolgozzunk, az nem egy real-life scenario. Lehet szükség $\mathrm{Double}$ listákra, $\mathrm{String}$ listákra stb. Mivel pedig maga a funkcionalitás ugyanaz mindháromban elviekben, nagyon error-prone megközelítés lenne copypaste gyártani minden típusra egy újabb és újabb osztályt pl. így:

trait IntLista {
  def filter(p: Int=>Boolean): IntLista
}
case object UresIntLista extends IntLista {
  override def filter(p: Int=>Boolean) = UresIntLista
}
case class NemuresIntLista(head: Int, tail: IntLista) {
  override def filter(p: Int=>Boolean) =
    if (p(head)) NemuresIntLista(head, tail.filter(p)) else tail.filter(p)
}
trait DoubleLista {
  def filter(p: Double=>Boolean): DoubleLista
}
case object UresDoubleLista extends DoubleLista {
  override def filter(p: Double=>Boolean) = UresDoubleLista
}
case class NemuresDoubleLista(head: Double, tail: DoubleLista) {
  override def filter(p: Double=>Boolean) =
    if (p(head)) NemuresDoubleLista(head, tail.filter(p)) else tail.filter(p)
}
trait StringLista {
  def filter(p: String=>Boolean): StringLista
}
case object UresStringLista extends StringLista {
  override def filter(p: String=>Boolean) = UresStringLista
}
case class NemuresStringLista(head: String, tail: StringLista) {
  override def filter(p: String=>Boolean) =
    if (p(head)) NemuresStringLista(head, tail.filter(p)) else tail.filter(p)
}

Ilyenkor, mikor az osztályok tényleg összesen egy mező típusában különböznek, ésszerűnek látszik az igény: bárcsak lehetne ezt parametrikusan csinálni, egyetlen osztályt implementálni mondjuk $\mathrm{Lista}$ néven és valahogy futás közben megmondani, hogy most épp egy $\mathrm{Int}$ listát, vagy $\mathrm{Double}$ listát akarunk létrehozni.

És lehet: (ahogy egyébként Javában is) a parametrikus típussal ellátott osztályt generic osztálynak nevezik és ilyen a szintaxisa a listánk esetében:

trait Lista[T] {
  def filter(p: T=>Boolean): Lista[T]
}
case class Ures[T]() extends Lista[T] {
  override def filter(p: T=>Boolean) = Ures()
}
case class Nemures[T](head: T, tail: Lista[T]) extends Lista[T] {
  override def filter(p: T=>Boolean) = if (p(head)) Nemures(head, tail.filter(p)) else tail.filter(p)
}

val intList = Nemures[Int]( 1, Nemures[Int](4, Nemures[Int](2, Ures[Int]() )))
val intList2: Nemures[Int] = Nemures(1,Nemures(4,Nemures(2,Ures())))
val stringList: Nemures[String] = Nemures("dinnye", Nemures("szilva", Nemures("narancs", Ures())))
println( intList.filter { _%2 == 1 } )

Itt tehát azt mondjuk, hogy a $\mathrm{Lista}$ osztályunk kap egy $[T]$ típusparamétert, ami bármi lehet: $\mathrm{Int}$, $\mathrm{String}$, $\mathrm{Boolean}$, sőt akár $\mathrm{Lista}[\mathrm{Int}]$ is (ekkor int listák listáját tároljuk), és ezt a $T$ paramétert az osztály belsejében teljesen legális módon, mint típust használhatjuk, ahogy a fenti kód is mutatja. Létrehozáskor pl. eljárhatunk úgy is, ahogy a kód alsó részén felépítünk egy $\mathrm{Int}$ és egy $\mathrm{String}$ listát.

A $\mathrm{map}$ azért elsőre még mindig úgy tűnhet, mintha külön-külön kéne kezelnünk a $T\Rightarrow\mathrm{Int}$, $T\Rightarrow\mathrm{String}$, $T\Rightarrow\mathrm{Boolean}$ függvényeket (meg az összes többit, ami előjöhet) és ezek mindegyikére a megfelelő típusú kimeneti listát produkáltatni:

trait Lista[T] {
  def filter(p: T=>Boolean): Lista[T]
  def mapInt(f: T=>Int): Lista[Int]
  def mapBoolean(f: T=>Boolean): Lista[Boolean]
  def mapString(f: T=>String): Lista[String]
}
case class Ures[T]() extends Lista[T] {
  override def filter(p: T=>Boolean) = Ures()
  override def mapInt(f: T=>Int) = Ures()
  override def mapBoolean(f: T=>Boolean) = Ures()
  override def mapString(f: T=>String) = Ures()
}
case class Nemures[T](head: T, tail: Lista[T]) extends Lista[T] {
  override def filter(p: T=>Boolean) = if (p(head)) Nemures(head, tail.filter(p)) else tail.filter(p)
  override def mapInt(f: T=>Int) = Nemures(f(head), tail.mapInt(f))
  override def mapBoolean(f: T=>Boolean) = Nemures(f(head), tail.mapBoolean(f))
  override def mapString(f: T=>String) = Nemures(f(head), tail.mapString(f))
}
val intList = Nemures[Int]( 1, Nemures[Int](4, Nemures[Int](2, Ures[Int]() )))
println( intList.filter { _%2 == 1 } )
println( intList.mapString { _.toBinaryString }) //prints Nemures(1,Nemures(100,Nemures(10,Ures())))

(egyébként ha mindegyiket csak $\mathrm{map}$nak neveznénk el, akkor nem fordul le, mert a JVM nem tud különbséget tenni a különböző szignatúrájú függvények mint paraméterek között). Láthatjuk, hogy itt is mennyivel jobb lenne, ha a bejövő paraméterben az a $\mathrm{Boolean}$, $\mathrm{Int}$, $\mathrm{String}$ valami (másik, mert nem feltétlenül ugyanaz, mint a $T$ nevű paraméter) típus is parametrizálható is lenne - és az!

trait Lista[T] {
  def filter(p: T=>Boolean): Lista[T]
  def map[U](f: T=>U): Lista[U]
}
case class Ures[T]() extends Lista[T] {
  override def filter(p: T=>Boolean) = Ures()
  override def map[U](f: T=>U) = Ures()
}
case class Nemures[T](head: T, tail: Lista[T]) extends Lista[T] {
  override def filter(p: T=>Boolean) = if (p(head)) Nemures(head, tail.filter(p)) else tail.filter(p)
  override def map[U](f: T=>U) = Nemures(f(head), tail.map(f))
}
val intList = Nemures[Int]( 1, Nemures[Int](4, Nemures[Int](2, Ures[Int]() )))
println( intList.filter { _%2 == 1 } )
println( intList.map { _.toBinaryString }) //prints Nemures(1,Nemures(100,Nemures(10,Ures())))

Egyébként a $T$ és az $U$ csak nevezéktan: általában az első típusparaméter "neve" $T$, a másodiké $U$ szokott lenni, de ettől számos eltérés van, ha a paramétereknek van valami konkrétabb jelentésük. Azt láthatjuk tehát, hogy függvényeket is lehet generic paraméterekkel ellátni, a példában a $\mathrm{map}$ metódus lett generic egy $U$ nevű típusparaméterrel, a $T$-re parametrizált típusú listánkon belül, ezért lett a paraméterének a szignatúrája $f:T\Rightarrow U$ és a kimenete $\mathrm{Lista}[U]$ típusú. De ettől eltekintve az $U$ típust, miután generic paraméternek deklaráltuk, ugyanúgy használhatunk a metódus szignatúrájában és törzsében, mint bármilyen másik "létező" típust.
Egy szépséghibája azért még mindenképp van a kódnak, amit láthatunk: object nem lehet generic, ezért az üres lista már case class lett, és emiatt ki kell rakjuk utána a zárójeleket is. (Ezt még később megoldjuk, amikor a kovariáns genericeket meg a $\mathrm{Nothing}$ típust nézzük.)

12 - map és filter

Felmerül a kérdés, hogy mégis mikor érdemes valamit tagfüggvényként implementálni egy osztályon belül, és mikor rajta kívül. Van, amikor nincs más választásunk, mint bent deklarálni (pl. amikor olyan adathoz fér hozzá a függvény, ami csak az osztályon belül látható - a láthatósági módosítókról is lesz később poszt). Mindenesetre, ha van az $\mathrm{IntList}$ünk, és egy alkalmazásban szeretnénk pl. egy függvényt, ami visszaad egy listát, amiben minden elem kétszerese az eredeti listabelinek (tehát pl. a $(1,4,2,8,5,7)$ listán hívva a $(2,8,4,16,10,14)$ új listát adja vissza), azt persze leimplementálhatjuk így is:

trait IntList {
  def szorzasKettovel: IntList
}
case object Ures extends IntList {
  override val szorzasKettovel = Ures
}
case class Nemures(head: Int, tail: IntList) {
  override def szorzasKettovel = Nemures(head * 2, tail.szorzasKettovel)
}

de (remélhetőleg) azt érzi ilyenkor az ember valahol belül, hogy ez így nem lesz jó, mindenkinek, aki valamikor később használni fogja az $\mathrm{IntList}$ osztályunkat, ki lesz ajánlva egy szorzás kettővel függvény, amit jó eséllyel nem használna, mert csak egy bizonyos alkalmazásban egy bizonyos célra volt rá szükség. Pláne, ha egy másik alkalmazásban épp kilenccel kell szorozni az elemeket, egy másikban hármat hozzáadni... és egy nagyon furcsa abomination kezd kifejlődni, ha ezt az utat követjük:

trait IntList {
  def szorzasKettovel: IntList
  def szorzasKilenccel: IntList
  def pluszHarom: IntList
}
case object Ures extends IntList {
  override def szorzasKettovel = Ures
  override def szorzasKilenccel = Ures
  override def pluszHarom = Ures
}
case class Nemures(head: Int, tail: IntList) {
  override def szorzasKettovel = Nemures(head * 2, tail.szorzasKettovel)
  override def szorzasKilenccel = Nemures(head * 9, tail.szorzasKilenccel)
  override def pluszHarom = Nemures(head + 3, tail.pluszHarom)
}

és ez az a pont, ahol egy kicsit messzebbről szemlélve a kódot valami "általánosabb" mintát láthatunk benne, amivel elég csak egy függvényt implementálni: mivel funkcionális programozásban próbálunk gondolkodni, észrevehetjük, hogy itt valójában két dolog szerepel inputként: a lista és egy művelet, ami a lista elemeit transzformálja valahogy egyenként, függetlenül. Az első esetben a kettővel szorzás függvény, a másodikban a kilenccel szorzás, a harmadikban a hármat hozzáadás. Ezt így is meg lehet csinálni:

trait IntList {
  def map(f: Int=>Int): IntList
}
case object Ures extends IntList {
  override def map(f: Int=>Int) = Ures
}
case class Nemures(head: Int, tail: IntList) extends IntList {
  override def map(f: Int=>Int) = Nemures(f(head), tail.map(f))
}
val list = Nemures(1,Nemures(4,Nemures(2,Ures)))
println(list.map({x: Int => 2*x})) //prints Nemures(2,Nemures(8,Nemures(4,Ures)))
println(list.map { x => 9*x })     //prints Nemures(9,Nemures(36,Nemures(18,Ures)))
println(list.map { _+3 })          //prints Nemures(4,Nemures(7,Nemures(5,Ures)))
val myFavFunc: Int=>Int = { x => 7*x }
println(list.map(myFavFunc))       //prints Nemures(7,Nemures(28,Nemures(14,Ures)))

Az alsó három példában láthatjuk, hogy így miért is tudtuk egy füst alatt lekezelni a (valószínűleg) alkalmazásfüggő "szorozd konstanssal"-like függvényeket: egyszerűen csak a transzformációt kell átadjuk argumentumként. Névtelen, lambda-függvényként átadni pl. úgy lehet, ahogy a fenti példában látjuk. Ha ugyanazt a transzformációt használjuk sok helyen a kódban, akkor persze érdemes kimenteni egy (mondjuk) $\mathrm{val}$ mezőbe, és akkor látszik is, hogy miért is csináljuk, amit -- és ha változtatni kell  a függvényt, akkor elég lesz egy helyen piszkálni a kódot.

Egy másik gyakran használt listaművelet a $\mathrm{filter}$: pl. ha az $\mathrm{IntList}$ünkben gondolkodunk, akkor lehet az egy feladat, hogy legyűjtsük a pozitív értékeket egy listába, vagy a páratlan számokat:

trait IntList {
  def pozitivak: IntList
  def paratlanok: IntList
}
case object Ures extends IntList {
  override def pozitivak = Ures
  override def paratlanok = Ures
}
case class Nemures(head: Int, tail: IntList) extends IntList {
  override def pozitivak = if (head>0) Nemures(head, tail.pozitivak) else tail.pozitivak
  override def paratlanok = if (head%2==1) Nemures(head, tail.paratlanok) else tail.paratlanok
}

és ugyanúgy, mint az előbb, rájöhetünk arra is, hogy ez egy általános minta, amit egy predikátum (az objektumból, mint most az $\mathrm{Int}$, $\mathrm{Boolean}$ba képző függvényeket hívják így) átadásával tudunk egységesen kezelni:

trait IntList {
  def filter(p: Int=>Boolean): IntList
}
case object Ures extends Intlist {
  override def filter(p: Int=>Boolean) = Ures
}
case class Nemures(head: Int, tail: IntList) extends IntList {
  override def filter(p: Int=>Boolean) = if (p(head)) Nemures(head, tail.filter(p)) else tail.filter(p)
}
val list = Nemures(1,Nemures(4,Nemures(2,Ures)))
println(list.filter { _%2==1 }) //prints Nemures(1,Ures)

Már csak az üthet szöget a fejünkbe, hogy mi van, ha nem csak $\mathrm{Int}$eket tároló listákkal akarunk dolgozni, ez a következő poszt témája

folytköv

11 - class member függvények

$\mathrm{class}$on, $\mathrm{object}$en belül is lehet függvényeket vagy értékeket is deklarálni, pl:

case class Vektor(x: Double, y: Double) {
  def length = Math.sqrt(this.x * this.x + this.y * this.y)
}
val v = Vektor(1.0,2.0)
println(v.length)  //prints 2.23606797749979

Mi történik ennél a hívásnál?

• Ha a $C$ osztályban egy $f(x_1:T_1,\ldots,x_n:T_n)$ tagmetódusát hívjuk az $a$ példányon (amit pl. $\mathrm{val}~a~=\ldots$ deklaráltunk), akkor $$a.f(a_1,\ldots,a_n)$$ hívjuk a függvényt, ahol az $a_i$ argumentumok $T_i$ típusúak (most nincs argumentum, de nemsokára lesz)
• a függvény törzsében az $x_i$-k helyére az $a_i$ értékek kerülnek
• és a $\mathrm{this}$ kulcsszó helyére pedig maga az $a$ érték.

(matematikailag legalábbis ez történik, ha pure funkcionális stílusban programozunk.)

Pl. a fenti $\mathrm{v.length}$ hívásnál:

$$\begin{align*}\mathrm{v.length}&\triangleright \mathrm{Vektor}(1.0,2.0)\mathrm{.length}\\&\triangleright \mathrm{Math.sqrt}(\mathrm{Vektor}(1.0,2.0).x\cdot \mathrm{Vektor}(1.0,2.0).x+\mathrm{Vektor}(1.0,2.0).y\cdot\mathrm{Vektor}(1.0,2.0).y)\\&\triangleright \mathrm{Math.sqrt}(1.0\cdot 1.0+2.0\cdot 0.2)\\&\triangleright\mathrm{Math.sqrt}(5.0)\\&\triangleright 2.2360679\ldots\end{align*}$$

Az előző kód példája egy paraméter nélküli metódus volt. Ilyenkor a Scala fordító elfogadja zárójelekkel is $\mathrm{def~length}() = \ldots$ és mint fent, anélkül is. A konvenció az, hogy ilyenkor azokat a metódusokat írjuk zárójel nélkül, melyeknek nincs mellékhatásuk. A fenti $\mathrm{length}$ például ilyen, csak az adattagokból számít ki valamit. Ha megnézzük a hívást, $\textrm{v.length}$, szemre akár egy $\mathrm{val}$ member adatmező is lehetne. És tényleg:

case class Vektor(x: Double, y: Double) {
  def length_def = Math.sqrt(this.x * this.x + this.y * this.y)
  val length_val = Math.sqrt(this.x * this.x + this.y * this.y)
  lazy val length_lazy_val = Math.sqrt(this.x * this.x + this.y * this.y)
}
val v = Vektor(1.0,2.0)
println(v.length_def)  //prints 2.23606797749979
println(v.length_val)  //prints 2.23606797749979
println(v.length_lazy_val)  //prints 2.23606797749979

Nem csak a már korábban látott $\mathrm{val}$ és $\mathrm{def}$, hanem a $\mathrm{lazy~val}$ is opció. A különbségek köztük:

• a  $\mathrm{val}$ értéke az objektum létrehozásakor (ez a $\mathrm{val}~v=\mathrm{Vektor(1.0,2.0)}$ értékadás jobb oldali kifejezésének kiértékelésekor történik) kiszámítódik, ez az érték bekerül plusz egy adattagba, innentől kezdve ezt adjuk vissza.
• a $\mathrm{def}$ értéke minden egyes lekérdezéskor újra és újra kiértékelődik a definíciójának megfelelően, viszont nem foglalódik neki plusz adattag objektumpéldányonként.
• a $\mathrm{lazy~val}$nak foglalódik egy plusz adattag, de létrehozáskor még nem értékelődik ki, csak az első lekérdezéskor. Ekkor az érték bekerül az adattagba és onnantól kezdve nem számolódik újra.

Tehát: a $\mathrm{val}$ok kicsit több helyet foglalnak, a $\mathrm{val}$ mindenképp kiszámolja létrehozáskor az értékét, a $\mathrm{def}$ lekérdezésenként tovább tart, mire megjön az eredmény. A $\mathrm{lazy~val}$ sem mindig jobb választás, mint a $\mathrm{val}$, mert annak is van plusz költsége (adattagban is,  és a $\mathrm{val}$ lekérdezéseként is), hogy minden lekérdezéskor fut egy check, hogy ki van-e már számolva ez az érték. Ezt minden esetben a programozó kell mérlegelje, hogy a három lehetőség közül melyik lenne a legjobb - de a jó hír, hogy ha később mégiscsak váltani lenne jobb és átírja az osztályban az egyik kulcsszót a másikra, akkor nem töri el a hívó kódokat, mert számukra teljesen transzparens, hogy ez most épp melyik a három közül.

Ennek megfelelően ennek a kódnak:

case class Vektor(x: Double, y: Double) {
  def length_def = { println("def"); Math.sqrt(this.x * this.x + this.y * this.y) }
  val length_val = { println("val"); Math.sqrt(this.x * this.x + this.y * this.y) }
  lazy val length_lazy_val = { println("lazy_val"); Math.sqrt(this.x * this.x + this.y * this.y) }
}

val v = Vektor(1.0,2.0)
println("start")
v.length_def
v.length_val
v.length_lazy_val
v.length_def
v.length_val
v.length_lazy_val
v.length_def
v.length_val
v.length_lazy_val

a kimenete:

val
start
def
lazy_val
def
def

(Figyeljük meg a debug printlnt: így, hogy két kifejezés van egymás után, a másodiknak az értéke lesz az érték, az elsőt eldobjuk - ami úgyis $\mathrm{Unit}$, tehát $\mathrm{()}$ -, ez is egy módja a debugolásnak, de fogunk azért látni jobbat is.

Nem csak classba vagy objectbe, de traitbe is írhatunk defet vagy valt (lazy valt nem). Ha például szeretnénk az $\mathrm{IntList}$ traitünket felruházni egy $\mathrm{sum}$ függvénnyel, ami visszaadja az elemei összegét:

trait IntList {
  def sum: Int
}
case object Empty extends IntList {
  override def sum = 0
}
case class Nonempty extends IntList {
  override def sum = head + tail.sum
}
//így használjuk
val list = Nonempty(3, Nonempty(4, Nonempty(7, Empty)))
println(list.sum) // prints 14

Világos, hogy ahhoz, hogy egy listára, amiről annyit tudunk, hogy $\mathrm{IntList}$ a típusa, hívhassuk a $\mathrm{sum}$ függvényt, és ez leforduljon, tényleg kellhet az, hogy már eleve az $\mathrm{IntList}$ traitben meglegyen a függvény deklarációja. Típust is kell adjunk neki, de definíciót nem tudunk adni ezen a ponton - szerencsére nem is kell, traitekben megengedett dolog csak deklarálni, de nem definiálni a függvényt.
A case objectben és a case classban viszont, ha akarunk is belőlük példányt létrehozni, minden létező metódusnak kell már legyen definíciója - meg kell adjuk a $\mathrm{sum}$ függvényt mindkét esetben. Célszerű ilyenkor a def elé beírni az $\mathrm{override}$ kulcsszót is: ez a kulcsszó azt jelzi a fordítónak, hogy legyen szíves leellenőrizni, hogy ugye volt már egy pont ilyen nevű és szignatúrájú metódus feljebb a hierarchiában (az $\mathrm{extends}$eken keresztül) és ha nem, akkor dobjon hibát. Ezzel magunkat védjük: egyrészt ha elgépeljük a fentebbről örökölt (inherited) metódus nevét, akkor erre hamar fény derül, másrészt ha majd mások olvassák a kódunkat, ebből ránézésre látják majd ő is, hogy ebből a metódusból van följebb is másmilyen.

Persze nem csak paraméter nélküli metódust lehet létrehozni:

case class Vektor(x: Double, y: Double) {
  def plus(that: Vektor) = Vektor(this.x+that.x, this.y+that.y)
}
val u = Vektor(1.0, 2.0)
val v = Vektor(3.0, 4.0)
println(u.plus(v)) //prints Vektor(4.0,6.0)

Itt tehát az történik, hogy a $\mathrm{Vektor}$ osztályunknak (amihez korábban az osztályon kívül deklaráltunk egy összeadó függvényt és kb $\mathrm{add(v1: Vektor, v2: Vektor): Vektor}$ volt a fejléce, így is hívtuk meg) belülre deklarálunk egy összeadó metódust, aki így már csak egy további vektort vár, hiszen a bal oldali vektor az lesz, akin hívjuk, aki behelyettesítődik a $\mathrm{this}$ helyére. (Egyébként Scalában bevett konvenciónak számít, hogy ha egy osztálynak egy függvénye egyváltozós, és ugyanannak az osztálynak várja egy másik példányát, akkor ezt a formális paramétert $\mathrm{that}$nak nevezik el. Nem kötelező, a $\mathrm{that}$ nem kulcsszó, csak szokás.) Ez már talán eggyel kulturáltabban néz ki, hogy az $\mathrm{add}$ függvény a két vektor között van, mintha tényleg pl egy bináris operátor lenne...
...de bizony ezt lehet hívni így is

println( u plus(v) )

(a pont sok esetben elhagyható, ennek a konvencióiról azért még majd írok, van, aki szerint olvashatóbb a kód pontokkal, van, aki szerint nem; szerintem ha hosszú chainelés van, akkor külön sorba érdemes írni a lánc elemeit és ekkor kell is kirakni a pontot, ha meg rövid, én nem szoktam kirakni általában)
..sőt lehet hívni így is

println( u plus v )

egyváltozós member function argumentuma körül a kerek zárójel is legtöbbször elhagyható (olyankor lehet belőle értelmezési zavar, ha pl. tovább folytatjuk a kifejezést egy ponttal és pont egy olyan függvényt, mondjuk $\mathrm{toString}$et hívunk rajta, ami van az argumentumnak is és az eredménynek is).
ez így már majdnem annyira kényelmesen néz ki, mint egy rendes, infix módon írt összeadás.
És hát why not?

case class Vektor(x: Double, y: Double) {
  def +(that: Vektor) = Vektor(this.x+that.x, this.y+that.y)
}
val u = Vektor(1.0, 2.0)
val v = Vektor(3.0, 4.0)
println( u + v ) //prints Vektor(4.0,6.0)

Scalában nagyon, nagyon sok minden elmegy metódusnévnek, itt például a metódus neve az lett, hogy $\mathrm{+}$. És így már két vektor összeadása úgy is néz ki, mint két $\mathrm{Int}$ összeadása, egy nagyon természetes szintaxist ad a függvényhívásnak, könnyen olvashatót programozó számára.
Nem véletlen egyébként a hasonlóság: a $2+3$-at úgy is írhatjuk, hogy $2.+(3)$, mert a $+$ jel ebben az esetben az $\mathrm{Int}$ osztály (azaz majdnem az $\mathrm{Int}$ osztály but still) egyik tagfüggvényének a neve. Persze ettől még primitív típusra fog lefordulni, hatékony lesz, csak forráskódi szinten, kinézetre kezelődik minden úgy, mintha objektum lenne, ideértve a "built-in" operátorokat is.
Legközelebb nézünk néhány standard tagfüggvényt, fókuszálva a $\mathrm{List}$ osztályra.

folytköv