diff --git a/Advanced/Mock a Mockingbird/main.tex b/Advanced/Mock a Mockingbird/main.tex index 5c0c358..023bf25 100755 --- a/Advanced/Mock a Mockingbird/main.tex +++ b/Advanced/Mock a Mockingbird/main.tex @@ -7,6 +7,9 @@ \usepackage{mathtools} % for \coloneqq +%\usepackage{lua-visual-debug} + +\usepackage{censor} \usepackage{alltt} @@ -37,10 +40,24 @@ } % Logic block comment -\newcommand{\cmnt}[1]{ - \textcolor{gray}{\# #1} +\newcommand{\cmnt}[1]{\textcolor{gray}{\# #1}} + +\newcounter{allttLineCounter} +\setcounter{allttLineCounter}{0} + +\newcommand{\linenoref}[1]{\colorbox{gray!30!white}{#1}} +\newcommand{\lineno}{ + \stepcounter{allttLineCounter}% + \linenoref{\ifnum\value{allttLineCounter}<10 0\fi\arabic{allttLineCounter}}% } +% Redefine alltt so it automatically +% resets allttLineCounter +\let\oldalltt\alltt +\renewenvironment{alltt} + {\setcounter{allttLineCounter}{0}\begin{oldalltt}} + {\end{oldalltt}} + \newcommand{\thus}{\(\Rightarrow\)} \newcommand{\qed}{\(\blacksquare\)} @@ -59,5 +76,5 @@ \input{parts/00 intro} \input{parts/01 tmam} - + \input{parts/02 kestrel} \end{document} \ No newline at end of file diff --git a/Advanced/Mock a Mockingbird/parts/00 intro.tex b/Advanced/Mock a Mockingbird/parts/00 intro.tex index eb070f3..9eef4df 100644 --- a/Advanced/Mock a Mockingbird/parts/00 intro.tex +++ b/Advanced/Mock a Mockingbird/parts/00 intro.tex @@ -38,7 +38,9 @@ We say a bird $C$ \textit{composes} $A$ with $B$ if for any bird $x$, $$ Cx = A(Bx) $$ -In other words, this means that $C$'s response to $x$ is the same as $A$'s response to $B$'s response to $x$. +In other words, this means that $C$'s response to $x$ is the same as $A$'s response to $B$'s response to $x$. \\ +Note that $C$ is exactly the kind of bird $L_1$ guarantees. + \vfill \pagebreak \ No newline at end of file diff --git a/Advanced/Mock a Mockingbird/parts/01 tmam.tex b/Advanced/Mock a Mockingbird/parts/01 tmam.tex index e8a37e2..c23d6fa 100644 --- a/Advanced/Mock a Mockingbird/parts/01 tmam.tex +++ b/Advanced/Mock a Mockingbird/parts/01 tmam.tex @@ -1,11 +1,11 @@ \section{To Mock a Mockingbird} \problem{} -The bear, a lifelong resident of the forest, tells you that any bird $A$ is fond of at least one other bird. \\ +Mark tells you that any bird $A$ is fond of at least one other bird. \\ Complete his proof. \begin{alltt} let A \cmnt{Let A be any any bird.} - let Cx := A(Mx) \cmnt{Define C as the composition of A and M} + let Cx = A(Mx) \cmnt{Define C as the composition of A and M} \cmnt{The rest is up to you.} CC = ?? @@ -20,17 +20,16 @@ Complete his proof. \begin{solution} \begin{alltt} - let A \cmnt{Let A be any any bird.} - let Cx := A(Mx) \cmnt{Define C as the composition of A and M} - CC = A(MC) - = A(CC) \qed{} + \lineno{} let A \cmnt{Let A be any any bird.} + \lineno{} let Cx = A(Mx) \cmnt{Define C as the composition of A and M} + \lineno{} CC = A(MC) + \lineno{} = A(CC) \qed{} \end{alltt} \end{solution} \vfill \problem{} -We say a bird $A$ is \textit{egocentric} if it is fond if itself. - +We say a bird $A$ is \textit{egocentric} if it is fond if itself. \\ Show that the laws of the forest guarantee that at least one bird is egocentric. @@ -42,12 +41,12 @@ Show that the laws of the forest guarantee that at least one bird is egocentric. \begin{solution} \begin{alltt} - \cmnt{We know M is fond of at least one bird.} - let E so that ME = E - - ME = E \cmnt{By definition of fondness} - ME = EE \cmnt{By definition of M} - \thus{} EE = E \qed{} + \lineno{} \cmnt{We know M is fond of at least one bird.} + \lineno{} let E so that ME = E + \lineno{} + \lineno{} ME = E \cmnt{By definition of fondness} + \lineno{} ME = EE \cmnt{By definition of M} + \lineno{} \thus{} EE = E \qed{} \end{alltt} \end{solution} @@ -57,7 +56,7 @@ Show that the laws of the forest guarantee that at least one bird is egocentric. \problem{} We say a bird $A$ is \textit{agreeable} if for all birds $B$, there is at least one bird $x$ on which $A$ and $B$ agree. \\ -This means that $Ax = Bx$. +In other words, $A$ is agreeable if $Ax = Bx$ for some $x$ for all $B$. \begin{helpbox} \texttt{Def:} $Mx := xx$ @@ -73,15 +72,14 @@ This means that $Ax = Bx$. \problem{} Take two birds $A$ and $B$. Let $C$ be their composition. \\ -Show that $A$ must be agreeable if $C$ is agreeable. \\ -The bear has again given you a hint. +Show that $A$ must be agreeable if $C$ is agreeable. \begin{alltt} \cmnt{Given information} let A, B - let Cx := A(Bx) + let Cx = A(Bx) let D \cmnt{Arbitrary bird} - let Ex := D(Bx) \cmnt{Define E as the composition of D and B} + let Ex = D(Bx) \cmnt{Define E as the composition of D and B} Cy = ?? \end{alltt} @@ -93,15 +91,16 @@ The bear has again given you a hint. \begin{solution} \begin{alltt} - \cmnt{Given information} - let A, B - let Cx := A(Bx) - - let D \cmnt{Arbitrary bird} - let Ex := D(Bx) \cmnt{Define E as the composition of D and B} - Cy = Ey \cmnt{For some y, because C is agreeable} - \thus{} A(By) = Ey - \thus{} A(By) = D(By) \qed{} + \lineno{} \cmnt{Given information} + \lineno{} let A, B + \lineno{} let Cx = A(Bx) + \lineno{} + \lineno{} let D \cmnt{Arbitrary bird} + \lineno{} let Ex = D(Bx) \cmnt{Define E as the composition of D and B} + \lineno{} let y so that Cy = Ey \cmnt{Such a y must exist because C is agreeable} + \lineno{} + \lineno{} A(By) = Ey + \lineno{} = D(By) \qed{} \end{alltt} \end{solution} @@ -109,18 +108,18 @@ The bear has again given you a hint. \pagebreak \problem{} -Given three arbitrary birds $A$, $B$, and $C$, show that there exists a bird $D$ defined by $Dx = A(B(Cx))$ +Given three arbitrary birds $A$, $B$, and $C$, show that there exists a bird $D$ satisfying $Dx = A(B(Cx))$ \begin{solution} \begin{alltt} - let A, B, C - - \cmnt{Invoke the Law of Composition:} - let Q := BC - let D := AQ - - D = AQ - = A(BC) \qed{} + \lineno{} let A, B, C + \lineno{} + \lineno{} \cmnt{Invoke the Law of Composition:} + \lineno{} let Q = BC + \lineno{} let D = AQ + \lineno{} + \lineno{} D = AQ + \lineno{} = A(BC) \qed{} \end{alltt} \end{solution} @@ -133,7 +132,7 @@ Note that $x$ and $y$ may be the same bird. \\ Show that any two birds in this forest are compatible. \\ \begin{alltt} let A, B - let Cx := A(Bx) + let Cx = A(Bx) \end{alltt} \begin{helpbox} @@ -143,16 +142,16 @@ Show that any two birds in this forest are compatible. \\ \begin{solution} \begin{alltt} - let A, B - - let Cx := A(Bx) \cmnt{Composition} - let y := Cy \cmnt{Let C be fond of y} - - Cy = y - \thus{} A(By) = y - - let x := By \cmnt{Rename By to x} - Ax = y \qed{} + \lineno{} let A, B + \lineno{} + \lineno{} let Cx = A(Bx) \cmnt{Composition} + \lineno{} let y = Cy \cmnt{Let C be fond of y} + \lineno{} + \lineno{} Cy = y + \lineno{} = A(By) + \lineno{} + \lineno{} let x = By \cmnt{Rename By to x} + \lineno{} Ax = y \qed{} \end{alltt} \end{solution} @@ -163,13 +162,13 @@ Show that any bird that is fond of at least one bird is compatible with itself. \begin{solution} \begin{alltt} - let A - let x so that Ax = x - Ax = x \qed{} + \lineno{} let A + \lineno{} let x so that Ax = x \cmnt{A is fond of at least one other bird} + \lineno{} Ax = x \qed{} \end{alltt} + That's it. \end{solution} - \vfill \pagebreak \ No newline at end of file diff --git a/Advanced/Mock a Mockingbird/parts/02 kestrel.tex b/Advanced/Mock a Mockingbird/parts/02 kestrel.tex new file mode 100644 index 0000000..66018eb --- /dev/null +++ b/Advanced/Mock a Mockingbird/parts/02 kestrel.tex @@ -0,0 +1,137 @@ +\section{The Curious Kestrel} + +\definition{} +Recall that a bird is \textit{egocenteric} if it is fond of itself. \\ +A bird is \textit{hopelessly egocentric} if $Bx = B$ for all birds $x$. + +\definition{} +More generally, we say that a bird $A$ is \textit{fixated} on a bird $B$ if $Ax = B$ for all $x$. \\ +Convince yourself that a hopelessly egocentric bird is fixated on itself. + + + +\problem{} +Say $A$ is fixated on $B$. Is $A$ fond of $B$? + +\begin{solution} + Yes! See the following proof. + \begin{alltt} + \lineno{} let B + \lineno{} let B + \lineno{} let A so that Ax = B + \lineno{} \thus{} AB = B \qed{} + \end{alltt} +\end{solution} +\vfill + + + +\definition{} +The \textit{Kestrel} $K$ is defined by the following relationship: +$$ + (Kx)y = x +$$ +In other words, this means that for every bird $x$, the bird $Kx$ is fixated on $x$. + +\problem{} +Show that an egocenteric Kestrel is hopelessly egocentric + +\begin{solution} + \begin{alltt} + \lineno{} KK = K + \lineno{} \thus{} (KK)y = K + \lineno{} \thus{} Ky = K \qed{} + \end{alltt} +\end{solution} + +\vfill +\pagebreak + + +\problem{} +Assume the forest contains a Kestrel. \\ +Given $L_1$ and $L_2$, show that at least one bird is hopelessly egocentric. + +\begin{helpbox}[0.75] + \texttt{Def:} $K$ is defined by $(Kx)y = x$ \\ + \texttt{Def:} $A$ is fond of $B$ if $AB = B$ \\ + \texttt{???:} You'll need one more result from the previous section. Good luck! +\end{helpbox} + +\begin{solution} + The final piece is a lemma we proved earler: \\ + Any bird is fond of at least one bird + + \begin{alltt} + \lineno{} let A so that KA = A \cmnt{Any bird is fond of at least one bird} + \lineno{} (KA)y = y \cmnt{By definition of the kestrel} + \lineno{} \thus{} Ay = A \qed{} \cmnt{By 01} + \end{alltt} +\end{solution} + +\vfill + +\problem{Kestrel Left-Cancellation} +In general, $Ax = Ay$ does not imply $x = y$. However, this is true if $A$ is $K$. \\ +Show that $Kx = Ky \implies x = y$. + +\begin{alltt} + \cmnt{This is a hint.} + let x, y so that Kx = Ky +\end{alltt} + +\begin{solution} + \begin{alltt} + \lineno{} let x, y so that Kx = Ky + \lineno{} let z + \lineno{} + \lineno{} (Kx)z = (Ky)z \cmnt{By 01} + \lineno{} + \lineno{} \cmnt{By the definition of K} + \lineno{} (Kx)z = x + \lineno{} (Ky)z = y + \lineno{} + \lineno{} \thus{} x = (Kx)z = (Ky)z = y \qed{} + \end{alltt} +\end{solution} + +\vfill +\pagebreak + +\problem{} +Show that if $K$ is fond of $Kx$, $K$ is fond of $x$. + +\begin{solution} + \begin{alltt} + \lineno{} let x so that K(Kx) = Kx + \lineno{} (K(Kx))y = (Kx)y + \lineno{} = Kx \cmnt{By definition of K} + \lineno{} x = Kx \cmnt{By 03 and definition of K} + \end{alltt} +\end{solution} + +\vfill + +\problem{} +An egocentric Kestrel must be extremely lonely. Why is this? + +\begin{solution} + If a Kestrel is egocenteric, it must be the only bird in the forest: + + \begin{alltt} + \lineno{} \cmnt{Given} + \lineno{} Kx = K for some x + \lineno{} \cmnt{We have shown that an egocentric kestrel is hopelessly egocentric} + \lineno{} Kx = K for all x + \lineno{} + \lineno{} let x, y + \lineno{} Kx = K + \lineno{} Ky = K + \lineno{} Kx = Ky + \lineno{} x = y for all x, y \cmnt{By \ref{leftcancel}} + \lineno{} x = y = K \qed{} \cmnt{By 10, and since K exists} + \end{alltt} +\end{solution} + +\vfill +\pagebreak \ No newline at end of file