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}