[PDF] A Proof Method based on Folding Lemmas: Applications to

View - Download A Proof Method based on Folding Lemmas: Applications to

Previous PDF

Next PDF

APro ofMetho dbasedonFoldingLemmas?ApplicationstoAlgorithmCorrectnessSta?anBONNIER

?LaurentFRIBOURGLab oratoired?Informatique? URA 1327du CNRSD?epartement de Math?ematiques et d?InformatiqueEcole Normale Sup?erieure

Link?opingUniversity? SwedenLIENS ? 92?28Decemb er 1992 APro ofMetho dbasedonFoldingLemmas?ApplicationstoAlgorithmCorrectnessSta?anBonnier

1? LaurentFrib ourgL?I?E?N?S ?URA 1327CNRS? ? 45rue d?Ulm? 75005Paris ?Francee?mail:b onnier?frib ourg?dmi?ens?frAbstract

In?Fri92?apro ofmetho dwasdevelop edforprovingarithmeticconse?quencesofHornclauseprograms de?nedoverintegerlistsandintegers?Tob eapplicable?themetho drequirestherecursionschemesofallpredicatesinvolvedtob ecompatible?Thisistoguaranteeasequenceofunfoldtrans?formations to eventuallyleadto a foldableclause?Inthispap erwe considerthecasewhensuchacompatibilityisnotpresent?To enablefoldingfoldinglemmasare constructed?The pro of then pro ceeds using the old metho d? andthetheoremisproved withthelemmasashyp otheses?Themetho disillus?trated by proving correctness criteria for Boyer and Mo ore?s string matchingalgorithm and for Dijkstra?s descendingsubsequencealgorithm?1Intro ductionIn ?Fri92?? ametho d wasdevelop ed forproving implications of the form:p

1 ?L? X1 ??? ? ??pn ?L?Xn ? ??a?X1 ? ? ?Xn ?whereLis a list variable? each Xi is avector of integer variables? anda?X1 ? ? ?Xn

?is anarithmetic formula?The metho d works by transforming the hyp othesis oftheimplication into an arithmetic formulab?

X1 ? ? ? ?Xn ?? satisfying the equivalence:9L:p1 ?L? X1 ??? ? ??pn ?L?Xn ???b?X1 ? ? ? ?Xn ?Proving the initial implication is thus reduced to proving the arithmetic formula:b? X1 ? ? ? ?Xn ???a?X1 ? ? ?Xn

1On leave from Link?oping University? Link?oping? Sweden?Financial supp ort from the SwedishNational Board for Industrial and Technical Development and from the Swedish Institute is grate?fully acknowledged?1

A crucial step in generatingb?X1

? ? ? ?Xn ? is the synthesis of a new predicatep? suchthat:p?L? X1 ? ? ?Xn ???p1 ?L?X1 ??? ? ??pn ?L?Xn ?This synthesis is done by applying the unfold?fold transformations due to Sato and

Tamaki ?TS84 ? to the conjunctionp1

?L? X1 ??? ? ??pn ?L?Xn

??Inadditiontothebasicscheme in?Fri92??several extensionsofthemetho dareconsidered?suchastheadmissionofmorethanonelistvariable?Animp ortantassumption made in ?Fri92? which is common toall extensions is that the recursionschemes of thepi

?s are compatible? and? moreover? that the b o dy of a recursive clausede?ningsomepi

containsonlyarithmeticconstraintsinadditiontotherecursivecall?Thisis essential forthe unfoldingtransformationstoeventually yield aclausewhich can b e completely folded? and hence for making the synthesis of the predicate

pp ossible?Itmayhoweverb edesirabletoallowoneormorepi

