En annen måte å denere F på

Signaturen er ikke regulær, og^bf;Zero^cF er ikke veldenert fordi den kan enten ha verdien fNateller fNeg. Hadde vi lagt til en deklarasjon f : Zero^!Int ville signaturen vært regulær og funksjonene^bc_F og^bc veldenerte.

Funksjonen^bcF (og dermed også^bc) er veldenert og beregnbar når signaturen er regulær.

Å velge F =^ff_w^jf ² _w^!_s^g har også en annen svakhet. Anta nemlig at de unødvendige deklarasjonene is even : NzNeg^!Bool og is even : NzPos^!Boolikkeer med i signaturen

. Den fjerde regelen i eks. 6.1 kan likefullt være

(⁸y : NzNeg) is even(y)^;!is even(opp(y)) Siden de ovennevnte deklarasjonene har forsvunnet er imidlertid

bis even(y:NzNeg)^c=^bis even;NzNeg^c_F(y) = is even_Int(y) og

bis even(opp(y: NzNeg))^c= ::: =^bis even;NzPos^cF(^bopp;NzNeg^cF(y)) = is evenInt(oppNzNeg(y)) og vi ender opp med å måtte vise

is evenInt(y)is evenInt(oppNzNeg(y)) som aldri gjelder for noen fornuftig ordning.

6.3.2 En annen måte å denere

^F

på

Den andre tilnærmingsmåten bøter på dette problemet ved å denere den utypede funk-sjonssymbolmengden

F = ^ffw^0j9s^jw⁰w^{^}f ²w^!s^g

dvs. dersom f : w^!s er en deklarasjon i, så er fw⁰ med i F for alle sekvenser av typer w⁰ der w⁰w. Denne denisjonen har en rekke fordeler. For det første er den nere oppdelt enn den forrige. Uansett om deklarasjonene is even : Nz^!Bool og is even : NzNat^!Bool er med i signaturen eller ikke, vil

F =^f:::;is evenInt;is evenNat;is evenNeg;is evenZero;is evenNzNeg;is evenNzPos;:::^g

fordi is even ² Int^!Bool. Den andre fordelen med denne metoden er at det går meget raskt å beregne^bcF fordi ^bf;s¹;:::;sn^cF etter denne siste denisjonene av^bcF settes lik f_s¹_;:::;sⁿ. Den tredje fordelen med å velge denne denisjonen av F er at det i dette tilfelle er tilstrekkelig å forlange at signaturen er preregulær. Funksjonen ^bc er i dette tilfellet alltid veldenert, da ^bf(t¹;:::;t_n)^c = ^bf;LS(t¹);:::;LS(t_n)^c_F(:::) = f_LS⁽_t¹⁾_;:::;LS⁽_tⁿ⁾(:::).

Ordningene indusert av at F er denert på denne måten vil, som skal se senere, være minst like sterke som den forrige varianten. Ulempen med en slik større F er at man får mange er symboler å jobbe med. Jeg ville uansett helt klart anbefale denne siste denisjonen av F, men overlater til brukeren å avgjøre dette ved å arbeide med begrepene F og ^{b c}_F i denne oppgaven.

Man kan selvfølgelig kombinere variantene ved å utvide signaturen. Det eneste kravet man må stille er at den utvidede signaturen blir kvasiregulær, der en kvasiregulær signatur er en signatur som ville vært regulær dersom enhver for slapp deklarasjon f : w^!s ble byttet ut med en deklarasjon f : w^!LS(f(x : w)). Gitt en preregulær signatur kan denne faktisk alltid utvides til en kvasiregulær signatur, som i sin tur kan strammes inn til en regulær signatur. Jeg vil i mine eksempler bruke den første denisjonen av F, nemlig F =^ff_w^jf ²_w^!_s^g, men dette erutelukkendefor å øke leseligheten.

6.4 Funksjonssymbolsprang

