Ordproblem (matematik)

Den här artikeln handlar om algoritmiska ordproblem inom matematik och datavetenskap. För annan användning, se Word-problem .

I beräkningsmatematik är ett ordproblem problemet med att avgöra om två givna uttryck är ekvivalenta med avseende på en uppsättning omskrivningsidentiteter . Ett prototypiskt exempel är ordet problem för grupper , men det finns många andra exempel också. Ett djupt resultat av beräkningsteorin är att svaret på denna fråga i många viktiga fall är oavgjorda .

Bakgrund och motivation

I datoralgebra vill man ofta koda matematiska uttryck med hjälp av ett uttrycksträd. Men det finns ofta flera ekvivalenta uttrycksträd. Frågan uppstår naturligtvis om det finns en algoritm som, givet som indata två uttryck, avgör om de representerar samma element. En sådan algoritm kallas en lösning på ordet problem . Föreställ dig till exempel att $x,y,z$ är symboler som representerar reella tal - då skulle en relevant lösning på ordproblemet, givet ingången ${\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (x/z)\cdot y} , producera utdata EQUAL och producera$ på liknande sätt NOT_EQUAL från $(x\cdot y)/z\mathrel {\overset {?}{=}} (x/x)\cdot y$ .

Den mest direkta lösningen på ett ordproblem har formen av en normalformsats och algoritm som mappar varje element i en ekvivalensklass av uttryck till en enda kodning som kallas normalformen - ordproblemet löses sedan genom att jämföra dessa normalformer via syntaktisk jämlikhet . Till exempel kan man bestämma att $x\cdot y\cdot z^{-1}$ är normalformen av $(x\cdot y) /z$ , $(x/z)\cdot y$ , och $(y/z)\cdot x$ , och utforma ett transformationssystem att skriva om dessa uttryck till den formen, i processen att bevisa att alla ekvivalenta uttryck kommer att skrivas om till samma normala form. Men alla lösningar på ordproblemet använder inte en normalformsats – det finns algebraiska egenskaper som indirekt antyder att det finns en algoritm.

Medan ordproblemet frågar om två termer som innehåller konstanter är lika, frågar en korrekt förlängning av ordproblemet känt som unification problem om två termer $t_{1},t_{2}$ som innehåller variabler har instanser som är lika, eller med andra ord om ekvationen $t_{1}=t_{2}$ har några lösningar. Som ett vanligt exempel är $2+3{\stackrel {?}{=}}8+(-3)$ är ett ordproblem i heltalsgruppen ℤ , medan $2+x{\stackrel {?}{=}}8+(-x)$ är ett föreningsproblem i samma grupp; eftersom de förra termerna råkar vara lika i ℤ, har det senare problemet substitutionen { $\displaystyle \{x\mapsto 3\}}$ som lösning.

Historia

Ett av de mest djupgående studerade fallen av ordet problem är teorin om semigrupper och grupper . En tidslinje med artiklar som är relevanta för Novikov-Boone-satsen är följande:

• 1910 ( 1910 ) : Axel Thue ställer ett allmänt problem med termomskrivning på trädliknande strukturer. Han konstaterar "En lösning av detta problem i det mest allmänna fallet kan kanske hänga samman med oöverstigliga svårigheter".
• 1911 ( 1911 ) : Max Dehn ställer ordet problem för ändligt presenterade grupper.
• 1912 ( 1912 ) : Dehn presenterar Dehns algoritm och bevisar att den löser ordproblemet för de grundläggande grupperna av slutna orienterbara tvådimensionella grenrör av släktet större än eller lika med 2. Efterföljande författare har kraftigt utvidgat den till ett brett spektrum av gruppteoretiska beslutsproblem .
• 1914 ( 1914 ) : Axel Thue ställer ordproblemet för ändligt presenterade semigrupper.
• 1930 ( 1930 ) – 1938 ( 1938 ) : The Church-Turing-tesen framträder och definierar formella föreställningar om beräkningsbarhet och oavgörbarhet.
• 1947 ( 1947 ) : Emil Post och Andrey Markov Jr. konstruerar oberoende av varandra ändligt presenterade semigrupper med olösliga ordproblem. Posts konstruktion är byggd på Turing-maskiner medan Markovs använder Posts normala system.
• 1950 ( 1950 ) : Alan Turing visar att ordet problem för annulleringssemigrupper är olösligt, genom att främja Posts konstruktion. Beviset är svårt att följa men markerar en vändpunkt i ordproblemet för grupper.
• 1955 ( 1955 ) : Pyotr Novikov ger det första publicerade beviset på att ordet problem för grupper är olösligt, med hjälp av Turings annulleringssemigruppresultat. Beviset innehåller ett "Principal Lemma" som motsvarar Brittons Lemma .
• 1954 ( 1954 ) – 1957 ( 1957 ) : William Boone visar självständigt att ordet problem för grupper är olösligt, med hjälp av Posts semigroup-konstruktion.
• 1957 ( 1957 ) – 1958 ( 1958 ) : John Britton ger ytterligare ett bevis på att ordet problem för grupper är olösligt, baserat på Turings resultat av annulleringssemigrupper och en del av Brittons tidigare arbete. En tidig version av Brittons Lemma dyker upp.
• 1958 ( 1958 ) – 1959 ( 1959 ) : Boone publicerar en förenklad version av sin konstruktion.
• 1961 ( 1961 ) : Graham Higman karakteriserar undergrupperna av ändligt presenterade grupper med Higmans inbäddningsteorem , kopplar samman rekursionsteori med gruppteori på ett oväntat sätt och ger ett helt annat bevis på ordproblemets olöslighet.
• 1961 ( 1961 ) – 1963 ( 1963 ) : Britton presenterar en mycket förenklad version av Boones 1959 bevis på att ordet problem för grupper är olösligt. Den använder sig av ett gruppteoretiskt tillvägagångssätt, i synnerhet Brittons Lemma . Detta bevis har använts i en forskarutbildning, även om det finns mer moderna och förtätade bevis.
• 1977 ( 1977 ) : Gennady Makanin bevisar att den existentiella teorin om ekvationer över fria monoider är lösbar.

Ordet problem för semi-Thue-system

Tillgänglighetsproblemet för strängomskrivningssystem (semi-Thue-system eller semigroups) kan anges på följande sätt: Givet ett semi-Thue-system $T:=(\Sigma ,R)$ och två ord (strängar) $u,v\in \Sigma ^{*}$ , kan $u$ omvandlas till $v$ genom att tillämpa regler från $R$ ? Observera att omskrivningen här är enkelriktad. Ordet problem är tillgänglighetsproblemet för symmetriska omskrivningsrelationer, dvs Thue-system.

Tillgänglighets- och ordproblemen är oavgjorda , dvs det finns ingen generell algoritm för att lösa detta problem. Detta gäller även om vi begränsar systemen till att ha ändliga presentationer, dvs en ändlig uppsättning symboler och en ändlig uppsättning relationer på dessa symboler. Inte ens ordproblemet begränsat till grundtermer kan avgöras för vissa slutligt presenterade semigrupper.

Ordet problem för grupper

Huvudartikel: Ordproblem för grupper

Givet en presentation $\langle S\mid {\mathcal {R}}\rangle$ för en grupp G , är ordproblemet det algoritmiska problemet att avgöra, givet som indata två ord i S , om de representerar samma element av G . Ordet problem är ett av tre algoritmiska problem för grupper som föreslogs av Max Dehn 1911. Det visades av Pyotr Novikov 1955 att det finns en ändligt presenterad grupp G så att ordet problem för G är obestämbart .

Ordproblemet i kombinatorisk kalkyl och lambdakalkyl

Huvudartikel: Kombinatorisk logik § Oavgörbarhet av kombinatorisk kalkyl

Ett av de tidigaste bevisen på att ett ordproblem är oavgörbart var för kombinatorisk logik : när är två strängar av kombinatorer likvärdiga? Eftersom kombinatorer kodar för alla möjliga Turing-maskiner , och motsvarigheten av två Turing-maskiner är obestämbar, följer det att ekvivalensen mellan två strängar av kombinatorer är obestämbar. Alonzo Church observerade detta 1936.

På samma sätt har man i huvudsak samma problem i (otypad) lambda-kalkyl : givet två distinkta lambda-uttryck, finns det ingen algoritm som kan urskilja om de är ekvivalenta eller inte; likvärdighet är obestämbar . För flera typade varianter av lambda-kalkylen kan ekvivalens avgöras genom jämförelse av normala former.

