From fb4f4d9f49fe43ab7359caf7c8a7e8f394410ced Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 8 Mar 2012 08:24:25 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter6.ma | 48 ++++++++++++++++++++++++------------- 1 file changed, 32 insertions(+), 16 deletions(-) diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma index 1a8b65aa3..679331198 100644 --- a/weblib/tutorial/chapter6.ma +++ b/weblib/tutorial/chapter6.ma @@ -1,10 +1,12 @@ -include "tutorial/chapter5.ma". - -(* In this chapter we shall apply our notion of DeqSet, and the list operations +(* +h1 class="section"Formal Languages/h1 +In this chapter we shall apply our notion of DeqSet, and the list operations defined in Chapter 4 to formal languages. A formal language is an arbitrary set of words over a given alphabet, that we shall represent as a predicate over words. -A word (or string) over an alphabet S is just a list of elements of S. *) +*) +include "tutorial/chapter5.ma". +(* A word (or string) over an alphabet S is just a list of elements of S.*) definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S. (* For any alphabet there is only one word of length 0, the iempty word/i, which is @@ -19,7 +21,10 @@ String concatenation is just the append operation over lists, hence there is no point to define it. Similarly, many of its properties, such as the fact that concatenating a word with the empty word gives the original word, follow by general results over lists. +*) +(* +h2 class="section"Operations over languages/h2 Languages inherit all the basic operations for sets, namely union, intersection, complementation, substraction, and so on. In addition, we may define some new operations induced by string concatenation, and in particular the concatenation @@ -32,7 +37,13 @@ definition cat : ∀S,l1,l2,w.Prop ≝ notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. interpretation "cat lang" 'middot a b = (cat ? a b). -(* Given a list of words, the flatten operation concatenates them all. *) + +(* Given a language l, the Kleene's star of l, denoted by l*, is the set of +finite-length strings that can be generated by concatenating arbitrary strings of +l. In other words, w belongs to l* is and only if there exists a list of strings +w1,w2,...wk all belonging to l, such that l = w1w2...wk. +We need to define the latter operations. The following flatten function takes in +input a list of words and concatenates them together. *) let rec flatten (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S ≝ match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ]. @@ -43,16 +54,22 @@ all words in l are in r, that is for every w in l, r w holds. *) let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝ match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a conjunct ? tl r ]. -(* Given a language l, the kleene's star of l, denoted by l*, is the set of -finite-length strings that can be generated by concatenating arbitrary strings of -l. In other words, w belongs to l* is and only if there exists a list of strings -lw all belonging to l, such that l = flatten lw. *) +(* We are ready to give the formal definition of the Kleene's star of l: +a word w belongs to l* is and only if there exists a list of strings +lw such that (conjunct lw l) and l = flatten lw. *) definition star ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw.a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"conjunct/a ? lw l. notation "a ^ *" non associative with precedence 90 for @{ 'star $a}. interpretation "star lang" 'star l = (star ? l). -(* Equality between languages is just the usual extensional equality between +(* The derivative of a language A with respect to a character a is the set of +all strings w such that aw is in A. *) + +definition deriv ≝ λS.λA:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.λa,w. A (aa title="cons" href="cic:/fakeuri.def(1)":/a:w). + +(* +h2 class="section"Language equalities/h2 +Equality between languages is just the usual extensional equality between sets. The operation of concatenation behaves well with respect to this equality. *) lemma cat_ext_l: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. @@ -106,10 +123,7 @@ lemma distr_cat_r_eps: ∀S.∀A,C:a href="cic:/matita/tutorial/chapter6/word.d #S #A #C @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"distr_cat_r/a |@a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"eqP_union_l/a @a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"epsilon_cat_l/a] qed. -(* The derivative of a language A with respect to a character a is the set of -all strings w such that aw is in A. *) - -definition deriv ≝ λS.λA:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.λa,w. A (aa title="cons" href="cic:/fakeuri.def(1)":/a:w). +(* The following is a major property of derivatives *) lemma deriv_middot: ∀S,A,B,a. a title="logical not" href="cic:/fakeuri.def(1)"¬/a A a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a → a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S (Aa title="cat lang" href="cic:/fakeuri.def(1)"·/aB) a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S A a) a title="cat lang" href="cic:/fakeuri.def(1)"·/a B. #S #A #B #a #noteps #w normalize % @@ -123,8 +137,10 @@ lemma deriv_middot: ∀S,A,B,a. a title="logical not" href="cic:/fakeuri.def(1) ] qed. -(* We conclude this section with some important properties of Kleene's -star that will be usde in the following chapters. *) +(* +h2 class="section"Main Properties of Kleene's star/h2 +We conclude this section with some important properties of Kleene's +star that will be used in the following chapters. *) lemma espilon_in_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a. -- 2.39.2