Day: 3. marts 2013

Kategorier
Datalogi Matematik

Liden semi-Thue kan vælte stort læs, eller: Programmering ved omskrivning

Thue

Da jeg var studerende og fulgte kurset Modeller for beregnelighed, var ét af emnerne andre modeller for beregnelighed end Turing-maskiner. Her stødte jeg på Chomskys generelle grammatikker og på Thue-systemer. Den slags underviser vi ikke i længere (nu er det nemlig mig, der underviser i efterkommeren af det gamle kursus) – lærebogen lægger ikke op til det, og der er andre emner, der er mere centrale. På en måde er det nu en skam.

Thue-systemer dukker op allerede omkring forrige århundredeskifte i den norske matematiker Axel Thues arbejde om såkaldte ordproblemer for frie algebraer. Et Thue-system T er en endelig mængde af uordnede par af strenge

T = \{ (u_1,v_1), \ldots, (u_k,v_k)\}

Tænk på dem som at u_i kan skrives om til v_i – og at v_i kan skrives om til u_i. Vi tillader også at strenge kan skrives om i en kontekst, dvs. at s u_i t kan skrives om til s v_i t – og omvendt. En streng kan selvfølgelig altid “skrives om” til sig selv. Det vi har fat i her, er altså en ækvivalensrelation, “kan skrives om til ved brug af T“, og ordproblemet for Thue-systemer er nu

Givet et Thue-system T og to strenge u og v, kan u så skrives om til v ved brug af T?

Dette problem er uafgørbart (ideen i beviset er at lave et Thue-system ud fra en Turing-maskine M; konstruktionen er oplagt: strengene i Thue-systemet er konfigurationer i M).

I et semi-Thue-system

S = \{ (u_1,v_1), \ldots, (u_k,v_k)\}

er parrene nu ordnede, og (u_i,v_i) betegner at u_i kan omskrives til v_i – men ikke omvendt (medmindre (v_i,u_i) \in S). Også for semi-Thue-systemer er ordproblemet uafgørbart, for et Thue-system er jo bare et symmetrisk semi-Thue-system.

Først for ganske nylig er det gået op for mig, at der findes et programmeringssprog, der baserer sig på semi-Thue-systemer! Sproget hedder Thue (men burde hedde Semi-Thue). Det blev udviklet i 2000 af en amerikaner ved navn John Colagioia. I et Thue-program definerer man en samling omskrivningsregler.

Her er et lille eksempel (lånt fra Esolangs side om Thue, en af de få kilder til oplysninger om dette sprog). Det er et program, der kan lægge 1 til et binært tal (der i dette eksempel er 1111111111).

1_::=1++
0_::=1

01++::=10
11++::=1++0

_0::=_
_1++::=10

::= _1111111111_

Egentlig er ideen ikke så urimelig. Genskrivning af strenge kunne man selvfølgelig også udtrykke i et sædvanligt applikativt programmeringssprog som ML eller Haskell – eller i et logikprogrammeringssprog, for den sags skyld. Men man kunne bruge ideen til at give en koncis repræsentation af strukturel operationel semantik for abstrakte maskiner eller såmænd “bare” for almindelige programmeringssprog, for alle regler i den slags semantikker er jo netop genskrivningsregler (eller kan formuleres som sådanne, hvis man bruger evalueringskontekster).

Det kunne faktisk være et interessant projekt for studerende – at genoplive Thue eller lave et helt nyt programmeringssprog, hvor termgenskrivning er den centrale kontrolstruktur.