Funksjoner: f : Nat ! Int - Terminering av typeordnet omskriving

a : Int b : Nat

Regel:

^b^;^!^a

Termen f(b) kan her ikke skrives om til f(a) fordi denne siste ikke er velformet.

Dette kapitlet vil omhandle typeordnet omskrivning generelt, mens neste kapittel vil ta for seg typeordnet komplettering og egenskaper som naturlig hører med under komplettering.

Jeg vil peke på forskjeller mellom utypet og typeordnet omskrivning og komplettering uten å gå inn på spissndigheter vi også kjenner fra utypet omskrivning.

Siden jeg omtalertermomskrivning antar jeg at alle signaturene er regulære; dette fører til at termalgebraen^T(;X) representerer alle-algebraer.

4.1 Den typeordnede omskrivningsrelasjonen

En likning (⁸X) l r kalles en omskrivningsregel dersom den brukes operasjonelt i en bestemt retning.

Denisjon 4.1 (Omskrivningsregel ([GKK90]))

Entypeordnet omskrivningsregel er en typeordnet likning(⁸X) lr som tilfredsstiller^V(r)^V(l)og skrives (⁸X) l^;^!r. I utypet omskrivning forlanger man ikke lenger^V(r)^V(l) og Waldmann ([Wal92]) sier ogsåwe do not restrict to rules where^V(r)^V(l), following [DJ90] . [DJ90] omhandler utypet omskrivning, og jeg vil i avsnitt 8.2 vise at det i dette henseende er en fundamental forskjell mellom utypet og typeordnet omskrivning.

Denisjon 4.2 (Typeordnet omskrivningssystem)

^Ettypeordnet omskrivningssystem er et par^h;^Ri der er en typeordnet signatur og ^Rer en (endelig eller uendelig) meng-de ^Sⁿ_i⁼¹^fli^;^!ri^g av omskrivningsregler der ⁸i ² 1::n^jli;ri ² ^T(;X) for en typeordnet variabelmengde X.

Jeg skriver ofte^Rfor^h;^Rinår signaturenfremgår av signaturen eller er uten interesse i sammenhengen.

4.1 Den typeordnede omskrivningsrelasjonen Vi har allerede sett at kontekst-applikasjon kan føre til at en velformet term omskrives til en ikke-velformet term. Omskrivningsrelasjonen må opplagt omskrive en velformet til en ny velformet term, men er dette kravet tilstrekkelig? La oss vurdere

Eksempel 4.2

La den koherente (dvs. regulære og lokalt ltrerte) signaturenog regel-mengden^Rvære

Typer:

^s;s¹^;s²

s¹ s s² s

Funksjoner:

^{f : s}¹^!^s

f : s²^!s a : s¹ b : s²

Regel:

^a^;^!^b

Spørsmålet man kan vurdere er hvorvidt f(a)^;^R^!f(b) skal være en omskrivning i ^R samtidig som vi registrerer at både f(a) og f(b) er velformede termer.

For å besvare spørsmålet må man se på hva et omskrivningssystem egentlig er ment å være.

(Utypet) omskrivning bygger mye på kontekst-applikasjonsbegrepet. Representerer a^;^!b forholdet a^'b må også t[a]p ^'t[b]p gjelde dersom t[a]p^;^!t[b]p.

Hvis a^;^!b fordi (a) = (b) for alle homomorer fra den aktuelle termelagebraen inn i enhver modell av systemet, så er også (t[a]_p) = (t[b]_p) i alle tilsvarende utypede systemer.

Omskrivningssystemer handler selvfølgelig ikke bare om likhetsrelasjoner, men uansett må det generelt gjelde at dersom a^;^R^!b, så må samme f brukes på både f(:::;a;:::) og f(:::;b;:::).

Eksempel (forts. av eks. 4.2)

^La ^A være en tolkning av signaturen i eksempel 4.2 gitt ved^A_s =^Z; ^A_s¹ =^f:::;^;2;^;1;0^g og^A_s² =^f0;1;2;:::^g. Både a og b tolkes i

Asom elementet 0. Funksjonssymbolet f tolkes^A^s_f^1!^s= x²^As¹ :^;12 og^A^s_f^2!^s= x²^A_s² : +55. Algebraen^Aer en typeordnet -algebra.

