Skip to content

Commit 78b404a

Browse files
seanmclseanmcl
committed
misc
1 parent ffaa622 commit 78b404a

33 files changed

+2880
-436
lines changed

‎.latexmkrc

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
$pdf_mode = 1;
2+
@default_files = ('thesis');

‎thesis.old/bin/check-bib ‎bin/check-bib

File renamed without changes.

‎thesis.old/bin/check-commands ‎bin/check-commands

File renamed without changes.

‎chapter-aws.tex

+6
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,8 @@
11
\chapter{Case Study: Networking in the Cloud}
22
\label{chapter-aws}
3+
4+
% Amazon Web Services is a computing infrastructure service provided
5+
% by Amazon, Inc. For example, you can create virtual networks, including
6+
% IP subnetting, routing tables, NAT, and security mechanisms such as
7+
% firewalls. Inside these networks, you can create virtual machines,
8+
% databases, and other computing services.

‎chapter-constr.tex

+228
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,228 @@
1+
\chapter{Constraints}
2+
\label{chapter-constraints}
3+
4+
5+
\begin{figure}
6+
\footnotesize
7+
\[
8+
\arraycolsep=15pt
9+
\begin{array}{c}
10+
\begin{array}{ccc}
11+
\infer[\mbox{E-R}]{\CSeq{\Phi}{\Gamma}{E}}{\Phi \models E}
12+
&
13+
\infer[\mbox{E-L}]{\CSeq{\Phi}{\Gamma, E}{C}}{\CSeq{\Phi \And E}{\Gamma}{C}}
14+
&
15+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma, \Ps)}{\Pt}}{\Phi \models \vec{s} \EEq \vec{t}}
16+
\end{array}
17+
\\[2em]
18+
19+
\begin{array}{cc}
20+
\infer[\Top$-R$]{\CSeq{\Phi}{\Gamma}{\Top}}{}
21+
&
22+
\mbox{No rule for $\Top$-L}
23+
\end{array}
24+
\\[2em]
25+
26+
\begin{array}{cc}
27+
\mbox{No rule for $\Bot$-R}
28+
&
29+
\infer[\Bot$-L$]{\CSeq{\Phi}{\Gamma, \Bot}{C}}{}
30+
\end{array}
31+
\\[2em]
32+
33+
\begin{array}{cc}
34+
\infer[\And$-R$]{\CSeq{\Phi}{\Gamma}{A \And B}}{\CSeq{\Phi}{\Gamma}{A} & \CSeq{\Phi}{\Gamma}{B}}
35+
&
36+
\infer[\And$-L$]{\CSeq{\Phi}{\Gamma, A \And B}{C}}{\CSeq{\Phi}{\Gamma, A, B}{C}}
37+
\end{array}
38+
\\[2em]
39+
40+
\begin{array}{ccc}
41+
\infer[\Or$-R$_1]{\CSeq{\Phi}{\Gamma}{A \Or B}}{\CSeq{\Phi}{\Gamma}{A}}
42+
&
43+
\infer[\Or$-R$_2]{\CSeq{\Phi}{\Gamma}{A \Or B}}{\CSeq{\Phi}{\Gamma}{B}}
44+
&
45+
\infer[\Or$-L$]{\CSeq{\Phi}{\Gamma, A \Or B}{C}}{\CSeq{\Phi}{\Gamma, A}{C} & \CSeq{\Phi}{\Gamma, B}{C}}
46+
\end{array}
47+
\\[2em]
48+
49+
\begin{array}{cc}
50+
\infer[\Imp$-R$]{\CSeq{\Phi}{\Gamma}{A \Imp B}}{\CSeq{\Phi}{\Gamma, A}{B}}
51+
&
52+
\infer[\Imp$-L$]{\CSeq{\Phi}{\Gamma, A \Imp B}{C}}{\CSeq{\Phi}{\Gamma, B}{C} & \CSeq{\Phi}{\Gamma, A \Imp B}{A}}
53+
\end{array}
54+
\\[2em]
55+
56+
\begin{array}{cc}
57+
\infer[\All$-R$]{\CSeq{\Phi}{\Gamma}{\All x.~A(x)}}{\CSeq{\Phi}{\Gamma}{A(a)} & a\not\in\Phi, \Gamma, A}
58+
&
59+
\infer[\All$-L$]{\CSeq{\Phi}{\Gamma, \All x.~A(x)}{C}}{\CSeq{\Phi}{\Gamma, \All x.~A(x), A(t)}{C}}
60+
\end{array}
61+
\\[2em]
62+
63+
\begin{array}{cc}
64+
\infer[\Ex$-R$]{\CSeq{\Phi}{\Gamma}{\Ex x.~A(x)}}{\CSeq{\Phi}{\Gamma}{A(t)}}
65+
&
66+
\infer[\Ex$-L$]{\CSeq{\Phi}{\Gamma, \Ex x.~A(x)}{C}}{\CSeq{\Phi}{\Gamma, A(a)}{C} & a\not\in\Phi, \Gamma, A}
67+
\end{array}
68+
\\[2em]
69+
70+
\end{array}
71+
\]
72+
\caption{The backward constraint calculus, \C.}
73+
\label{fig:backward}
74+
\end{figure}
75+
76+
\begin{figure}
77+
\[
78+
\arraycolsep=15pt
79+
\begin{array}{c}
80+
\begin{array}{cc}
81+
\infer[\mbox{id}]{\Phi \models \Phi}{}
82+
&
83+
\infer[\mbox{trans}]{\Phi_1 \models \Phi_3}{\Phi_1\models\Phi_2 & \Phi_2\models\Phi_3}
84+
\end{array}
85+
\\[2em]
86+
\begin{array}{ccc}
87+
\infer[\And_1]{\Phi_1 \And \Phi_2 \models \Phi_1}{}
88+
&
89+
\infer[\And_2]{\Phi_1 \And \Phi_2 \models \Phi_2}{}
90+
&
91+
\infer[\And]{\Phi \models \Phi_1 \And \Phi_2}{\Phi \models \Phi_1 & \Phi \models \Phi_2}
92+
\end{array}
93+
\\[2em]
94+
\begin{array}{ccc}
95+
\infer[$refl$]{\Phi \models t\EEq t}{}
96+
&
97+
\infer[$sym$]{\Phi \models s\EEq t}{\Phi\models t\EEq s}
98+
&
99+
\infer[$vec$]{\Phi \models \vec{s}\EEq \vec{t}}{|s| = |t| = n & \Phi\models s_1\EEq t_1 & \cdots & \Phi\models s_n\EEq t_n}
100+
\end{array}
101+
\\[2em]
102+
\end{array}
103+
\]
104+
\caption{Properties of the entailment relation.}
105+
\label{fig:entailment}
106+
\end{figure}
107+
108+
\begin{lemma}[Constraint Weakening]\label{lem:e-weaken}
109+
For any $\Phi, \Phi', \Gamma, C$, if $\Phi'\models \Phi$ and $\CSeq{\Phi}{\Gamma}{C}$
110+
then $\CSeq{\Phi'}{\Gamma}{C}$.
111+
\end{lemma}
112+
\begin{proof}
113+
By induction on the derivation $\CSeq{\Phi}{\Gamma}{C}$. Some cases:
114+
\begin{description}
115+
\item[Case]
116+
\[\infer[$E-R$]{\CSeq{\Phi}{\Gamma}{E}}{\Phi\models E}\]
117+
By transitivity of entailment (rule trans) we have $\Phi'\models E$ so
118+
$\CSeq{\Phi'}{\Gamma}{E}$ by rule E-R.
119+
\item[Case]
120+
\[\infer[$E-L$]{\CSeq{\Phi}{\Gamma, E}{C}}{\CSeq{\Phi\And E}{\Gamma}{C}}\]
121+
By entailment reasoning, we have $\Phi'\And E\models\Phi\And E$. By induction
122+
hypothesis we have that $\CSeq{\Phi'\And E}{\Gamma}{C}$ so $\CSeq{\Phi'}{\Gamma, E}{C}$
123+
by rule E-L.
124+
\end{description}
125+
\end{proof}
126+
127+
\begin{lemma}[Inversion]\label{lem:e-invert}
128+
For any $\Phi, \Gamma, E, C$ if $\CSeq{\Phi}{\Gamma, E}{C}$ then $\CSeq{\Phi\And E}{\Gamma}{C}$.
129+
\end{lemma}
130+
\begin{proof} Easy induction on the derivation. \end{proof}
131+
132+
\begin{lemma}[Contraction]\label{lem:contract}
133+
If $\CSeq{\Phi}{\Gamma, \Ps, \Pt}{C}$ and $\Phi\models\vec{s}\EEq\vec{t}$ then
134+
$\CSeq{\Phi}{\Gamma, \Ps}{C}$.
135+
\end{lemma}
136+
137+
\begin{proof}
138+
Induction on the derivation $\D$ of $\CSeq{\Phi}{\Gamma, \Ps, \Pt}{C}$.
139+
\begin{description}
140+
\item[Case] $\D$ is
141+
\[
142+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma', \Pu}{\Pv}}{\Phi \models \vec{u} \EEq \vec{v}}
143+
\]
144+
We have $C = \Pv$ and $\Gamma, \Ps, \Pt = \Gamma', \Pu$.
145+
If $\vec{u} \neq \vec{t}$ then we already have
146+
$\CSeq{\Phi}{(\Gamma'\setminus \Pt), \Pu}{\Pv}$ by rule E-init. Otherwise
147+
we have $\Gamma' = \Gamma, \Ps$ and $\Phi\models\vec{t} \EEq \vec{v}$ and $\Phi\models\vec{s} \EEq \vec{t}$ so
148+
$\Phi\models\vec{s} \EEq \vec{v}$. Then $\CSeq{\Phi}{\Gamma, \Ps}{\Pv}$
149+
by rule E-init.
150+
\item[Case] $\D$ is
151+
\[
152+
\infer[\mbox{E-L}]{\CSeq{\Phi}{\Gamma, \Ps, \Pt, E}{C}}{\CSeq{\Phi\And E}{\Gamma}{C}}
153+
\]
154+
Since $E$ can not be an atomic formula, $E\neq \Ps$ and, $E\neq \Pt$.
155+
Since $\Phi\models \vec{s}\EEq\vec{t}$, $\Phi\And E\models \vec{s}\EEq\vec{t}$, so
156+
the induction hypothesis applies and we have $\CSeq{\Phi\And E}{\Gamma, \Ps}{C}$.
157+
The result follows from an application of rule E-L.
158+
\end{description}
159+
\end{proof}
160+
161+
\begin{lemma}[Constraint Substitution]\label{lem:subst}
162+
If $\CSeq{\Phi}{\Gamma}{\Ps}$ and $\Phi\models\vec{s}\EEq\vec{t}$ then
163+
$\CSeq{\Phi}{\Gamma}{\Pt}$.
164+
\end{lemma}
165+
166+
\begin{proof}
167+
Induction on the derivation $\D$ of $\CSeq{\Phi}{\Gamma}{\Ps}$.
168+
\begin{description}
169+
\item[Case] $\D$ is
170+
\[
171+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma', \Pu}{\Pv}}{\Phi \models \vec{u} \EEq \vec{v}}
172+
\]
173+
\end{description}
174+
\end{proof}
175+
176+
177+
\begin{proof}[Proof of Theorem~\ref{thm:cut-admissible}]
178+
Let $\D :: \CSeq{\Phi}{\Gamma}{A}$ and $\E :: \CSeq{\Phi}{\Gamma, A}{C}$.
179+
We proceed by induction on $A, \D, \E$. The majority of the cases don't modify
180+
the constraints in any way, and the cases are identical with Pfenning's proof. We
181+
show the cases where constraints play a significant role.
182+
183+
\begin{description}
184+
\item[Case]
185+
Initial cuts. These are cuts where one of the derivations is initial with A as
186+
its principle formula.
187+
\begin{description}
188+
\item[Case]
189+
$\D$ is \[\infer[$E-R$]{\CSeq{\Phi}{\Gamma}{E}}{\Phi\models E}\]
190+
Since $A = E$ we have $\CSeq{\Phi}{\Gamma, E}{C}$. By inversion (Lemma~\ref{lem:e-invert}) we
191+
have a derivation of $\CSeq{\Phi\And E}{\Gamma}{C}$.
192+
Then since $\Phi\models E$, we have $\Phi\models\Phi\And E$ (constraint rules id and $\And$) so by
193+
constraint weakening (Lemma~\ref{lem:e-weaken}) we have $\CSeq{\Phi}{\Gamma}{C}$ as required.
194+
\item[Case]
195+
$\D$ is \[\infer[$E-init$]{\CSeq{\Phi}{\Gamma', \Ps}{\Pt}}{\Phi\models \vec{s}\EEq\vec{t}}\]
196+
Then $\Gamma = \Gamma', \Ps$, $A = \Pt$. By assumption we
197+
have $\CSeq{\Phi}{\Gamma', \Ps, \Pt}{C}$. By contraction (Lemma~\ref{lem:contract})
198+
we have $\CSeq{\Phi}{\Gamma', \Ps}{C}$ as required.
199+
\item[Case]
200+
$\E$ is \[\infer[$E-init$]{\CSeq{\Phi}{\Gamma, \Ps}{\Pt}}{\Phi\models \vec{s}\EEq\vec{t}}\]
201+
Then $A = \Ps, C = \Pt$. By assumption we
202+
have $\CSeq{\Phi}{\Gamma}{\Ps}$. The result follows by constraint substitution (Lemma~\ref{lem:subst}).
203+
\end{description}
204+
205+
\item[Case]
206+
Principal cuts.
207+
\begin{description}
208+
\item[Case] Foo
209+
\item[Case] Bar
210+
\end{description}
211+
212+
\item[Case]
213+
Left commutative cuts.
214+
\begin{description}
215+
\item[Case] Foo
216+
\item[Case] Bar
217+
\end{description}
218+
219+
\item[Case]
220+
Right commutative cuts.
221+
\begin{description}
222+
\item[Case] Foo
223+
\item[Case] Bar
224+
\end{description}
225+
226+
\end{description}
227+
228+
\end{proof}

‎chapter-fol.tex

+10-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,12 @@
1-
\chapter{Prop}
2-
\label{chapter-prop}
1+
\chapter{FOL}
2+
\label{chapter-fol}
33

4+
Get a Datalog interpreter for free by attempting $\Bot$ and reading off facts
5+
from the saturated database.
46

5-
Prop!\cite{cervesato13substructural}
7+
Get a Prolog interpreter for almost-free by using the magic sets transformation.
8+
9+
\section{History}
10+
11+
The earliest algorithm for enumerating unprovable sequents is found in Ketonen's
12+
thesis~\cite{Ketonen.1944.Thesis}.

0 commit comments

Comments
 (0)