Vi begynner dermed å bli klare for å kikke på regelmengden i en speiling. Omskrivningssys-temet i eks. 6.1 var typebevarende, dvs. venstre- og høyresiden i hver regel hadde samme minste type for alle substitusjoner av variablene i regelen. Man er ikke alltidsåheldig med regelmengdene. Eksempelvis ville den første likningen i NatStack-spesikasjonen i eks. 3.1 orienteres til regel (⁸s:Stack; n:Nat) pop(push(s;n))^;!s hvis instans når s = empty er ekte typeminskende. La oss derfor heller se på følgende system:

Eksempel 6.8

La det typeminskende systemet ^Rvære

Typer:

^s;s1;s2

Termene kan speiles på måten beskrevet i forrige avsnitt slik at ^bf(b)^c = f_s¹(b) og ^bf(g(b))^c = fs²(gs¹(b)). Systemet kan representeres i form av de utypede regle-ne fs¹(b)^;!fs²(gs¹(b)) og a^;!b. I en speiling ^hF;^{b c};R⁰ⁱ må enhver omskrivning

6.4 Funksjonssymbolsprang t^;R!t⁰ kunne representeres av en omskrivningssekvens^bt^{c;R+!0 b}t^0c. Dette introduser-er hovedproblemet med speilingintroduser-er, nemlig vanskeligheten av å få dem lukket undintroduser-er regelapplikasjon. Med bruk av den andre regelen ns det en typeordnet omskriv-ning f(g(a))^;R!f(g(b)), slik at en speiling må oppfylle^bf(g(a))^{c;R+!0 b}f(g(b))^c. Siden

bf(g(a))^c = f_s(g_s(a)) og^bf(g(b))^c = f_s²(g_s¹(b)) blir alle F-funksjonssymbolene for-andret selv om den typeordnede omskrivningen foregår i posisjon 1:1! Det er lett å se at R⁰=^ffs¹(b)^;!fs²(gs¹(b)); a^;!b^g ikkeoppfyller fs(gs(a))^;R+!0 fs²(gs¹(b)) og derfor ikke er en speiling.

Bruk av en typeminskende (instans av en) regel kan altså gi opphav til at funksjons-symboler i ^bt^c forandres i ^bt^0c langt fra posisjonen der en typeomskrivning omskrivning t^;R!t⁰ foregår. Jeg vil kalle disse sideeektene av en typeordnet omskrivning for F -funksjonssymbolsprang.

Denisjon 6.7 (

^F

-funksjonssymbolsprang)

Anta at det er gitt et typeordnet omskriv-ningssystem ^h;^Ri, en utypet funksjonssymbolmengde F og en termspeilingsfunksjon

bc:^T(;X)^!T(F;V ). Anta videre at en typeordnet omskrivningt^;R!t⁰ skjer i posisjonp i t. Det har skjedd et F-funksjonssymbolsprang i posisjonq dersom (F-)funksjonssymbolet i posisjonq i termen ^bt^c er forskjellig fra funksjonssymbolet i posisjon q i ^bt^0c og det ikke ns en (tom eller ikke-tom) posisjonr slik atq = p:r.

Jeg skriver ofte F-sprangfor F-funksjonssymbolsprang.

Eksempel (forts. av eks. 6.8)

I omskrivningen f(g(a))^;R!f(g(b)) nevnt i eks. 6.8 er det to F-sprang, i posisjonene og 1.

Det viser seg som vi skal se at F-sprang alltid skjer i posisjoner i en term t mellom roten (posisjon ) og posisjonen p der omskrivningen foretas, og jeg vil derfor få bruk for følgende denisjoner som også vil brukes i beviser i kapittel 8.

Denisjon 6.8

For en termtog en posisjonp = p¹:p²:::::pnit, deneres posisjonenp(i), der 0in, ved p(i) = p¹:p²:::::p_n^;_i.

Posisjonen p(i) angir altså posisjonen man får når man går i skritt fra posisjon p i t oppover den éntydige veien mot roten.

Eksempel 6.9

Anta at en posisjon p = 1:2:1:3:2. Da er p(0) = 1:2:1:3:2 , p(1) = 1:2:1:3 , p(3) = 1:2 , p(5) = mens p(8) er udenert.

Denisjon 6.9

DybdenDp til en posisjon p er lik lengden til sekvensenp.

