Korrekthetsbevis for TT2- mpo -metoden

lik TT0-mpo), mens TT1 som vi har sett ikke var en ekte utvidelse av TT0. Med TT2-mpo kan man vise terminering av systemet i eksempel 6.15 med presedensen fsFfs⁰F aF b.

Følgende eksempel viser at TT2-mpokan vise terminering av et system som hverken TT0-mpo(en utypetmpo-analyse) eller TT1-mpokan vise terminerer:

Eksempel 7.1

Omskrivningssystemet

terminerer, noe som på grunn av den første regelen ikke kan vises ved en utypet (TT0-) analyse.

Følgende må vises for speilingen R⁰: fs¹(x) mpo fs²(gs¹(x)) TT1-mpoikke kan vise terminering av eksemplet.

Bruker vi imidlertid TT2-mpogir for eksempel presedensen f_sF f_s¹_F f_s¹¹ _F f_s² _Fg_s¹_Fb_Fa

at de 4 reglene i speilingen gitt over er mpo-minskende samtidig som krav 7.1 er tilfredsstilt. Vi har dermed vist terminering av det typeordnede systemet.

7.2 Korrekthetsbevis for TT2- mpo -metoden

Jeg skal i dette avsnittet bevise at TT2-mpo-metoden er korrekt, dvs. at ^R virkelig ter-minerer dersom alle betingelsene til TT2-mpo-metoden i g. 7.1 er oppfylt. For å få til dette vil jeg vise at det ns en speiling ^hF;^{b c};R⁰⁰ⁱ av et typeordnet system^h ;^Ri som terminerer når TT2-mpo-betingelsene holder. Forskjellen fra TT1-speilingen er at F-like funksjonssymboler blir slått sammen i den nye speilingen R⁰⁰, og at alle ekstraregler på formen f_w(x¹;:::;x_n)^;!f_w⁰(x¹;:::;x_n) fjernes dersom f_wFf_w⁰. Beviset vil innføre en ny termspeilingsfunksjon ^{b c} som bare brukes her. Bruken av TT-metodene vil som nevnt hele tiden basere seg på termspeilingsfunksjonen^bcbeskrevet i forrige kapittel.

7.2.1 Speilingen

I dette avsnittet skal jeg denere en speiling ^hF;^{b c};R⁰⁰ⁱ og vise at den virkelig er en speiling av et typeordnet system^h ;^Ri.

Funksjonssymbolmengden

^F

Den utypede funksjonssymbolmengden F vil være den samme som beskrevet i avsnitt 6.3 for TT1-metoden.

Termspeilingsfunksjonen

^bc

Jeg har tidligere vist at _F indusert av en kvasiordning ^%_F er en ekvivalensrelasjon og dermed danner ekvivalensklasser over F. Hovedidéen bak TT2-speilingen er at F-like fw;fw⁰;fw⁰⁰;::: skal representeres i speilingen av ett (felles) funksjonssymbol, dvs. av ett element i _F -ekvivalensklassen [f_w]^F. Dersom [f_w]^F er en ekvivalensklasse, så kan den imidlertid inneholde både f'er og andre funksjonssymboler fra , f. eks. g. De utypede symbolene fw og gw⁰ kan ha forskjellig aritet. Noen reduksjonsordninger, som bl. a.lpo, er generelt ikke denert for utypede systemer der et funksjonssymbol kan ha variabel aritet, så vi må være litt forsiktige med å slå sammen funksjonssymboler med forskjellig aritet til ett symbol. For å være på den sikre siden, og for å ha et mer generelt bevis, denerer jeg enkanonisk representant utifra funksjonssymboler i. Det betyr for at for enhver f ² velger jeg en f-kanonisk representant, kalt f-crep([fw]^F) i [fw]^F.

