6110feb4.tex

\documentclass[11pt,a4paper,svgnames]{article}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb,amsthm}
\usepackage{makeidx}
\usepackage{graphicx}
\usepackage{float}
\usepackage{wrapfig}
\usepackage{algorithm}
\usepackage{algorithmicx}
\usepackage{ccaption}
\usepackage{mathpartir}
\usepackage{xspace}
\usepackage{stmaryrd}
\usepackage{mathtools}
\usepackage{algpseudocode}
\usepackage{titlesec}
\usepackage{listings}
%\usepackage{floatrow}
\usepackage{tikz}
\usetikzlibrary{automata,trees,fit,backgrounds,shapes,snakes}
\usetikzlibrary{decorations.shapes}


\usepackage{xcolor}
%\titleformat*{\section}{\itshape}



\usepackage{leestd}

\lstset{ %
  language=Caml,                % the language of the code
  basicstyle=\footnotesize,           % the size of the fonts that are used for the code
  numbers=left,                   % where to put the line-numbers
  numberstyle=\tiny\color{gray},  % the style that is used for the line-numbers
  stepnumber=1,                   % the step between two line-numbers. If it's 1, each line 
                                  % will be numbered
  numbersep=10pt,                  % how far the line-numbers are from the code
  backgroundcolor=\color{white},      % choose the background color. You must add \usepackage{color}
  showspaces=false,               % show spaces adding particular underscores
  showstringspaces=false,         % underline spaces within strings
  showtabs=false,                 % show tabs within strings adding particular underscores
  mathescape=true,
  frame=leftline,                   % adds a frame around the code
  rulecolor=\color{gray},        % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
  tabsize=2,                      % sets default tabsize to 2 spaces
  captionpos=t,                   % sets the caption-position to bottom
  breaklines=true,                % sets automatic line breaking
  breakatwhitespace=false,        % sets if automatic breaks should only happen at whitespace
  title=\lstname,                   % show the filename of files included with \lstinputlisting;
                                  % also try caption instead of title
  escapeinside={\%*}{*)},            % if you want to add LaTeX within your code
  morekeywords={*,...},              % if you want to add more keywords to the set
  deletekeywords={...}              % if you want to delete keywords from the given language
}
\setlength{\parindent}{0pt}