toviolatetheserestrictions?Inparticularthisisthecasewhenformulating correctnesscriteria foralgorithms; Several algorithms? which are themselves de?ned in terms of subroutines?do indeed contain extra literals in conjunction with the recursive calls when enco dedasHorn clause programs?Inthispap erwedevelopanextensionofthemetho dgivenin?Fri92??Inordertomake foldingp ossiblealsointhepresence ofpredicatesviolatingthementionedrestrictions?theextendedmetho dallowsaruleoffoldingenablingtob eappliedduring the synthesis ofp?The rule allows replacements of b o dies of clauses? so thatan unfoldable clause can b e turned into a foldable one?The prerequisites of applyingtherule constitutefoldinglemmasonwhich the?nalpro ofrelies? andwhich henceneed to b e proved separately?We then apply the extended metho d in order to provecorrectnesscriteriaforBoyerandMo ore?sstringmatchingalgorithm?BM79?andfor Dijkstra?sdescending subsequence algorithm ?Dij80??Thepap erisorganizedasfollows:Section2presentsthegeneralaimofthemetho d? andintro ducessome notionsandnotationusedin theremaining sections?Section 3 describ es the principles b ehind thebasic method? that is? the pro of metho ddevelop ed in ?Fri92??The limitations of the basic metho d which serve as motivationforthepresentpap erarealsodiscussedinthissection?Thefollowingsectioncon?stitute the core of the pap er in that it intro duces the notions offoldinglemmasandfoldingenabling?Finally?Section5presentstwoapplicationsofthenewmetho d?andthe pap eris then concluded in Section 6?2GeneralAimLet in the following ? denote a program de?ning certain predicates?It will withoutfurther mention b e assumed that each argument of these predicates is either of typ e?non?negative? integer or of typ e list of ?non?negative? integers?Standard arithmeticpredicatesareallowedtoo ccurintheb o diesoftheclausesin??Ourgeneralaim2

is todesign ametho d forproving

2formulae ofthe form:A

1 ?? ? ??An ??I?1?whereA1 ? ? ? ? An

are atoms de?ned by ?? and whereIis an arithmetic formula?Wefurthermorewishthemetho dtocarryouteachpro ofbyusingA1

?? ? ??An togenerate anarithmetic formulaJsuch that:A 1 ?? ? ??An

??J?2?andhencetoreducetheproblemofproving?1?tothatofprovingthearithmeticimplication:J??I?3?The formulaJshould thus b e as strong as p ossible?Indeed? ideally it should satisfy:?9

L:A1 ?? ? ??An ???J?4?where Lis the vector of all list variables o ccurring inA1 ?? ? ??An ?When ?2? holds?the metho d is said to b ecorrect?forA1 ?? ? ??An ??When ?4? holds? the metho d issaid tob ecomplete?forA1 ?? ? ??An

??3TheBasicMetho d3?1GeneralprinciplesThe pro of metho d presented in this pap er extends the metho d develop ed in ?Fri92??

This latter metho d will from now onb e referred to asthebasicmethod?It relies initself on Sato and Tamakis unfold?fold transformation system ?TS84 ? with which thereaderisassumedtob efamiliar?Inordertogiveanaccountofthebasicmetho dwe ?rst need tode?ne the op erationofpro jection?Tosimplify notationwe assumein the following that each atom is of the formp?

L ?N?? whereLis the vector of listarguments and

Nis the vector ofinteger arguments?De?nition3?1Theprojectionofp?

L ?N?istheatomp

??N??wherep ?isanewpredicate corresp ondingtop?ByP ?wedenotethe programobtainedby replacingeach nonarithmetic atom inPby its pro jection? Thefollowingarethestepsprescrib edbythebasicmetho d?startingfromthehy?p othesisA1 ?? ? ??An in ?1?:Step1?De?ne anew predicatep?noto ccurring in ?? by the equivalenceE:p?

L?N???A1

?? ? ??Anwhere

L?Nareall variableso ccurring inA1

? ? ? ? An

2That is? proving the truth in the least mo del of ? over the domain of non?negative integers?3

Step2?Let? b e the result ofapplying unfold?fold transformationsto ?? fEg?

3Step3?Pro ject ? toobtain?

??Step4?Generate anarithmetic formulaJ? such that:J? N???p ??N?holdsin the leastmo del of?

??Incertain casestheformulaJinStep4may b egeneratedby anextended form ofb ottom?up evaluation?FVP92??Example 3?2Supp osewe wishto prove that:min?L?M??memb?E?L???M?Ewhereresp ectivelymin?L?M?andmemb?E?L?holdsi?Mistheminimal element ofthe listL? andEis a memb er ofL?The following clauses de?ningminandmembareassumed to b ein ?:min??X??X??memb?X??X?L???min??X?L??X???memb?X??Y?L????min?L?Y??memb?X?L??X?Y?min??X?L??Y???min?L?Y??X?Y?InStep1the following equivalenceEis de?ned:p?L?M?E???min?L?M??memb?E?L?By doing unfold?fold computations inStep 2we arrive at the program ? containingthe following clauses? in additionto the clausesde?ningmin:p??XjL??X?X???p??X??X?X??min?L?Y??X?Y?p??XjL??M?X???min?L?M??X?M?p??XjL??X?E???p??XjL??M?E???X?Y?X?M?p?L?Y?E??p?L?M?E??Pro jectionof?inStep3thusyieldstheprogram?

