[isabelle] 2 new AFP entries

Two new entries are available at http://isa-afp.org/

POSIX Lexing with Derivatives of Regular Expressions
by Fahad Ausaf, Roy Dyckhoff, and Christian Urban

Brzozowski introduced the notion of derivatives for regular
expressions. They can be used for a very simple regular expression
matching algorithm. Sulzmann and Lu cleverly extended this algorithm
in order to deal with POSIX matching, which is the underlying
disambiguation strategy for regular expressions needed in lexers. In
this entry we give our inductive definition of what a POSIX value is
and show (i) that such a value is unique (for given regular expression
and string being matched) and (ii) that Sulzmann and Lu's
algorithm always generates such a value (provided that the regular
expression matches the string). We also prove the correctness of an
optimised version of the POSIX matching algorithm.

Cardinality of Equivalence Relations
by Lukas Bulwahn

This entry provides formulae for counting the number of equivalence
relations and partial equivalence relations over a finite carrier set
with given cardinality.  To count the number of equivalence relations,
we provide bijections between equivalence relations and set
partitions, and then transfer the main results of the two AFP entries,
Cardinality of Set Partitions and Spivey's Generalized Recurrence
for Bell Numbers, to theorems on equivalence relations. To count the
number of partial equivalence relations, we observe that counting
partial equivalence relations over a set A is equivalent to counting
all equivalence relations over all subsets of the set A. From this
observation and the results on equivalence relations, we show that the
cardinality of partial equivalence relations over a finite set of
cardinality n is equal to the n+1-th Bell number.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.