From c977cdf955edac2de69c2268390099b3a059fa8c Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 2 Jun 2020 15:57:38 +0200
Subject: [PATCH] add notebook for PDAs
---
info4/kapitel-3/PDA-Kellerautomaten.ipynb | 706 ++++++++++++++++++++++
1 file changed, 706 insertions(+)
create mode 100644 info4/kapitel-3/PDA-Kellerautomaten.ipynb
diff --git a/info4/kapitel-3/PDA-Kellerautomaten.ipynb b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
new file mode 100644
index 0000000..0765b60
--- /dev/null
+++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
@@ -0,0 +1,706 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# PDA (Push Down Automata - Kellerautomaten)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "Ein __(nichtdeterministischer) Kellerautomat__ \n",
+ "(kurz PDA für __push-down automaton__) ist ein $6$-Tupel \n",
+ " $M = (\\Sigma, \\Gamma, Z, \\delta , z_0, \\#)$, wobei\n",
+ "* $\\Sigma$ das Eingabe-Alphabet ist, \n",
+ "* $\\Gamma$ das Kelleralphabet, \n",
+ "* $Z$ eine endliche Menge von Zuständen,\n",
+ "* $\\delta : Z \\times (\\Sigma \\cup \\{\\lambda\\}) \\times \\Gamma\n",
+ " \\rightarrow \\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ die\n",
+ " Überführungsfunktion,\n",
+ "* $z_0 \\in Z$ der Startzustand,\n",
+ "* $\\# \\in \\Gamma$ das Bottom-Symbol im Keller.\n",
+ "\n",
+ "\n",
+ "Anmerkung: $\\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ ist die Menge aller\n",
+ " __endlichen__ Teilmengen von $Z \\times \\Gamma^{\\ast}$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PDA"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PDA\n",
+ "/* B Modell eines PDA */\n",
+ "SETS\n",
+ " Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand\n",
+ " SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n",
+ "DEFINITIONS\n",
+ " Σ == {a,b}; // das Eingabe-Alphabet\n",
+ " Γ == {A,BOT}; // das Kelleralphabet\n",
+ " \n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",
+ " ANIMATION_FUNCTION == {2}*α \\/ {3}*(γ);\n",
+ " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n",
+ " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",
+ " SET_PREF_PRETTY_PRINT_SEQUENCES == TRUE\n",
+ "CONSTANTS δ\n",
+ "PROPERTIES\n",
+ " /* A PDA für {a^mb^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",
+ " δ = { (z0,a,BOT) ↦ (z0,[A,BOT]),\n",
+ " (z0,a,A) ↦ (z0,[A,A]),\n",
+ " (z0,b,A) ↦ (z1,[]),\n",
+ " (z1,lambda,BOT) ↦ (z1,[]),\n",
+ " (z1,b,A) ↦ (z1,[]) }\n",
+ "VARIABLES \n",
+ " z, α, γ // Konfiguration in dem sich der PDA befindet\n",
+ "INVARIANT\n",
+ " z ∈ Z ∧ // der aktuelle Zustand\n",
+ " α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts\n",
+ " γ ∈ seq(Γ) // aktuelle Kellerinhalt\n",
+ "INITIALISATION\n",
+ " z := z0 ||\n",
+ " γ := [BOT] || // Initialisierung des Stapels\n",
+ " α := [a,a,b,b] // das Eingabewort\n",
+ "OPERATIONS\n",
+ " // die Operationen Schritt und LambdaSchritt modellieren\n",
+ " // Schritte in der Ableitungsrelation\n",
+ " Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧\n",
+ " z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN\n",
+ " z := z‘ || // in den neuen Zustand wechseln\n",
+ " α := tail(α) || // das erste Symbol auf der Eingabe löschen\n",
+ " γ := s^tail(γ) // s auf den Stapel packen\n",
+ " END;\n",
+ " LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧\n",
+ " z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN\n",
+ " z := z‘ || // in den neuen Zustand wechseln\n",
+ " γ := s^tail(γ) // s auf den Stapel packen\n",
+ " END;\n",
+ " Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN \n",
+ " /* Wir akzeptieren wenn Eingabe und Stapel leer sind */\n",
+ " skip END\n",
+ "END\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 46,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 47,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,{(1|->A),(2|->BOT)})"
+ ]
+ },
+ "execution_count": 48,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 49,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,{(1|->A),(2|->BOT)})"
+ ]
+ },
+ "execution_count": 49,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 50,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 50,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 51,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(\\mathit{z0}\\mapsto\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{b}),(3\\mapsto \\mathit{b})\\}\\mapsto\\{(1\\mapsto \\mathit{A}),(2\\mapsto \\mathit{BOT})\\})$"
+ ],
+ "text/plain": [
+ "(z0↦{(1↦a),(2↦b),(3↦b)}↦{(1↦A),(2↦BOT)})"
+ ]
+ },
+ "execution_count": 51,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(z,α,γ)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 52,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,{(1|->A),(2|->A)})"
+ ]
+ },
+ "execution_count": 52,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 53,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,{(1|->A),(2|->A)})"
+ ]
+ },
+ "execution_count": 53,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 54,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 54,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z1,{})"
+ ]
+ },
+ "execution_count": 55,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 56,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,{})"
+ ]
+ },
+ "execution_count": 56,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 57,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 57,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 58,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z1,{})"
+ ]
+ },
+ "execution_count": 58,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 59,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,{})"
+ ]
+ },
+ "execution_count": 59,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 60,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 60,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 61,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(z1,{})"
+ ]
+ },
+ "execution_count": 61,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 62,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(z1,{})"
+ ]
+ },
+ "execution_count": 62,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 63,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 63,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 64,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Akzeptieren()"
+ ]
+ },
+ "execution_count": 64,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 65,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Akzeptieren()"
+ ]
+ },
+ "execution_count": 65,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Akzeptieren"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Das Eingabewort ``aabb`` wurde akzeptiert."
+ ]
+ },
+ {
+ "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
+}
--
GitLab