??containingthefollowingclauses in addition tothe pro jection of the clauses de?ningmin:

3We also allow here the removal of clauses on which the de?nition ofpis not dep endent?4

p ??X?X???p ??X?X??min ??Y??X?Y?p ??M?X???min ??M??X?M?p ??X?E???p ??M?E???X?Y?X?M?p ??Y?E??p

??M?E??TakingJ?M?E?inStep4tob eM?E?itisnoweasilyseenthatthefollowingequivalence holdsin the least mo del of?

?:p ??M?E???J?M?E?Thusthe pro ofof the originaltheorem hasb een reduced toproving:M?E??M?E

3?2CorrectnessBythede?nitionofpmadeinStep1?andbythefactthattheunfold?foldtrans?formationsinStep2preservetheleastmo delofaprogram?TS84??thefollowingimplication holds in the least mo del of???:?9

L:A1 ?? ? ??An ????9L:p?L ?N???5?Furthermore?asiseasilyseen?thegroundatomp n?hasanSLD?refutationin? ?wheneverthisisthecaseforp?

l ?n?in??Thus?bythecompleteness ofSLD?resolution?Llo87?andbythe de?nitionofJinStep4?the implications b elow holdin the least mo del of ?

???:?9

L:p?L ?N????p

??N???J?N??6?By?5???6?andthefactthat?do esnotde?nep?wemaynowconcludethatthefollowing implication holds in the least mo del of?:A

1 ?? ? ??An ??J?

N?This settles the correctness of the basicmetho d?3?3LimitationsDuetothe equivalence preservationoftheunfold?foldrules? theimplication in ?5?isinfactbidirectional?Furthermore?in?Fri92?certainsyntacticalconditionsonA

1 ?? ? ??An

and ? were imp osed? e?ectively ensuring the program ? resulting fromStep 2to b eindependentofitslistarguments?5

De?nition3?3? is said to b eindependentofitslistargumentsi?? for each predi?cateqde?ned by ?? the following equivalence holdsin the least mo del of?

???:?9

L:q?L?N????q

??N?

Hence?fortheclassofproblemsconsideredin?Fri92??alsothe?rstimplication in?6?is bidirectional? andthe basic metho d isthus complete?In general however? the unfold?fold transformation system is not p owerful enoughto transform ?? fEginto a program which is indep endent of its list arguments?Moregenerally; restricting thetransformationsinStep 2tounfoldingandfoldingputsade?nite limit to the class of theorems provable by the basic metho d:The implication?1?canb eobtainedonlyifthereexistsasequenceofunfold?foldtransformationsresulting in ?? such that:p

N? ??Iholds in the least mo del of?

???7?Themain obstacle inachieving ?7?isthatfolding?intro ductionofrecursion?oftenis notapplicable due tothe syntactical form ofthe unfolded clauses?Example 3?4Letthe equivalenceEde?ned in Step 1b e:p?L?N1?N2???a1?L?N1??a2?L?N2??Supp osethe following arethe clauses in ? de?ninga1anda2:a1?l1?n1??a2?l2?n2??a1?L?f1?N????a2?L?f2?N????e1?T?L??e2?T?L??a1?T?N??a2?T?N??ThenEunfolds into clauses 1to4 b elow:1p?L?n1?n2???L?l1?L?l2?2p?l1?n1?f2?N2????e2?T?l1??a2?T?N??3p?l2?f1?N1??n2???e1?T?l2??a1?T?N??4p?L?f1?N1??f2?N2????e1?T1?L??a1?T1?N1??e2?T2?L??a2?T2?N2??UnfoldingofthelastclausecanonlyleadtoaclausefoldablebyEife1ande2?when unfolded? identifyT1andT2?

6