\newcommand{\ba}[1]{\left\langle#1\right\rangle}
\newcommand{\Iff}[3]{\co{if}~{#1}~\co{then}~{#2}~\co{else}~{#3}}
\newcommand{\Whilee}[2]{\co{while}~#1~\co{do}~#2}
\author{Lee Gao}
\title{CS 6110: Feb 4}
\begin{document}
\maketitle

\section{Inference Rules}
When you define a rule, you're really definintg a set of rule instances, that with consistent substitution of metavariables that must also satisfy some side conditions.

Now,
$$
\inferrule*[right=~]{3 \times 2 \to 5}{3\times 2 + 1 \to 5 + 1}
$$
is a valid (albeit incorrect) instance of the rule. But if we're at the axiom leaves, then side condition must be obeyed as well.

A logical instance is just
$$
\inferrule*[right=Instance]{x_1 \and x_2 \and x_3 \and \dots}{x}
$$
so that $x,x_i \in S$. Let the relation or whatever be defined as $A$ (so that $\to = A$ in the case of the operational semantics, then $A \subseteq S$.

Let's have a rule operator $R(B)$, (a notion of entailment): what does the things in $B$ entail? (AKA, if we're allowed to assume $B$, then 
$$R(B) = \Rec{x \mid \inferrule{x_1 \and \dots \and x_n}{x}, \Rec{x_1,\dots,x_n}\subseteq B}$$

So $R(\varnothing)$ is the set of axioms (that do not have premises). Note, if an axiom has a side condition but no premise, then it's still an axiom.


\begin{description}
\item[Consistency] $A \subseteq R(A)$

\item[Closure] $R(A) \subseteq A$
\end{description}

These two conditions says that $A = R(A)$. So $A$ is a fixed point of $R$. There could potentially be an infinite number of fixed points of $R$, so we need to pick the appropriate one.

A set of inference rules is an inductive definition. So $A$ is the elements derivable in a \emph{finite} number of steps.

\begin{table}[H]
\centering
\begin{tabular}{cc}
times & set \\
0 & $\varnothing$ \\
1 step & $R(\varnothing)$ \\
2 & $R^2(\varnothing)$ \\
\vdots & \vdots
\end{tabular}
\end{table}

So just get the fixed point, aka
$$
A = \bigcup_{n} R^n(\varnothing)
$$

Prove that this is a fixed point. 

$R$ is monotonic, that is, if $B \subseteq C$, then $R(B) \subseteq R(C)$.
So
$$
\varnothing \subseteq R(\varnothing) \subseteq R^2(\varnothing) \dots
$$
So that $\bigcup_i^n R^i(\varnothing) = R^n$. So if some element shows up in these sets, then it stays. So
$$
x \in A \implies \exists n. x \in R^n(\varnothing)
$$
\begin{theorem}[Closure]
$$
R(A) \subseteq A
$$
\begin{proof}
Let $x \in R(A)$ where
$$
R(A) = R\pa{\bigcup_n R^n(\varnothing)}
$$
then it must be the case that $x$ is the conclusion of some rule 
$$
\inferrule*[right=Instance]{x_1 \and \dots \and x_n}{x}
$$
where $x_1,\dots,x_n \in A$ (implicit: finite $n$). Therefore, each of $x_1,\dots,x_n$ occurs in some $R^n$. Now, pick some finite $m$ such that all of $x_1,\dots,x_n \in R^m(\varnothing)$. Then $x \in R^{m+1}(\varnothing) \subseteq A$; so $x \in A$, which concludes the proof.
\end{proof}
\end{theorem}

\begin{theorem}[Consistency]
$$
A \subseteq R(A)
$$
\begin{proof}
Let $x \in A$, then there must exist some $n$ such that $x \in R^n(A)$. Since $x \in R^n(\varnothing) \implies x \in R(A)$, because
$$
R^{n-1}(\varnothing) \subseteq A \implies R^{n} \subseteq R(A)
$$
which concludes the proof.
\end{proof}
\end{theorem}

Therefore, $A$ is a fixed point of $R$.

Which fixed point is it? It turns out that $A$ is the least possible (smallest) fixed point of $R$.

\begin{theorem}[Least FP]
$A$ is the smallest fixed point of $R$
\begin{proof}
let $B$ be a fixed point of $R$, so $B = R(B)$. Obviously, $\varnothing \subseteq B$, so
$$
\varnothing \subseteq B \implies R(\varnothing) \subseteq R(B) = B \implies \dots
$$
So therefore
$$
\bigcup_n R^n(\varnothing) \subseteq B
$$
which concludes the proof.
\end{proof}
\end{theorem}

So it's interesting to think about what the other fp do. The least fixed point is the intersection of all closed sets. The greatest fp is the union of all consistent sets.

The greatest fp (max fp) allows infinite ``proof''. So for example, we can have
$$
\inferrule*[right=?]{x}{x}
$$
so we can derive $x$ arbitrarily as
$$
\inferrule*[right=?]{\inferrule*[right=?]{\inferrule*[right=?]{\vdots}{x}}{x}}{x}
$$
so for the $\bstep$ relation, the LFP gives the terminating executions and the MFP gives that and also the nonterminating executions. MFP is also called coinduction.

Do we really need to restrict rules to have a finite number of premises?

Let's build a rule for interesting
\begin{mathpar}
\inferrule*[right=1]{~}{1 \in I} \and
\inferrule*[right=Next]{n' \in I \and n' = n + 1}{n \in I}
\inferrule*[right=Prev]{\forall m > n. m \in I}{n \in I}
\end{mathpar}
So that
\begin{align*}
R(\varnothing) &= \Rec{1} \\
R^2 &=  \Rec{1,2} \\
\vdots \\
R^n &= \Rec{1,\dots,n}
\end{align*}
so 
$$
\bigcup_n R^n = \Rec{1,\dots} = \mathbb{N}
$$
but $0 \in R(\mathbb{N})$, so $A$ isn't a fixed point of $R$ anymore.

Recall that we defined the free variables $\f{Fvs}(e)$ inductively as
\begin{mathpar}
\f{Fvs}(x) = \Rec{x} \and 
\f{Fvs}(e_1~e_2) = \f{Fvs}(e_1) \cup \f{Fvs}(e_2) \and
\f{Fvs}(\lambda x.e) = \f{Fvs}(e)\backslash \Rec{x}
\end{mathpar}
then we an define the $\mapsto$ relation meaning that $e$ has free variables $\Rec{\dots}$, so that
\begin{mathpar}
\inferrule*[right=Var]{~}{x \mapsto \Rec{x}} \and
\inferrule*[right=App]{e_1 \mapsto v_0 \and e_2 \mapsto v_2 \and v = v_2 \cup v_1}{e_1 ~ e_2 \mapsto v} \and
\inferrule*[right=Lam]{e \mapsto v}{\lambda x. e \mapsto v \backslash \Rec{x}}
\end{mathpar}

\begin{theorem}
Exactly one $v$ for each $e$ such that $e \mapsto v$.
\begin{proof}
By induction on the height of $e$. In the base case, we have height 0, so $e = x$. Here, there's only one rule that applies, which shows the case. Next, the inductive step
\begin{itemize}
\item $e = e_0 ~ e_1$. By induction, there's a unique $v_0,v_1$ such that $e_0 \mapsto v_0$ and $e_1 \mapsto v_1$. Then there is a unique set $v = v_0 \cup v_1$, and the rule gives that $e \mapsto v$, which also shows the case.
\item $e = \lambda x.e$ Same exact reasoning, appealing to uniqueness preservation of $v \backslash \Rec{x}$
\end{itemize}
\end{proof}
\end{theorem}

We're allowed to do this because there's only one rule that applies to each argument, and the argument on the RHS is smaller.

It's awkward to prove based on the height of the proof tree. Let's now move onto well-founded induction, which uses the concept of the well-founded relations: $\prec$
\end{document}