author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Thu, 29 Jan 2015 23:39:08 +0000 | |
changeset 55 | c33cfa1e813a |
child 57 | 7093e600ec2c |
permissions | -rw-r--r-- |
55
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
\documentclass[11pt]{article} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
\begin{document} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
A lemma which might be true, but can also be false, is as follows: |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
\begin{tabular}{lll} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
If & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
& (2) & $\vdash v_1 : der\;c\;r$, and\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
& (3) & $\vdash v_2 : der\;c\;r$ holds,\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
then & & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds. |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
\noindent It essentially states that if one value $v_1$ is |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
bigger than $v_2$ then this ordering is preserved under |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
injections. This is proved by induction (on the definition of |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
$der$\ldots this is very similar to an induction on $r$). |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
\bigskip |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
The case that is still unproved is the sequence case where we |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
assume $r = r_1\cdot r_2$ and also $r_1$ being nullable. |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
The derivative $der\;c\;r$ is then |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
$der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
or without the parentheses |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
$der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
In this case the assumptions are |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
\begin{tabular}{ll} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
(a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
(b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
(c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
(d) & $nullable(r_1)$ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
The induction hypotheses are |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
\begin{tabular}{ll} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
(IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2 |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
\;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\; |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
\vdash v_2 : der\;c\;r_1\qquad$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
& $\hfill\longrightarrow |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
(IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2 |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
\;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\; |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
\vdash v_2 : der\;c\;r_2\qquad$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
& $\hfill\longrightarrow |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
The goal is |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
\[ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
(goal)\qquad |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
inj\; (r_1 \cdot r_2)\;c\;v_2 |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
\] |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
If we analyse how (a) could have arisen (that is make a case |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
distinction), then we will find four cases: |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
\begin{tabular}{ll} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
86 |
RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
\noindent |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
We have to establish our goal in all four cases. |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
\subsubsection*{Case LR} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
98 |
The corresponding rule (instantiated) is: |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
\begin{tabular}{c} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
$len\,|w_1| \geq len\,|w_2|$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
103 |
\hline |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
$Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
\subsubsection*{Case RL} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
The corresponding rule (instantiated) is: |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
\begin{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
\begin{tabular}{c} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
$len\,|w_1| > len\,|w_2|$\\ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
\hline |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
$Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$ |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
\end{tabular} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
\end{center} |
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
|
c33cfa1e813a
added some notes (still incomplete)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
\end{document} |