4ExtendingtheBasicMetho d4?1AimoftheextensionOuraim istoallowothertransformationsinStep2thanunfoldingandfolding?sothat the resulting program ? is guaranteed to b e indep endent of its list arguments?Thatis?completeness shouldnotb elostwhenpro jecting?inStep3?Sinceinde?p endenceoflistargumentsisaquiteunmanageableprop ertyofprograms?itisinfact undecidable?? we ?rst intro duce asu?cient condition for it tohold?Lemma 4?1Supp ose? satis?esthe following two conditions:1?No list variable o ccurs more thanonce in the b o dyofa clause in ??2?Foreachheadp?

Lh?N h?ofaclausein??andforeachatomp?Lb?N b?o c?curring in the b o dyofa clause in ?? Lhis aninstance ofLb?Then ?is indep endent ofits list arguments?

TheconditionprovidedbyLemma4?1isstrictlyweakerthantheconditionsonlist?recursiveness givenin?Fri92??Thenexttaskisthustoreformulate Step2?Tothisendwewillsaythattransformationsappliedtoobtain?from?? fEgarecorrectnesspreservingi?theimplication?5?holdsintheleastmo delof????Whentheconverseoftheimplicationholds?thetransformationsaresaidtob ecompletenesspreserving?Step 2a b elow now provides a ?rst approximation of a newversion of Step 2:Step2a?Let?b eaprogramsatisfyingLemma4?1?suchthat?istheresultofcorrectness preserving transformationsof ?? fEg?Notethattheimplications?5?and?6?arestillvalid?sothemetho dobtainedbyreplacing Step 2 by Step 2a is also correct?As already p ointed out? the requirementon? tosatisfy Lemma 4?1 furthermore ensures that?6?can b e replaced by:?9

L:p?L ?N????p

??N???J?N?Thus?wheneverthetransformationsinStep2aarecompletenesspreserving?thegenerated arithmetic expressionJsatis?es ?4?? i?e?the metho d is complete?We will however not worry so much ab out completeness preservation of the newrules; As long as some order of their application yields a ?nal ? such that ?7? holds?they are ?su?ciently? complete for provingthe theorem athand?7

4?2GoaldeletionGoaldeletion allowstheremoval ofarbitraryatomsinb o diesofclauses?LetPb eaprogram andletCb e aclause?The rule may then b eformulated asfollows:Goal deletionallowsP? fCgto b e transformed intoP? fC

0g? whereC

0is obtainedfromCby the removal ofone ormore b o dyatoms inC?

Adding goal deletion to the unfold?fold system do es not violate correctness preserva?tion of the transformations in Step 2?Completeness is however usually not preserved?It is worthwhile noting that by the application of goal deletion? any program can b etransformedintoonewhichsatis?estherequirementsinLemma4?1?Thus?whengoaldeletion is p ermitted? Step 2acanalways b e carried out successfully?4?3FoldingenablingAs p ointed out in Section 3?3? the limitations of the basic metho d b ecome apparent

whenunfolding in Step2do esnotlead tofoldable clauses?Our aim is therefore tointro duce a transformation rule which allows folding to b e enabled in situations sim?ilar to the one in Example 3?4?What we have in mind is essentially a variant of thegoalreplacement rule in ?TS84 ??More precisely? the rule shouldallow replacementsof b o diesof clauses? so thatan unfoldable clause can b eturned into a foldable one?The prerequisites of applying the rule will then constitute afoldinglemmaon whichthe ?nal pro ofwill rely?De?nition4?2LetCb eaclauseH:?B1

? ? ? ? Bm ?where eachBi isbuilt from apredicatede?nedby??AfoldinglemmaforCandtheequivalencep?

L?N???A

1 ?? ? ??An is a conjunction?oftwo implications of the forms 1 and2b elow:1?B1 ?? ? ??Bm ??9 L

0:?L2?B1

?? ? ??Bm ??L ??9 N 0:A 01 ?? ? ??A 0n ??Nwhere:?EachA 0i isobtainedfromAi bythereplacementof

L?Nfornewvariables

L 0?N

0noto ccurring inHor inB1

? ? ? ? Bm ???N is anarithmetic expression? called theintegerrelationof????L isa conjunction ofatoms? called thelistwitnessof?? 8

Usingthesame notationasinDe?nition 4?2?therule offoldingenablingmay nowb e formulated asfollows:Folding enablingallowsP?fH:?B1

