\documentclass[11pt]{article}

\newcommand{\wshop}{
    7
}
\newcommand{\subtitle}{
    (Un)Decidability
}

% Page Setup
\usepackage{geometry}
\geometry{
    a4paper,
    margin={2.5cm}
}

% Basic Packages
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{mathpartir}
\usepackage{enumitem}
\usepackage{mathabx}

% Font
\usepackage{charter}

% Bibliography and index
\usepackage[backend=biber, style=numeric]{biblatex}
\addbibresource{refs.bib}
\usepackage{makeidx}
\makeindex

% Colors and Graphics
\usepackage[dvipsnames, x11names]{xcolor}
\usepackage{tikz}
\usetikzlibrary{
    cd,
    fit,
    calc,
    positioning,
    arrows,
    automata,
    shapes
}
\tikzset{
    baseline = (current bounding box.center),
    every state/.append style = {
        rectangle,
        rounded corners=5pt,
		inner sep = 3pt,
		minimum size = 18pt,
		initial text = {},
        fill=Azure1
	},
	every edge/.append style = {
		->,
		>=stealth,
		bend angle=10,
		thick
	}
}
\usepackage{musicography}
\usepackage{graphicx}
\usepackage{svg}
\graphicspath{../imgs/}

% Hyperlinks
\usepackage{hyperref}
\hypersetup{
    colorlinks,
    linkcolor   = black,
    filecolor   = RubineRed,
    urlcolor    = RubineRed,
    citecolor   = RubineRed,
    pdftitle    = {Notes on Behavioural PDEs}
}
\usepackage[capitalize]{cleveref}

% Environments
\theoremstyle{theorem} % In Italics
\newtheorem{theorem}        {{\color{Purple}Theorem}}
\newtheorem{lemma}          [theorem]   {{\color{Magenta}Lemma}}
\newtheorem{proposition}    [theorem]   {Proposition}
\newtheorem{corollary}      [theorem]   {Corollary}
\newtheorem{question}                   {{\color{red}Question}}

\theoremstyle{definition} % Not in italics
\newtheorem{definition}     [theorem]   {{\color{NavyBlue}Definition}}
\newtheorem{example}        [theorem]   {{\color{ForestGreen}Example}}
\newtheorem{problem}                    {{\color{BurntOrange}Problem}}

\theoremstyle{remark} % Subdued label
\newtheorem{remark}[theorem]        {{\color{Gray}Remark}}

% (1), (2), ...
\renewcommand\labelenumi{(\theenumi)}

% Go nuts with line breaks 
\allowdisplaybreaks

%%%%%%%%%%
% MACROS %
%%%%%%%%%%

\newcommand{\op}{\mathrm{op}}               % Opposite
\newcommand{\inv}{{-1}}                     % Inverse
\newcommand{\id}{\mathsf{id}}               % Identity f(x) = x
\newcommand{\Det}{\mathrm{Det}}             % determinize
\newcommand{\Lang}{\mathcal{L}}             % Language

\newcommand{\incl}{\mathsf{incl}}           % Inclusion
\newcommand{\proj}{\mathsf{proj}}           % Projection

% Numbers and Standard notation
\newcommand{\NN}{\mathbb{N}}                % 0, 1, 2, 3, 4, ...
\newcommand{\ZZ}{\mathbb{Z}}                % ..., -2, -1, 0, 1, 2, ...
\newcommand{\QQ}{\mathbb{Q}}                % n/m for n and m in \NN and m > 0
\newcommand{\RR}{\mathbb{R}}                % real numbers
\newcommand{\pRR}{\mathbb{R}_{+}}           % positive real numbers

\newcommand{\dom}{\mathrm{dom}}             % Domain
\newcommand{\cod}{\mathrm{cod}}             % Codomain

\newcommand{\Grph}{\operatorname{Grph}}     % Graph of a function