Jeg vil i dette tilfellet at s^;^R^!t skal representere (s) = (t) for den éntydige homo-moren :^T()^!A. Algebraen^A tilfredsstiller dette ønsket fordi (a) = (b) = 0.

Dersom f(a)^;^R^!f(b) så skulle også (f(a)) = (f(b)), men dette holder ikke fordi (f(a)) =^;12 og (f(b)) = 55. Dermed bør vi ikke ha f(a)^;^R^!f(b) selv om a^;^R^!b og både f(a) og f(b) er velformede termer.

Siden s¹./ s² er det faktisk ingensammenheng mellom ^A^s_f¹^!^s og^A^s_f²^!^s. Deklarasjo-nen f : s²^!s kunne like gjerne vært skrevet g : s²^!s. Utifra dette hadde det også vært unaturlig å ha en omskrivning f(a)^;^R^!f(b).

Problemet oppstår fordi et funksjonssymbol kan tolkes på forskjellig måte avhengig av typene til argumentene, selv om argumentene har samme verdi, i dette tilfellet 0. Det ville gått bra dersom^A^s_f^1!^sog^A^s_f^2!^s hadde gitt samme resultat for samme argument.

Eksempel (forts. av eks. 4.2)

For å sikre at^A^s_f¹^!^s=^A^s_f²^!^spå^As¹^\^As² må signaturen

utvides med en deklarasjon f : s^!s.

Tolkningen^A^s_f^!^små da tilfredsstille^A^s_f^!^s =^A^s_f^1!^s på^A_s¹ og^A^s_f^!^s=^A^s_f^2!^spå^A_s² som gir ønskede^A^s_f¹^!^s =^A^s_f^!^s =^A^s_f²^!^s på^A_s¹^\^A_s².

Rent konkret ville det i vårt tilfelle bety at dersom (a) = (b) = 0 ville også

As^1!s(0) = ^A^s^2!^s(0) slik at man kunne si f(a)^;^R^!f(b) når man med ^;^R^! vil mene likhet i -algebraer.

For at samme f blir brukt på f(:::;a;:::) og f(:::;b;:::) må det altså nnes en type s slik at f(:::;x:s;:::) er veldenert og a og b er med i ^T(;X)_s. Dette blir sikret av krav 2 til den typeordnede omskrivningsrelasjonen som deneres på følgende måte:

Denisjon 4.3 (Typeordnet omskrivningsrelasjon)

En term t²^T(;X)omskrives til en term t⁰ med en omskrivningsregel (⁸Y ) l^;^!r i et omskrivningssystem ^h;^Ri i en posisjonp, som skrivest^;^R^!_Xt⁰, når

1. det ns en substitusjon : Y^!T(;X)slik atl = t^jp og t⁰= t[r]p og

2. det ns en typesslik att[x:s]_p er en velformet term samtidig soml;r²^T(;X)_s. Når det ikke erheltnødvendig å eksplisitt nevne variabelmengdene vil jeg i denne innfør-ingen skrive ^;^R^! for^;^R^!_X.

4.2 Typeminskende omskrivningssystemer (1)

Ovenstående krav 2 til omskrivningsrelasjoner gjør (som vi skal se mange eksempler på) det vanskelig å resonnere om omskrivningssystemer. Det hadde i mange tilfeller vært ønskelig med et krav til f. eks. regelmengden som er enklere å beregne enn krav 2 men som sikrer kontekstapplikasjon. Vi kaller derfor en regel (⁸Y ) l^;^!r kompatibel dersom bruk av denne regelen gjør at krav 2 til omskrivningsrelasjonen alltid er oppfylt². Mer formelt er (⁸Y ) l^;^!r kompatibel hvis krav 2 til omskrivningsrelasjonen er tilfredsstilt for enhver term t²^T(;X) og substitusjon :Y^!T(;X) der l = t^jp.

Et kriterium sikrer kompatibilitet ertypeminskningav reglene. En regel l^;^!r er typemins-kende dersom LS(l)LS(r) for alle instanser l^;^!r av regelen. Typen s i punkt 2 i denisjon 4.3 kan da være lik LS(l) siden LS(r)LS(r) impliserer r²^T(;X)_LS⁽_l⁾. Et omskrivningssystem er typeminskende når enhver regel i systemet er det. En typemins-kende regel l^;^!r ertypebevarendenår LS(l) = LS(r) for alle instanser l^;^!r av rege-len. En regel sies å væreekte typeminskendedersom den er typeminskende men ikke type-bevarende, mens en regelinstansl^;^!r er ekte typeminskende dersom LS(r) < LS(l).