? ? ? ? Bm gto b e transformed into the programP? fH:??N ? A 01 ? ? ? ? A 0n g?The transformationis said tob ejusti?edby?? The purp ose of the integer relation is to preserve certain arithmetic consequences ofB 1 ?? ? ??Bm and to provide an appropriate relation in b etween the integer variablesinHand those in N

0?Note that without such a relation? the program resulting fromfoldingenablingcanb eusedtoderive thatanyintegersareintherelationde?nedbyH?assuming that9

L 0:A 01 ?? ? ??A 0n

holdsin the least mo del of ???Thepurp oseofthelistwitnessisjusttosp ecifyvaluesforthelistvariablesin

L

0? and hence to facilitate the realization ?the pro of ?that the second implication of?holdstrue?sinceotherwiseapro ofofthisimplication wouldrequiretheexplicitconstruction ofappropriate lists?In all subsequent examples? the list witnesses willhave the form:L

01 ?L1?? ? ??L 0n ?LnwhereL 01 ? ? ? ? L 0n areallvariablesin L

0?Henceimplication1inDe?nition4?2willhold trivially and will therefore in general b e omitted?Example 4?3Any folding lemma for clause 4 andEin Example 3?4 has the form:e1?T1?L??a1?T1?N1??e2?T2?L??a2?T2?N2???9L???L?e1?T1?L??a1?T1?N1??e2?T2?L??a2?T2?N2???L

??9N1?? N2??a1?L??N1???a2?L??N2??When taking for instance ? L to b eL

0?T1and ?N

to b eN1

0?N1?N2

0?g?N1?N2??the ab ove lemma immediately reduces to:e1?T1?L??a1?T1?N1??e2?T2?L??a2?T2?N2???a2?T1?g?N1? N2??

Itstillremainstogiveconditionsunderwhichfoldingenablingtogetherwithun?foldingandfoldingyieldscorrectnesspreservingtransformations?Thiswillb ethe9

casewhenthefollowingtwoconditionshold?Thenotationisthesameastheoneused in De?nition 4?2:Correctnessconditions?1??holds in the least mo del of??2?For each groundsubstitution?forHthere is a groundsubstitution?fortheremaining variables in?? such that if ?B1

?? ? ??Bm ??L ?? ?holds in the leastmo del of ?? then:??N ? ?holdsin the leastmo del of?? and?EachA 0i ?hasarank?consistentproofintheprogramresultingfromthefolding enablingjusti?ed by??

Condition2isneededtoensurethatinvariantI2in?TS84 ?ispreserved?Thiscondition will however not b e further considered in this pap er?The reader is insteadreferredto?TS84 ?forthede?nitionofrank?consistencyandforconditionsunderwhich it holds?4?4TheextensionWe can nowmake a?nal reformulation of Step2 ofthe basic metho d:Step2f?Let?b eaprogramsatisfyingLemma4?1?suchthat?isobtainedbytransforming ?? fEgusing unfold?folding? goal deletion and folding enabling?5TwoExamples5?1TheBoyer?Mo orestringmatchingalgorithmTheproblemThe Boyer?Mo ore string matching algorithm ?BM79? deals with the problem of ?nd?

ing the p ositionof the ?rst o ccurrence of a patternPin a stringS?Let us call thisp osition?whenitexists? thestringpositionofthepatterninthestring?andlet usdenote it??P ? S??Forinstance? if the pattern is:P?123andthe string is:S?121241231234then??P?S? is5?assuming the numb ering of the p ositionsstartswith0??10

