Caves Travel Graphics Mizar Articles Cuisine Lemkov Contact Polski  
Base Texts & Articles YAC Software  
 Back
List
Market Research
in Poland - 2007
Accessing
Protected
Members
Mizar-MSE
Syntax
Regular Expression
Quantifiers -
at least m
Occurrences
String Rewriting
Systems
Regular Expression
Quantifiers - m
to n Occurrences
Formal Languages
- Concatenation
and Closure
Boolean
Properties of Sets
Homomorphisms
and Isomorphisms
of Groups;
Quotient Group
Integers
ARTICLES
List
Below you will find links to my articles and texts:

Market Research in Poland - 2007

Accessing Protected Members

Mizar-MSE Syntax

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 of sets, and the intersection 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).