\documentclass[a4paper]{scrartcl}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{cite}
\usepackage{url}
\usepackage{eulervm}
\usepackage{version}
\usepackage{mathpartir}
\usepackage{alltt}
\usepackage{tcolorbox}

\title{COMP3161/9164 24T3 Assignment 0\\
       Latex Snippets}

% \date{}

\begin{document}

\maketitle

\section{Purpose}
This document quotes the \LaTeX{} source of some of the assignment spec
document, both as a guide and example. You can use this to use the same fonts
and styles for math terms in your answers as used in the questions, if you
like.

Note that there will be no marks won or lost for purely aesthetic concerns such
as using the same fonts as the spec document.

\subsection*{Part A}

The language of boolean expressions $\mathcal{P}$ contains terms such as:
$$ \{ \mathtt{True}, \mathtt{False}, \neg \mathtt{True}, \neg \mathtt{False}, \mathtt{True} \leftrightarrow \mathtt{False},  \neg(\mathtt{True} \leftrightarrow \mathtt{False}), \dots \} $$


The \emph{abstract syntax} of $\mathcal{B}$ contains:
          $$ \mathcal{B} ::= \mathsf{Not}\ \mathcal{B}\ |\ \mathsf{Iff}\ \mathcal{B}\ \mathcal{B}\ |\ \mathsf{True}\ |\ \mathsf{False} $$

The big-step semantics of $\mathcal{B}$ is defined by:
          \begin{gather*}
             \inferrule{ x \Downarrow \mathsf{True} }{\mathsf{Not}\ x \Downarrow \mathsf{False}}(\textsc{N}_1)\quad
             \inferrule{ x \Downarrow \mathsf{False } }{\mathsf{Not}\ x \Downarrow \mathsf{True}}(\textsc{N}_2)\quad
             \inferrule{ \quad }{ \mathsf{True} \Downarrow \mathsf{True} }(\textsc{N}_3)\quad
             \inferrule{ \quad }{ \mathsf{False} \Downarrow \mathsf{False} }(\textsc{N}_4) \\
             \inferrule{ x \Downarrow \mathsf{False} \quad \mathsf{Not}\ y \Downarrow v}{\mathsf{Iff}\ x\ y \Downarrow v}(\textsc{N}_5)\quad
             \inferrule{ x \Downarrow \mathsf{True} \quad y \Downarrow v}{\mathsf{Iff}\ x\ y \Downarrow v}(\textsc{N}_6)
          \end{gather*}

There is a question involving $v^{-1}$, understood to be defined by the following equations:
          \[
          \begin{array}{lcl}
            \mathsf{True}^{-1} = \mathsf{False} \\
            \mathsf{False}^{-1} = \mathsf{True}
          \end{array}
          \]

\subsection*{Stacking Natural Deduction}

Here is, as an example, one of the derivations of
$1 \times 2 \times 3\ \mathbf{PExp}$ from Week 2's slides:

        $$
            \inferrule{\inferrule{\inferrule{1 \in \mathbb{Z}}{1\ \mathbf{Atom}}}{1\ \mathbf{PExp}}
                    \quad \inferrule{\inferrule{\inferrule{2 \in \mathbb{Z}}{2\ \mathbf{Atom}}}{2\ \mathbf{PExp}}
                               \quad \inferrule{\inferrule{3 \in \mathbb{Z}}{3\ \mathbf{Atom}}}{3\ \mathbf{PExp}}}
                                 {2 \times 3\ \mathbf{PExp}}}
                      {1 \times 2 \times 3\ \mathbf{PExp}}
        $$

\subsection*{Part B}

The small-step for $\mathcal{L}$ is characterised by these rules:
\begin{gather*}
    \inferrule{ c \mapsto c' }{(\texttt{If}\ c\ t\ e) \mapsto (\texttt{If}\ c'\ t\ e) }(1)\quad
    \inferrule{ }{(\texttt{If}\ \texttt{True}\ t\ e) \mapsto t }(2)\quad
    \inferrule{ }{(\texttt{If}\ \texttt{False}\ t\ e) \mapsto e }(3)
\end{gather*}


Part B includes questions about $e \Downarrow v$ and $e \stackrel{\star}{\mapsto} v$.




\subsection*{Part D}

Here is a term in $\lambda$-calculus:
$$ (\lambda n.\ \lambda f.\ \lambda x.\ (n\ f\ (f\ x)))\ (\lambda f.\ \lambda x.\ f\ x) $$


Part D includes questions about $\beta$-reduction and $\eta$-reduction.

\subsection*{Part E}

Here's some concrete syntax:
  \[
  \begin{array}{l}
    \mathsf{let} \\
    \;\;\mathit{g}(\mathit{x}) = \neg\mathit{x} \\
    \mathsf{in} \\
    \;\; \mathit{g}(\mathsf{True})\\
    \mathsf{end}
  \end{array}
  \]

\end{document}