Ordet problem för abstrakta omskrivningssystem

Att lösa ordproblemet: att bestämma om $x{\stackrel {*}{\leftrightarrow }}y$ kräver vanligtvis heuristisk sökning ( röd , grön ), samtidigt som man bestämmer $x\ nedåtpil =y\nedåtpil$ är enkel ( grå ).

Ordet problem för ett abstrakt omskrivningssystem (ARS) är ganska kortfattat: givna objekt x och y är de ekvivalenta under ${\stackrel {*}{\leftrightarrow }}$ ? Ordet problem för en ARS är i allmänhet oavgörbart . Det finns dock en beräkningsbar lösning för ordproblemet i det specifika fallet där varje objekt reduceras till en unik normalform i ett ändligt antal steg (dvs systemet är konvergent ): två objekt är ekvivalenta under ${\ stackrel {*}{\leftrightarrow }}$ om och endast om de reduceras till samma normala form. Knuth -Bendix-kompletteringsalgoritmen kan användas för att omvandla en uppsättning ekvationer till ett konvergent termomskrivningssystem .

Ordet problem i universell algebra

I universell algebra studerar man algebraiska strukturer som består av en genereringsmängd A, en samling operationer på A av finit aritet (typiskt binära operationer) och en finit uppsättning identiteter som dessa operationer måste uppfylla. Ordproblemet för en algebra är då att bestämma, givet två uttryck (ord) som involverar generatorerna och operationerna, om de representerar samma element i algebra modulo identiteterna. Ordproblemen för grupper och semigrupper kan formuleras som ordproblem för algebror.

Ordet problem på fria Heyting algebror är svårt. De enda kända resultaten är att den fria Heyting-algebra på en generator är oändlig, och att den fria fullständiga Heyting-algebra på en generator existerar (och har ett element mer än den fria Heyting-algebra).

Ordet problem för fria galler

Exempel på beräkning av x ∧ z ~ x ∧ z ∧( x ∨ y )

x ∧ z ∧( x ∨ y ) ≤ ~ x ∧ z vid 5. eftersom x ∧ z ≤ ~ x ∧ z vid 1. eftersom x ∧ z = x ∧ z

x ∧ z ≤ ~ x ∧ z ∧( x ∨ y ) vid 7. eftersom x ∧ z ≤ ~ x ∧ z och x ∧ z ≤ ~ x ∨ y vid 1. eftersom x ∧ z = x ∧ z vid 6. eftersom x ∧ z ≤ ~ x vid 5. eftersom x ≤ ~ x vid 1. eftersom x = x

Ordet problem på fria gitter och mer allmänt fritt avgränsade gitter har en avgörbar lösning. Begränsade gitter är algebraiska strukturer med de två binära operationerna ∨ och ∧ och de två konstanterna ( nullära operationer ) 0 och 1. Mängden av alla välformade uttryck som kan formuleras med hjälp av dessa operationer på element från en given uppsättning generatorer X kommer att kallas W ( X ). Denna uppsättning ord innehåller många uttryck som visar sig beteckna lika värden i varje gitter. Till exempel, om a är något element av X , då a ∨ 1 = 1 och a ∧ 1 = a . Ordet problem för fritt avgränsade gitter är problemet med att bestämma vilka av dessa element i W ( X ) som betecknar samma element i det fria avgränsade gittret FX , och därmed i varje avgränsat gitter.

Ordproblemet kan lösas på följande sätt. En relation ≤ _~ på W ( X ) kan definieras induktivt genom att ställa in w ≤ _~ v om och endast om något av följande gäller:

1.   w = v (detta kan begränsas till fallet där w och v är element i X ),
2.   w = 0,
3.   v = 1,
4.   w = w ₁ ∨ w ₂ och både w ₁ ≤ _~ v och w ₂ ≤ _~ v håller,
5.   w = w ₁ ∧ w ₂ och antingen w ₁ ≤ _~ v eller w ₂ ≤ _~ v gäller,
6.   v = v ₁ ∨ v ₂ och antingen w ≤ _~ v ₁ eller w ≤ _~ v ₂ gäller,
7.   v = v ₁ ∧ v ₂ och både w ≤ _~ v ₁ och w ≤ _~ v ₂ håller.