For enhver ekvivalensklasse og hvert funksjonssymbol i (som er representert i ekviva-lensklassen) nnes altså en f-crep([fw]^F) ² F. Denne f-kanoniske representanten for [fw]^F velger jeg å kalle fw. Dersom [fw]^F bare inneholder ett element som stammer fra en f i , skriver jeg av og til bare f_w for den éntydige f_w¹. For å sammenfatte disse nye begrepene er altså fw = f-crep([fw]^F) et funksjonssymbol fw⁰ i F der fwFfw⁰ og der fw og fw⁰ har lik aritet.

Eksempel (forts. av eks. 7.1)

Ekvivalensklassen [fs²]^F indusert av presedensen ^%_F denert tidligere i eksempel 7.1 består av elementene fs²;gs¹ og b. Her vil da f-crep([f_s²]^F) = f_s², g-crep([f_s²]^F) = g_s¹ og b-crep([f_s²]^F) vil være lik b. Tilsvarende kunne vi ha f-crep([fs¹¹]^F) = fs¹¹ = fs¹.

La nå den nye termspeilingsfunksjonen^{b c} :^T(;X)^!T(F;V ) være denert ved at ^bt^c er lik^bt^cmed den forskjellen at ethvert symbol f_w i t blir erstattet med symbolet f_w. Mer formelt er en funksjonssymbolsmerkingsfunksjon^bcF:S^!F denert ved

bf;w^c_F= f-crep([^bf;w^c_F]^F)

der^bc_F er som denert i forrige kapittel. Funksjonen ^bc er på vanlig måte utvidelsen av

bcF til en termspeilingsfunksjon.

1Er man meget pirkete kan^fta ulikt antall argumenter dersom^f:^s!sog^f:^s;s!ser to deklarasjoner i. Hvis nå^{fsFfs; s}vil^fsta enten ett eller to argumenter. Dette kan bøtes på ved å denere^fssom et^F-symbol som tar ett argument og^{fs; s} som et annet^F-symbol som tar to argumenter. Dette vil ikke forårsake problemer da^F-sprang fra^fs til^{fs0; s0} eller omvendt aldri kan forekomme.

7.2 Korrekthetsbevis for TT2-mpo-metoden

Eksempel (forts. av eks. 7.1)

Den eneste forskjellen mellom ^bt^c og ^bt^c ville være at enhver forekomst av fs¹¹ i^bt^cville bli erstattet med fs¹ i^bt^c. Eksempelvis er^bf(b)^c= f_s¹¹(b) mens^bf(b)^c= f_s¹(b).

Regelmengden

^R00

Den speilende regelmengden R⁰⁰ består som før av to mengder regler. De opprinnelige reglene blir som for TT1, dvs. for alle regler l^;!r i ^R og for alle spesialiseringer for variablene i l er^bl^c;!br^c med i R⁰⁰.

Ekstrareglene i R⁰beholdes også, unntatt de som i det tilfellet ville gitt en regel som ikke gjør noe som helst. Formalisert vil det si at mengden av ekstraregler i R⁰⁰er gitt ved

R⁰⁰=^ffw(x¹;:::;xn)^;!fw⁰(x¹;:::;xn)^jfw;fw^{0 2}F ^{^}s⁰< s^{^}fw⁶= fw^0g

R⁰⁰er altså mengden av de opprinnelige reglene og ekstrareglene.

Eksempel (forts. av eks. 7.1)

Hvis vi denerer f-crep([f_s¹]^F) = f_s¹ = f_s¹ = f_s^{1 1} ville den speilende regelmengden R⁰⁰ til systemet i eksempel 7.1 blitt som følger:

fs¹(x)^;!fs²(gs¹(x))

fs¹(x)^;!fs²(gs¹(x)) (fordi fs¹¹ = fs¹) f_s¹(b)^;!f_s¹(a) (også fordi f_s¹¹= f_s¹) fs¹(y)^;!b (tilsvarende her)

Disse er de jeg kaller de opprinnelige reglene i R⁰⁰. Ekstrareglene er da fs(x)^;!fs¹(x)

f_s(x)^;!f_s²(x)

