Logika a formální sémantika:
4. Kategoriální gramatika a lambda kalkul
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik
pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
doc. PhDr. Jiří Raclavský, Ph.D. ([email protected])
Department of Philosophy, Masaryk University, Brno
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
1
IV. Kategoriální gramatika
- kategoriální gramatika („categorial grammar“), ev. teorie syntaktických kategorií
- výraz je výsledkem aplikace podvýrazů „na sebe“
- např. predikát je kategorie výrok/term (tj. odečtením termu od výroku dostaneme
predikát)
- výrok/term na term = výrok
- Lambekovy kalkuly
- kategoriální gramatika je v základě syntaktický aparát („gramatika“)
potíže s některými neintuitivními výsledky, protože se příliš mechanicky poléhalo
na syntax, nehledělo se na sémantiku
- docela populární i mezi lingvisty
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
2
IV. Kategoriální gramatika (pokr.)
pokr.)
- zakladatelé Lesniewski, Husserl
- Adjukiewicz, K. (1935): Die syntaktische Konexitaet, Studia Philosophica 1, 1-27
- Bar-Hillel, Yehoshua (1953): On Syntactical Categories, Journal of Symbolic Logic 15
- Lambek, Joachim (1958): The mathematic of sentence structure; reprinted In:
Categorial Grammar, Wojciech Buszkowski & Witold Marciszewski & Johan van
Benthem (eds.), Amsterdam,Philadelphia: John Benjamins Publishing Company
- lambda-kategoriální gramatika (lambda categorial grammar) - fúze kategoriální
gramatiky s prvky lambda kalkulu
- např. abstrahujeme-li z věty „∀x(člověk(x) -> smrtelný(x))“ predikáty, nahradíme-li
je proměnnými (p, q, ..), získáme λp(λq(∀x(p(x) -> q(x)))), tedy výraz pro „každý“
CRESSWELL, Max J. (1973): Logics and Languages. London: Methuen & Co Ltd
CRESSWELL, Max J. (1977): Categorial Languages. Bloomington (Indiana): Indiana University Linguistics Club
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
3
IV. Teorie zobecněných kvantifikátorů
- generalised quantifiers
- absolutní kvantifikátory (kvantifikátory) - označují třídy tříd individuí
- relativní kvantifikátory (determinátory) - označují podmnožiny třídy tříd individuí
(např. „většina“); sémantika pomocí lambda-abstrakce
- aplikace determinátoru na predikátu je kvantifikátor
- např. BARWISE, Jon & COOPER, R. (1981): Generalized Quantifiers and Natural
Language, Linguistics and Philosophy 4, 159-219, BENTHEM, Johan van (1986): Essays on
Logical Semantics. Dordrecht: Riedel
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
4
IV. Teorie typů
- theory of types
- kategoriální gramatika funguje analogicky (kategorie výrazů), avšak ta je
syntaktická
- Russell (Mathematical Logic as Based on the Theory of Types 1908, Principia
Mathematica 1911)
- výrazy vyjadřují objekty určitého typu (jméno individuum, vlastnost množinu
individuí, atd.)
- vyvinuta kvůli zabránění paradoxům (např. těm, které vznikají aplikací funkce na
sebe)
- při analýze výrazů přirozeného jazyka se uplatňuje typová analýza
- teorie typů není samostatný logický aparát
- CHURCH, Alonzo (1940): A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5, 56-68
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
5
IV. Lambda kalkul
- redukce všech matematických operací na tři fundamentální druhy
- ryze funkcionální charakter
- aspirace na to sloužit základům matematiky
- lambda kalkul je aparát, který chápe funkce nikoli jako zobrazení z množiny do
množiny, ale jako jisté výpočetní procedury
- populární např. v informatice či logické sémantice (Montague a jiní), ale ne příliš v
matematice a matematické logice
- zakladatel Alonzo Church (1941 The Calculi of Lambda-Conversion; Annals of
Mathematical Studies 6, Princeton UP)
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
6
IV. Lambda kalkul (pokr., pokr.)
- klasika: BARENDREGT, Henk (1992): Lambda Calculi With Types.
ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z , v tisku: In: Abramsky, S.,
Gabbay, D.M., Maibaum, T.S.E. (eds.), Handbook of Logic in Computer Science, vol.
II, Oxford: Oxford UP.
- Zlatuška, Jiří (1993): Lambda kalkul, Brno: Masarykova univerzita
- Alama, Jesse (2014): The Lambda Calculus. In: The Stanford Encyclopedia of Philosophy,
Edward N. Zalta (ed.), URL =
<http://plato.stanford.edu/archives/sum2014/entries/lambda-calculus/>
- lambda kalkulu je isomorfní kombinatorická logika
- zakladatel je Haskell B. Curry
- kombinatorická logika nepoužívá proměnné jen kombinátory (vlastně jde jen o
jeden operátor, ostatní jsou pomocné)
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
7
IV. Lambda kalkul (pokr., pokr., pokr.)
- jazyk:
1) konstanty
2) proměnné (x, y)
3) aplikace [F A], kde A je argument (popř. n-tice), F funkce; tato aplikace
vypočítává hodnotu funkce F na tomto argumentu A; např. [+ <2,3>] vypočítává
číslo 5
4) lambda abstrakce λx [...x...], konstruuje samotnou funkce F tím, že nechá
proběhnout všechny hodnoty pro (nyní vázanou) hodnotu proměnné x; např.
λx [+ <x,3>] charakterizuje funkci přičtení čísla 3 k jakémukoli číslu přiřazenému
valuací proměnné x
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Jiří Raclavský (2014): Logika a formální sémantika - 4. Kategoriální gramatika a lambda kalkul
8
IV. Lambda kalkul (pokr., pokr., pokr., pokr.)
- operace beta-redukce je to, díky čemu lambda-kalkul "počítá"; aplikace abstrakce
na odpovídající argument je ekvivalentní aplikaci funkci na daný argument (např.
[λx [+ <x,3>] 2] je totéž jako [+ <2,3>])
- dále tzv. alfa-ekvivalence (korektní přejmenování proměnných) či eta-ekvivalence
- lambda kalkul s typy (tzv. typed lambda calculi; česky chybně: typovaný lambda
kalkul); zamezuje aplikování funkce na sebe (což je např. zajímavé v popisu
programovacích jazyků)
- v ČR využití v datovém modelu HIT
Logika: systémový rámec rozvoje oboru v ČR a koncepce logických propedeutik pro mezioborová studia (reg. č. CZ.1.07/2.2.00/28.0216, OPVK)
Download

Logika a formální sémantika: 4. Kategoriální gramatika a lambda