% Transitions
\newcommand{\tr}[1]{
    \mathrel{
        \raisebox{-1pt}{
            \(\xrightarrow{#1}\)
        }
    }
}
\newcommand{\bisim}{\mathrel{\raisebox{1pt}{\(\underline{\leftrightarrow}\)}}}

% Text
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\codeblock}[1]{
    \begin{center}
        \parbox{0.8\textwidth}{
            \ttfamily
            #1
        }
    \end{center}
}

% Boolean statements
\newcommand{\OR}{~\mathrm{or}~}
\newcommand{\AND}{~\mathrm{and}~}
\newcommand{\NOT}{\mathrm{not}~}
\newcommand{\IMPLIES}{~\mathrm{implies}~}
\newcommand{\FORALL}{\mathrm{for\ all}~}
\newcommand{\EXISTS}{\mathrm{there\ exists}~}
\newcommand{\SUCHTHAT}{~\mathrm{such\ that}~}



% Title
\title{CSCI 341 Workshop \wshop}
\author{\subtitle}
% \date{
%     \today
% }

\pagestyle{empty}

\begin{document}


\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% START OF WORK SHOP.                                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{problem}
    \label{firstprob}
    Show that the language \(L_{TM} = \{\lfloor \mathcal T \rfloor \mid \mathcal T \text{ is a Turing machine}\}\) is decidable using the following theorem.
\end{problem}

\begin{theorem}
    [CFL in Dec]
    Every context-free language is decidable.
    That is, \(\mathsf{CFL} \subseteq \mathsf{Dec}\).
\end{theorem}

\vfill \emph{\footnotesize Hint: cook up a grammar for the BuckLang programming language.}
\pagebreak

\begin{problem}
    Prove that the following language
    \[
        L_{11} = \{\lfloor \mathcal T \rfloor \mathtt{*}x \mid \text{\(x\) halts on input \(\mathtt{11}\) in the Turing machine \(\mathcal T\)}\}
    \]
    is undecidable by showing that \(L_\varepsilon\) reduces to \(L_{11}\).
\end{problem}


\vfill\emph{\footnotesize Hint: see next page for a general methodology if you get stuck.}
\pagebreak

\subsection*{Technique for Problem 2}

\begin{enumerate}
    \item Assume for a contradition that there is a Turing machine \(\mathcal E\) with a state \(x_{11}\) that decides \(L_{11}\).\\
    
    \framebox{\parbox{0.9\textwidth}{We are going to build a decision procedure for \(L_\varepsilon\) using \(x_{11}\).
    That is, given a Turing machine \(\mathcal T\) with a state \(x\), we are going to use \(x_{11}\) to decide if \(x\) halts on input \(\varepsilon\).}}\\

    \item Show that the following Turing program halts on input \(\varepsilon\) if and only if \(x\) (in \(\mathcal T\)) halts on input \(11\):
    \codeblock{
        state start \\
        if \_ : write 1.write 1.move right.goto \(x\)\\
        if 0 : write 1.write 1.move right.goto \(x\)\\
        if 1 : write 1.write 1.move right.goto \(x\)\\
        \(\lfloor \mathcal T\rfloor\) \hfill({\normalfont include all of the code that programs \(\mathcal T\)})        
    }

    \item Let \(\mathcal W\) at state \(y\) be a Turing program that takes any string of the form \(\lfloor \mathcal T\rfloor \mathtt{*} x\) as input and outputs the string immediately above this followed by \(\mathtt{*start}\).
    
    \item Now, what is \(\mathcal E_{x_{11}}(\mathcal W_{y}(\lfloor \mathcal T \rfloor \mathtt{*} x))\) if 
    \begin{enumerate}[label=\Alph*.]
        \item \(x\) halts on input \(\varepsilon\)? 
        \item \(x\) does not halt on input \(\varepsilon\)? 
    \end{enumerate}
\end{enumerate}

\pagebreak

The definitions and theorem below, taken together, form a swift technique for telling that a given language is undecidable.

\begin{definition}
    [Non-trivial and Extensional]
    Let \(\mathbf{TM}\) be the set of all pairs \((\mathcal T, x)\) where \(\mathcal T\) is a Turing machine and \(x\) is a state of \(\mathcal T\).
    Let \(P \subseteq \mathbf{TM}\) (called a \emph{property of Turing programs}).
    \begin{enumerate}
        \item
            \(P\) is \emph{nontrivial} if \(P \neq \{\}\) and \(P \neq \mathbf{TM}\).
            I.e., there is at least one Turing program that satisfies the property and at least one Turing program that does not.
        
        \item
            \(P\) is \emph{extensional} if the following holds: 
            for any \((\mathcal T, x) \in P\) and any \((\mathcal S, y) \in \mathbf{TM}\), if \(\mathcal T_x = \mathcal S_y\), then \((\mathcal S, y) \in P\) also.
            I.e., if \(\mathcal T\) at \(x\) implements the same string transformer as \(\mathcal S\) at \(y\), then either \((\mathcal T, x)\) and \((\mathcal S, y)\) both satisfy the property or neighter do.1
    \end{enumerate}
\end{definition}

\begin{theorem}[Rice's]
    Let \(P \subseteq \mathbf{TM}\) be nontrivial and extensional. 
    Then the language 
    \[
        L_P = \{\lfloor \mathcal T \rfloor \mathtt{* x} \mid (\mathcal T, x) \in P\}
    \]
    is undecidable.
\end{theorem}

\begin{problem}
    Use Rice's Theorem to prove that all of the following languages are undecidable.
    \begin{enumerate}
        \item \(L_1 = \{\lfloor \mathcal T \rfloor \mathtt{*}x \mid \text{\(x\) accepts the word \(01101\)}\}\)
        \item \(L_2 = \{\lfloor \mathcal T \rfloor \mathtt{*}x \mid \text{\(x\) does not accept the word \(01101\)}\}\)
        \item \(L_3 = \{\lfloor \mathcal T \rfloor \mathtt{*}x \mid \text{\(x\) recognizes every even-length word}\}\)
        \item \(L_4 = \{\lfloor \mathcal T \rfloor \mathtt{*}x \mid \text{\(\mathcal T_x = \mathcal U_c\) where \(\mathcal U\) at \(c\) is a universal Turing program}\}\)
        \item \(L_5 = \{\lfloor \mathcal T \rfloor \mathtt{*}x\mathtt{*}w \mid \text{\(\mathcal T_x(w) = \varepsilon\)}\}\)
    \end{enumerate}
    Why can't Rice's theorem be used to show that the language in Problem 1 is undecidable?
\end{problem}

\pagebreak
\ 
\vfill\noindent\emph{\footnotesize Hint: in each case, the defining property of the language is a property of Turing programs. Explain why the property is nontrivial and extensional.}

\end{document}