ChengsongTanPhdThesis/Chapters/Further.tex
author Chengsong
Fri, 12 Aug 2022 00:39:23 +0100
changeset 576 3e1b699696b6
parent 532 cc54ce075db5
permissions -rwxr-xr-x
thesis chap5
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
532
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     1
% Chapter Template
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     2
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     3
\chapter{Further Improvements} % Main chapter title
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     4
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     5
\label{Further} %In Chapter 5\ref{Chapter5} we discuss stronger simplifications to improve the finite bound
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     6
%in Chapter 4 to a polynomial one, and demonstrate how one can extend the
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     7
%algorithm to include constructs such as bounded repetitions and negations.
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     8
 
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
     9
%----------------------------------------------------------------------------------------
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    10
%	SECTION strongsimp
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    11
%----------------------------------------------------------------------------------------
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    12
\section{Zippers}
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    13
%TODO: search for isabelle proofs of algorithms that check equivalence 
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    14
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    15
Unfortunately using zippers causes a similar effect like the "break up" rule
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    16
and does not preserve the $\POSIX$ property.
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    17
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    18
cc54ce075db5 restructured
Chengsong
parents:
diff changeset
    19