...
 
Commits (2)
id: teaching/lbs1920
narration-base: http://mathhub.info/teaching/1920
narration-base: http://mathhub.info/teaching/lbs1920
abstract Assignment3 = {
-- TODO
}
This diff is collapsed.
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Assignment 3\n",
"\n",
"The purpose of this assignment is to revisit NL -> Logic pipeline we explored with fragment 1.\n",
"Your task will be to implement this pipeline for a different, very small fragment that covers sentences like\n",
"* *John is happy*\n",
"* *Mary is smart and happy*\n",
"* *John isn't happy*\n",
"* *Mary is smart and happy or sad*\n",
"\n",
"The resulting logical expressions should be\n",
"* `happy' john'`\n",
"* `(smart' mary') ∧ (happy' mary')`\n",
"* `¬ (happy' john')`\n",
"* `((smart' mary') ∧ (happy' mary')) ∨ ¬(happy' mary')`, `(smart' mary') ∧ ((happy' mary') ∨ ¬(happy' mary'))`\n",
"\n",
"i.e. the last sentence is ambiguous.\n",
"Also note that we define *sad* as not being *happy*.\n",
"\n",
"There is nothing tricky happening in the grammar, so we won't provide you much guidance.\n",
"You should support at least 3 names and 3 adjectives and should cover the example sentences above.\n",
"You do not have to support sentences like *Mary is smart and not happy* (negation is only introduced in the form of *isn't*)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### The Grammar\n",
"\n",
"Since it is such a small problem, we won't split the grammar in to a lexicon and the grammar rules.\n",
"\n",
"**Tip:** It is easier to have one rule for combining adjectives with *and* and one for combining them with *or*, rather than having a general `adjectivephrase -> connective -> adjectivephrase -> adjectivephrase` rule.\n",
"\n",
"**Tip 2:** Use `S` as a category for complete sentences, since this is the default category GF uses for parsing."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Defined Assignment3"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"abstract Assignment3 = {\n",
" -- TODO\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
"concrete Assignment3Eng of Assignment3 = {\n",
" -- TODO\n",
"}"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This should be it. Try parsing a few sentences to make sure everything works."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Category S is not in scope"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"parse \"Mary isn't smart and happy\""
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Defining the Target Logic and Domain Theory\n",
"\n",
"Now we are done with the GF part.\n",
"Before we define the semantics construction (= translation into logic), we need to define a logic and a domain theory.\n",
"The logic will again be PLNQ, which is already provided.\n",
"However, we still need a domain theory `A3DomainTheory` that is based on PLNQ.\n",
"\n",
"It has to introduce the logical equivalents to *John*, *Mary*, *happy*, ...\n",
"\n",
"Your task is to declare the corresponding constants in `A3DomainTheory`.\n",
"To make things a little more interesting: Do not declare *sad* in your domain theory.\n",
"Instead we will define it as \"not happy\" during the semantics construction."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created theory plnq"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"theory plnq : ur:?LF =\n",
" proposition : type ❘ # o ❙\n",
" \n",
" negation : o ⟶ o ❘ # ¬ 1 prec 25 ❙\n",
" disjunction : o ⟶ o ⟶ o ❘ # 1 ∨ 2 prec 15 ❙\n",
" conjunction : o ⟶ o ⟶ o ❘ = [a,b] ¬ (¬ a ∨ ¬ b) ❘ # 1 ∧ 2 prec 20 ❙\n",
" implication : o ⟶ o ⟶ o ❘ = [a,b] ¬ a ∨ b ❘ # 1 ⇒ 2 prec 10 ❙\n",
" equivalence : o ⟶ o ⟶ o ❘ = [a,b] (a ⇒ b) ∧ (b ⇒ a) ❘ # 1 ⇔ 2 prec 5 ❙\n",
" \n",
" individual : type ❘ # ι ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created theory A3DomainTheory"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"theory A3DomainTheory : ?plnq =\n",
" // TODO ❙\n",
"❚"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### At Last: The Semantics Construction\n",
"\n",
"Combining adjectives with logical connectives is a little bit trickier than what we saw in fragment 1.\n",
"\n",
"The reason for this is that combining e.g. `happy'` and `smart'` should not result in an expression `(happy' ∧ smart')`,\n",
"since that is not a valid expression in PLNQ.\n",
"\n",
"Instead, it should result in a function that takes an individual `x` and returns\n",
"`(happy' x) ∧ (smart' x)`.\n",
"You can achieve this using an extra lambda expression (i.e. `[x] (happy' x) ∧ (smart' x)`)\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"view A3SemanticsConstruction : http://mathhub.info/teaching/lbs1920/Assignment3.gf?Assignment3 -> ?A3DomainTheory =\n",
" // TODO fill in missing things ❙\n",
" \n",
" john = john' ❙\n",
" mary = mary' ❙\n",
" happy = happy' ❙\n",
" smart = smart' ❙\n",
"❚"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Let's try it out!"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parse \"John is happy\" | construct -v A3SemanticsConstruction"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parse \"John isn't happy\" | construct -v A3SemanticsConstruction"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parse \"John is happy and smart\" | construct -v A3SemanticsConstruction"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parse \"John isn't happy and smart\" | construct -v A3SemanticsConstruction"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parse \"Mary is happy or sad and smart\" | construct -v A3SemanticsConstruction"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "GLF",
"language": "gf",
"name": "glf"
},
"language_info": {
"codemirror_mode": {
"name": "gf",
"version": 3
},
"file_extension": ".gf",
"mimetype": "text/gf",
"name": "gf"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
concrete Assignment3Eng of Assignment3 = {
-- TODO
}
namespace http://mathhub.info/teaching/lbs1920/assignment3 ❚
theory plnq : ur:?LF =
proposition : type ❘ # o ❙
negation : o ⟶ o ❘ # ¬ 1 prec 25 ❙
disjunction : o ⟶ o ⟶ o ❘ # 1 ∨ 2 prec 15 ❙
conjunction : o ⟶ o ⟶ o ❘ = [a,b] ¬ (¬ a ∨ ¬ b) ❘ # 1 ∧ 2 prec 20 ❙
implication : o ⟶ o ⟶ o ❘ = [a,b] ¬ a ∨ b ❘ # 1 ⇒ 2 prec 10 ❙
equivalence : o ⟶ o ⟶ o ❘ = [a,b] (a ⇒ b) ∧ (b ⇒ a) ❘ # 1 ⇔ 2 prec 5 ❙
individual : type ❘ # ι ❙
theory A3DomainTheory : ?plnq =
// TODO ❙
view A3SemanticsConstruction : http://mathhub.info/teaching/lbs1920/assignment3/Assignment3.gf?Assignment3 -> ?A3DomainTheory =
// TODO ❙
john = john' ❙
mary = mary' ❙
berti = berti' ❙
happy = happy' ❙
smart = smart' ❙