En regel har imidlertid (oftest) uendelige mange instanser, slik at det er nødvendig å nne et enklere kriterium for typeminskning. Det er ikke tilstrekkelig at sjekke LS(l) og LS(r), men det er nok å sjekke l^;^!r for alle typer termer variable kan instansieres med.

2Med utypet tankegang betyr dette at en omskrivning alltid kan foretas dersom en regel matcher.

4.2 Typeminskende omskrivningssystemer (1)

Denisjon 4.4 (Spesialisering)

^En spesialisering : X^!X⁰ er en variabeltilordning =^fx¹:s¹ ^7! x¹:s⁰¹;:::;xn:sn^7! xn:s⁰n^g der s⁰i si for allei ²1::n og X = ^S_i²¹_::nxi. Den homomorfe utvidelsen :^T(;X)^!T(;X⁰)av skrives også .

Jeg bruker stort sett samme navn på variable i spesialiseringer selv om de tilhører ulike variabelmengder. En spesialisering gir kort fortalt en variabel en mindre (eller like stor) type.

Eksempel 4.3

Anta at (S;) = s⁰⁰ < s⁰ < s og X = ^fx¹ : s; x² : s⁰; x³ : s⁰⁰^g. Da er =^fx¹^7!x¹:s⁰⁰; x² ^7!x²:s⁰⁰; x³ ^7!x³:s⁰⁰^g og ⁰=^fx¹ ^7!x¹:s⁰; x²^7!x²:s⁰; x³^7!

x³:s⁰⁰^g to spesialiseringer av X. Variabelen x¹ kan gis typene s;s⁰ eller s⁰⁰, x²typene s⁰eller s⁰⁰mens x³ må beholde typen s⁰⁰. Det ns følgelig 6 spesialiseringer av X.

En endelig variabelmengde har et endelig antall spesialiseringer sålenge enhver type har endelige mange typer mindre enn seg.

Teorem 4.5 ([GKK90])

Et omskrivningssystem ^Rer typeminskende dersom LS(l)LS(r)

for enhver regell^;^!r i ^Rog enhver spesialisering av variable il.

Jeg kaller l^;^!r for enregelspesialisering når l^;^!r er en regel og er en spesialisering av variable i l. For endelig systemer er altså typeminskning greit beregnbart.

Eksempel 4.4

La en signatur være gitt

Typer:

^s;s⁰

s⁰s

Funksjoner:

^{f : s}^!^s

f : s⁰^!s⁰ g : s^!s⁰ a : s

I denne signaturen ville en regel (⁸x : s) f(x)^;^!g(x) vært typeminskende, mens en regel (⁸x : s) f(x)^;^!aikkeville vært det, fordi dens spesialisering (⁸x : s⁰) f(x)^;^!a er typeøkende.

Typeminskning synes å være et forholdsvis restriktivt krav. I eksempelet over ville faktisk alle muligeregler vært kompatible, men typeminskningskravet diskvaliserer ere av disse.

Det kan derfor synes litt underlig når både Gnaedig, Kirchner og Kirchner i [Gn92a] (som ikkedreier seg om komplettering), [GKK90] og [GKK87] og Waldmann i [Wal92] alle antar at regelmengdene er typeminskende, noe jeg også vil gjøre i del II av denne oppgaven.

Man kan spørre hvor restriktivt typeminskningskravet egentlig er. Gnaedig et al. påstår at det viser seg i praksis at regler i et omskrivningssystem (eller likninger under komplettering) gjerne er (evt. lar seg orientere slik at de blir) typeminskende. Følgende eksempel viser at det av og til kan dukke opp systemer som opplagt vil føre til typeøkende regler:

Eksempel 4.5 (av Lars With, sitert i [CH93])

Den naturlige måten å denere en funk-sjonsquare(som ganger et tall med seg selv) på (gitt spesikasjonen for Int og Nat og denisjonen av) er:

Typer:

^Int;Nat

NatInt

In document Terminering av typeordnet omskriving (sider 58-62)