Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
P
prob-teaching-notebooks
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Iterations
Wiki
Requirements
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Test cases
Artifacts
Deploy
Releases
Package registry
Container registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Code review analytics
Issue analytics
Insights
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
general
stups
prob-teaching-notebooks
Commits
31390aa9
Commit
31390aa9
authored
Apr 30, 2020
by
Michael Leuschel
Browse files
Options
Downloads
Patches
Plain Diff
add Notebook for Grammars
parent
3c4c7517
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
info4/kapitel-1/Grammatiken.ipynb
+871
-0
871 additions, 0 deletions
info4/kapitel-1/Grammatiken.ipynb
with
871 additions
and
0 deletions
info4/kapitel-1/Grammatiken.ipynb
0 → 100644
+
871
−
0
View file @
31390aa9
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Grammatiken\n",
"\n",
"Dieses Notebook begleitet Teil 2 der Vorlesung 3."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Eine __Grammatik__ ist ein Quadrupel \n",
"$G = (\\Sigma , N, S, P)$, wobei\n",
"* $\\Sigma$ ein Alphabet (von so genannten __Terminalsymbolen__) ist,\n",
"* $N$ eine endliche Menge (von so genannten __Nichtterminalen__) mit\n",
" $\\Sigma \\cap N = \\emptyset$,\n",
"* $S \\in N$ das __Startsymbol__ und\n",
"* $P \\subseteq (N \\cup \\Sigma)^+ \\times (N \\cup \\Sigma)^{\\ast}$ die\n",
" endliche Menge der __Produktionen__ (Regeln).\n",
" \n",
"Diese mathematische Definition setzen wir im Notebook folgendermaßen um.\n",
"Wir verwenden eine B Maschine um eine neue Basismenge an Symbolen (ΣN) einführen zu können.\n",
"Hier steht ```seq1(T)``` für die nicht leeren Folgen über T, also $T^+$ in der Notation des Skripts."
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: Grammatik"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
"MACHINE Grammatik\n",
"SETS ΣN = {a,b,c, S}\n",
"CONSTANTS Σ, N, P\n",
"PROPERTIES\n",
" Σ = {a,b,c} ∧\n",
" Σ ∩ N = {} ∧\n",
" Σ ∪ N = ΣN ∧\n",
" S ∈ N ∧\n",
" P ⊆ seq1(ΣN) × seq(ΣN) ∧\n",
" \n",
" // Die Beispiel Grammatik G1 von den Folien\n",
" P = { [S] ↦ [],\n",
" [S] ↦ [a,S,b]\n",
" }\n",
"DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
"END"
]
},
{
"cell_type": "code",
"execution_count": 41,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{abl} = /*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} \\expn \\mathit{p} \\expn \\mathit{z} \\land \\mathit{v} = \\mathit{x} \\expn \\mathit{q} \\expn \\mathit{z})\\}$\n",
"* $\\mathit{RHS} = []$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tabl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}\n",
"\tRHS = []"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[S] ↦ RHS ∈ P"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Mit dem relationalen Bild können wir alle Regeln mit der Folge S auf der rechten Seite finden:"
]
},
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,\\mathit{S},b]\\}$"
],
"text/plain": [
"{[],[a,S,b]}"
]
},
"execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"P[{[S]}]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Definiere die __unmittelbare Ableitungsrelation__ bzgl. $G$ so\n",
"\n",
"* $u \\vdash_{G} v \\Longleftrightarrow u = xpz, v = xqz$,\n",
"\n",
"wobei $x,z \\in (N \\cup \\Sigma)^{\\ast}$ und $p \\rightarrow q$ eine Regel in $P$\n",
"ist.\n",
"\n",
"Im Notebook können wir dies so umsetzen, können aber leider nicht das Symbol $\\vdash_G$ verwenden.\n",
"Aus $u \\vdash_{G} v$ wird $u \\mapsto v \\in abl$."
]
},
{
"cell_type": "code",
"execution_count": 44,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}/*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} ⌒ \\mathit{p} ⌒ \\mathit{z} \\land \\mathit{v} = \\mathit{x} ⌒ \\mathit{q} ⌒ \\mathit{z})\\}$"
],
"text/plain": [
"/*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ⌒ p ⌒ z ∧ v = x ⌒ q ⌒ z)}"
]
},
"execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let abl {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Da diese Relation unendlich ist wird diese im Notebook symbolisch gehalten. Wir können aber prüfen ob Paare an Folgen in der Relation sind:"
]
},
{
"cell_type": "code",
"execution_count": 45,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{abl} = /*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} \\expn \\mathit{p} \\expn \\mathit{z} \\land \\mathit{v} = \\mathit{x} \\expn \\mathit{q} \\expn \\mathit{z})\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tabl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}"
]
},
"execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[S] ↦ [a,S,b] ∈ abl"
]
},
{
"cell_type": "code",
"execution_count": 46,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{FALSE}$"
],
"text/plain": [
"FALSE"
]
},
"execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[S] ↦ [a,b] ∈ abl"
]
},
{
"cell_type": "code",
"execution_count": 47,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{x} = []$\n",
"* $\\mathit{abl} = /*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} \\expn \\mathit{p} \\expn \\mathit{z} \\land \\mathit{v} = \\mathit{x} \\expn \\mathit{q} \\expn \\mathit{z})\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tx = []\n",
"\tabl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}"
]
},
"execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[S] ↦ x : abl"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Mit dem relationalen Abbild können wir die Menge aller Umschreibungen berrechnen:"
]
},
{
"cell_type": "code",
"execution_count": 48,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,\\mathit{S},b]\\}$"
],
"text/plain": [
"{[],[a,S,b]}"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"abl[ {[S]} ]"
]
},
{
"cell_type": "code",
"execution_count": 49,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,b],[a,a,S,b,b]}"
]
},
"execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"abl[ {[a,S,b]} ]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Durch mehrfache Anwendung bekommen wir die Ergebnisse von immer längeren Ableitungen:"
]
},
{
"cell_type": "code",
"execution_count": 50,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,b],[a,a,S,b,b]}"
]
},
"execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"abl[ abl[ {[S]} ] ]"
]
},
{
"cell_type": "code",
"execution_count": 51,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,a,b,b],[a,a,a,S,b,b,b]}"
]
},
"execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"abl[ abl[ abl[ {[S]} ] ] ]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Durch $n$-malige Anwendung von $\\vdash_{G}$ erhalten wir\n",
" $\\vdash_{G}^{n}$. Das heiß t:\n",
" \n",
"* $u \\vdash_{G}^{n} v \\Longleftrightarrow u = x_0 \\vdash_{G} x_1\n",
"\\vdash_{G} \\cdots \\vdash_{G} x_n = v$\n",
"\n",
"Im Notebook kann man für die n-malige Anwendung einer binären Relation den Operator ```iterate``` verwenden:"
]
},
{
"cell_type": "code",
"execution_count": 52,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{abl} = /*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} \\expn \\mathit{p} \\expn \\mathit{z} \\land \\mathit{v} = \\mathit{x} \\expn \\mathit{q} \\expn \\mathit{z})\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tabl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}"
]
},
"execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[S] ↦ [a,b] ∈ iterate(abl,2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Die Menge $\\{w \\mid S \\vdash_{G}^{n} w\\}$ kann direkt mit dem relationalen Bild berechnet werden. Zum Beispiel für n = 0,1,2,3,4:"
]
},
{
"cell_type": "code",
"execution_count": 53,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[S]\\}$"
],
"text/plain": [
"{[S]}"
]
},
"execution_count": 53,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" iterate(abl,0)[ {[S]} ]"
]
},
{
"cell_type": "code",
"execution_count": 54,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,\\mathit{S},b]\\}$"
],
"text/plain": [
"{[],[a,S,b]}"
]
},
"execution_count": 54,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" iterate(abl,1)[ {[S]} ]"
]
},
{
"cell_type": "code",
"execution_count": 55,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,b],[a,a,S,b,b]}"
]
},
"execution_count": 55,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" iterate(abl,2)[ {[S]} ]"
]
},
{
"cell_type": "code",
"execution_count": 56,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,a,b,b],[a,a,a,S,b,b,b]}"
]
},
"execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" iterate(abl,3)[ {[S]} ]"
]
},
{
"cell_type": "code",
"execution_count": 57,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[a,a,a,b,b,b],[a,a,a,a,S,b,b,b,b]}"
]
},
"execution_count": 57,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" iterate(abl,4)[ {[S]} ]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Die von der Grammatik $G$ erzeugte Sprache ist\n",
" definiert als\n",
"$L(G) = \\{w \\in \\Sigma^* \\mid S \\vdash_{G}^{\\ast} w\\}.$\n",
"\n",
"Bis zur Länge 4 gibt es folgende abgeleitenen Wörter über $\\Sigma \\cup N$\n",
"(auch Satzformen genannt):"
]
},
{
"cell_type": "code",
"execution_count": 58,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,b],[S],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{S},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}"
]
},
"execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Wenn wir mit $\\Sigma^*$ schneiden bekommen wir Wörter der von der Grammatik generierten Sprache:"
]
},
{
"cell_type": "code",
"execution_count": 61,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,b],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[],[a,b],[a,a,b,b],[a,a,a,b,b,b]}"
]
},
"execution_count": 61,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ]) /\\ seq(Σ)"
]
},
{
"cell_type": "code",
"execution_count": 62,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: Grammatik"
]
},
"execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
"MACHINE Grammatik\n",
"SETS ΣN = {a,b,c, S}\n",
"CONSTANTS Σ, N, P\n",
"ABSTRACT_CONSTANTS abl\n",
"PROPERTIES\n",
" Σ = {a,b,c} ∧\n",
" Σ ∩ N = {} ∧\n",
" Σ ∪ N = ΣN ∧\n",
" S ∈ N ∧\n",
" P ⊆ seq1(ΣN) × seq(ΣN) ∧\n",
" \n",
" // Die Beispiel Grammatik G1 von den Folien\n",
" P = { [S] ↦ [],\n",
" [S] ↦ [a,S,b]\n",
" }\n",
" \n",
" ∧ \n",
" abl = {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}\n",
"DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
"END"
]
},
{
"cell_type": "code",
"execution_count": 63,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 63,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Wir können die Ableitungsrelationen für alle Satzformen bis zu einer gegebenen Tiefe auch grafisch darstellen."
]
},
{
"cell_type": "code",
"execution_count": 66,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[],[a,b],[S],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{S},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
],
"text/plain": [
"{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}"
]
},
"execution_count": 66,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let SF UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])"
]
},
{
"cell_type": "code",
"execution_count": 68,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
]
},
"execution_count": 68,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":pref DOT_DECOMPOSE_NODES=FALSE"
]
},
{
"cell_type": "code",
"execution_count": 69,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"354pt\" height=\"404pt\"\n",
" viewBox=\"0.00 0.00 354.00 404.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 400)\">\n",
"<title>state</title>\n",
"<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-400 351,-400 351,5 -4,5\"/>\n",
"<!-- [a,a,a,S,b,b,b] -->\n",
"<g id=\"node1\" class=\"node\"><title>[a,a,a,S,b,b,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"160.312,-126 67.6878,-126 67.6878,-90 160.312,-90 160.312,-126\"/>\n",
"<text text-anchor=\"middle\" x=\"114\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,S,b,b,b]</text>\n",
"</g>\n",
"<!-- [a,a,a,a,S,b,b,b,b] -->\n",
"<g id=\"node3\" class=\"node\"><title>[a,a,a,a,S,b,b,b,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"112.472,-36 -0.471819,-36 -0.471819,-0 112.472,-0 112.472,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,a,S,b,b,b,b]</text>\n",
"</g>\n",
"<!-- [a,a,a,S,b,b,b]->[a,a,a,a,S,b,b,b,b] -->\n",
"<g id=\"edge2\" class=\"edge\"><title>[a,a,a,S,b,b,b]->[a,a,a,a,S,b,b,b,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M102.541,-89.614C94.0659,-76.7551 82.389,-59.0384 72.8518,-44.5682\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"75.6633,-42.4739 67.2378,-36.0504 69.8186,-46.3261 75.6633,-42.4739\"/>\n",
"<text text-anchor=\"middle\" x=\"99.5526\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [a,a,a,b,b,b] -->\n",
"<g id=\"node5\" class=\"node\"><title>[a,a,a,b,b,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"213.349,-36 130.651,-36 130.651,-0 213.349,-0 213.349,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"172\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,b,b,b]</text>\n",
"</g>\n",
"<!-- [a,a,a,S,b,b,b]->[a,a,a,b,b,b] -->\n",
"<g id=\"edge4\" class=\"edge\"><title>[a,a,a,S,b,b,b]->[a,a,a,b,b,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M125.459,-89.614C133.934,-76.7551 145.611,-59.0384 155.148,-44.5682\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"158.181,-46.3261 160.762,-36.0504 152.337,-42.4739 158.181,-46.3261\"/>\n",
"<text text-anchor=\"middle\" x=\"157.553\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [a,a,S,b,b] -->\n",
"<g id=\"node6\" class=\"node\"><title>[a,a,S,b,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"222.154,-216 149.846,-216 149.846,-180 222.154,-180 222.154,-216\"/>\n",
"<text text-anchor=\"middle\" x=\"186\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,S,b,b]</text>\n",
"</g>\n",
"<!-- [a,a,S,b,b]->[a,a,a,S,b,b,b] -->\n",
"<g id=\"edge6\" class=\"edge\"><title>[a,a,S,b,b]->[a,a,a,S,b,b,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M171.775,-179.614C161.155,-166.634 146.485,-148.704 134.585,-134.16\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"136.992,-131.574 127.95,-126.05 131.574,-136.006 136.992,-131.574\"/>\n",
"<text text-anchor=\"middle\" x=\"165.553\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [a,a,b,b] -->\n",
"<g id=\"node9\" class=\"node\"><title>[a,a,b,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"241.188,-126 178.812,-126 178.812,-90 241.188,-90 241.188,-126\"/>\n",
"<text text-anchor=\"middle\" x=\"210\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,b,b]</text>\n",
"</g>\n",
"<!-- [a,a,S,b,b]->[a,a,b,b] -->\n",
"<g id=\"edge8\" class=\"edge\"><title>[a,a,S,b,b]->[a,a,b,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M190.742,-179.614C194.149,-167.119 198.808,-150.037 202.69,-135.804\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"206.095,-136.619 205.35,-126.05 199.342,-134.777 206.095,-136.619\"/>\n",
"<text text-anchor=\"middle\" x=\"209.553\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [a,S,b] -->\n",
"<g id=\"node10\" class=\"node\"><title>[a,S,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"274,-306 220,-306 220,-270 274,-270 274,-306\"/>\n",
"<text text-anchor=\"middle\" x=\"247\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,S,b]</text>\n",
"</g>\n",
"<!-- [a,S,b]->[a,a,S,b,b] -->\n",
"<g id=\"edge10\" class=\"edge\"><title>[a,S,b]->[a,a,S,b,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M234.948,-269.614C226.035,-256.755 213.754,-239.038 203.723,-224.568\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"206.393,-222.275 197.819,-216.05 200.64,-226.263 206.393,-222.275\"/>\n",
"<text text-anchor=\"middle\" x=\"230.553\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [a,b] -->\n",
"<g id=\"node13\" class=\"node\"><title>[a,b]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"295,-216 241,-216 241,-180 295,-180 295,-216\"/>\n",
"<text text-anchor=\"middle\" x=\"268\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n",
"</g>\n",
"<!-- [a,S,b]->[a,b] -->\n",
"<g id=\"edge12\" class=\"edge\"><title>[a,S,b]->[a,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M251.149,-269.614C254.131,-257.119 258.207,-240.037 261.603,-225.804\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"265.014,-226.59 263.931,-216.05 258.205,-224.965 265.014,-226.59\"/>\n",
"<text text-anchor=\"middle\" x=\"268.553\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [S] -->\n",
"<g id=\"node14\" class=\"node\"><title>[S]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"318,-396 264,-396 264,-360 318,-360 318,-396\"/>\n",
"<text text-anchor=\"middle\" x=\"291\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">[S]</text>\n",
"</g>\n",
"<!-- [S]->[a,S,b] -->\n",
"<g id=\"edge14\" class=\"edge\"><title>[S]->[a,S,b]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M282.307,-359.614C275.999,-346.998 267.353,-329.705 260.195,-315.391\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"263.128,-313.429 255.525,-306.05 256.867,-316.56 263.128,-313.429\"/>\n",
"<text text-anchor=\"middle\" x=\"281.553\" y=\"-328.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"<!-- [] -->\n",
"<g id=\"node17\" class=\"node\"><title>[]</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"346,-306 292,-306 292,-270 346,-270 346,-306\"/>\n",
"<text text-anchor=\"middle\" x=\"319\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n",
"</g>\n",
"<!-- [S]->[] -->\n",
"<g id=\"edge16\" class=\"edge\"><title>[S]->[]</title>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M296.532,-359.614C300.508,-347.119 305.943,-330.037 310.471,-315.804\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"313.878,-316.641 313.575,-306.05 307.208,-314.518 313.878,-316.641\"/>\n",
"<text text-anchor=\"middle\" x=\"316.553\" y=\"-328.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
],
"text/plain": [
"<Dot visualization: expr_as_graph [SFablSF={[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]} & abl=uv#x,z,p,q.((p,q):{([S],[]),([S],[a,S,b])} & u=x^p^z & v=x^q^z)(\"abl\",SF<|abl|>SF)]>"
]
},
"execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":dot expr_as_graph (\"abl\",SF <| abl |> SF)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",
"name": "prob2"
},
"language_info": {
"codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
"mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
"nbformat": 4,
"nbformat_minor": 2
}
%% Cell type:markdown id: tags:
## Grammatiken
Dieses Notebook begleitet Teil 2 der Vorlesung 3.
%% Cell type:markdown id: tags:
Eine __Grammatik__ ist ein Quadrupel
$G = (
\S
igma , N, S, P)$, wobei
*
$
\S
igma$ ein Alphabet (von so genannten __Terminalsymbolen__) ist,
*
$N$ eine endliche Menge (von so genannten __Nichtterminalen__) mit
$
\S
igma
\c
ap N =
\e
mptyset$,
*
$S
\i
n N$ das __Startsymbol__ und
*
$P
\s
ubseteq (N
\c
up
\S
igma)^+
\t
imes (N
\c
up
\S
igma)^{
\a
st}$ die
endliche Menge der __Produktionen__ (Regeln).
Diese mathematische Definition setzen wir im Notebook folgendermaßen um.
Wir verwenden eine B Maschine um eine neue Basismenge an Symbolen (ΣN) einführen zu können.
Hier steht
```seq1(T)```
für die nicht leeren Folgen über T, also $T^+$ in der Notation des Skripts.
%% Cell type:code id: tags:
```
prob
::load
MACHINE Grammatik
SETS ΣN = {a,b,c, S}
CONSTANTS Σ, N, P
PROPERTIES
Σ = {a,b,c} ∧
Σ ∩ N = {} ∧
Σ ∪ N = ΣN ∧
S ∈ N ∧
P ⊆ seq1(ΣN) × seq(ΣN) ∧
// Die Beispiel Grammatik G1 von den Folien
P = { [S] ↦ [],
[S] ↦ [a,S,b]
}
DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE
END
```
%% Output
Loaded machine: Grammatik
%% Cell type:code id: tags:
```
prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
```
prob
[S] ↦ RHS ∈ P
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\mathit{TRUE}$
**Solution:**
* $\mathit{abl} = /*@symbolic*/ \{\mathit{u},\mathit{v}\mid\exists(\mathit{x},\mathit{z},\mathit{p},\mathit{q})\qdot(\mathit{p} \mapsto \mathit{q} \in \{([S]\mapsto []),([S]\mapsto [a,\mathit{S},b])\} \land \mathit{u} = \mathit{x} \expn \mathit{p} \expn \mathit{z} \land \mathit{v} = \mathit{x} \expn \mathit{q} \expn \mathit{z})\}$
* $\mathit{RHS} = []$
TRUE
Solution:
abl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}
RHS = []
%% Cell type:markdown id: tags:
Mit dem relationalen Bild können wir alle Regeln mit der Folge S auf der rechten Seite finden:
%% Cell type:code id: tags:
```
prob
P[{[S]}]
```
%% Output
$\{[],[a,\mathit{S},b]\}$
{[],[a,S,b]}
%% Cell type:markdown id: tags:
Definiere die __unmittelbare Ableitungsrelation__ bzgl. $G$ so
*
$u
\v
dash_{G} v
\L
ongleftrightarrow u = xpz, v = xqz$,
wobei $x,z
\i
n (N
\c
up
\S
igma)^{
\a
st}$ und $p
\r
ightarrow q$ eine Regel in $P$
ist.
Im Notebook können wir dies so umsetzen, können aber leider nicht das Symbol $
\v
dash_G$ verwenden.
Aus $u
\v
dash_{G} v$ wird $u
\m
apsto v
\i
n abl$.
%% Cell type:code id: tags:
```
prob
:let abl {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}/*@symbolic*/ \{\mathit{u},\mathit{v}\mid\exists(\mathit{x},\mathit{z},\mathit{p},\mathit{q})\qdot(\mathit{p} \mapsto \mathit{q} \in \{([S]\mapsto []),([S]\mapsto [a,\mathit{S},b])\} \land \mathit{u} = \mathit{x} ⌒ \mathit{p} ⌒ \mathit{z} \land \mathit{v} = \mathit{x} ⌒ \mathit{q} ⌒ \mathit{z})\}$
/*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ⌒ p ⌒ z ∧ v = x ⌒ q ⌒ z)}
%% Cell type:markdown id: tags:
Da diese Relation unendlich ist wird diese im Notebook symbolisch gehalten. Wir können aber prüfen ob Paare an Folgen in der Relation sind:
%% Cell type:code id: tags:
```
prob
[S] ↦ [a,S,b] ∈ abl
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\mathit{TRUE}$
**Solution:**
* $\mathit{abl} = /*@symbolic*/ \{\mathit{u},\mathit{v}\mid\exists(\mathit{x},\mathit{z},\mathit{p},\mathit{q})\qdot(\mathit{p} \mapsto \mathit{q} \in \{([S]\mapsto []),([S]\mapsto [a,\mathit{S},b])\} \land \mathit{u} = \mathit{x} \expn \mathit{p} \expn \mathit{z} \land \mathit{v} = \mathit{x} \expn \mathit{q} \expn \mathit{z})\}$
TRUE
Solution:
abl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}
%% Cell type:code id: tags:
```
prob
[S] ↦ [a,b] ∈ abl
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
```
prob
[S] ↦ x : abl
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\mathit{TRUE}$
**Solution:**
* $\mathit{x} = []$
* $\mathit{abl} = /*@symbolic*/ \{\mathit{u},\mathit{v}\mid\exists(\mathit{x},\mathit{z},\mathit{p},\mathit{q})\qdot(\mathit{p} \mapsto \mathit{q} \in \{([S]\mapsto []),([S]\mapsto [a,\mathit{S},b])\} \land \mathit{u} = \mathit{x} \expn \mathit{p} \expn \mathit{z} \land \mathit{v} = \mathit{x} \expn \mathit{q} \expn \mathit{z})\}$
TRUE
Solution:
x = []
abl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}
%% Cell type:markdown id: tags:
Mit dem relationalen Abbild können wir die Menge aller Umschreibungen berrechnen:
%% Cell type:code id: tags:
```
prob
abl[ {[S]} ]
```
%% Output
$\{[],[a,\mathit{S},b]\}$
{[],[a,S,b]}
%% Cell type:code id: tags:
```
prob
abl[ {[a,S,b]} ]
```
%% Output
$\{[a,b],[a,\mathit{a},\mathit{S},\mathit{b},b]\}$
{[a,b],[a,a,S,b,b]}
%% Cell type:markdown id: tags:
Durch mehrfache Anwendung bekommen wir die Ergebnisse von immer längeren Ableitungen:
%% Cell type:code id: tags:
```
prob
abl[ abl[ {[S]} ] ]
```
%% Output
$\{[a,b],[a,\mathit{a},\mathit{S},\mathit{b},b]\}$
{[a,b],[a,a,S,b,b]}
%% Cell type:code id: tags:
```
prob
abl[ abl[ abl[ {[S]} ] ] ]
```
%% Output
$\{[a,\mathit{a},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},b]\}$
{[a,a,b,b],[a,a,a,S,b,b,b]}
%% Cell type:markdown id: tags:
Durch $n$-malige Anwendung von $
\v
dash_{G}$ erhalten wir
$
\v
dash_{G}^{n}$. Das heiß t:
*
$u
\v
dash_{G}^{n} v
\L
ongleftrightarrow u = x_0
\v
dash_{G} x_1
\v
dash_{G}
\c
dots
\v
dash_{G} x_n = v$
Im Notebook kann man für die n-malige Anwendung einer binären Relation den Operator
```iterate```
verwenden:
%% Cell type:code id: tags:
```
prob
[S] ↦ [a,b] ∈ iterate(abl,2)
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\newcommand{\expn}{\mathbin{\widehat{\mkern1em}}}\mathit{TRUE}$
**Solution:**
* $\mathit{abl} = /*@symbolic*/ \{\mathit{u},\mathit{v}\mid\exists(\mathit{x},\mathit{z},\mathit{p},\mathit{q})\qdot(\mathit{p} \mapsto \mathit{q} \in \{([S]\mapsto []),([S]\mapsto [a,\mathit{S},b])\} \land \mathit{u} = \mathit{x} \expn \mathit{p} \expn \mathit{z} \land \mathit{v} = \mathit{x} \expn \mathit{q} \expn \mathit{z})\}$
TRUE
Solution:
abl = /*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ^ p ^ z ∧ v = x ^ q ^ z)}
%% Cell type:markdown id: tags:
Die Menge $
\{
w
\m
id S
\v
dash_{G}^{n} w
\}
$ kann direkt mit dem relationalen Bild berechnet werden. Zum Beispiel für n = 0,1,2,3,4:
%% Cell type:code id: tags:
```
prob
iterate(abl,0)[ {[S]} ]
```
%% Output
$\{[S]\}$
{[S]}
%% Cell type:code id: tags:
```
prob
iterate(abl,1)[ {[S]} ]
```
%% Output
$\{[],[a,\mathit{S},b]\}$
{[],[a,S,b]}
%% Cell type:code id: tags:
```
prob
iterate(abl,2)[ {[S]} ]
```
%% Output
$\{[a,b],[a,\mathit{a},\mathit{S},\mathit{b},b]\}$
{[a,b],[a,a,S,b,b]}
%% Cell type:code id: tags:
```
prob
iterate(abl,3)[ {[S]} ]
```
%% Output
$\{[a,\mathit{a},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},b]\}$
{[a,a,b,b],[a,a,a,S,b,b,b]}
%% Cell type:code id: tags:
```
prob
iterate(abl,4)[ {[S]} ]
```
%% Output
$\{[a,\mathit{a},\mathit{a},\mathit{b},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},\mathit{b},b]\}$
{[a,a,a,b,b,b],[a,a,a,a,S,b,b,b,b]}
%% Cell type:markdown id: tags:
Die von der Grammatik $G$ erzeugte Sprache ist
definiert als
$L(G) =
\{
w
\i
n
\S
igma^
*
\m
id S
\v
dash_{G}^{
\a
st} w
\}
.$
Bis zur Länge 4 gibt es folgende abgeleitenen Wörter über $
\S
igma
\c
up N$
(auch Satzformen genannt):
%% Cell type:code id: tags:
```
prob
UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])
```
%% Output
$\{[],[a,b],[S],[a,\mathit{a},\mathit{b},b],[a,\mathit{S},b],[a,\mathit{a},\mathit{a},\mathit{b},\mathit{b},b],[a,\mathit{a},\mathit{S},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},\mathit{b},b]\}$
{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}
%% Cell type:markdown id: tags:
Wenn wir mit $
\S
igma^
*
$ schneiden bekommen wir Wörter der von der Grammatik generierten Sprache:
%% Cell type:code id: tags:
```
prob
UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ]) /\ seq(Σ)
```
%% Output
$\{[],[a,b],[a,\mathit{a},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{b},\mathit{b},b]\}$
{[],[a,b],[a,a,b,b],[a,a,a,b,b,b]}
%% Cell type:code id: tags:
```
prob
::load
MACHINE Grammatik
SETS ΣN = {a,b,c, S}
CONSTANTS Σ, N, P
ABSTRACT_CONSTANTS abl
PROPERTIES
Σ = {a,b,c} ∧
Σ ∩ N = {} ∧
Σ ∪ N = ΣN ∧
S ∈ N ∧
P ⊆ seq1(ΣN) × seq(ΣN) ∧
// Die Beispiel Grammatik G1 von den Folien
P = { [S] ↦ [],
[S] ↦ [a,S,b]
}
∧
abl = {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}
DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE
END
```
%% Output
Loaded machine: Grammatik
%% Cell type:code id: tags:
```
prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags:
Wir können die Ableitungsrelationen für alle Satzformen bis zu einer gegebenen Tiefe auch grafisch darstellen.
%% Cell type:code id: tags:
```
prob
:let SF UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])
```
%% Output
$\{[],[a,b],[S],[a,\mathit{a},\mathit{b},b],[a,\mathit{S},b],[a,\mathit{a},\mathit{a},\mathit{b},\mathit{b},b],[a,\mathit{a},\mathit{S},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},b],[a,\mathit{a},\mathit{a},\mathit{a},\mathit{S},\mathit{b},\mathit{b},\mathit{b},b]\}$
{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}
%% Cell type:code id: tags:
```
prob
:pref DOT_DECOMPOSE_NODES=FALSE
```
%% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE
%% Cell type:code id: tags:
```
prob
:dot expr_as_graph ("abl",SF <| abl |> SF)
```
%% Output
<Dot visualization: expr_as_graph [SFablSF={[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]} & abl=uv#x,z,p,q.((p,q):{([S],[]),([S],[a,S,b])} & u=x^p^z & v=x^q^z)("abl",SF<|abl|>SF)]>
%% Cell type:code id: tags:
```
prob
```
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment