Vi visar ett komplett resultat för Multiplicativ Exponential Linear Logic (MELL): vi visar att relationsmodellen är injicerande för MELL proof-nets, d.v.s. Likheten mellan MELL-proof-nets i relationsmodellen är exakt axiomatized genom cut-eliminering. I den seminala papper av Harvey Friedman [11], har det visat sig att jämlikhet mellan helt enkelt-typade lambda termer i den fullskrivna strukturen M X över en infnite uppsättning X är helt axiomatized av β och η: Ett naturligt problem är att veta om ett liknande resultat kunde erhållas för linjär Logic. Ett sådant resultat kan ses som en "separation" sats. För att erhålla sådana separationsteoremer, är det en prerequesite att ha en "kanonisk" syntax. När Jean-Yves Girard introducerade Linjär Logic (LL) [12] införde han inte bara ett sekventiellt kalkylsystem utan också "proof-nets". När det gäller LJ och LK (sekventa kalkylsystem för intuitionslogik respektive klassisk logik) kan olika bevis i LL sequent calculus representera "moraliskt" samma bevis: proof-nets infördes för att hitta en unik representant för dessa bevis. Tekniken med bevisnät var helt tillfredsställande för det multiplikativa fragmentet utan enheter. För proof-nät med tillsatser, sammandragningar eller försvagningar var det lätt att uppvisa olika proof-nät som borde identifieras. Trots vissa brister var upptäckten av bevisnät slående. Vincent Danos bevisade med syntaktiska medel [3] sammanflödet av dessa bevisnät för det multiplikativa exponentiella linjära logiska fragmentet (MELL). När det gäller tillsatser har problemet med att ha ett tillfredsställande begrepp om bevisnät tagits upp [15]. För MELL infördes en "ny syntax" [4]. I den ursprungliga syntaxen fanns inte följande egenskaper hos försvagningen och sammandragningen: • sammandragningens associativitet; • neutraliteten i försvagningen för sammandragningen; • sammandragningen och försvagningen som morfism hos kolgebras. Men de håller i den nya syntaxen; åtminstone för MELL fick vi en syntax som var en bra kandidat som förtjänade att betraktas som "kanonisk". Sedan försöker bevisa att två (η-expanderade) MELL-proof-nät som är lika i vissa denotationala semantik är β-kominable har blivit förnuftig och hade åtminstone de två följande motiven: • att bevisa kanoniciteten hos den "nya syntaxen" (om vi quotienterar mer normala proof-nät, då skulle vi identifiera proof-nets som har olika semantik); • att bevisa med semantik betyder konfluensen (om ett proof-net minskar till två cut-free proof-nets, då har de samma semantik, så de skulle vara β-joinable, alltså lika). 1 För det multiplikativa fragmentet med enheter har det nyligen visat sig [14] att det på något sätt inte finns någon tillfredsställande uppfattning om bevisnät. Våra proof-nets har inget hopp, så de identifierar för många sequent calculus-bevis, men inte mer än relationssemantiken.
De Carvalho visade att relationsmodellen är injicerande för MELL REF.
The relational model is injective for Multiplicative Exponential Linear Logic
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science', 'Mathematics']}