PrinciplesofthealgorithmLet resp ectivelyP?i? andS?j? denote thei?th and thej?th element in the patternPand the stringS?Let furthermorenb e an integer less thanthe length ofPand letdb e an integer less than or equal ton?The main insight underlying the correctnessofBoyer andMo ore?salgorithm can nowb e expressed by the formula??n? d?:??n? d???8i:n?d?i?n??P?i?6?S?n??????P ? S??d? 1?8?Informally??n? d? can b e explained as follows; Supp oseScontains the elementeinitsn?th p osition?Supp osefurthermore that then?th p ositioninP? aswell asthedconsecutive p ositions to the left of then?th? contain elements distinct frome?Thenthestringp ositionofPinSmustb eatleastd? 1?Hence?whencomputingthestring p ositionit is safestarting searching forPfrom thed? 1?th p ositioninS?LettingjPjandjSjresp ectively denotethelengthsofSandP?andlettingSjidenotethesu?xofSobtainedbyremoving the?rstip ositionsofS?wemay nowgive the following informal recursive formulation ofBoyer andMo ore?s algorithm:?BAS?IfjPj?jSj? then??P ? S? is unde?ned?IfPmatchesS? then??P ? S? ? 0??REC?Supp osejPj ? jSjandthatPdo esnotmatchS?Letnb ethelast?largest?p ositionsuchthatP?n?6?S?n??andletdb ethelargestnumb ersuchthat??n? d? in ?8?holds?Then??P ? S? ???P ? Sj?d? 1?? ?d? 1?The following is atrace of the algorithm whenPandSare de?ned asab ove:P?123andS?121241231234Thelastmismatch isthep ositionn?2?withS?2? ?1?Thusd?1?andwedropthe two ?rstp ositionsofS?P?123andS?1241231234Thelastmismatch isagainn?2?butS?2? ?4whichdo esnoto ccurinP?sowehave alsod?2?Droppingthe three ?rstp ositionsofSnowyields:P?123andS?1231234Thus a match is found?In the concrete formulation of the algorithm given in ?BM79??thesearch fornstartsfrom theendofPandpro ceedstowardsitsb eginning?Themain reasonfor the e?ciency ofthe algorithm is thatthe function which computesdwhengivennandS?n?canb ecompletely synthesized fromPintoane?cientlyaccessible ?nite table?11

Thede?nitionofacorrectnesscriterionOur aim is to apply the pro of metho d in order to prove ?8? whennanddare chosenasintherecursivecaseoftheformulationofthealgorithm?Thetheoremtob eproved may thus b eexpressed as follows:strpos?P?S?Pos??lastnomatch?P?S?C?Nm??delta?C?Nm?P?D???Pos?D?1wherebrief descriptionsofeachofthepredicatesstrpos?lastnomatchanddeltaare given b elow together with their de?nitions:strpos?P?S?Pos?holdsi?PmatchesSatp ositionPos?Thusstrposdo esinfactgeneralize?asitwasde?nedab ove?Itshouldhoweverb eemphasizedthatthepro ofcouldb ecarriedoutjustaswellwithoutthisgeneralization?The reason for doing it is to keep the pro of free from certain irrelevant detailswhich wouldobscure the presentation?strpos?P?S?0???match?P?S??strpos?P??X?S??Pos?1???strpos?P?S?Pos??The predicatematchis de?ned in the standard way?We will however not applyunfolding tomatch? andtherefore its de?nition is notgiven explicitly?lastnomatch?P?S?C?Nm?holdsi?Nmisthelastp ositiononwhichPandSdonotagree? andCis the element attheNm?s p ositioninS?lastnomatch??X?P???Y?S??C?0???X6?Y?match?P?S??lastnomatch??X?P???Y?S??C?Pos?1???lastnomatch?P?S?C?Pos??delta?C?Nm?P?D?holdsi?thereareexactlyDconsecutivep ositionsnotcon?tainingCtothe left ofp ositionNminP?delta?C?0?P?0??delta?C?D?1??C?P??D???delta?C?D?P?D??delta?C?D?1??X?P??D?1???C6?H?delta?C?D?P?D??delta?C?Nm?1??X?P??D???D?Nm?delta?C?Nm?T?D??12

Thepro ofStep1is carried outby de?ning the equivalenceE:p?P?S?Pos?D?Nm?C???strpos?P?S?Pos??lastnomatch?P?S?C?Nm??delta?C?Nm?P?D?Step2fis commenced by unfoldingstrposinE? which yields the two clauses:1?1p?P?S?0?D?Nm?C???match?P?S??lastnomatch?P?S?C?Nm??delta?C?Nm?P?D??1?2p?P??X?S??Pos?1?D?Nm?C???strpos?P?S?Pos??lastnomatch?P??X?S??C?Nm??delta?C?Nm?P?D??Unfold?fold transformations of a new predicate? de?ned to b e equivalent to the b o dy

