#+title: Logik-Basierte Sprachverarbeitung WS22/23 - Summary #+author: Florian Guthmann #+email: florian.guthmann@fau.de #+options: toc:nil num:nil \n:t html-style:nil html5-fancy:t #+html_doctype: xhtml5 #+html_head: #+html_head: #+html_head: #+macro: abbr @@html:$2@@ This an attempt at a concise summary for the LBS lecture based on WS22/23. Further resources: [[https://kwarc.info/teaching/LBS/notes.pdf][Lecture notes]] [[https://gl.mathhub.info/Teaching/LBS2223][LBS Lab]] (most of the GF and MMT code snippets were taken from here) * Natural Language - Abstraction :: "car" and "automobile" have the same meaning - Ambiguity :: A "bank" can be be a financial institution or a geographical feature - Composition :: "Every[1] student[2] sleeps[3]" \to $\forall x[1]. student[2](x) \implies sleep[3](x)$ ** Waterfall Model A model for {{{abbr(Natural Language Understanding, NLU)}}} 1. speech processing: acoustic signal \to word hypothesis graph 2. *syntactic processing*: word sequence \to phrase structure 3. *semantics construction*: phrase structure \to (quasi-)logical form 4. *semantic pragmatic analysis*: (quasi-)logical form \to knowledge representation 5. problem solving: using the generated knowledge ** Context and Interpretation #+begin_quote Everyone is here. #+end_quote - Radical Semantic View :: The sentence literally means that everyone in the world is here, so is generally false. An interpreter recognizes that the speaker said something false. - Radical Pragmatic View :: The semantics are incomplete and what the sentence means is determined by the context of utterance and speaker's intentions. - Intermediate View :: The quantifier "every" contains a slot for information which is contributed by the context. Extralinguistic information is required to fix the meaning. ** Epistemology - Proposition :: A *proposition* is a sentence about the actual world or a class of worlds deemed possible whose meaning can be expressed as being /true/ or /false/ - Belief :: A *belief* is a proposition that an agent holds true about a class of worlds - Knowledge :: *knowledge* is /justified/, /true/ belief (summarist's objection: [[https://plato.stanford.edu/entries/knowledge-analysis/#GettProb][Gettier Problem]]) - Observation :: Given a world $w$, the /observed value/ of a proposition $\varphi$ can be determined by *observations*. An *observer* is an agent that perceives $\varphi$ is as true in $w$. An observation is *reproducible*, iff it can be observed by different observers in different situations. - Phenomenon :: A *phenomenom* is a proposition that is /reproducibly observable/ to be true in a class of worlds. - Explanation :: A proposition $\psi$ *follows from* a proposition $\varphi$, iff $\psi$ is true in any worlds where $\varphi$ is. An *explanation* of a /phenomenom/ $\varphi$ is a set $\Phi$ of /propositions/, such that $\varphi$ follows from $\Phi$. - Counterexample :: A world $w$ is a *counterexample* to a proposition $\varphi$, if $\varphi$ is /observably false/ in $w$. A proposition is *falsifiable*, iff counterexamples are theoretically possible and feasibly observable. - Hypothesis :: A *hypothesis* is a proposed /explanation/ of a /phenomenom/ that is falsifiable. - Foundational Meaning Theory :: A meaning theory that tries to explain /why/ language expressions have the meaning they have in terms of mental states of individuals and groups *** Semantic Meaning Theory A *semantic meaning theory* assigns semantic contents to expressions of language. - Singular Term :: A *singular term* is a phrase that denotes a particular person, place or object (e.g. "Michael Kohlhase", "Odysseus") - Sinn und Bedeutung [Gottlob Frege] :: A singular term separately has a *sense* (Sinn) and/or *referent* (Bedeutung). "Odysseus" does not have a /referent/, but it does have a /sense/! - Most Certain Principle [Cresswell] :: If we have two sentences $A$ and $B$, and $A$ is true and $B$ is false, then $A$ and $B$ do not mean the same. - Truth Conditions :: The *thruth conditions* of a sentences are the conditions of the world under which it is true. - Compositionality :: A meaning theory $T$ is *compositional*, iff the meaning of an expression is a function of the meanings of its parts. - Congruence :: A meaning theory $T$ obeys the *congruence principle*, iff whenever $A$ is part of $B$ and $A'$ means the same as $A$, then replacing $A$ with $A'$ in B does not change $B$'s meaning. ** The Method of Fragments (Montague) A *natural language fragment* is the language of a context-free grammar *** Grammatical Framework (GF) A *grammar* in *GF* consists of - an *abstract grammar* that specifies well-formed *abstract syntax trees* (AST) - a collection of *concrete grammars* that specify how an AST can be *linerarized* into natural language strings #+begin_src gf abstract Grammar = { cat Name; -- proper name ("Ethel", ...) TransVerb; InTransVerb; VP; S; Conn; -- connectives like "and", "or", ... NP; -- noun phrases Noun; Det; -- determiner ("the", "every", "a", ...) fun makeVP : TransVerb -> NP -> VP; makeVP2 : InTransVerb -> VP; makeS : NP -> VP -> S; negateVP : VP -> VP; makeNP : Det -> Noun -> NP; -- "the" -> "cat" -> "the cat" makeNP2 : Name -> NP; -- "Peter" -> "Peter" -- "howl" -> "scream" -> "howl and scream" combineVP : VP -> Conn -> VP -> VP; combineS : S -> Conn -> S -> S; and : Conn; or : Conn; the : Det; every : Det; some : Det; cat_ : Noun; dog: Noun; teacher: Noun; peter : Name; mary : Name; fido : Name; love : TransVerb; poison : TransVerb; sleep : InTransVerb; laugh : InTransVerb; } #+end_src #+begin_src gf concrete GrammarEng of Grammar = { lincat Name = Str; TransVerb = {fin: Str; inf: Str}; InTransVerb = {fin: Str; inf: Str}; VP = {fin: Str; inf: Str}; S = Str; ReflexiveVerb = Str; Conn = Str; NP = Str; Noun = Str; Det = Str; lin dog = "dog"; cat_ = "cat"; teacher = "teacher"; peter = "Peter"; mary = "Mary"; fido = "Fido"; love = {fin="loves"; inf="love"}; poison = {fin="poisons"; inf="poison"}; sleep = {fin="sleeps"; inf="sleep"}; laugh = {fin="laughs"; inf="laugh"}; and = "and"; or = "or"; the = "the"; every = "every"; some = "a" | "some"; makeNP determiner noun = determiner ++ noun; makeNP2 name = name; combineVP v1 c v2 = { fin=v1.fin++c++v2.fin; inf=v1.inf++c++v2.inf }; combineS s1 c s2 = s1 ++ c ++ s2; negateVP vp = { fin="doesn't" ++ vp.inf; inf="not" ++ vp.inf }; makeVP verb name = { inf=verb.inf ++ name; fin=verb.fin ++ name }; makeVP2 verb = {fin=verb.fin; inf=verb.inf}; makeS name vp = name ++ vp.fin; } #+end_src * Logic - Formula :: A *formula* is a sequence/tree of symbols - Interpretation :: An *interpretation* maps formulae into models ** Properties of Calculi - Soundness :: A calculus $C$ is *sound*, iff $\mathcal{H} \vDash A$ whenever $\mathcal{H} \vdash_C A$ - Completeness :: A calculus $C$ is *complete*, iff $\mathcal{H} \vdash_C A$ whenever $\mathcal{H} \vDash A$ - Deduction Theorem :: A calculus $C$ obeys the deduction theorem if \[ \mathcal{H}, A \vdash_C B \text{ iff } \mathcal{H} \vdash_C A \implies B \] - Entailment Theorem :: A Logic obeys the entailment theorem if \[ \mathcal{H}, A \vDash B \text{ iff } \mathcal{H} \vDash A \implies B \] ** Predicate Logic without Quantifiers #+begin_src mmt theory plnq : ur:?LF = prop : type ❘ # o ❙ ind : type ❘ # ι ❙ and : o ⟶ o ⟶ o ❘ # 1 ∧ 2 prec 50 ❙ not : o ⟶ o ❘ # ¬ 1 prec 60 ❙ or : o ⟶ o ⟶ o ❘ # 1 ∨ 2 prec 40 ❘ = [x : o] [y : o] ¬ (¬ x ∧ ¬ y) ❙ implies : o ⟶ o ⟶ o ❘ = [x : o] [y : o] ¬ x ∨ y ❘ # 1 ⇒ 2 prec 30 ❙ biimplication : o ⟶ o ⟶ o ❘ = [x : o] [y : o] (x ⇒ y) ∧ (y ⇒ x) ❘ # 1 ⇔ 2 prec 20 ❙ ❚ #+end_src *** Natural Deduction #+begin_src mmt theory plnq_proofs : ur:?LF = include ?plnq ❙ ded : o ⟶ type ❘ # ⊢ 1 prec 5 ❙ andEl : {A:o} {B:o} ⊢ A ∧ B ⟶ ⊢ A ❘ # aEl 3 ❙ andEr : {A:o} {B:o} ⊢ A ∧ B ⟶ ⊢ B ❘ # aEr 3 ❙ andI : {A:o} {B:o} ⊢ A ⟶ ⊢ B ⟶ ⊢ A ∧ B ❘ # aI 3 4 ❙ orIl : {A:o} {B:o} ⊢ A ⟶ ⊢ A ∨ B ❙ orIr : {A:o} {B:o} ⊢ B ⟶ ⊢ A ∨ B ❙ orE : {A:o} {B:o} {C:o} ⊢ A ∨ B ⟶ (⊢ A ⟶ ⊢ C) ⟶ (⊢ B ⟶ ⊢ C) ⟶ ⊢ C ❙ implE : {A:o} {B:o} ⊢ A ⟶ ⊢ A ⇒ B ⟶ ⊢ B ❙ implI : {A:o} {B:o} (⊢ A ⟶ ⊢ B) ⟶ ⊢ A ⇒ B ❘ # ⇒I 3 ❙ ❚ #+end_src *** Tableau Calculus #+begin_src elpi kind o type. type neg o -> o. type and o -> o -> o. type or o -> o -> o. kind iota type. type mary iota. type john iota. type love iota -> iota -> o. type atomic o -> prop. atomic (neg _A) :- !, fail. atomic (and _A _B) :- !, fail. atomic (or _A _B) :- !, fail. atomic _A. kind mo type. type markF o -> mo. type markT o -> mo. type member mo -> (list mo) -> prop. member X [X|_]. member X [_|Xs] :- member X Xs. type tableau (list mo) -> (list mo) -> prop. tableau [markT (and A B)|T] M :- tableau [markT A, markT B | T] M. tableau [markF (and A _B)|T] M :- tableau [markF A | T] M. tableau [markF (and _A B)|T] M :- tableau [markF B | T] M. tableau [markT (neg A)|T] M :- tableau [markF A | T] M. tableau [markF (neg A)|T] M :- tableau [markT A | T] M. tableau [markF A |T] [markF A |M] :- atomic A, tableau T M, not (member (markT A) M). tableau [markT A |T] [markT A |M] :- atomic A, tableau T M, not (member (markF A) M). tableau [] []. #+end_src ** First Order Logic #+begin_src mmt theory fol : ur:?LF = include ?plnq ❙ forall : (ι ⟶ o) ⟶ o ❘ # ∀ 1 ❙ exist : (ι ⟶ o) ⟶ o ❘ # ∃ 1 ❘ = [s : ι ⟶ o] ¬ (∀ [x : ι] (¬ s x)) ❙ equal : ι ⟶ ι ⟶ o ❘ # 1 ≐ 2 prec 80 ❙ exists1 : (ι ⟶ o) ⟶ o ❘ # ∃! 1 ❘ = [s : ι ⟶ o] ∃ [x : ι] s x ∧ ∀ [y : ι] s y ⇒ x ≐ y ❙ descr : (ι ⟶ o) ⟶ ι ❘ # the 1 ❙ ❚ #+end_src *** Natural Deduction #+begin_src mmt theory fol_proofs : ur:?LF = include ?plnq_proofs ❙ include ?fol ❙ forallE : {B : ι ⟶ o} {C : ι} ⊢ ∀ B ⟶ ⊢ B C ❙ existsI : {B : ι ⟶ o} {C : ι} ⊢ B C ⟶ ⊢ ∃ B ❙ forallI : {B : ι ⟶ o} ({X : ι} ⊢ B X) ⟶ ⊢ ∀ B ❙ existsE : {B : ι ⟶ o} {C : o} ⊢ ∃ B ⟶ ({w : ι} ⊢ B w ⟶ ⊢ C) ⟶ ⊢ C ❙ equalI : {A : ι} ⊢ A ≐ A ❙ equalE : {A : ι} {B : ι} {P : ι ⟶ o} ⊢ A ≐ B ⟶ ⊢ P A ⟶ ⊢ P B ❙ description_axiom : {S : ι ⟶ o} {a : ι} ⊢ ((S a ∧ ∃! S) ⇔ (the S) ≐ a) ❙ ❚ #+end_src * Fragment 1 We define the /phrasal categories/: | S | Sentence | | NP | Noun phrase | | N | Noun | | N_{pr} | Proper Name | | InTransVerb | Intransitive Verb | | TransVerb | Transitive Verb | | Conj | Connective | | Adj | Adjective | * Fragment 3 #+begin_quote Ethel howled and screamed. #+end_quote We introduce a new phrasal category *{{{abbr(verb phrase, VP)}}}*. In the concrete grammar we need to introduces *tenses* to distinguish e.g. "poisons" and "poison". We assign types to phrasal categories: #+attr_html: :border 2 :rules all :frame border | Category | Type | Intuition | |-------------+-----------------------+-----------------| | S | o | thruth value | | NP | \iota | individual | | N_{pr} | \iota | individuals | | VP | \iota \to o | property | | InTransVerb | \iota \to o | unary predicate | | TransVerb | \iota \to \iota \to o | binary relation | ** Simply Typed Lambda Calculus - \alpha-equivalence :: $(\lambda x.\, A) =_{\alpha} (\lambda y.\, [y/x]A)$ - \beta-reduction :: $(\lambda x.\, A) B =_{\beta} [B/x]A$ - \eta-reduction :: $(\lambda x.\, A x) =_{\eta} A$ , iff $x$ is not free in $A$ * Fragment 4 ** Higher-Order Abstract Syntax We want to encode quantifiers in the lambda calculus with $\Pi$ and $\Sigma$ types. If we interpret objects of type $\iota \to o$ as sets, we can define: \begin{align*} (\forall x_{\alpha}.\, A) &:= \Pi_{\alpha} (\lambda x_{\alpha}. A)\\ (\exists x_{\alpha}.\, A) &:= \Sigma_{\alpha} (\lambda x_{\alpha}. A) \end{align*} ** Equality ** Description Operator "The" cannot be treated with regular quantifiers. ** Views #+begin_src mmt view GrammarSemantics : http://mathhub.info/tmpGLIF/default/Grammar.gf?Grammar -> ?people = Name = ι ❙ TransVerb = ι ⟶ ι ⟶ o ❙ InTransVerb = ι ⟶ o ❙ VP = ι ⟶ o ❙ S = o ❙ Conn = o ⟶ o ⟶ o ❙ Noun = ι ⟶ o ❙ Det = (ι ⟶ o) ⟶ (ι ⟶ o) ⟶ o ❙ NP = (ι ⟶ o) ⟶ o ❙ // makeNP : Det ⟶ Noun ⟶ NP ❙ makeNP = [det:(ι ⟶ o) ⟶ (ι ⟶ o) ⟶ o] [noun:ι ⟶ o] det noun ❙ // makeNP2 : Name ⟶ NP ❙ makeNP2 = [name:ι] ([vp:ι⟶o] vp name) ❙ // makeVP : TransVerb -> NP -> VP; ❙ makeVP = [tv:ι⟶ι⟶o] [np:(ι⟶o)⟶o] [x:ι] np (tv x) ❙ makeVP2 = [itv:ι⟶o] [x:ι] itv x ❙ // makeS : NP ⟶ VP ⟶ S ❙ makeS = [np:(ι⟶o)⟶o][vp:ι⟶o] np vp ❙ // makeS = [n:ι][v:ι⟶o] v n ❙ // combineVP : VP -> Conn -> VP -> VP; ❙ combineVP = [vpa: ι⟶o] [c: o⟶o⟶o] [vpb: ι⟶o] [x:ι] c (vpa x) (vpb x) ❙ // combineS : S -> Conn -> S -> S; ❙ combineS = [x: o] [c: o ⟶ o ⟶ o] [y: o] c x y ❙ // negateVP : VP -> VP; ❙ negateVP = [vp: ι⟶o] [x:ι] ¬ (vp x) ❙ and = [x] [y] x ∧ y ❙ or = [x] [y] x ∨ y ❙ some = [noun: ι⟶o] [vp: ι ⟶ o] ∃ [x] noun x ∧ vp x ❙ every = [noun: ι⟶o] [vp: ι ⟶ o] ∀ [x] noun x ⇒ vp x ❙ the = [noun: ι⟶o] [vp: ι ⟶ o] vp (descr noun) ❙ teacher = teacher' ❙ cat_ = cat' ❙ dog = dog' ❙ peter = peter' ❙ mary = mary' ❙ fido = fido' ❙ love = love' ❙ sleep = sleep' ❙ laugh = laugh' ❙ poison = poison' ❙ ❚ #+end_src ** Davidsonian Semantics #+begin_quote John killed the cat in a bathroom with a hammer. #+end_quote To allow modifiers on verbs we extend the argument structure of *action verbs* with an event argument. \[ \exists e.\, \exists x,y.\, \mathrm{bathroom}(x) \land \mathrm{hammer}(y) \land \mathrm{kill}(e, \text{peter}, \iota\, \text{cat}) \land \mathrm{in}(e,x) \land \mathrm{with}(e,y) \] ** Neo-Davidsonian Systems Take apart davidsonian predicates further, add event participants via thematic roles. #+begin_quote John killed the cat with a hammer #+end_quote \[ \exists e.\, \exists x.\, \mathrm{hammer}(x) \land \mathrm{killing}(e) \land \mathrm{agent}(e,\text{peter}) \land \mathrm{patient}(e, \iota\, \text{cat}) \land \mathrm{with}(e,x) \] As a neo-davidsonian system can get by without functions and only unary and binary predicates, model generation is easier. Some modifiers are incompatible with some events. | event type | example | |-------------------+--------------------------------------| | *state* | know the answer, stand in the corner | | *process* | run, eat apples | | *accomplishments* | run a mile, eat an apple | | *achievements* | reach the summit | * Dynamic NL Semantics Natural language contains dynamic phenomena which pose problems for our semantics. - Quantifier Scope :: #+begin_quote A man sleeps. He snores. #+end_quote \[ (\exists X.\, \mathrm{man}(X) \land \mathrm{sleeps}(X)) \land \mathrm{snores}(X) \] $X$ is /not bound/ in the second conjunct! - Donkey Sentence :: #+begin_quote If a farmer owns a donkey, he beats it. #+end_quote \[ \forall X,Y.\, \mathrm{farmer}(X) \land \mathrm{donkey}(Y) \land \mathrm{owns}(X,Y) \implies \mathrm{beat}(X,Y) \] Dynamic phenomena are not limited to inter-sentential anaphora! ** Discourse Representation Theory Deal with dynamic phenomena by replacing existential quantifiers. - Discourse :: A *discourse* is a sequence of sentences. - Discourse Representation Theory (DRT) :: A logical system which uses *discourse referents* to model quantification and pronouns. - Discourse Representation Structures (DRS) :: A DRT formula that introduces a set of /discourse referents/ and specifies their meaning via *conditions*. #+begin_quote A student owns a book. #+end_quote #+attr_html: :border 2 :rules cols :frame border :class drs-table | $X,Y$ | |-----------------------| | $\mathrm{student}(X)$ | | $\mathrm{book}(Y)$ | | $\mathrm{own}(X,Y)$ | #+begin_quote If a farmer owns a donkey, he beats it. #+end_quote #+attr_html: :border 2 :rules cols :frame border :class drs-table | $X,Y$ | $\Longrightarrow$ | | |----------------------+-------------------+----------------------| | $\mathrm{farmer}(X)$ | | $\mathrm{beat}(X,Y)$ | | $\mathrm{donkey}(Y)$ | | | | $\mathrm{own}(X,Y)$ | | | *** TODO DRS merging ** Higher-Order Dynamics * Modal Logics #+begin_src mmt theory proplog : ur:?LF = prop : type ❘ # o ❙ not : o ⟶ o ❘ # ¬ 1 ❙ and : o ⟶ o ⟶ o ❘ # 1 ∧ 2 ❙ | #+end_src