Commit d78a5c21 authored by jfschaefer's avatar jfschaefer

updated frag3 and frag4

parent 28910297
......@@ -27,7 +27,7 @@
},
{
"cell_type": "code",
"execution_count": 1,
"execution_count": 21,
"metadata": {},
"outputs": [
{
......@@ -46,7 +46,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 22,
"metadata": {},
"outputs": [
{
......@@ -65,7 +65,7 @@
},
{
"cell_type": "code",
"execution_count": 3,
"execution_count": 23,
"metadata": {},
"outputs": [
{
......@@ -96,7 +96,7 @@
},
{
"cell_type": "code",
"execution_count": 4,
"execution_count": 24,
"metadata": {},
"outputs": [
{
......@@ -136,7 +136,7 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 25,
"metadata": {},
"outputs": [],
"source": [
......@@ -164,7 +164,7 @@
},
{
"cell_type": "code",
"execution_count": 6,
"execution_count": 26,
"metadata": {},
"outputs": [],
"source": [
......@@ -211,7 +211,7 @@
},
{
"cell_type": "code",
"execution_count": 7,
"execution_count": 27,
"metadata": {},
"outputs": [
{
......@@ -241,7 +241,7 @@
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 28,
"metadata": {},
"outputs": [],
"source": [
......@@ -265,7 +265,7 @@
},
{
"cell_type": "code",
"execution_count": 33,
"execution_count": 29,
"metadata": {},
"outputs": [
{
......@@ -286,7 +286,7 @@
},
{
"cell_type": "code",
"execution_count": 34,
"execution_count": 30,
"metadata": {},
"outputs": [],
"source": [
......@@ -297,13 +297,13 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 31,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Ethel is wealthy and Prudence is messy or the cake is wealthy\n"
"the dog laughs or sings\n"
]
},
"metadata": {},
......@@ -312,7 +312,7 @@
{
"data": {
"text/plain": [
"it is not the case that it is not the case that the cake is disgusting\n"
"it is not the case that it is not the case that Chester is crazy\n"
]
},
"metadata": {},
......@@ -321,7 +321,7 @@
{
"data": {
"text/plain": [
"Chester screams\n"
"the lecturer is messy or Fiona isn't wealthy or the golfer is Chester\n"
]
},
"metadata": {},
......@@ -330,7 +330,7 @@
{
"data": {
"text/plain": [
"it is not the case that the golfer isn't happy or it is not the case that Ethel is happy\n"
"Jo doesn't poison the student\n"
]
},
"metadata": {},
......@@ -339,7 +339,7 @@
{
"data": {
"text/plain": [
"it is not the case that Chester isn't happy or the dog isn't messy and Fiona is wealthy\n"
"it is not the case that Jo is crazy or it is not the case that Fiona is crazy\n"
]
},
"metadata": {},
......@@ -352,13 +352,13 @@
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "653a56b326614267a848faae39d08ff4",
"model_id": "9ab43eadbd6f495f9482b2caa07c9d6d",
"version_major": 2,
"version_minor": 0
},
......@@ -390,7 +390,7 @@
},
{
"cell_type": "code",
"execution_count": 15,
"execution_count": 33,
"metadata": {},
"outputs": [
{
......@@ -417,7 +417,7 @@
},
{
"cell_type": "code",
"execution_count": 16,
"execution_count": 34,
"metadata": {},
"outputs": [
{
......@@ -440,7 +440,7 @@
" pred2 : type ❘ = ι ⟶ ι ⟶ o ❙\n",
" equal : pred2 ❘ # 1 == 2 ❙\n",
" \n",
" noun : type ❙\n",
" noun : type ❘ = ι ⟶ o❙\n",
" the : noun ⟶ ι ❙\n",
"❚"
]
......@@ -454,7 +454,7 @@
},
{
"cell_type": "code",
"execution_count": 17,
"execution_count": 35,
"metadata": {},
"outputs": [
{
......@@ -488,7 +488,7 @@
},
{
"cell_type": "code",
"execution_count": 18,
"execution_count": 36,
"metadata": {},
"outputs": [
{
......@@ -531,7 +531,7 @@
},
{
"cell_type": "code",
"execution_count": 19,
"execution_count": 37,
"metadata": {},
"outputs": [
{
......@@ -591,12 +591,12 @@
" // s3 : Sentence ⟶ Conjunction ⟶ Sentence ⟶ Sentence ❙\n",
" // s3 : o ⟶ (o ⟶ o ⟶ o) ⟶ o ⟶ o ❙\n",
" s3 = [s1,conj,s2] conj s1 s2 ❙\n",
"❚\n"
"❚"
]
},
{
"cell_type": "code",
"execution_count": 30,
"execution_count": 38,
"metadata": {},
"outputs": [
{
......@@ -624,7 +624,7 @@
},
{
"cell_type": "code",
"execution_count": 31,
"execution_count": 39,
"metadata": {},
"outputs": [
{
......@@ -652,7 +652,7 @@
},
{
"cell_type": "code",
"execution_count": 32,
"execution_count": 40,
"metadata": {},
"outputs": [
{
......
......@@ -25,7 +25,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 71,
"metadata": {},
"outputs": [
{
......@@ -54,7 +54,7 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 72,
"metadata": {},
"outputs": [
{
......@@ -78,7 +78,21 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 73,
"metadata": {},
"outputs": [],
"source": [
"concrete Frag4CatEng of Frag4Cat = Frag3CatEng ** {\n",
" lincat\n",
" Det = Str;\n",
" Prep = Str;\n",
" PrepPhrase = Str;\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 74,
"metadata": {},
"outputs": [
{
......@@ -92,7 +106,7 @@
}
],
"source": [
"abstract Frag4Grammar = Frag3Grammar, Frag4Cats ** {\n",
"abstract Frag4Grammar = Frag3Grammar, Frag4Cat ** {\n",
" fun\n",
" n2np : Det -> Noun -> NounPhrase ;\n",
" makePP : Prep -> NounPhrase -> PrepPhrase ;\n",
......@@ -111,20 +125,34 @@
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 75,
"metadata": {},
"outputs": [],
"source": [
"concrete Frag4GrammarEng of Frag4Grammar = Frag3GrammarEng, Frag4CatEng ** {\n",
" lin\n",
" n2np det noun = det ++ noun ;\n",
" makePP prep np = prep ++ np ;\n",
" prepnp np pp = np ++ pp ;\n",
" prepvp vp pp = mkT (vp!Inf ++ pp) (vp!Fin ++ pp) ;\n",
" every = \"every\" ;\n",
" the = \"the\" ;\n",
" some = \"some\" ;\n",
" a_Det = \"a\" ;\n",
" in_Prep = \"in\" ;\n",
" with_Prep = \"with\" ;\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 76,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"invalid unit: http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics?[http://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar]/n2np?definition: Judgment |- [det,noun]det noun : (noun⟶pred1⟶o)⟶(noun⟶ι)\n",
"invalid unit: http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics?[http://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar]/n2np?definition: Judgment |- [det,noun]det noun : (noun⟶pred1⟶o)⟶(noun⟶ι)\n",
"unbound token: ∀\n",
"invalid unit: http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics?[http://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar]/every?definition: Judgment |- [P,Q]∀ [x](P x)⇒(Q x) : noun⟶pred1⟶o\n",
"unbound token: ∃\n",
"invalid unit: http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics?[http://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar]/some?definition: Judgment |- [P,Q]∃ [x](P x)∧(Q x) : noun⟶pred1⟶o\n",
"keyword expected, within module http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics\n",
"invalid element: view is not total: http://mathhub.info/Teaching/lbs1920?Frag4GrammarSemantics"
"Defined Frag4Lex"
]
},
"metadata": {},
......@@ -132,28 +160,285 @@
}
],
"source": [
"view Frag4GrammarSemantics : https://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar -> ?frag3DomainTheory =\n",
" include ?Frag3GrammarSemantics ❙\n",
" // noun = ι ⟶ o ❙\n",
" Det = noun ⟶ pred1 ⟶ o ❙\n",
"abstract Frag4Lex = Frag4Cat ** {\n",
" fun\n",
" prudence, ethel, chester, jo, bertie, fiona : ProperName ;\n",
" book, cake, katze, golfer, dog, lecturer, student, singer : Noun ;\n",
" run, laugh, sing, howl, scream : VerbIntransitive ;\n",
" read, poison, eat, like, loath, kick : VerbTransitive ;\n",
" and, or : Conjunction ;\n",
" happy, crazy, messy, disgusting, wealthy : Adjective ;\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [],
"source": [
"concrete Frag4LexEng of Frag4Lex = Frag4CatEng ** {\n",
" lin\n",
" prudence = \"Prudence\"; ethel = \"Ethel\"; chester = \"Chester\"; jo = \"Jo\"; bertie = \"Bertie\"; fiona = \"Fiona\";\n",
" book = \"book\"; cake = \"cake\"; katze = \"cat\"; golfer = \"golfer\"; dog = \"dog\"; lecturer = \"lecturer\"; student = \"student\"; singer = \"singer\"; \n",
" run = mkTs \"run\"; laugh = mkTs \"laugh\"; sing = mkTs \"sing\"; howl = mkTs \"howl\"; scream = mkTs \"scream\";\n",
" read = mkTs \"read\"; poison = mkTs \"poison\"; eat = mkTs \"eat\"; like = mkTs \"like\"; loath = mkTs \"loath\"; kick = mkTs \"kick\";\n",
" and = \"and\"; or = \"or\";\n",
" happy = \"happy\"; crazy = \"crazy\"; messy = \"messy\"; disgusting = \"disgusting\"; wealthy = \"wealthy\";\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 78,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Defined Frag4"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"abstract Frag4 = Frag4Grammar, Frag4Lex ** {\n",
"\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 79,
"metadata": {},
"outputs": [],
"source": [
"concrete Frag4Eng of Frag4 = Frag4GrammarEng, Frag4LexEng ** {\n",
"\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 80,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created view Frag4CatSemantics"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"view Frag4CatSemantics : http://mathhub.info/Teaching/lbs1920/generated/Frag4Cat.gf?Frag4Cat -> ?plnq =\n",
" Sentence = o ❙\n",
" NounPhrase = (ι ⟶ o) ⟶ o ❙\n",
" Noun = ι ⟶ o ❙\n",
" ProperName = ι ❙\n",
" VerbIntransitive = ι ⟶ o ❙\n",
" VerbTransitive = ι ⟶ ι ⟶ o ❙\n",
" VerbPhraseFin = ι ⟶ o ❙\n",
" VerbPhraseInf = ι ⟶ o ❙\n",
" Conjunction = o ⟶ o ⟶ o ❙\n",
" Adjective = ι ⟶ o ❙\n",
" Det = (ι ⟶ o) ⟶ (ι ⟶ o) ⟶ o ❙\n",
" Prep = ι ⟶ (ι ⟶ ι) ❙\n",
" PrepPhrase = ι ⟶ ι ❙\n",
" n2np = [det,noun] det noun ❙\n",
" makePP = [prep, np] prep np ❙\n",
" prepnp = [np,pp] pp np ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 81,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created theory fol"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"theory fol : ur:?LF =\n",
" include ?plnq ❙\n",
" forall : (ι ⟶ o) ⟶ o ❘ # ∀ 1 ❙\n",
" exists : (ι ⟶ o) ⟶ o ❘ = [P] ¬ ∀ [x] (¬ (P x)) ❘ # ∃ 1 ❙\n",
" exists1 : (ι ⟶ o) ⟶ o ❘ = [P] ∃ [x] ((P x) ∧ ∀ [y] (P y) ⇒ (x == y)) ❘ # ∃1 1 ❙\n",
" \n",
" ded : o ⟶ type ❘ # ⊢ 1 ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 82,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created theory frag4DomainTheory"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"theory frag4DomainTheory : ?fol =\n",
" include ?frag3DomainTheory ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 83,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created view Frag4GrammarSemantics"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"view Frag4GrammarSemantics : http://mathhub.info/Teaching/lbs1920/generated/Frag4Grammar.gf?Frag4Grammar -> ?frag4DomainTheory =\n",
" include ?Frag4CatSemantics ❙\n",
" v1 = [happy] happy ❙\n",
" v2 = [run] run ❙\n",
" // v3 : VerbTransitive ⟶ NounPhrase ⟶ VerbPhraseInf ❙\n",
" // v3 : (ι ⟶ ι ⟶ o) ⟶ ((ι ⟶ o) ⟶ o) ⟶ (ι ⟶ o) ❙\n",
" v3 = [VT,np] [x] np (VT x) ❙\n",
" \n",
" // v4 : NounPhrase ⟶ VerbPhraseFin \"the teacher\" -> \"is the teacher\"❙\n",
" v4 = [NP] [x] NP ([y] x == y) ❙\n",
" v5 = [and, run, laugh] ([john] and (run john) (laugh john)) ❙\n",
" v6 = [and, runs, laughs] [john] and (runs john) (laughs john) ❙\n",
" v7 = [laugh] [john] ¬ (laugh john) ❙\n",
" v8 = [P] [john] (P john) ❙\n",
" // n1 : ProperName ⟶ NounPhrase ❙\n",
" n1 = [john] [P] (P john) ❙\n",
" // n2 : Noun ⟶ NounPhrase ❙\n",
" n2 = [n : ι ⟶ o] [P : ι ⟶ o] (P (the n)) ❙\n",
" s1 = [john] [run] (john run) ❙\n",
" s2 = [x] ¬ x ❙\n",
" s3 = [s1,conj,s2] conj s1 s2 ❙\n",
" \n",
" \n",
" n2np = [det : (ι ⟶ o) ⟶ (ι ⟶ o) ⟶ o, n : ι ⟶ o] (det n) ❙\n",
" makePP = [pr, np] [x] chester ❙\n",
" prepnp = [np,pp] np ❙\n",
" // prepvp : (ι ⟶ o) ⟶ PrepPhrase ⟶ (ι ⟶ o) ❙\n",
" prepvp = [vp,pp] [x] vp (pp x) ❙\n",
" every = [P,Q] ∀[x] (P x) ⇒ (Q x) ❙\n",
" some = [P,Q] ∃[x] (P x) ∧ (Q x) ❙\n",
""
""
]
},
{
"cell_type": "code",
"execution_count": null,
"execution_count": 84,
"metadata": {},
"outputs": [],
"source": []
"outputs": [
{
"data": {
"text/plain": [
"Created theory Frag4Lex"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"theory Frag4Lex : ?fol =\n",
" include ☞http://mathhub.info/Teaching/lbs1920/generated/Frag4Cat.gf?Frag4Cat ❙\n",
" include ☞http://mathhub.info/Teaching/lbs1920/generated/Frag3Lex.gf?Frag3Lex ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 85,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created view Frag4LexSemantics"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"view Frag4LexSemantics : http://mathhub.info/Teaching/lbs1920/generated/Frag4Lex.gf?Frag4Lex -> ?frag4DomainTheory =\n",
" include ?Frag4CatSemantics ❙\n",
" \n",
" prudence = prudence ❙ ethel = ethel ❙ chester = chester ❙ jo = jo ❙ bertie = bertie ❙ fiona = fiona ❙\n",
" book = book ❙ cake = cake ❙ katze = cat ❙ golfer = golfer ❙ dog = dog ❙ lecturer = lecturer ❙ student = student ❙ singer = singer ❙\n",
" run = run ❙ laugh = laugh ❙ sing = sing ❙ howl = howl ❙ scream = scream ❙\n",
" read = read ❙ poison = poison ❙ eat = eat ❙ like = like ❙ loath = loath ❙ kick = kick ❙\n",
" and = conjunction ❙ or = disjunction ❙\n",
" happy = happy ❙ crazy = crazy ❙ messy = messy ❙ disgusting = disgusting ❙ wealthy = wealthy ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 86,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Created view Frag4Semantics"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"view Frag4Semantics : http://mathhub.info/Teaching/lbs1920/generated/Frag4.gf?Frag4 -> ?frag4DomainTheory =\n",
" include ?Frag4GrammarSemantics ❙\n",
" include ?Frag4LexSemantics ❙\n",
"❚"
]
},
{
"cell_type": "code",
"execution_count": 89,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"∀[x](cat x)⇒(run x)"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"parse -cat=Sentence \"every cat is happy\" | construct -v Frag4Semantics"
]
}
],
"metadata": {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment