Historia monoid

Inom matematik och datavetenskap är en historiemonoid ett sätt att representera historien om samtidigt pågående datorprocesser som en samling strängar , där varje sträng representerar en processs individuella historia. Historiemonoiden tillhandahåller en uppsättning synkroniseringsprimitiver (såsom lås , mutexer eller trådanslutningar ) för att tillhandahålla mötespunkter mellan en uppsättning självständigt exekverande processer eller trådar .

Historiemonoider förekommer i teorin om samtidig beräkning och ger en matematisk grund på låg nivå för processkalkyler , såsom CSP språket för att kommunicera sekventiella processer , eller CCS, kalkylen för kommunicerande system . Historia monoider presenterades först av MW Shields.

Historiemonoider är isomorfa för att spåra monoider (fria delvis kommutativa monoider) och till monoiden av beroendegrafer . Som sådana är de fria objekt och är universella . Historiemonoiden är en typ av semi-abelsk kategorisk produkt i kategorin monoider.

Produktmonoider och projektion

Låta

$A=(\Sigma _{1},\Sigma _{2},\ldots ,\Sigma _{n})$

beteckna en n -tuppel av (inte nödvändigtvis parvis disjunkta) alfabet $\Sigma _{k}$ . Låt $P(A)$ beteckna alla möjliga kombinationer av en ändlig sträng från varje alfabet:

$P(A)=\Sigma _{1}^{*}\times \Sigma _{2}^{*}\times \cdots \times \Sigma _{n}^{*}$

(På ett mer formellt språk är $P(A)$ den kartesiska produkten av de fria monoiderna i $\Sigma _{k}$ . Stjärnan är Kleene-stjärnan .) Sammansättningen i produkten monoid är komponentvis, så att, för

$\mathbf {u} =(u_{1},u_{2},\ldots ,u_{n})\,$

och

$\mathbf {v} =(v_{1},v_{2},\ldots ,v_{n})\,$

sedan

$\mathbf {uv} =(u_{1}v_{1},u_{2}v_{2},\ ldots ,u_{n}v_{n})\,$

för alla $\mathbf {u} ,\mathbf {v}$ i $P(A)$ . Definiera det fackliga alfabetet som ska vara

$\Sigma =\Sigma _{1}\cup \Sigma _{2}\cup \cdots \cup \Sigma _{n}.\,$

(Föreningen här är den fastställda unionen , inte den disjunkta unionen .) Givet vilken sträng ${\displaystyle w\in \Sigma ^{*}} som helst$ , kan vi välja ut bara bokstäverna i vissa ${\ displaystyle \Sigma _{k}^{*}}$ med motsvarande strängprojektion $\pi _{k}:\Sigma ^{*}\to \Sigma _{k} ^{*}$ . En fördelning $\pi :\Sigma ^{*}\to P(A)$ är avbildningen som fungerar på $w\in \Sigma ^{ *}$ med alla $\pi _{k}$ , separera den i komponenter i varje fri monoid:

$\pi (w)\mapsto (\pi _{1}(w),\pi _{2}(w),\ldots ,\pi _{n}(w)).\,$

Historier

För varje $a\in \Sigma$ kallas tuppeln ${\displaystyle \pi (a)} den$ elementära historien för en . Den fungerar som en indikatorfunktion för inkludering av en bokstav a i ett alfabet $\Sigma _{k}$ . Det är,

$\pi (a)=(a_{1},a_{2},\ldots ,a_{n})$

var

$a_{k}={\begin{cases}a{\mbox{ if }}a\in \Sigma _{k}\\\varepsilon {\mbox{ annars }}.\end{cases}}$

Här betecknar ${\displaystyle \varepsilon } den$ tomma strängen . Historiens monoid $H(A)$ är submonoiden för produkten monoid $P(A)$ som genereras av de elementära historierna: ${\displaystyle H(A)=\{\pi (a)|a\in \Sigma \}^{*}} ($ där den upphöjda stjärnan är Kleene-stjärnan tillämpad med en komponentvis definition av sammansättning enligt ovan). Elementen i $H(A)$ kallas global historia och projektionerna av en global historia kallas individuella historier .

Koppling till datavetenskap