Her kan man legge merke til at ekstraregelen fs¹(x)^;!fs¹¹(x) som vi ville hatt i en TT1-speiling forsvinner. Med presedensen ^%_F gitt tidligere kan man med hjelp av mpoellerlpovise at regelmengden R⁰⁰terminerer, noe jeg snart vil vise også impliserer terminering av^R.

Dersom t er en utypet term, vil jeg skrive t for termen som fremkommer når alle funk-sjonssymboler fw i t erstattes med tilhørende f-kanoniske representanten fw.

Det må nå vises at^hF;^bc;R⁰⁰ⁱvirkelig er en speiling av et typeordnet omskrivningssystem

h ;^Ri.

Teorem 7.1

^{8t;t02T(;X)jt;R!t0=)btc;R+!0 0 bt0c}

Bevis:

Beviset tar utgangspunkt i speilingen^hF;^bc;R⁰ⁱ vi brukte i TT1-beviset. Husk at

bt^c bare er^bt^c med alle funksjonssymboler fw byttet ut med fw. Vi hadde i beviset for teorem 6.15 en omskrivningssekvens

bt^{c;op pR!0} t^1;eksR!0 t^2;eksR!0 tn=^bt^0c

der n 1, og der symbolet ^{;op pR!0} står for bruk av én av de opprinnelige reglene i R⁰ og^;eksR!0 står for bruk av en ekstraregel. Siden vi i R⁰⁰ ikke har fjernet noen av de opprinnelige reglene i R⁰ og fordi enhver f_w i både^bt^c og R⁰_opp erstattes med en f_w i

bt^c og R⁰⁰opp gjelder

bt^{c;op pR!00} t¹

Det er opplagt at dersom ti^;eksR!0 ti⁺¹ så er enten ti^;eksR!00 ti⁺¹ eller ti = ti⁺¹ for alle termer ti;ti⁺¹²T(F;V ). Dette kommer av vi bare har fjernet ekstraregler som ikke forandrer på noe som helst i R⁰⁰. Dermed kan ovenstående sekvens bli til

bt^c;oppR!00 t^{1eks;R!0 0} t^{2 eks;R!00} tn =^bt^0c

Siden vi har^bt^{c;op pR!00} t¹ inneholder ovenstående sekvens minst ett omskrivningssteg og kan derfor skrives på den ønskede formen

bt^{c;R+!0 0 b}t^0c

2

7.2.2 Terminering av

^R

Siden ^hF;^{b c};R⁰⁰ⁱ er en speiling av ^h ;^Ri er det tilstrekkelig å vise at R⁰⁰ terminerer når TT2-mpo-betingelsene i g. 7.1 er oppfylt for å fastslå terminering ^R.

Følgende lemma, som såvidt er nevnt (uten bevis) i kapittel 2, vil vise seg være nyttig:

Lemma 7.2

^{8t2T(F;V )jt}mpot

Bevis:

Beviset er ved induksjon på oppbygning av termen t.

t

variabel:

Dersom t = x er også t = x og x^%_mpox følger av regel mpo-3 siden x_F x og^;%multi_mpo ^; ved regelmulti-1.

t

konstant eller sammensatt term:

Anta at t = f(t¹;:::;t_n) der n 0. Da er t = f(t¹;:::;tn) og induksjonshypotesen gir oss timpoti for alle i. Der-som n > 0 gir multi-2 brukt n ganger at ^ft¹;:::;tn^g%multimpo ^ft¹;:::;tn^g og n nye tilfeller av multi-2 gir ^ft¹;:::;t_n^g%multi_mpo ^ft¹;:::;t_n^g. Hvis n = 0 er

;%multimpo ^;. Siden f_Ff gir regelmpo-3både f(x¹;:::;x_n)^%_mpof(t¹;:::;t_n) og f(t¹;:::;t_n)^%_mpof(t¹;:::;t_n) som gir ønskede t_mpot.

2

Det er da trivielt å vise

Lemma 7.3

For alle termer t;t⁰ i T(F;V )gjelder t_mpot⁰=⁾t_mpot⁰