I følgende lemmata antar jeg hele tiden at t^;R!t⁰ er en typeordnet omskrivning med en regelapplikasjon i posisjon p og at ^{b c} er utvidelsen av en funksjon ^{b c}F denert som beskrevet i avsnitt 6.3.

Lemma 6.10

Det kan bare være F-sprang i posisjonene p(0); p(1);:::;p(D_p).

Bevis:

Følger av at^bc er en homomor og at en term har trestruktur.²

Et F-sprang kan bare oppstå i en omskrivning dersom regelinstansen som er brukt til omskrivningen er ekte typeminskende, noe som fører til et F-sprang i posisjon p(1). Men termen t^jp⁽¹⁾kan på grunn av monotoni-egenskaper til signaturen være av en større type enn t^0jp⁽¹⁾, noe kan føre til et F-sprang i posisjon p(2) osv., så for å gjøre noe med F-sprangene må man vite hvordan de ser ut. Siden jeg i denne oppgaven ikke har antatt at signaturene er monotone, trenger jeg følgende egenskap:

Lemma 6.11

En preregulær signatur er LS-monoton, dvs.

LS(t)LS(t⁰) =⁾LS(f(:::;t;:::))LS(f(:::;t⁰;:::))

Bevis:

Husk at LS(f(t¹;:::;tn)) = min^fs^jf ²s¹;:::;s^n!s^{^8}i²1::n^jLS(ti)si^g. Anta så at LS(f(:::;t;:::)) = s og LS(f(:::;t⁰;:::)) = s⁰. Denisjonen av LS gir at s⁰ ikke kan være større enn s. Situasjonen s ./ s⁰ kan heller ikke oppstå, fordi både s⁰ og én eller annen s⁰⁰ s ville vært minimale typer til f(:::;t⁰;:::), men det er umulig da preregularitet forlanger at enhver term har éntydig minste type.²

Lemma 6.12

Anta at s⁰_i s_i,^bf;s¹;:::;s_i;:::;s_n^c_F = f_w og at ^bf;s¹;:::;s⁰_i;:::;s_n^c_F = fw⁰. Da er w⁰w.

Bevis:

Uansett hvilken av de to tidligere nevnte denisjonene av F og ^bcF som brukes, følger w⁰w av denisjonen av^bc_F og det faktum at^bc_F er veldenert.²

Disse lemmata fører til at vi kan karakterisere F-sprang der jeg skriver at termen t er lik et symbol f i posisjon p dersom t^j_p= f(t¹;:::;t_n) for n0.

Teorem 6.13

^{La t;R!t0} være en typeordnet omskrivning i posisjon p. Dersom det fore-kommer et F-sprang i posisjon p(i)(1iDp) og^bt^c er lik fw i posisjonp(i), og ^bt^0c er likg_w⁰ på samme sted, så er f = gog w⁰< w.

Bevis:

Denisjonen av^{b c} og ^{b c}F gir trivielt f = g. Siden omskrivningssystemet er ty-peminskende, gjelder LS(t^jp)LS(t^0jp). Itereres lemma 6.11 gir dette LS(t^jp⁽i^;1)) LS(t^0j_p⁽_i^;1)). Termen ^bt^c er lik symbolet ^bf;LS(t¹);:::;LS(t^j_p⁽_i^;1));:::;LS(t_n)^c_F i posisjon p(i). Tilsvarende er^bt^0c lik^bf;LS(t¹);:::;LS(t^0jp⁽i^;1));:::;LS(tn)^cF i posi-sjon p(i). Lemma 6.12 sier da at w⁰w, og siden det har forekommet et F-sprang, kan disse ikke være like, slik at w⁰< w.²

Teorem 6.13 indikerer at vi kan kompensere for F-sprang ved å innføre en regel fw(x¹;:::;xn)^;!fw⁰(x¹;:::;xn)

(der variablene x¹;:::;xn er innbyrdes disjunkte) i speilingen for hvert par fw;fw⁰ i F der w⁰< w. Jeg velger å kalle en slik regel for enekstraregeli R⁰.

In document Terminering av typeordnet omskriving (sider 87-91)