\documentclass{article}

% Language setting
% Replace `english' with e.g. `spanish' to change the document language
\usepackage[english]{babel}

% Set page size and margins
% Replace `letterpaper' with`a4paper' for UK/EU standard size
\usepackage[letterpaper,top=1in,bottom=1in,left=1in,right=1in]{geometry}

% Useful packages
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{mathpartir}
\usepackage{enumerate}
\usepackage{array}
\usepackage[colorlinks=true, allcolors=blue]{hyperref}

\makeatletter
\def\arcr{\@arraycr}
\makeatother

\title{CS 599 A1: Assignment 6}
\author{YOUR NAME, BU ID}
\date{}

\newcommand{\lc}{$\lambda$-calculus}

\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\mi}[1]{\mathit{#1}}
\newcommand{\mb}[1]{\mathbf{#1}}
\newcommand{\mt}[1]{\mathtt{#1}}
\newcommand{\elam}[2]{\lambda{#1}.\,{#2}}
\newcommand{\eapp}[2]{#1 \; #2}
\newcommand{\step}{\mapsto}
\newcommand{\val}[1]{#1 \; \m{value}}
\newcommand{\eval}{\Downarrow}
\newcommand{\num}[1]{\overline{#1}}
\newcommand{\numf}[1]{\underline{#1}}
\newcommand{\eif}[3]{\m{if} \; #1 \; \m{then} \; #2 \; \m{else} \; #3}
\newcommand{\multval}[1]{#1 \; \m{mult{-}value}}
\newcommand{\closed}[1]{#1 \; \m{closed}}
\newcommand{\tint}{\m{int}}
\newcommand{\tbool}{\m{bool}}
\newcommand{\elet}[3]{\m{let} \; #1 = #2 \; \m{in} \; #3}
\newcommand{\G}{\Gamma}
\newcommand{\R}[1]{\textcolor{red}{#1}}
\newcommand{\tfloat}{\m{float}}
\newcommand{\emptybox}{\boxed{\textcolor{white}{QWERTY}}}
\newcommand{\mstep}{\step^{*}}
\newcommand{\zero}{\m{zero}}
\renewcommand{\succ}[1]{\m{succ}(#1)}
\newcommand{\semi}{\,;\,}
\newcommand{\natrec}[5]{\m{natrec}(#1 \semi #2 \semi #3.\, #4. \, #5)}
\newcommand{\tnat}{\m{nat}}
\newcommand{\Red}{\m{Red}}
\newcommand{\natred}[1]{#1 \downarrow}
\newcommand{\issubst}{\Vdash}
\newcommand{\ift}{\m{int{-}or{-}float}}
\newcommand{\ecase}[3]{\m{case} \; #1 \; (#2 \Rightarrow #3)}
\newcommand{\ecaselr}[3]{\m{case} \; #1 \; (\m{inl} \Rightarrow #2 \mid \m{inr} \Rightarrow #3)}
\newcommand{\case}[2]{\m{case} \; #1 \; (#2)}
\newcommand{\erecv}[2]{#2 \leftarrow \m{recv} \; #1}
\newcommand{\esend}[2]{\m{send} \; #1 \; #2}
\newcommand{\esendl}[2]{#1.#2}
\newcommand{\ewait}[1]{\m{wait} \; #1}
\newcommand{\eclose}[1]{\m{close} \; #1}
\newcommand{\fwd}[2]{#1 \leftrightarrow #2}
\newcommand{\espawn}[3]{#1 \leftarrow #2 \; #3}
\newcommand{\ichoice}[1]{\oplus\{#1\}}
\newcommand{\echoice}[1]{\&\{#1\}}
\newcommand{\with}{\,\&\,}
\newcommand{\one}{\mathbf{1}}
\newcommand{\tensor}{\otimes}
\newcommand{\lolli}{\multimap}
\newcommand{\config}{\mathcal{C}}
\newcommand{\dc}{\mathcal{D}}
\newcommand{\D}{\Delta}
\newcommand{\T}{\Theta}
\newcommand{\poised}[1]{#1 \; \m{poised}}
\newcommand{\proc}[2]{\m{proc}(#1, #2)}
\newcommand{\msg}[2]{\m{msg}(#1, #2)}
\newcommand{\fresh}[1]{(#1 \; \m{fresh})}
\newcommand{\up}{\,\uparrow^{\m{S}}_{\m{L}}}
\newcommand{\down}{\,\downarrow^{\m{S}}_{\m{L}}}

\newcommand{\cons}{\mathcal{C}}
\newcommand{\vars}{\mathcal{V}}
\newcommand{\proves}{\vDash}
\newcommand{\oseq}[2]{#1 \Longrightarrow #2}
\newcommand{\fuse}{\bullet}
\newcommand{\under}{\backslash}
\renewcommand{\over}{\slash}

\newcommand{\tforall}[1]{\forall #1. \, }
\newcommand{\texists}[1]{\exists #1. \, }
\newcommand{\tassertop}{{?}}  % -fp was: ?
\newcommand{\tassumeop}{{!}}  % -fp was: !
\newcommand{\tassert}[1]{\tassertop\{#1\}. \,} % -fp was: \; \tassertop
\newcommand{\tassume}[1]{\tassumeop\{#1\}. \,} % -fp was: \; \tassumeop

\newcommand{\esendn}[2]{\m{send} \; #1 \; \{#2\}}
\newcommand{\erecvn}[2]{\{#2\} \leftarrow \m{recv} \; #1}
\newcommand{\eassume}[2]{\m{assume} \; #1 \; \{#2\}}
\newcommand{\eassert}[2]{\m{assert} \; #1 \; \{#2\}}
\newcommand{\eimposs}{\m{impossible}}

\newcommand{\epair}[2]{\langle #1, #2 \rangle}
\newcommand{\letpair}[4]{\m{let} \; \langle #1, #2 \rangle = #3 \; \m{in} \; #4}
\newcommand{\inl}[1]{\m{inl}(#1)}
\newcommand{\inr}[1]{\m{inr}(#1)}
\newcommand{\match}[5]{\m{match} \; #1 \; \m{with} \; \{\,\m{inl}(#2) \to #3 \mid \m{inr}(#4) \to #5\,\}}
\newcommand{\letapp}[4]{\m{let} \; #1 = #2 \; #3 \; \m{in} \; #4}

\newcommand{\limpl}{\supset}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Real}{\mathbb{R}}
\newcommand{\seq}{\Longrightarrow}
\newcommand{\cseq}{\longrightarrow}
\newcommand{\irseq}{\overset{\m{R}}{\longrightarrow}}
\newcommand{\ilseq}{\overset{\m{L}}{\longrightarrow}}
\newcommand{\icseq}{\overset{\m{C}}{\longrightarrow}}
\newcommand{\pt}{\; \m{true}}

\newtheorem{problem}{Problem}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newenvironment{solution}{\textbf{Solution.}}{}

\begin{document}
\maketitle


\begin{problem}[Mandatory; No LLMs; 10 pts]
    Refer the rules in Appendix~\ref{app:inference_rules}. Which operators in ordered logic are commutative?
    For each operator $*$ that is commutative, provide the proofs of equivalence of $A * B$ and $B * A$,
    i.e., $A * B \seq B * A$ and $B * A \seq A * B$.
\end{problem}

\begin{solution}

\end{solution}

\begin{problem}[Mandatory; No LLMs; 20 pts]
    Refer the rules in Appendix~\ref{app:inference_rules}. Which operators in ordered logic are associative?
    For each operator $*$ that is associative, provide the proofs of equivalence of $A * (B * C)$ and $(A * B) * C$,
    i.e., $A * (B * C) \seq (A * B) * C$ and $(A * B) * C \seq A * (B * C)$.
\end{problem}

\begin{solution}
    
\end{solution}

\begin{problem}[Mandatory; No LLMs; 40 pts]
Which inference rules in Appendix~\ref{app:inference_rules} are invertible? For each rule that is invertible,
provide a proof of its invertibility.

\textbf{Hint:} Use the cut admissibility theorem.
\end{problem}

\begin{solution}
    
\end{solution}

\begin{problem}[Mandatory; No LLMs; 10 pts]
Suppose we change the $\under L$ to the following:
\begin{mathpar}
\inferrule*[right=$\under L^*$]
{\oseq{\Omega_L \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; A \; (A \under B) \; \Omega_R}{C}}
\end{mathpar}
Instead of allowing an arbitrary $\Omega$ to the left of $(A \under B)$, we require that
the proposition on the left of $(A \under B)$ must be $A$.
Based on this, answer the following questions:
\begin{enumerate}
    \item Does this violate identity expansion? If yes, provide a brief justification.
    If not, provide a derivation of identity expansion.
    \item Does this violate cut admissibility? If yes, provide a brief justification.
    If not, provide a derivation of cut admissibility.
    \item Give an example of a proposition that is derivable in ordered logic
    but no longer derivable if we use $\under L^*$ instead of $\under L$.
\end{enumerate}
\end{problem}

\begin{solution}
    
\end{solution}

\begin{problem}[Mandatory; No LLMs; 10 pts]
We define a new operator $A \diamond B$ with the following left and right rules:
\begin{mathpar}
    \inferrule*[right=$\diamond R$]
    {\Omega_L \seq A \and \Omega_R \seq B}
    {\Omega_L \; \Omega \; \Omega_R \seq A \diamond B}
    \and
    \inferrule*[right=$\diamond L$]
    {\Omega_L \; A \; \Omega \; B \; \Omega_R \seq C}
    {\Omega_L \; (A \diamond B) \; \Omega_R \seq C}
\end{mathpar}
Does this operator satisfy identity expansion? Does it satisfy cut admissibility?
In each case, provide a proof if the property holds, and a brief justification if it does not.
\end{problem}

\begin{solution}
    
\end{solution}

\begin{problem}[Mandatory; No LLMs; 10 pts]
We define a new operator $A \Diamond B \Box C$ with the following right rule:
\begin{mathpar}
    \inferrule*[right=$\Diamond \Box R$]
    {\Omega_1 \; \Omega_2 \seq A \and \Omega_1 \seq B \and \Omega_2 \seq C}
    {\Omega_1 \; \Omega_2 \seq A \Diamond B \Box C}
\end{mathpar}
Design appropriate left rule(s) for $A \Diamond B \Box C$ such that identity expansion
and cut admissibility hold for this operator. You do not need to show the proofs of these
properties. If it is not possible to design correct left rule(s), please provide a brief justification.
\end{problem}

\begin{solution}
    
\end{solution}

\section{Optional Problems}
\begin{problem}[Optional; No LLMs; 20 pts]
    Prove identity expansion (Theorem~\ref{thm:id}) in ordered logic.
\end{problem}

\begin{solution}
    
\end{solution}

\begin{problem}[Optional; No LLMs; 30 pts]
    Provide a (partial) proof of cut admissibility (Theorem~\ref{thm:cut}) in ordered logic.
    You only need to show all the principal and commutative cases of $\over$ operator (over).
\end{problem}

\begin{solution}
    
\end{solution}

\newpage

\appendix

\section{Ordered Logic Inference Rules}\label{app:inference_rules}


\subsection*{Fuse ($\fuse$)}

\begin{mathpar}
\inferrule*[right=$\fuse R$]
{\oseq{\Omega_L}{A} \\ \oseq{\Omega_R}{B}}
{\oseq{\Omega_L \; \Omega_R}{A \fuse B}}

\inferrule*[right=$\fuse L$]
{\oseq{\Omega_L \; A \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; (A \fuse B) \; \Omega_R}{C}}
\end{mathpar}

\subsection*{Under ($\under$)}

\begin{mathpar}
\inferrule*[right=$\under R$]
{\oseq{A \; \Omega}{B}}
{\oseq{\Omega}{A \under B}}

\inferrule*[right=$\under L$]
{\oseq{\Omega}{A} \\ \oseq{\Omega_L \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; \Omega \; (A \under B) \; \Omega_R}{C}}
\end{mathpar}

\subsection*{Over ($\over$)}

\begin{mathpar}
\inferrule*[right=$\over R$]
{\oseq{\Omega \; A}{B}}
{\oseq{\Omega}{B \over A}}

\inferrule*[right=$\over L$]
{\oseq{\Omega}{A} \\ \oseq{\Omega_L \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; (B \over A) \; \Omega \; \Omega_R}{C}}
\end{mathpar}

\subsection*{With ($\with$)}

\begin{mathpar}
\inferrule*[right=$\with R$]
{\oseq{\Omega}{A} \\ \oseq{\Omega}{B}}
{\oseq{\Omega}{A \with B}}

\inferrule*[right=$\with L_1$]
{\oseq{\Omega_L \; A \; \Omega_R}{C}}
{\oseq{\Omega_L \; (A \with B) \; \Omega_R}{C}}

\inferrule*[right=$\with L_2$]
{\oseq{\Omega_L \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; (A \with B) \; \Omega_R}{C}}
\end{mathpar}

\subsection*{Plus ($\oplus$)}

\begin{mathpar}
\inferrule*[right=$\oplus R_1$]
{\oseq{\Omega}{A}}
{\oseq{\Omega}{A \oplus B}}

\inferrule*[right=$\oplus R_2$]
{\oseq{\Omega}{B}}
{\oseq{\Omega}{A \oplus B}}

\inferrule*[right=$\oplus L$]
{\oseq{\Omega_L \; A \; \Omega_R}{C} \\ \oseq{\Omega_L \; B \; \Omega_R}{C}}
{\oseq{\Omega_L \; (A \oplus B) \; \Omega_R}{C}}
\end{mathpar}

\subsection*{Unit ($1$)}

\begin{mathpar}
\inferrule*[right=$1R$]
{ }
{\oseq{\cdot}{1}}

\inferrule*[right=$1L$]
{\oseq{\Omega_L \; \Omega_R}{C}}
{\oseq{\Omega_L \; 1 \; \Omega_R}{C}}
\end{mathpar}

\subsection*{Identity}

\begin{mathpar}
\inferrule*[right=Id]
{ }
{\oseq{p}{p}}
\end{mathpar}

\begin{theorem}[Identity Expansion]\label{thm:id}
    For an arbitrary proposition $A$, $\oseq{A}{A}$ is derivable.
\end{theorem}

\begin{theorem}[Cut Admissibility]\label{thm:cut}
    Given derivations of $\Omega \seq A$ and $\Omega_L \; A \; \Omega_R \seq C$, we can construct a derivation for
    $\Omega_L \; \Omega \; \Omega_R \seq C$.
\end{theorem}






\end{document}