|
|
 |
| Articles |
 |
Below you will find links to my articles and texts:
Equivalence of Deterministic and Epsilon Nondeterministic Automata
Based on concepts introduced in REWRITE3,
semiautomata and left-languages, automata and right-languages,
and languages accepted by automata are defined.
The powerset construction is defined for transition systems, semiautomata
and automata. Finally, the equivalence of deterministic
and epsilon nondeterministic automata is shown.
Labelled State Transition Systems
This article introduces labelled state transition systems,
where transitions may be labelled by words from a given alphabet.
Reduction relations from REWRITE1 are used
to define transitions between states, acceptance of words,
and reachable states. Deterministic transition systems are also defined.
Regular Expression Quantifiers - at least m Occurrences
This is the second article on regular expression quantifiers.
FLANG_2 introduced the quantifiers m to n occurrences and optional occurrence.
In the sequel, the quantifiers:
at least m occurrences and positive closure (at least 1 occurrence) are introduced.
String Rewriting Systems
Basing on the definitions from Compiler Construction,
semi-Thue systems, Thue systems, and direct derivations are introduced.
Next, the standard reduction relation is defined that, in turn,
is used to introduce derivations using the theory from Reduction Relations (REWRITE1).
Finally, languages generated by rewriting systems are defined as all strings
reachable from an initial word. This is followed by the introduction
of the equivalence of semi-Thue systems with respect to the initial word.
Regular Expression Quantifiers - m to n Occurrences
This article includes proofs of several facts
that are supplemental to the theorems proved in the previous article.
Next, it builds upon that theory to extend the framework
for proving facts about formal languages in general
and regular expression operators in particular.
In this article, two quantifiers are defined and their properties are shown:
m to n occurrences (or the union of a range of powers)
and optional occurrence. Although optional occurrence
is a special case of the previous operator (0 to 1 occurrences),
it is often defined in regex applications as a separate
operator - hence its explicit definition and properties in the article.
Formal Languages- Concatenation and Closure
Formal languages are introduced as subsets of the set of all
0-based finite sequences over a given set (the alphabet). Concatenation,
the n-th power and closure (Kleene closure / star closure) are defined and their properties are shown.
Finally, it is shown that the closure of the alphabet
(understood here as the language of words of length 1)
equals to the set of all words over that alphabet,
and that the alphabet is the minimal set with this property.
Boolean Properties of Sets
The article contains the definition of the empty set and (Mizar-MSE) axioms that introduce
elements of sets, set inclusion, the union, intersection, and difference of sets.
Next, several facts concerning the above mentioned relations and functions are proved.
Homomorphisms and Isomorphisms of Groups; Quotient Group
Homomorphisms and isomorphisms of groups, and quotient group are introduced.
The so called isomorphism theorems are proved.
Integers
In the article the following concepts were introduced:
the set of integers and its elements, congruences,
the ceiling and floor functors, also the fraction part of a real number,
integer division and the remainder of integer division.
The following schemes were also included: the separation scheme,
the schemes of integer induction, the minimum and maximum schemes
(the existence of minimum and maximum integers satisfying a given property).
Top
|
|
|
|
Mizar
