1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/tex/theory1_ex8.tex Wed Jul 13 01:26:19 2011 +0200
1.3 @@ -0,0 +1,53 @@
1.4 +\documentclass[a4paper, 10pt, pagesize, smallheadings]{article}
1.5 +\usepackage{graphicx}
1.6 +%\usepackage[latin1]{inputenc}
1.7 +\usepackage{amsmath, amsthm, amssymb}
1.8 +\usepackage{typearea}
1.9 +\usepackage{algorithm}
1.10 +\usepackage{algorithmic}
1.11 +\usepackage{fullpage}
1.12 +\usepackage{mathtools}
1.13 +\usepackage[all]{xy}
1.14 +\title{Theory I, Sheet 8 Solution}
1.15 +\author{Eugen Sawin}
1.16 +\renewcommand{\familydefault}{\sfdefault}
1.17 +\newcommand{\Pos}{\mathcal{P}os}
1.18 +\include{pythonlisting}
1.19 +
1.20 +\pagestyle{empty}
1.21 +\begin{document}
1.22 +\maketitle
1.23 +
1.24 +\section*{Exercise 8.1}
1.25 +Let $s, t \in T(\Sigma, X)$ be terms over $X$ and $p, q$ be strings over the natural numbers. We provide proofs by induction.
1.26 +\subsection*{1. $pq \in \Pos(s) \implies p \in \Pos(s)$ }
1.27 +$(IH): pq \in \Pos(s) \implies p \in \Pos(s)$\\\\
1.28 +\emph{Base case:}\\
1.29 +From $s \in X$ or $s \in \Sigma^{(0)}$ follows $\Pos(s) = \{\epsilon\}$.\\
1.30 +Trivially it follows that $pq \in \Pos(s) \iff pq = \epsilon$ and $pq \in \Pos(s) \implies p \in \Pos(s)$ with $pq \notin \Pos(s) \lor pq = p = \epsilon$. \\
1.31 +
1.32 +\noindent \emph{Inductive case:}\\
1.33 +Let $s = f(t_1, ...,t_n) \in T(\Sigma, X)$ it follows $\Pos(s) = \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\}$.\\
1.34 +\begin{align*}
1.35 +pq \in \Pos(s) &\implies p \in \Pos(s)\\
1.36 +\iff pq \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\} &\implies p \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\}\\
1.37 +\end{align*}
1.38 +
1.39 +\section*{Exercise 8.2}
1.40 +\subsection*{1. $t = \neg (x \land (\top \lor y)), \sigma = \{x \mapsto \bot, y \mapsto \top \land x\}, \tau = \{z \mapsto \top, x \mapsto \top\}$}
1.41 +\begin{align*}
1.42 +\sigma(t) &= \neg (\bot \land (\top \lor ( \top \land x)))\\
1.43 +\tau \sigma(t) &= \tau(\neg (\bot \land (\top \lor ( \top \land x)))) = \neg (\bot \land (\top \lor (\top \land \top)))\\
1.44 +\end{align*}
1.45 +
1.46 +\subsection*{2. $t = \neg(\top \land (\bot \lor y)), s = \neg(x \land (\bot \lor (x \land \bot)))$}
1.47 +\[\sigma(t) = \sigma(s) \text{ with } \sigma = \{x \mapsto \top, y \mapsto \top \land \bot \} \]
1.48 +
1.49 +\subsection*{3.}
1.50 +Substitution composition is \emph{not} commutative, we give a counterexample.
1.51 +Let $t = x$, $\sigma = \{x \mapsto \bot\}$ and $\tau = \{x \mapsto \top\}$, it follows:
1.52 +\[\tau\sigma(t) = \bot\]
1.53 +\[\sigma\tau(t) = \top\]
1.54 +We see that $\tau\sigma(t) \neq \sigma\tau(t)$.
1.55 +
1.56 +\end{document}