hvor t er termen tder alle funksjonssymboler fw er erstattet medfw.

7.3 Generalisering av TT2

Bevis:

Følger trivielt av lemma 7.2 og egenskaper ved kvasiordninger siden tmpotmpot⁰mpot⁰.²

Jeg kan nå vise korrekthet av TT2-mpo-metoden.

Teorem 7.4 (Korrekthet av TT2-

mpo

)

Gitt en preregulær typeordnet signatur der ingen type har et uendelig antall typer under seg. Anta at^R er et typeminskende omskriv-ningssystem iog atF og^bc er denert som i kapittel 6. La så ^%_F være en kvasiordning overF slik at w⁰< w^{^}fw;fw^{0 2}F =⁾fw^%Ffw⁰ og anta at^bl^cmpo^(%F)br^c gjelder for alle regelspesialiseringerl^;!ri ^R.

Da terminerer^Rdersom enten ^R ellerer endelig eller ^%_F er velfundert.

Bevis:

^{Dersom R00} beskrevet tidligere i dette kapittel terminerer, gir teorem 6.5 at ^R terminerer.

R⁰⁰ består av en mengde opprinnelige regler

fbl^c;!br^{c j} l^;!r regelspesialisering i ^Rg og en mengde ekstraregler

ffw(x¹;:::;xn)^;!fw⁰(x¹;:::;xn) ^j w⁰ < w ^{^}fw;fw^{0 2} F ^{^}fw ⁶= fw^0g. Kravet

bl^c_mpo^(%F)br^c og lemma 7.3 gir ^bl^c_mpo^(%F)br^c for alle opprinnelige reg-ler i R⁰⁰ og kravene fw^%F fw⁰ og fw⁶= fw⁰ gir fwFfw⁰ og følgelig

fw(x¹;:::;xn)mpo^(%F)fw⁰(x¹;:::;xn) for alle ekstrareglene i R⁰⁰. Alle reglene i R⁰⁰ er dermed inneholdt i _mpo^(%F). Hviser endelig, er også F endelig og siden _mpo^(%F) er en forenklingsordning så terminerer R⁰⁰. Når ^%_F er velfundert er også mpo^(%F)

velfundert og da terminerer også R⁰⁰. I det siste tilfellet, nemlig at ^R er endelig, er enhver sekvens t^{1;R!0 0} t^2;R!00 av grunntermer bygget opp av en endelig mengde funksjonssymboler², slik at en uendelig sekvens av disse termene ville vært selvomslut-tende. Denne selvomsluttende sekvensen kan ikke nnes da^;R!00 mpo^(%F) .

I alle tre tilfellene terminerer R⁰⁰og følgelig også^R.²

7.3 Generalisering av TT2

Metoden TT2-mpo kan generaliseres til å kunne brukes på alle utypede termineringsord-ninger, ved at man gir symbolene f_w og f_w⁰ lik vekt/verdi innenfor ordningen. Man må da huske på at alle F-funksjonssymbolene fw⁰⁰ der w⁰ < w⁰⁰ < w også blir tilordnet denne samme vekten. Når w⁰< w og symbolene fw og fw⁰ ikkehar samme vekt, må man også sikre at ekstraregelen f_w(x¹;:::;x_n)^;!f_w⁰(x¹;:::;x_n) er-minskende.

Det kan forøvrig bemerkes at forandringen fra TT1 til TT2 tok utgangspunkt i ulemper ved stiordningene. Speilingen^hF;^bc;R⁰⁰ⁱer faktisk svakere enn TT1-speilingen^hF;^bc;R⁰ⁱ i termineringshenseende siden R⁰ alltid terminerer når R⁰⁰ gjør det. For andre klasser av ordninger kan det derfor være aktuelt med andre forbedringer av TT1-speilingen, men TT2-metoden er alltid minst like sterk som TT0- og TT1-metodene for alle ordninger.

2noe som kan vises på samme måte som for TT1

TT3-metoden en utvidelse av

In document Terminering av typeordnet omskriving (sider 101-107)