### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# FORMAL LANG & AUTOMATA THEORY COT 5310

University of Central Florida

GPA 3.74

### View Full Document

## 35

## 0

## Popular in Course

## Popular in Engineering and Tech

This 33 page Class Notes was uploaded by Lamont Block on Thursday October 22, 2015. The Class Notes belongs to COT 5310 at University of Central Florida taught by Staff in Fall. Since its upload, it has received 35 views. For similar materials see /class/227695/cot-5310-university-of-central-florida in Engineering and Tech at University of Central Florida.

## Similar to COT 5310 at University of Central Florida

## Reviews for FORMAL LANG & AUTOMATA THEORY

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 10/22/15

Term Rewriting Systems Ferucio Laurentiu Tiplea Visiting Professor School of Computer Science University of Central Florida E mail tiplea csucfedu November 18 2004 6 Term Rewriting Systems Contents 0 Motivations 0 Terms and term rewriting systems 0 Canonical form 0 Proving termination o Proving confluence UCPSQSTelm Rewriting SystenISi dov 132iu39i4F L TiplpJ 6 Term Rewriting Systems Bibliography Term Rewriting Systems Cambridge Tracts in Theoret ica Computer Science 55 Cambridge University Press 2003 884 pages ix F Baader T Nipkow Term Rewriting and All That Cambridge University Press 1998 301 pages UCFig QSTellil Rowiiring Systems40V llt2i39u39i4F L Tiplm 6 Motivations Syntactically rewrite rules are a special kind of equations that can be applied in one direction only A term rewriting system trs for short is a set of rewrite rules They have many applications to o theorem proving o algebraic specification of data types programs etc 0 computer algebra o A calculus o implementation of declarative languages 0 operational semantics of programming languages lJiiFrgtfTellii Frowu ring SystemsNov 1lt2v39u39i4F L Tim 1 6 Motivations Example Ackerman Peter function f N gtlt NHN R1 f07yy1 R2 fw170fw71 R3 fw 1731 1 fw7fw 1731 for all xy N A few values of this function 0 f07yy1 o f17yy2 0 f27y2y3 for ally E N IJKFiS39QSTellll Rowliring Systems40V la2i39it39i4F L Tiplm 6 Motivations Example of computation K271 33 I H f17f270 f17f270 f17f171 f17f171 f17f07f170 f17f07f170 R2IH1 R37 107 ygt0 my f17f07f071 f17f07f071 EH f17f072 mi oa my 173 UKF SQSTQIIII Rowliring Systems40V la2i39it39i4F L Tiplm Motivations Conclusions each element of this computation is a term 0 each computation step is based on applying one of the equations R1 R2 or R3 each equation is used in one direction only from left to right 0 each equation is based on a substitution Mel gap which matches the left hand side of the equation to some subterm of the current term 0 the immediate successor of a term t is obtained by re placing a subterm oft by an instance of the right hand side of some equation LHZFrSi Telin Rewriting SiwgtmnsNCv llt2v39rti4F L Tiplm 6 Terms and Term Rewriting Systems Let f be a set of function symbols each of which having associated an arity and let X be a set of variables Assume that f and X are disjoint sets The set of terms over f and X is defined inductively as follows 0 each function symbol of arity O is a term 0 each variable is a term 0 if t1tn are terms and f is a function symbol of arity n2 1 then ft1tn is a term Function symbols of arity O are usually called constant sym bols Denote by TfX the set of all terms over f and X IJiZFrSi Telin Rewiring SystmnsNCv llt2v39iu4F L Tiplm 6 Terms and Term Rewriting Systems Examples of terms 0 an is a term for any variable as o a is a term for any constant symbol a o facac is a term where f is a function symbol of arity 2 o ffxxa is a term 0 fgaffxxa is a term where g is a function sym bo of arity 1 0 all expressions in the computation f271f173 of the Ackerman Peter function are terms LHZFrSifgTelin FromHing SystmnsNCv llt2v39iu4F L Tiplm 6 Terms and Term Rewriting Systems Variables in a term t Given a term t we denote by Vart the set of all variables occurring int If Vart 2 then t is called a ground term Example if t fxgyxz then Vart 573172 Subterms Given a term t we denote by Subt the set of all subterms oft Example ift fxgyxz then Subt txyzgyz UliF S QSTellll Povviiring SystmnsNcv 1lt2v39u39i4F L Tiplm 6 Terms and Term Rewriting Systems t1t2 also written as Rewrite rule a pair of terms r r t1gtt2 such that 0 t1 is not a variable 0 Vart2 Q Vart1 t1 t2 resp is usually called the left hand side right hand side resp of r and it is denoted by lhsr rhsr resp Example 0 fac 10gtfxl is a rewrite rule 0 neither xa ma nor fx7ygtfOz is a rewrite rule A non empty set of rewrite rules is called a term rewriting Tipll J IJiZFeb STelln Pawxiring SystmnsNcv 1lt2v39u39i4F L system 6 Terms and Term Rewriting Systems Substitution function from X into TfX Example 01XgtT7X given by 090 2 facac 0y a and 02 2 z for all z 7 an and z 7 y Substitutions can be applied to terms They substitute all variables but leave unchanged all function symbols Formally each substitution 0 XHT X is extended to a homomorphism from TfX to TfX which is also denoted by a lJiiFrSifgTelln Rewiring Systmnsl dcv 1lt2v39u39i4F L Tim 1 6 Terms and Term Rewriting Systems Example 0 0fw7w f0w70w ffw7w7fw7w o 0fwigy7wyz f0wygay70w70z ffw7wiga7fw7wyz The domain of a substitution 0 is D0ma 2 an E Xiax 7 an If Doma is finite Doma x1xn we may write a as a set a 140081 7avngtaavn In such a case 0t is usually writen as tx1ax1xnaxn LHZFrSifgTelin FromHing SystmnsNCv llt2v39iu4F L Tiplm 6 Terms and Term Rewriting Systems Unification A substitution 0 is called a unifier of two terms t1 and t2 if 0t1 0t2 Moreover t1 and t2 are called unifiable Example 0 let a XHT X given by 090 2 a 0y a and azz for all 27598 and 2723 0 let t1 fxx and t2 faa o a is a unifier of t1 and t2 0 let t3 fab where b7 a o a is not a unifier of t1 and t3 UliF S QSTellll Pomtiring SystmnsNcv 1lt2v39u39i4F L Tiplm 6 Terms and Term Rewriting Systems Rewriting Let R be a trs Define a binary relation on terms sR as follows t1 Rt2 HT 0 t1 utov where the decomposition utov means that to is a subterm of ti 0 there exist a rule r tat e R and a unifier a of to and t 0 t2 uatv 113 is the transitive closure and gtR is the reflexive and transitive closure of sR IJCFig QSTellil Rovviiring Systmnsl dov llt2i39u39i4F L Tiplm 6 Terms and Term Rewriting Systems Example Let R 71 f07yay17 T21 f00170 f90717 T31 90 1731 1Hf907f90 1730 Then 0 f271gtRf17f270 o f17f270gtRf17f171 o f17f171gtRf17f07f170 o f17f07f1703Rf17f072 Therefore K271 gtR f17f072 JCPS STelm Pomtiring SystmnsNcv 1lt2v39u394F L Tiplm 6 Canonical Form Let R be a trs o R is called terminating or noetherian if there is no infinite sequence of terms t1t2 such that tigtRtZ l for all i2 1 o R is called confluent or Church Rosser if Vtt1t2t gtR t1 t gtR t2 attl 113 tAtg gtR t o R is called canonical or complete if there it is terminating and confluent JFSCfTellll Romlilian Systems40V la2i39it39i4F L Tiplm Canonical Form Exercise Let Rr1 f07ygtyl r2 fxl0gtfxl T31 fltt 1731 1Hfw7fw illD Prove that R is a canonical trs Hint By mathematical induction on an and y lJCPSiSTelln Rowliring Sy it ililSNCW 132iu39i4F L TiplpJ e Canonical Form Let R be a trs and t a term Then 0 t is called irreducible or a normal or reduced form under R if there is not t such that t Rt o t is called a normal or reduced form oft under Rift 113 t and t is a normal form Example Let Rr1 fOygtyl l r2 fxl0gtfxl T31 90 1731 1Hf907f90 1730 Then 0 2 is a normal form 0 f1O RfO1 R2 and therefore 2 is a normal form of f10 UliF S QSTellll Pomtiring SystmnsNcv 1lt2v39u39i4F L Tiplm 6 Canonical Form Theorem 1 If R is a canonical term rewriting system then any term t has a unique normal form Proof Sketch Each term has at least a normal form by the termination property 1ft is a term and t1 and t2 are normal forms of t then t1 t2 by confluence D The unique normal form of a term t under a canonical trs R is called the canonical form oft under R and it is denoted by MR LHZFrSifgTelin Rewiring SystmnsNCv llt2v39iu4F L Tiplm 0 Canonical Form Why canonical forms are important Theorem 2 If R is a canonical term rewriting system then Rlt1t2 lt2 HtlllRZHt2HR7 for any terms t1 and t2 R l t1 t2 means that the equation t1 t2 can be deduced from the equations in R The theorem above provides us with a very natural procedure for deciding the equality of two terms we can decide whether or not t1 and t2 can be proved equal using the equations in R by checking whether their canonical forms are identical LHZFrSi Telin Rewriting SystemsNov llt2v39rti4F L Tiplm 6 Proving Termination Theorem 3 The following problem is undecidable Instance finite term rewriting system B and a term t Question are all computations starting with t terminating Proof Sketch Reduce the halting problem for Turing machines to this prob lem Instance Turing machine M and input w Question does M halt on w associate to M a trs RM and to each configuration 0 a term to such that 0 FM 0 lt2 tc RMtC D IJiiFrSifgTelin Rewiring SystmnsNCv llt2v39iu4F L Tim e Proving Termination Theorem 4 The following problem is undecidable Instance finite term rewriting system B Question is R terminating Proof Sketch Reduce the uniform halting problem for Turing machines to this problem Instance Turing machine M Question does M halt on all inputs IJCFig QSTellil Rnwiiring Systems40V llt2i39u39i4F L Tiplm 6 Proving Termination A trs R is called right ground if each rewrite rule t1gtt2 e R satisfies Vart2 2 Theorem 5 Let R be a right ground trs Then B does not terminate if and only if there exists a rule t1gtt2 e R such that t2 113 utg u ie t2 is a subterm of utgv Corollary 1 Termination for finite right ground trs is decid able lJiiFrSifgTelln FromHing SystemsNov 1lt2v39u39i4F L Tim 1 6 Proving Termination Decision procedure for the termination of right ground trs consider all right hand sides of the rewrite rules in R and simultaneously generate all reduction sequences starting with these terms ix if B does not terminate then there exists a right hand side t2 which generate utg u for some u and v where t2 is a subterm in th U Moreover ut2 U is obtained after finitely many steps A if R terminates then all computation trees are finite and they can be obtained after finitely many steps LHZFrSifgTelin Rewiring Systmnsl JCV llt2v39iu4F L Tiplm Proving Termination Therefore after finitely many steps 0 either we get a term utg u for some u and v where t2 is a subterm in utg u and in this case B does not terminate 0 or all computation trees associated to the right hand sides of the rewrite rules in R are finite and in this case B is terminating Example Let Rfxxgtga gxgtfgab Then 9a iR MaLbL which shows that R is not terminating LHZFrSi Telin Rewriting SystemsNov llt2v39rti4F L Tiplm Proving Termination Techniques for proving termination see 1 for details 1 semantic methods based on suitable interpretations a well founded monotone algebras b polynomial interpretations 2 syntactic methods based upon orders on terms a recursive path order b Knuth Bendix order 3 transformational methods based on applying transfor mations to term rewriting systems a dummy elimination b semantic labeling c abstract commutations LHZFrSi Telin Rewriting SystemsNov llt2v39m4F L Tiplm 6 Proving Confluence Theorem 6 The following problem is undecidable Instance finite term rewriting system B Question is R confluent Proof Sketch Reduce the word problem to this problem Instance set E of equations Question does t1 t2 can be deduced from E Vt1t2 associate to E a trs RE such that the word problem for E is decidable iff R is confluent D LHZFrSifgTelin Rewiring SystmnsNCv llt2v39iu4F L Tiplm e Proving Confluence A trs R is locally confluent if Vtt1t2t Rt1 tgtRt2 attl 113 t t2 gtR t Lemma 1 Newman Lemma Let R be a terminating trs Then R is confluent iff it is locally confluent Theorem 7 Confluence of finite and terminating trs is de cidable IJCFig QSTellll Romtiring Systems40V llt2i39u39i4F L Tiplm A Factor Replacement System FRS is a finite set of pair of positive integers F a1b1 anb Each pair is called a rule and may be denoted as a fraction biai or a grammar style rule aix bix or as a pair as shown in the definition A configuration ID x of a FRS is a positive integer A rule biai is enabled by some ID x ifx is divisible by a Computation is defined by multiplying x by the fraction biaiprovided the rule is enabled by x We define derivation in F by x F y iff y x x bawhere x is divisible by a The concept of derivation in zero or more steps 3 is then the reflexive transitive closure of 2F As usual we omit the F if it is understood by context The derivation or word problem for F is then the problem to determine of two arbitrary positive integers x and y whether or not x 3 y Ordered Factor Replacement Systems are merely FRS s where the rules are totally ordered and x 2 y iff y x x biaiwhere x is divisible by a and x is not divisible by any a jlti The halting problem for an ordered FRS F is the problem to determine of an arbitrary positive integer x whether or not there is some y such that x 2 y and y is terminal meaning that there is no 2 such thaty F 2 This means that y enables no rules An alternative version says there is no 2 z y such that y F 2 This allows termination by reaching a fixed point rather than having no applicable rule FRS s are not computationally complete whereas ordered FRS s are The notion of computation with ordered FRS s is typically to start with inputs as the exponents of successive primes starting with 3 eg if we call the Oth prime 2 the first 3 etc then 3X15X2 pquotquot represents a start with input x1 x2 xn When termination occurs we have the answer as the exponent of po 2 That is forfunction f FRS F computes f if for all x1 x2 xn 3X15X2 pnxquot 2 p0 quotquot quot Z where Z contains no factors of 2 Moreover the last ID above is terminal or a fixed point A Factor Replacement System with Residue is a finite set of quads of positive integers F a1b1c1d1 anbcd Each quad is called a rule and may be denoted as a a grammar style rule aix b cix d or as a quad as shown in the definition A configuration ID x of a FRS is a positive integer A rule aix b is enabled by some ID w ifw aix b for some positive integer x We define derivation in F by W F y iff y cix d where w aix bi The concept of derivation in zero or more steps 3 is then the reflexive transitive closure of 2F As usual we omit the F if it is understood by context The derivation or word problem for F is then the problem to determine of two arbitrary positive integers x and y whether or not x 3 y There is no need for a notion of ordered FRS s with residue as the unordered variety are complete computational devices The halting problem for an FRS with residue F is the problem to determine of an arbitrary positive integer w whether or not there is some y such that w 2 y and y is terminal meaning that there is no 2 such that y F 2 This means that y enables no rules An alternative version says there is no 2 z y such that y F 2 This allows termination by reaching a fixed point ratherthan having no applicable rule The notion of computation with FRS s with Residue is typically to start with inputs as the exponents of successive primes starting with 3 eg if we call the Oth prime 2 the first 3 etc then 3X15X2 pquotquot represents a start with input x1 x2 xn When termination occurs we have the answer as the exponent of po 2 That is forfunction f FRS F computes f if for all x1 x2 xn quot1 X2 pnxquot F po X1 X2quotquot quot Z where Z contains no factors of 2 Moreover the last ID above is terminal or a fixed point Of course these can compute multiple values so we restrict ourselves to FRS s with residue that have no overlapping rules That is for ii there is no w that enables both i and j A Petri Net is a 4tuple P STFW where S is a finite nonempty set of places or nodes T is a finite nonempty set of transitions 8 m T 9 F g SxT U TxS is the flow relation one associated with each transition W SxT U TxS a N is the weight function where Wxy 0 iff Xy e F A configuration ID M of a Petri Net aka a marking is a point in nonnegative integer S space The ith element of the marking vector Mi specifies the number of markers in the corresponding place Computation is defined by the firings of transitions A transition teT is enabled by some marking M denoted Mtgt if Wst 2 Ms for all seS lf teT is enabled by M then t may fire If it fires then M is changed to M where M s Ms Wst Wts for all seS We denote a single step derivation by firing t as M tgt M We define derivation in P by M gtp M iff M tgt M for some teT The concept of derivation in zero or more steps gtp is then the reflexive transitive closure of gtp As usual we omit the P if it is understood by context The derivation or word problem for P is then the problem to determine of two arbitrary markings M and M whether or not M gtp M Ordered Petri Nets are merely Petri Nets where the transitions are totally ordered and M tgt M ifft is the least numbered transition enabled by marking M The halting problem for an ordered Petri Net P is the problem to determine of an arbitrary marking M whether or not there is some M such that M gtp M and M is terminal meaning that there is no M such that M gtp M This means that M enables no transition For normal unordered transitions Petri Nets we are often interested in knowing if any firing sequence will lead to a deadlock defined as a terminal marking It is important to see that this is a different problem than halting since there can be many marking sequences in a normal Petri Net but only one such sequence in an ordered Petri Net Petri Nets are not computationally complete whereas ordered Petri Nets are The notion of computation with ordered Petri Nets is typically to start with inputs x1 x2 xn as the contents of successive nodes starting with node 1 and assuming a node n1 that will contain the answer That is for function f Petri Net P computes f if for all x1 x2 xn ltx1 x2 xn O Ogt gtp lt fx1 x2 xn gt Moreover this last ID is terminal A Vector Addition System VAS is a 4tuple V n R where n is a positive integer R is a finite nonempty set of rule vectors in integer nspace A configuration ID u of a VAS is a point in nonnegative integer nspace Computation is defined by the application of rule vectors A rule vector r ltr1 rngteR is enabled by some point u ltu1 ugt denoted urgt if u 2 ml for all r lt 0 If reR is enabled by u then r may be added to u If it is then u is changed to w where w u r We denote a single step derivation by firing r as u rgt w We define derivation in V by u w w iff u rgt w for some re R The concept of derivation in zero or more steps V is then the reflexive transitive closure of V As usual we omit the V if it is understood by context The derivation or word problem for V is then the problem to determine of two arbitrary points in nonnegative integer nspace u and w whether or not u w w Ordered VAS s are merely VAS s where the rule vectors are totally ordered and u rgt w iff r is the least numbered rule vector enabled by point u in nonnegative integer nspace The halting problem for an ordered VAS V is the problem to determine of an arbitrary point u in nonnegative integer nspace whether or not there is some w in nonnegative integer nspace such that u w w and w is terminal meaning that there is no x such that w gtp x This means that w enables no rule vector For normal unordered rules VAS s we are often interested in knowing if any derivation sequence will lead to a deadlock defined as a terminal point It is important to see that this is a different problem than halting since there can be many alternate derivations in a normal VAS but only one such sequence in an ordered VAS VAS s are not computationally complete whereas ordered VAS s are The notion of computation with ordered VAS s is typically to start with inputs x1 x2 xn as the contents of successive coordinates starting with the first and assuming an n1st coordinate that will contain the answer That is for function f VAS V computes f if forall x1 x2 xn ltx1 x2 xn O Ogt V lt fx1 x2 xn gt Moreover this last ID is terminal

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

#### "I signed up to be an Elite Notetaker with 2 of my sorority sisters this semester. We just posted our notes weekly and were each making over $600 per month. I LOVE StudySoup!"

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.