Logika nyelvészeknek, 12. óra A típuselmélet alapjai Lehetőség van a kvantorfogalom mellett a funktorfogalom általánosítására is. Az L1 elsőrendű nyelvben csak bizonyos típusú funktoraink voltak: • ami mondatból csinál mondatot (negáció) • ami két mondatból csinál mondatot (többi mondatfunktor) • ami terminusból csinál mondatot (egyargumentumú predikátum) • ami két terminusból csinál mondatot (kétargumentumú predikátumok és az azonosság) Minden egyes funktortípusra külön-külön explicit módon meg kellett adnunk, hogy milyen faktuális értéke lehet, ugyanis nem volt olyan eljárásunk, ami ezt általában megadta volna tetszőleges típusú bemenetű és tetszőleges típusú kimenetű funktorra. A funktorfogalom rendszeres és áttekinthető kezelését, és a megfelelő szemantikai érték hozzárendelését teszi lehetővé az ún. típuselmélet. 1. A típusok halmazának meghatározása Kiindulópont: vegyünk két elemi típust: e és t. 1. e ∈ Type és t ∈ Type 2. Ha α ∈ Type és β ∈ Type, akkor <α,β> ∈ Type. 3. Semmi más nem eleme a típusok halmazának. Ennek megfelelően a típusok halmazának eleme lesz például: <e,e>,
>, <e,<<e,t>,t,>>, nem lesz viszont például eleme: <e,e,e> <e,t,>, . e: terminusok típusa, t: formulák típusa, <α,β>: olyan funktorok típusa, amelyek bemenete α és kimenete β típusú. Példák: <e,t>: egyargumentumú predikátum : egyargumentumú mondatfunktor (pl. negáció) <e,e>: egyargumentumú névfunktor (pl. testvére) <e,<e,t>>: kétargumentumú predikátum <<e,t>,t>: általánosított kvantor <<e,t>,<<e,t>,t>>: determináns A típuselméleti nyelvben a szótárban (azaz amikor felsoroljuk a nyelvünk nem-logikai konstansait) meg kell adnunk minden egyes kifejezéshez, hogy mi a típusa. 2. Jólformált kifejezések osztályának meghatározása A jólformált kifejezések osztályát induktívan határozzuk meg. (Lényeges különbség az elsőrendű nyelvekkel összevetve: ott a formulák osztályát adtuk meg ilyen módon.)
Amennyiben φ konstans, amelynek típusa α, akkor φ ∈ Conα, azaz a φ kifejezés eleme az α típusú konstansok halmazának. Meghatározunk továbbá minden α ∈ Type típusra egy Varα halmazt, amely végtelen számú α típusú változót tartalmaz: Varα = {vα1, vα2, vα3, ...} A konstansok és változók elemei az α típusú jólformált kifejezések Expα halmazának: Varα ∪ Conα ⊆ Expα Elemei lesznek továbbá az egyes Expα halmazoknak az alábbi szintaktikai szabályok által előállítható kifejezések: Szintaktikai szabályok: 1. Amennyiben α ∈ Type, β ∈ Type, φ ∈ Exp<α,β>, és ψ ∈ Expα, akkor φ (ψ) ∈ Expβ Ez a szabály a funktorok körét határozza meg: az <α,β> típusú kifejezések olyan egyargumentumú funktorok, amelyek bemenete α típusú kifejezés, kimenete β típusú kifejezés. 2. Amennyiben α ∈ Type, β ∈ Type, φ ∈ Var<α>, és ψ ∈ Expβ, akkor λφ [ψ] ∈ Exp<α,β> Ez a lambda-absztrakció szintaktikai szabálya, ami azt mondja ki, hogy a lambdaoperátor két tetszőleges típusú kifejezésből olyan funktort fog képezni, amelynek a bemenetének a típusa azonos a φ kifejezés típusával, és kimenetének típusa azonos ψ típusával. 3. Fakultatív további szintaktikai szabályok, pl. logikai mondatfunktorok, klasszikus elsőrendű kvantorok: Amennyiben u ∈ Vare, és ψ ∈ Expt, akkor ∀u [ψ] ∈ Expt 4. A jólformált kifejezések Exp halmazát a különböző típusú jólformált kifejezések halmazainak úniójaként határozzuk meg: Exp = Uα ∈Type Expα 5. A konstansokon, változókon és a szabályokkal előállítható jólformált kifejezéseken kívül semmi más nem eleme a jólformált kifejezések osztályának. 3. A típuselméleti nyelv szemantikája 1. Adva van az elsőrendű nyelvekhez hasonlóan egy M = modell és egy g változóértékelés. Jelölje Dα az α típusú kifejezések lehetséges faktuális értékeinek az osztályát. Két ilyen osztályt rögzítünk: De = U Dt = 2 Azaz: az e típusú kifejezések (a terminusok) faktuális értéke az univerzum valamely eleme lehet, a formulák faktuális értéke pedig az igazságértékek egyike lehet. Ezen kívül jelöljük BA -val azon függvények halmazát, amelyek értelmezési tartománya az A halmaz, értékkészlete pedig B halmaz egy részhalmaza.
Az <α,β> típusú kifejezések lehetséges faktuális értékeit úgy határozzuk meg, hogy: D = D Dα <α,β>
β
Azaz: ezeknek a funktoroknak olyan függvény lehet a faktuális értéke, amely függvény értelmezési tartománya a funktor bemenetének a lehetséges faktuális értékeinek a halmaza, értékkészlete pedig a funktor kimenetének a lehetséges faktuális értékeinek a halmazának egy részhalmaza. Az I interpretációs függvényre és a g változóértékelésre ennek értelmében a következő feltételek fogalmazhatók meg: I⊆ D Conα
Uα
∈Type
α
azaz: I bármely α típusú konstanshoz Dα egy elemét rendeli hozzá szemantikai értékként. Ezzel analóg módon: g⊆ D Varα
Uα
∈Type
α
2. Szemantikai szabályok: a) Ha φ ∈ Conα , akkor [[ φ ]]M,g = I(φ). b) Ha u ∈ Varα, akkor [[ u ]]M,g = g(u). c) Ha φ ∈ Exp<α,β>, és ψ ∈ Expα, akkor [[φ (ψ) ]]M,g = [[ φ ]]M,g ([[ ψ ]]M,g) d) Amennyiben α ∈ Type, β ∈ Type, u ∈ Varα, és ψ ∈ Expβ, akkor [[ λu [ψ] ]]M,g az a h függvény (h ∈ D Dα), amelyre igaz, hogy minden a ∈ D -ra teljesül, hogy β
h(a) = [[ ψ ]]M,g[u/a]
α
Ezt a négy szabályt követhetik további szabályok, pl. logikai mondatfunktorok értelmezése, klasszikus elsőrendű kvantorok értelmezése stb. A szemantikai szabályok megadják a típuselméleti nyelv összes jólformált kifejezésének az értelmezését. Megjegyzések: 1. A c) szabály igen elemi szemantikai szabály, „függvény alkalmazása argumentumra” (function application) néven ismert, függvényből és argumentumból állítást hoz létre. 2. A d) szabály (a lambda-absztrakció) ennek fordítottjaként fogható fel: állításból függvényt hoz létre. 3. A d) szabály alapján a következő ekvivalencia érvényes (bármely α, β ∈ Type-ra): λxα [ P<α,β>(xα) ] (yα) ⇔ P<α,β>(yα) Így amennyiben van egy λxα [ P<α,β>(xα) ] (yα) formájú, β típusú kifejezésünk, ez mindig felcserélhető egy P<α,β>(yα) formájú β típusú kifejezéssel. Ezt hívják a lambda-konverzió törvényének (a felcserélés műveletét pedig lambda-konverziónak). 4. A bemutatott típuselméleti nyelvben a többargumentumú funktorokhoz nem többargumentumú függvényt rendelünk értelmezésként. Az elsőrendű nyelvben megismert többargumentumú funktoroknak megfelelő típuselméleti kifejezéseket egyargumentumú függvények többszöri alkalmazásával értelmezzük.
Példa: szeret (a) (b) típusa: <e,<e,t>; szemantikai értéke egy olyan függvény, amelynek bemenete individuum, kimenete pedig individuumoknak egy halmaza (illetve ennek karakterisztikus függvénye), pl.: [[ szeret<e,<e,t>> ]]M,g = {<János,<Judit,1>>, <János,<Mari,1>>, >, >} A szeret konstans először egy (e típusú) terminussal kapcsolódik össze, pl.: szeret (János), és így olyan <e,t> típusú funktort alkot, amelynek szemantikai értéke individuumoknak egy halmaza (illetve ennek karakterisztikus függvénye): Amenyiben szeret szemantikai értéke a fenti halmaz és [[ Jánose ]]M,g = János, akkor [[ szeret (János) ]]M,g = {<Judit,1>, <Mari,1>} (vagy ezzel egyenértékűen {Judit, Mari}). Ez a funktor ismét (e típusú) terminussal kapcsolódik össze, ezáltal (t típusú) formulát kapunk. A fenti példát folytatva szeret (János) (Judit) igaz, szeret (Judit) (János) viszont például nem. (Az, hogy ezt a formulát informálisan hogyan értelmezzük, ránk van bízva: szeret (János) például jelölhetné azoknak a halmazát, akik szeretik Jánost vagy azokét, akiket szeret János, stb. Ezt a szeret terjedelmének megadásakor el kell döntenünk.) 4. A típuselmélet egy nyelvészeti alkalmazása: a kategoriális grammatika Kategoriális grammatikának egy formális vagy természetes nyelv olyan grammatikáját (= szintaxis + szemantika) hívunk, amely szigorúan párhuzamosan építi fel a nyelv szintaxisát és szemantikáját, abban az értelemben, hogy minden adott szintaktikai kategóriájú kifejezés egyazon szemantikai kategóriájú értelmezést kap. A kategoriális grammatika szótárában minden atomi kifejezés egyértelmű típusbesorolást kap, amely meghatározza, hogy milyen típusú kifejezésekkel kapcsolható össze. A komplex kifejezéseket szigorúan funktor-argumentum-kapcsolatok sorozatára bontja fel. Szintaktikai jelölésmód: A\B: olyan funktor, amelynek B argumentuma és A kimenete, és B balra helyezkedik el a funktortól A/B: olyan funktor, amelynek B argumentuma és A kimenete, és B jobbra helyezkedik el a funktortól VP := S\NP, pl: fut
Péter fut NP
S\NP S
TV := (S\NP)/NP, pl.: látja
Mari látja
Mónikát
NP
NP
(S\NP)/NP S\NP S
A formális szemantikában az ilyen jellegű kategoriális szintaxishoz gyakran egy típuselméleti logikai nyelvet szokás rendelni szemantikaként. A leghíresebb ilyen rendszer az ún. Montague-grammatika (vö. Dowty/Wall/Peters 1981). Példa: mondatfunktorok és mint (disztributívan értelmezett) kétargumentumú névfunktor típusa: (NP/NP)\NP
Mari és
Mónika
NP
NP
(NP/NP)\NP NP/NP NP
Probléma: Milyen szemantikai típus tartozik az NP-khez? Az NP nem lehet e típusú (individuumot jelölő), mert a Mari és Mónika NP nem (egyetlen) individuumot jelöl. Montague megoldása: az NP-k a típuselméleti szemantikában <<e,t>,t> típusúak, azaz olyan kifejezések, amelyek predikátumot vesznek argumentumként, és így alkotnak mondatot, azaz általánosított kvantorok. [[ Mari<<e,t>,t> ]]M,g = {K ⊆ U: Mari ∈ K} azaz: a Mari tulajdonnév szemantikai értéke azon halmazok halmaza, amely halmazoknak eleme a Mari individuum, azaz: a Mari név által jelölt individuum megadható úgy, hogy felsoroljuk az összes tulajdonságát. Ezzel ekvivalensen a típuselméleti nyelvre a következő fordítást is adhatjuk, amennyiben ott rendelkezünk e típusú konstansokkal: MariNP := λP [ P(m)], ahol [[ m ]]M,g = Mari
és mint disztributívan értelmezett NP-funktor: <<<e,t>,t>, <<<e,t>,t>, <<e,t>,t>>> 1. bemenet
2. bemenet
kimenet
fordítása a típuselméleti nyelvre: és(NP/NP)\NP := λP λQ λP [P (P) & Q (P)] (P , Q ∈ Var<<e,t>,t>, P ∈ Var<e,t>) λP λQ λP [P (P) & Q (P)] (Mari<<e,t>,t>) (Mónika<<e,t>,t>) ⇔ λQ λP [Mari<<e,t>,t> (P) & Q (P)] (Mónika<<e,t>,t>) (lambda-konverzióval) ⇔ λP [Mari<<e,t>,t> (P) & Mónika<<e,t>,t> (P)] (lambda-konverzióval)
Mari és Mónika fut: λP [Mari<<e,t>,t> (P) & Mónika<<e,t>,t> (P)] (fut<e,t>) ⇔ Mari<<e,t>,t> (fut<e,t>) & Mónika<<e,t>,t> (fut<e,t>)
Irodalom: DOWTY, D./R. WALL/S. PETERS (1981) Introduction to Montague Semantics. Dordrecht: Reidel. STEEDMAN, M. (1996) Categorial Grammar. In: K. BROWN/J. MILLER (szerk.): Concise Encyclopedia of Syntactic Theories. Amsterdam: Elsevier, 31-43. GAMUT, L. T. F. (1991) Logic, language, and meaning. Vol. 2.: Intensional logic and logical grammar. Chicago: University of Chicago Press. 4. fejezet: The theory of types and categorial grammar, 75-116.
