equal
deleted
inserted
replaced
221 \end{center} |
221 \end{center} |
222 |
222 |
223 \noindent where @{const Stars}, @{text Left}, @{text Right} and @{text |
223 \noindent where @{const Stars}, @{text Left}, @{text Right} and @{text |
224 Char} are constructors for values. @{text Stars} records how many |
224 Char} are constructors for values. @{text Stars} records how many |
225 iterations were used; @{text Left}, respectively @{text Right}, which |
225 iterations were used; @{text Left}, respectively @{text Right}, which |
226 alternative is used. This `tree view' leads naturally to the |
226 alternative is used. This `tree view' leads naturally to the idea that |
227 idea that regular expressions act as types and values as inhabiting |
227 regular expressions act as types and values as inhabiting those types |
228 those types. This view was first put forward by ???. The value for the |
228 (see, for example, \cite{HosoyaVouillonPierce2005}). The value for |
229 single `iteration', i.e.~the POSIX value, would look as follows |
229 the single `iteration', i.e.~the POSIX value, would look as follows |
230 |
230 |
231 \begin{center} |
231 \begin{center} |
232 @{term "Stars [Seq (Char x) (Char y)]"} |
232 @{term "Stars [Seq (Char x) (Char y)]"} |
233 \end{center} |
233 \end{center} |
234 |
234 |
1251 a single statement would require an additional assumption about the |
1251 a single statement would require an additional assumption about the |
1252 two values @{term "Seq v\<^sub>1 v\<^sub>2"} and @{term "Seq w\<^sub>1 w\<^sub>2"} |
1252 two values @{term "Seq v\<^sub>1 v\<^sub>2"} and @{term "Seq w\<^sub>1 w\<^sub>2"} |
1253 being inhabited by the same regular expression. The |
1253 being inhabited by the same regular expression. The |
1254 complexity of the proofs involved seems to not justify such a |
1254 complexity of the proofs involved seems to not justify such a |
1255 `cleaner' single statement. The statements given are just the properties that |
1255 `cleaner' single statement. The statements given are just the properties that |
1256 allow us to establish our theorems. The proofs for Proposition~\ref{ordintros} |
1256 allow us to establish our theorems without any difficulty. The proofs |
1257 are routine. |
1257 for Proposition~\ref{ordintros} are routine. |
1258 |
1258 |
1259 |
1259 |
1260 Next we establish how Okui and Suzuki's orderings relate to our |
1260 Next we establish how Okui and Suzuki's orderings relate to our |
1261 definition of POSIX values. Given a @{text POSIX} value @{text "v\<^sub>1"} |
1261 definition of POSIX values. Given a @{text POSIX} value @{text "v\<^sub>1"} |
1262 for @{text r} and @{text s}, then any other lexical value @{text |
1262 for @{text r} and @{text s}, then any other lexical value @{text |