Assignment 3_Target Logic and Domain Theory

Master / Vertiefung Logik-Basierte Sprachverarbeitung
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Assignment 3_Target Logic and Domain Theory
Hello Frederik,

In the Target Logic and Domain Theory, I have mistakes which I cannot see. Can you check my code below? It outputs in the example sentences always “happy pelin”. I haven’t considered “happy= -sad” in the below code yet.

theory A3DomainTheory : ?plnq =
pred1 : type ❘ = ι ⟶ o ❙

john : ι ❙ mary : ι ❙ pelin : ι ❙
happy : pred1 ❙ smart : pred1 ❙ easy : pred1 ❙ strong : pred1 ❙ sad : pred1 ❙

view A3SemanticsConstruction : http://mathhub.info/Teaching/lbs1920/Assignment3.gf?Assignment3 → ?A3DomainTheory =
// TODO fill in missing things ❙

Sentence = o ❙
NounPhrase = ι ❙
ProperName = ι ❙
VerbPhrase = ι ⟶ o ❙
And = o ⟶ o ⟶ o ❙
Or = o ⟶ o ⟶ o ❙
AdjectivePhrase = ι ⟶ o ❙

v1 = [happy] happy ❙
v1_neg = [happy] [john] ¬ (happy john) ❙
a1 = [and, happy, easy] [pelin] and (happy pelin) (easy pelin) ❙
a2 = [or, happy, easy] [pelin] or (happy pelin) (easy pelin) ❙
n1 = [p] p ❙
s1 = [pelin] [happy] (happy pelin) ❙

john = john ❙ mary =  mary ❙ pelin =  pelin ❙ 
and = conjunction ❙ or = disjunction ❙
happy = happy ❙ smart = smart ❙ strong =  strong ❙ easy =  easy ❙ sad =  sad ❙

❚

Best,
Pelin

3

This is the problem we encountered during the lecture last week.

Theoretically, your code should work. However, there is a problem with variable binding in MMT (which apparently has some reasonable justification).

Workaround: You need to rename the variables so that they don’t have the same name as things in your domain theory.

For example: Replace [m][and, happy, easy] [pelin] and (happy pelin) (easy pelin)[/m] by [m][and1, happy1, easy1] [pelin1] and1 (happy1 pelin1) (easy1 pelin1)[/m]

This way, MMT knows that when you write happy1 you mean the bound variable, not the entry in the domain theory.

Best,
Frederik

4

Hi Frederik,

It worked. Thanks for help.

I added at the last part:
sad = negation(happy) ❙
but it gives error. Can you give me a clue about how it may work?

I have some other questions:

  why is "negated happy" described differently from "happy"? Why do we add john in the latter?
         v1 = [happy0] happy0 ❙
         v1_neg = [happy0] [john0] ¬ (happy0 john0) ❙

  The order of the lambda terms in two constructions are very similar but different. [happy0][john0]  &  [pelin3] [happy3]
  It gives error if I change the order. Can you explain why is that so?
         v1_neg = [happy0][john0]  ¬ (happy0 john0) ❙
         s1 = [pelin3] [happy3] (happy3 pelin3) ❙

   what is the difference between "theory plnq" and "theory A3DomainTheory"? 

   We used in "concrete Fragment0_1GrammarEng" parameter Plurality = Sg | Pl.
   It first looks at the NP if singular or plural then decides the correct form of the verb, right?
          NP = { s : Str ; p : Plurality };
          VP = Plurality => Str; 
          makeS n v = n.s ++ v ! n.p;
   can we use the same method in  "concrete Frag3GrammarEng" and define a record type for NP={s=Str ; v=Verbform} and put ...!n.v       
   instead of putting  mkT(....!Inf , ...!Fin)?

Best,
Pelin

5

Hi Pelin,

the first three questions all boil down to the same thing:
negation has the type o → o.
So it expects a proposition and returns a new proposition.
happy, however, has type i → o.
So you can’t apply negation to happy, because happy is not of type o.

That’s why we have to introduce an extra lambda:
[x] negation (happy x)
works, because (happy x) is of type o.
So for question 1: You need to to something like that
For question 2: That’s why we add [john0]. john0 corresponds to the x above.
For question 3: They are simply two different things. One takes a verb (type i → o) and negates it. The other rule combines an individual and a verb into a sentence (i.e. the result is o, not i->o).

The difference between plnq and A3DomainTheory:
plnq defines a logic (predicate logic without quantifiers, which you could also think of as propositional logic with individuals and predicates).
A3DomainTheory uses that logic to build up a domain theory. It creates constants like book, happy, love.
The reason for this is, because we can’t translate “John is happy and Mary is happy” into PLNQ without constants for John, Mary and happy. Of course, things like “and” are provided by plnq.
The separation into two theories helps to keep things more modular. Theoretically, we could have created one big theory instead.

About the grammar: things are a bit different in fragment 3, because we don’t allow for plural noun phrases.
So the rule to combine a noun phrase and a (fin) verb phrase into a sentence is quite simple:
s1 peter runs = peter ++ runs;
mkT is used in a different context: There we try to combine two verbs into a new verb. So we essentially have to combine two tables into a new table, which is different from picking the right form in a table to create a string.

I hope this helps :slight_smile:
Best, Frederik