Användningen av ordet historia i detta sammanhang, och kopplingen till concurrent computing, kan förstås på följande sätt. En individuell historia är ett register över sekvensen av tillstånd i en process (eller tråd eller maskin ); alfabetet $\Sigma _{k}$ är uppsättningen av tillstånd för processen.

En bokstav som förekommer i två eller flera alfabet fungerar som en synkroniseringsprimitiv mellan de olika individuella historierna. Det vill säga, om ett sådant brev förekommer i en enskild historia, måste det också förekomma i en annan historia, och tjänar till att "knyta" eller "träffa" dem tillsammans.

Betrakta till exempel $\Sigma _{1}=\{a,b,c\}$ och $\ Sigma _{2}=\{a,d,e\}$ . Fackliga alfabetet är givetvis $\Sigma =\{a,b,c,d,e\}$ . De elementära historierna är $(a,a)$ , $(b,\varepsilon )$ , $(c,\varepsilon )$ , $(\varepsilon ,d)$ och $(\varepsilon ,e)$ . I det här exemplet kan en individuell historik för den första processen vara $bcbcc$ medan den individuella historiken för den andra maskinen kan vara $ddded$ . Båda dessa individuella historier representeras av den globala historien $bcbdddcced$ , eftersom projektionen av denna sträng på de individuella alfabeten ger de individuella historierna. I den globala historien kan bokstäverna $b$ och $c$ anses pendla med bokstäverna $d$ och $e$ , genom att dessa kan ordnas om utan att ändras de individuella historierna. Sådan kommutering är helt enkelt ett uttalande om att den första och andra processen körs samtidigt och är oordnade i förhållande till varandra; de har (ännu) inte utbytt några meddelanden eller utfört någon synkronisering.

Bokstaven $a$ fungerar som en primitiv för synkronisering, eftersom dess förekomst markerar en plats i både den globala och individuella historien, som inte kan pendlas över. Således, även om bokstäverna $b$ och $c$ kan ordnas om efter $d$ och $e$ , kan de inte ordnas om efter $a$ . Sålunda har den globala historien $bcdabe$ och den globala historien $bdcaeb$ båda som individuella historier $bcab$ och ${ \displaystyle dae}$ , vilket indikerar att exekveringen av $d$ kan ske före eller efter $c$ . Bokstaven $a$ synkroniserar dock, så att $e$ garanterat inträffar efter $c$ , även om $e$ är i en annan process än ${\ displaystil c}$ .

Egenskaper

En historia monoid är isomorphic till en spår monoid , och som sådan, är en typ av semi-abelian kategorisk produkt i kategorin monoids. I synnerhet är historikmonoiden $H(\Sigma _{1},\Sigma _{2},\ldots ,\Sigma _{n})$ isomorf till spårmonoiden $\mathbb {M} (D)$ med beroenderelationen som ges av

$D=\left(\Sigma _{1}\times \Sigma _{1}\right)\cup \left(\Sigma _{2}\times \Sigma _{2}\right)\cup \ cdots \cup \left(\Sigma _{n}\times \Sigma _{n}\right).$

Enkelt uttryckt är detta bara det formella uttalandet i den informella diskussionen ovan: bokstäverna i ett alfabet $\Sigma _{k}$ kan omordnas kommutativt efter bokstäverna i ett alfabet ${\ displaystyle \Sigma _{j}}$ , såvida de inte är bokstäver som förekommer i båda alfabeten. Således är spår exakt globala historier, och vice versa.

Omvänt, givet varje spårmonoid ${\displaystyle \mathbb {M} (D)} , kan man konstruera en$$\ Sigma _{a,b}=\{a,b\}$ historiemonoid genom att ta en sekvens av alfabet där $(a,b)$ sträcker sig över alla par i $D$ .

Anteckningar

•   Antoni Mazurkiewicz, "Introduction to Trace Theory", s 3–41, i The Book of Traces , V. Diekert, G. Rozenberg, red. (1995) World Scientific, Singapore ISBN 981-02-2058-8
• Volker Diekert, Yves Métivier, " Partial Commutation and Traces ", I G. Rozenberg och A. Salomaa , redaktörer, Handbook of Formal Languages ​​, Vol. 3 , Beyond Words, sidorna 457–534. Springer-Verlag, Berlin, 1997.