Abstrakt. Vi utökar linjära π-kalculus med sammansatta regelbundna typer på ett sådant sätt att data som innehåller linjära värden kan delas mellan flera processer, om det inte finns någon överlappande tillgång till sådana värden. Vi beskriver en typkonstruktionsalgoritm för det utökade typsystemet och diskuterar några praktiska aspekter av dess genomförande. Den linjära π-calculus [15] är en formell modell för kommunikationsprocesser som skiljer mellan obegränsade och linjära kanaler. Obegränsade kanaler kan användas utan begränsningar, medan linjära kanaler endast kan användas för en kommunikation. Trots denna till synes allvarliga begränsning finns det bevis för att en betydande del av kommunikationen i de faktiska systemen sker på linjära kanaler [15]. Det har också visats att strukturerad kommunikation kan kodas med linjära kanaler och en fortsättnings-passerande stil [13, 3]. Intresset för linjära kanaler har solida motiv: linjära kanaler är effektiva att genomföra, de möjliggör viktiga optimeringar [9, 8, 15] och kommunikation på linjära kanaler har viktiga egenskaper såsom interferensfrihet och partiell konfluens [18, 15]. Av detta följer att förståelsen av huruvida en kanal används linjärt eller inte har en primär inverkan i analysen av system för kommunikationsprocesser. Typ rekonstruktion är problemet med att sluta sig till den typ av enheter som används i ett oannoterat (dvs. otypat) program. När det gäller den linjära π-calculus, översätter problemet till att förstå om en kanal är linjär eller obegränsad, och bestämma vilken typ av meddelanden som skickas över kanalen. Detta problem har åtgärdats och lösts [10]. Detta arbete har fått stöd av ICT COST Action IC1201 BETTY, MIER-projektet CINA, Ateneo/CSP-projektet SALT och det bilaterala projektet RS13MO12 DART. π-kalculus utsträckt med par, delade summor, och möjligen oändliga typer. Dessa egenskaper, om än standard, blir relevanta och kombineras på icke-triviala sätt med egenskaperna hos de linjära π-kalculus. Vi förklarar varför så är fallet i resten av detta avsnitt. Termen nedan modellerar ett program gjort av en ihållande tjänst (den *-prefixade processen väntar på meddelanden på kanal suc) som beräknar efterträdaren till ett nummer och en klient (den nya-scoped processen) som åberopar tjänsten och skriver ut resultatet av kallelsen. Varje meddelande som skickas till tjänsten är ett par av numret x och en fortsättningskanal y där tjänsten skickar resultatet av beräkningen tillbaka till klienten. Det finns tre kanaler i detta program, suc för åberopa tjänsten, skriva ut för utskriftsnummer, och en privat kanal en som används av kunden för att ta emot resultatet av kallelsen. I den linjära π-calculus, typer hålla reda på hur varje förekomst av en kanal används. Till exempel, ovanstående program är väl inskriven i miljön där typ av utskrift anger inte bara vilken typ av meddelanden som skickas över kanalen (int i detta fall), men också att utskrift aldrig används för inmatningsåtgärder (den 0 annotation) och används en gång för en utmatning (den 1 annotation).  När det gäller den begränsade kanalen a, dess högra förekomst används enligt typen [int] 1,0, Eftersom det en används för en inmatning av ett heltal tal; förekomsten av en i (39, a) är i ett meddelande som skickas på suc, och vi har redan hävdat att tjänsten använder denna kanal enligt typen [int] 0,1 ; typen av den vänstra, bindande förekomsten av en är kombinationen av dessa två typer, nämligen: Typen av en indikerar att programmet utför exakt en inmatning och exakt en utgång på en, därav a är en linjär kanal. Eftersom en är begränsad i programmet, även om programmet utökas med fler processer, är det inte möjligt att utföra operationer på en annan än de vi har spårat i sin typ. Den viktigaste ingrediensen i diskussionen ovan är begreppet typ kombination [15, 10, 24], vilket gör att vi kan samla det totala antalet input / output operationer som utförs på en kanal. Vi diskuterar nu hur typkombinationen sträcker sig till sammansatta och möjligen oändliga typer, vilket är den viktigaste nyheten i det nuvarande arbetet. TYPEN REKONSTRUKTION FÖR LINEAR π-CALCULUS Hittills har vi tagit för givet förmågan att utföra mönster matchning på meddelandet som tas emot av tjänsten på suc och att tilldela distinkta namn, x och y, till komponenterna i det par som analyseras. Mönstermatchning kompileras vanligen med hjälp av mer grundläggande operationer. Till exempel för par dessa operationer är fst och snd projektioner som respektive extrahera den första och den andra komponenten av paret. Så, en låg nivå modellering av den efterföljande tjänsten som använder fst och snd kan se ut så här: Denna version av tjänsten är operativt likvärdig med den tidigare, men från synpunkten att skriva det finns en intressant skillnad: i (1.1) de två komponenterna i paret ges distinkta namn x och y och varje namn används en gång i kroppen av tjänsten; i (1.2) det finns bara ett namn p för hela paret som projiceras två gånger i kroppen av tjänsten. Med tanke på att varje projektion endast kommer åt en av de två komponenterna i paret och ignorerar den andra, kan vi hävda att förekomsten av p i snd(p) används enligt typen int × [int] 0,1 (den 1 kommentaren återspeglar det faktum att den andra komponenten i p är en kanal som används för en utmatningsoperation) medan förekomsten av p i fst(p) används enligt typen int × [int] 0,0 (den andra komponenten i p används inte). Den viktigaste idén är alltså att vi kan utvidga typen kombinationsoperatör + komponent-wise till produkttyper för att uttrycka den totala typen av p som kombinationen av dessa två typer: Enligt resultatet av en sådan kombination, den andra komponenten av p används effektivt endast en gång trots de flera syntaktiska förekomster av p. Utvidgningen av typ kombination till produkter bär över till delade summor och även till oändliga typer. För att illustrera detta, betrakta den typ t-lista som uppfyller likheten som är den delade summan mellan Nil, typen av tomma listor, och Cons([int] 1,0 × t-lista ), typen av icke-tomma listor med huvud av typ [int] 1,0 och svans av typ t-lista (vi kommer inom kort att se att det finns en unik typ t-lista som uppfyller ovanstående jämlikhetsförhållande). Nu kan t-listan uttryckas som kombinationen t udda + t jämna, där t udda och t ens är de typer som uppfyller equalities t udda = Nil  på Cons ([int] 1,0 × t jämna ) och t jämn = Nil  på Cons ([int] 0,0 × t udda ) (1.3) (igen, det finns unika t udda och t även som uppfyller dessa equalities, se Avsnitt 3). Med ord, t udda är den typ av listor av kanaler där varje kanal i en udda indexerad position används för en inmatning, medan t ens är den typ av listor av kanal där varje kanal i en jämn indexerad position används för en inmatning. Anledningen till att denna speciella nedbrytning av t-listan kan vara intressant är att det möjliggör delning av en lista som innehåller linjära kanaler mellan två processer, om vi vet att en process använder listan enligt typ t udda och den andra processen använder samma lista enligt typ t även. För
I standard π-calculus, undantag från denna typ av linjäritet har studerats av Kobayashi i hans arbete om dödläge-fridom Padovani REF förlänger linjära π-kalculus med sammansatta regelbundna typer på ett sådant sätt att data som innehåller linjära värden kan delas mellan flera processer.
Type Reconstruction for the Linear \pi-Calculus with Composite Regular Types
{'venue': 'Logical Methods in Computer Science, Volume 11, Issue 4 (December 22, 2015) lmcs:1614', 'journal': None, 'mag_field_of_study': ['Computer Science', 'Mathematics']}