Detta definierar en förordning ≤ _~ på W ( X ), så en ekvivalensrelation kan definieras av w ~ v när w ≤ _~ v och v ≤ _~ w . Man kan då visa att det delvis ordnade kvotutrymmet W ( X )/~ är det fria gränsade gittret FX . Ekvivalensklasserna för W ( X )/~ är mängderna av alla ord w och v med w ≤ ~ v och v ≤ _~ w _. Två välformade ord v och w i W ( X ) betecknar samma värde i varje avgränsat gitter om och endast om w ≤ _~ v och v ≤ _~ w ; de senare villkoren kan effektivt avgöras med användning av ovanstående induktiva definition. Tabellen visar ett exempel på beräkning för att visa att orden x ∧ z och x ∧ z ∧( x ∨ y ) anger samma värde i varje avgränsat gitter. Fallet med gitter som inte är avgränsade behandlas på liknande sätt, utan reglerna 2 och 3 i ovanstående konstruktion av ≤ _~ .

Exempel: Ett termomskrivningssystem för att avgöra ordproblemet i den fria gruppen

Bläsius och Bürckert demonstrerar Knuth–Bendix-algoritmen på ett axiomuppsättning för grupper. Algoritmen ger ett sammanflytande och noterskt termomskrivningssystem som omvandlar varje term till en unik normalform . Omskrivningsreglerna är numrerade osammanhängande eftersom vissa regler blev överflödiga och raderades under algoritmkörningen. Likheten mellan två termer följer av axiomen om och endast om båda termerna omvandlas till bokstavligen samma normalformterm. Till exempel villkoren

$((a^{-1}\cdot a)\cdot (b\cdot b^{-1}))^{-1}{\stackrel {R2}{\rightsquigarrow }} (1\cdot (b\cdot b^{-1}))^{-1}{\stackrel {R13}{\rightsquigarrow }}(1\cdot 1)^{-1}{\stackrel {R1}{ \rightsquigarrow }}1^{-1}{\stackrel {R8}{\rightsquigarrow }}1$ och

$_ displaystyle b\cdot ((a\cdot b)^{-1}\cdot a){\stackrel {R17}{\rightsquigarrow }}b\cdot ((b^{-1}\cdot a^{-1} )\cdot a){\stackrel {R3}{\rightsquigarrow }}b\cdot (b^{-1}\cdot (a^{-1}\cdot a)){\stackrel {R2}{\rightsquigarrow } }b\cdot (b^{-1}\cdot 1){\stackrel {R11}{\rightsquigarrow }}b\cdot b^{-1}{\stackrel {R13}{\rightsquigarrow }}1}$

dela samma normala form, dvs. $1$ ; därför är båda termerna lika i varje grupp. Som ett annat exempel, termen $1\cdot (a\cdot b)$ och $b\cdot (1\cdot a)$ har det normala bilda $a\cdot b$ respektive $b\cdot a$ . Eftersom normalformerna är bokstavligen olika, kan inte de ursprungliga termerna vara lika i varje grupp. Faktum är att de vanligtvis är olika i icke-abelska grupper .

Gruppaxiom som används i Knuth–Bendix komplettering

A1	$1\cdot x$	$=x$
A2	$x^{-1}\cdot x$	$=1$
A3	$(x\cdot y)\cdot z$	$=x\cdot (y\cdot z)$

Termomskrivningssystem erhållet från Knuth–Bendix-komplettering

R1	$1\cdot x$	$\rightsquigarrow x$
R2	$x^{-1}\cdot x$	$\rightsquigarrow 1$
R3	$(x\cdot y)\cdot z$	$\rightsquigarrow x\cdot (y\cdot z)$
R4	$x^{-1}\cdot (x\cdot y)$	$\rightsquigarrow y$
R8	$1^{-1}$	$\rightsquigarrow 1$
R11	$x\cdot 1$	$\rightsquigarrow x$
R12	$(x^{-1})^{-1}$	$\rightsquigarrow x$
R13	$x\cdot x^{-1}$	$\rightsquigarrow 1$
R14	$x\cdot (x^{-1}\cdot y)$	$\rightsquigarrow y$
R17	$(x\cdot y)^{-1}$	$\rightsquigarrow y^{-1}\cdot x^{-1}$

Se även

• Konjugationsproblem
• Grupp isomorfism problem