๐”– Bobbio Scriptorium
โœฆ   LIBER   โœฆ

On phase semantics and denotational semantics: the exponentials

โœ Scribed by Antonio Bucciarelli; Thomas Ehrhard


Publisher
Elsevier Science
Year
2001
Tongue
English
Weight
281 KB
Volume
109
Category
Article
ISSN
0168-0072

No coin nor oath required. For personal study only.

โœฆ Synopsis


We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard (Ann. Pure. Appl. Logic 102 (3) (2000) 247). We deรฟne an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula A of linear logic, and a family A of elements of |A|, the interpretation of A in the category of sets and relations. Then A is provable in indexed linear logic i the family A is contained in the interpretation of some proof of A. We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard (2000), deรฟning the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A ( B contains informations about the behavior of this proof when applied to "chimeric" arguments of type A (for instance: booleans whose value can change during the computation). In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be "neutral" (that is, neither strictly coherent, nor strictly incoherent).


๐Ÿ“œ SIMILAR VOLUMES


Operational and goal-independent denotat
โœ Fausto Spoto ๐Ÿ“‚ Article ๐Ÿ“… 2000 ๐Ÿ› Elsevier Science ๐ŸŒ English โš– 454 KB

In this paper we propose an operational and a denotational semantics for Prolog. We deal with the control rules of Prolog and the cut operator. Our denotational semantics provides a goal-independent semantics. This means that the behaviour of a goal in a program is deยฎned as the evaluation of the go

On the semantics of polymorphism
โœ Mario Coppo ๐Ÿ“‚ Article ๐Ÿ“… 1983 ๐Ÿ› Springer-Verlag ๐ŸŒ English โš– 598 KB