کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662197 | 1633480 | 2012 | 30 صفحه PDF | دانلود رایگان |
We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach (in the sense of ludics, Girard, 2001 [11], ) related to game semantics (Hyland and Ong, 2000 [17], , Abramsky et al., 1994 [2], ) and the Danos–Regnier interpretation of GoI operators as paths in proof nets (Asperti et al., 1994 [3], , Danos and Regnier, 1995 [4], ). We show how we can retrieve from this locative framework both a categorical semantics for Multiplicative Linear Logic (MLL) with distinct units and a notion of truth. Moreover, we show how a restricted version of our model can be reformulated in the exact same terms as Girardʼs geometry of interaction (Girard, 2011 [14]). This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girardʼs geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions.
Journal: Annals of Pure and Applied Logic - Volume 163, Issue 12, December 2012, Pages 1808-1837