of clause 1?1? would show that this b o dy can not b e satis?ed ?b ecause of the presenceofmatch?P?S? andlastnomatch?P?S?C?Nm???Thus clause 1?1 can b e discarded?Unfolding oflastnomatchin 1?2nowresults inthe following clauses ?wheredeltahasb een subsequently unfolded toobtain1?2?1?:1?2?1p??Y?P???X?S??Pos?1?0?0?X???strpos??Y?P??S?Pos??Y6?X?match?P?S??1?2?2p??Y?P???X?S??Pos?1?D?Nm?1?C???strpos??Y?P??S?Pos??lastnomatch?P?S?C?Nm??delta?C?Nm?1??Y?P??D??Applyinggoaldeletiontoremovetheb o dyofclause1?2?1givesaunitclauseasresult:1?2?1?1p??Y?P???X?S??Pos?1?0?0?X??Unfolding ofdeltain clause 1?2?2 ?nally yields:1?2?2?1p??Y?P???X?S??Pos?1?Nm?Nm?1?Y???strpos??Y?P??S?Pos??lastnomatch?P?S?Y?Nm??delta?Y?Nm?P?Nm??13

1?2?2?2p??Y?P???X?S??Pos?1?Nm?1?Nm?1?C???strpos??Y?P??S?Pos??lastnomatch?P?S?C?Nm??Y6?C?delta?C?Nm?P?Nm??1?2?2?3p??Y?P???X?S??Pos?1?D?Nm?1?C???strpos??Y?P??S?Pos??lastnomatch?P?S?C?Nm??D?Nm?delta?C?Nm?P?D??It is clear that further unfolding of clauses 1?2?2?1 to 1?2?2?3 do es not lead to clauses

foldablebytheinitialequivalenceE?Thus?inordertoapplyfoldingenabling?weconstruct the following three folding lemmas:??1strpos??Y?P??S?Pos??lastnomatch?P?S?Y?Nm??delta?Y?Nm?P?Nm???L1

N1 ?Pos

0?Pos?1?C

0?Y?Nm

0?Nm?D

0?Nm? L1 ?P 0?P?S 0?S N2 ?Pos

0?Pos?1?C

0?C?Nm

0?Nm?D

0?Nm?Y6?C??Pos?Nm??Y?C??

L2 ?P 0?P?S 0?S ??9Pos??C??Nm??D??14 N3 ?Pos

0?Pos?1?C

0?C?Nm

0?Nm?D

0?D? L3 ?P 0?P?S

0?SFolding enabling justi?ed by??1 to??3followed by folding nowyields:1?2?2?1?1p??Y?P???X?S??Pos?1?Nm?Nm?1?Y????

N1 N2 N3

?p?P??S??Pos??D??Nm??C???Itisclearthatthepresentprogram??consistingofclauses1?2?1?1?1?2?2?1?1?1?2?2?2?1and1?2?2?3?1?satis?estherequirementinLemma4?1?Thusnofurthertransformationsareneeded?Step3consistsinpro jecting?toobtaintheclausesb elow:1?2?1?1?p

??Pos?1?0?0?X??1?2?2?1?1?p ??Pos?1?Nm?Nm?1?Y???? N1 ?p ??Pos??D??Nm??C???1?2?2?2?1?p ??Pos?1?Nm?1?Nm?1?C???? N2 ?p ??Pos??D??Nm??C???1?2?2?3?1?p ??Pos?1?D?Nm?1?C????quotesdbs_dbs19.pdfusesText_25

[PDF] TP Informatique no 8 Algorithme de Dijkstra - Arnaud Jobin

[PDF] TD d 'algorithmique avancée Corrigé du TD 11 : Plus courts chemins

[PDF] corrigé - Irif

[PDF] Algorithmes de factorisation des entiers

[PDF] Reconnaissance de caractères ? l 'aide de réseaux de neurones

[PDF] - Partie 6 - Routage IP

[PDF] Programmation Problème de seuil TI 82-statsfr

[PDF] Correction TD1 algorithme

[PDF] Second degré - Académie en ligne

[PDF] Chapitre 6 Algorithmes numériques

[PDF] LES ÉTAPES DE L 'ALGORITHME DU SIMPLEXE

[PDF] Chapitre 3 Méthode du simplexe - Cours

[PDF] Algorithmique au lycée

[PDF] le programme d 'algorithmique sans ordinateur - Mathématiques

[PDF] Algorithmique programmation en langage C - vol1 - Hal