Coherent Semantics

CS358, Spring 1995

1 Coherent Spaces

1.1. Definition (coherent space). A coherent space is a reflexive undirected graph, i.e. it consists of a set |X| together with a coherence relation between atoms, noted x⌢ ⌣y [mod X]. A clique a in X is a subset a of X made of pairwise coherent atoms. Two atoms x and y are strictly coherent in X (x⌢y [mod X]) if they are coherent and distinct. They are incoherent (x⌣ ⌢y [mod X]) if they are not strictly coherent. They are strictly incoherent (x⌣y [mod X]) if they are not coherent.

1.2. Definition (linear negation). The linear negation X^{⊥} of a coherent space X is defined by

• |X^{⊥}| = |X|,

• x⌢ ⌣y [mod X^{⊥}] iff x⌣ ⌢y [mod X].

1.3. Definition (multiplicatives). Given two coherent spaces X and Y, the multiplicative connectives ⊗ and ℘ define a new coherent space with

• |X ⊗ Y | = |X℘Y | = |X| × |Y |,

• (x, y)⌢ ⌣(x′, y′) [mod X ⊗ Y] iff x⌢ ⌣x′ [mod X] and y⌢ ⌣y′ [mod Y],

• (x, y)⌢(x′, y′) [mod X℘Y] iff x⌢x′ [mod X] or y⌢y′ [mod Y].

1.4. Definition (additives). Given two coherent spaces X and Y the additive connectives & and ⊕ define a new coherent space with

• |X&Y | = |X ⊕ Y | = |X| + |Y |,

• (x, 0)⌢ ⌣(x′, 0) [mod X&Y] or [mod X ⊕ Y] iff x⌢ ⌣x′ [mod X],

• (y, 1)⌢ ⌣(y′, 1) [mod X&Y] or [mod X ⊕ Y] iff y⌢ ⌣y′ [mod Y],

• (x, 0)⌢(y, 1) [mod X&Y] for all x ∈ |X| and y ∈ |Y |,

• (x, 0)⌣(y, 1) [mod X ⊕ Y] for all x ∈ |X| and y ∈ |Y |.

1.5. Definition (constants). Up to isomorphism there is a unique coherent space whose web consists of one atom, and a unique coherent space whose web doesn’t contain any atom. Both spaces are self dual. Denote the first one by 1 and ⊥, and the second by ⊤ and 0.

1.6. Definition (exponentials). If X is a coherent space, then !X and ?X are defined as follows

• |!X| = {{x_{1}, …, x_{n}} | x_{i}⌢ ⌣x_{j} [mod X] for all i and j },

• |?X| = {{x_{1}, …, x_{n}} | x_{i}⌣ ⌢x_{j} [mod X] for all i and j },

• {x_{1}, …, x_{n}}⌢ ⌣{y_{1}, …, y_{m}} [mod !X] iff x_{i}⌢ ⌣y_{j} [mod X] for all i and j,

• {x_{1}, …, x_{n}}⌢{y_{1}, …, y_{m}} [mod ?X] iff x_{i}⌢y_{j} [mod X] for some i and j.

2 Isomorphisms

The following isomorphisms follow immediately from the definitions: De Morgan equalities

(X ⊗ Y)^{⊥} = X^{⊥}℘Y^{⊥} (X℘Y)^{⊥} = X^{⊥} ⊗ Y^{⊥} (X&Y)^{⊥} = X^{⊥} ⊕ Y^{⊥} (X ⊕ Y)^{⊥} = X^{⊥}&Y^{⊥} (!X)^{⊥} = ?(X^{⊥}) (?X)^{⊥} = !(X^{⊥})

commutativity isomorphisms X ⊗ Y ≃ Y ⊗ X X℘Y ≃ Y ℘X X&Y ≃ Y &X X ⊕ Y ≃ Y ⊕ X

associativity isomorphisms X ⊗ (Y ⊗ Z) ≃ (X ⊗ Y) ⊗ Z X℘(Y ℘Z) ≃ (X℘Y)℘Z X&(Y &Z) ≃ (X&Y)&Z X ⊕ (Y ⊕ Z) ≃ (X ⊕ Y) ⊕ Z

distributivity isomorphisms

X ⊗ (Y ⊕ Z) ≃ (X ⊗ Y) ⊕ (X ⊗ Z) X℘(Y &Z) ≃ (X℘Y)&(X℘Z) neutrality isomorphisms

X⊗ 1 ≃ X X℘⊥ ≃ X X⊕ 0 ≃ X X&⊤ ≃ X

absorption isomorphisms

X⊗ 0 ≃ 0 X℘⊤ ≃ ⊤ exponential isomorphisms

!(X&Y) ≃ (!X) ⊗ (!Y) ?(X ⊕ Y) ≃ (?X)℘(?Y) !⊤ ≃ 1 ?0 ≃ ⊥

3 Interpretation of Proofs

3.1. Definition (interpretation of proofs). A proof π of a sequent ⊢ A_{1}, …, A_{n} is interpreted by a clique π^{∗} of the coherent space A_{1}℘ … ℘A_{n}. π^{∗} is defined by induction on the proof π of ⊢ A_{1}, …, A_{n}:

1. If π is the axiom ⊢ A, A^{⊥}, then π^{∗} = {xx | x ∈ |A|}.

2. If π is obtained from π′ and π′′ by the cut rule

\frac{⊢ Γ, A ⊢ A^{⊥}, Δ}{⊢ Γ, Δ}

then π^{∗} = {x⃗y⃗ | ∃z ∈ |A|. (x⃗z ∈ π′^{∗} and zy⃗ ∈ π′′^{∗})}.

3. If π is obtained from π′ by the exchange rule replacing Γ by a permutation σ(Γ), then π^{∗} = {σ(x⃗) | x⃗ ∈ π′^{∗}}.

4. If π is the axiom ⊢ 1, then π^{∗} consists of the single atom of the coherent space 1.

5. If π is obtained from π′ by the rule (⊥)

\frac{⊢ Γ}{⊢ ⊥, Γ}

then π^{∗} = {0x⃗ | x⃗ ∈ π′^{∗}} where 0 is the single atom of the coherent space 1.

6. If π is obtained from π′ and π′′ by (⊗)

\frac{⊢ A, Γ ⊢ B, Δ}{⊢ A ⊗ B, Γ, Δ}

then π^{∗} = {(z, z′)x⃗y⃗ | zx⃗ ∈ π′^{∗} and z′y⃗ ∈ π′′^{∗}}.

7. If π is obtained from π′ by the rule (℘)

\frac{⊢ A, B, Γ}{⊢ A℘B, Γ}

then π^{∗} = {(x, y)z⃗ | xyz⃗ ∈ π′^{∗}}.

8. If π is the axiom ⊢ ⊤, Γ, then π^{∗} = {}.

9. If π is obtained from π′ and π′′ by (&)

\frac{⊢ A, Γ ⊢ B, Γ}{⊢ A&B, Γ}

then π^{∗} = {(x, 0)y⃗ | xy⃗ ∈ π′^{∗}} ∪ {(x, 1)y⃗ | xy⃗ ∈ π′′^{∗}}.

10. If π is obtained from π′ by the rule (⊗L)

\frac{⊢ A, Γ}{⊢ A ⊕ B, Γ}

then π^{∗} = {(x, 0)y⃗ | xy⃗ ∈ π′^{∗}}.

11. If π is obtained from π′ by the rule (⊗R)

\frac{⊢ B, Γ}{⊢ A ⊕ B, Γ}

then π^{∗} = {(x, 1)y⃗ | xy⃗ ∈ π′^{∗}}.

12. If π is obtained from π′ by the weakening rule

\frac{⊢ Γ}{⊢?A, Γ}

then π^{∗} = {{}x⃗ | x⃗ ∈ π′^{∗}}.

13. If π is obtained from π′ by the dereliction rule

\frac{⊢ A, Γ}{⊢?A, Γ}

then π^{∗} = {{x}y⃗ | xy⃗ ∈ π′^{∗}}.

14. If π is obtained from π′ by the contraction rule

\frac{⊢?A,?A, Γ}{⊢?A, Γ}

then π^{∗} = {x ∪ y, z⃗ | xyz⃗ ∈ π′^{∗}}.

15. If π is obtained from π′ by the storage rule

\frac{⊢ A,?Γ}{⊢!A,?Γ}

then π^{∗} = {{x_{1}, …, x_{n}}y⃗ | y⃗ = y_{11} ∪…∪y_{n1}, …, y_{1m} ∪…∪y_{nm}, x_{i}y_{i1} … y_{im} ∈ π′^{∗} for i = 1, …, n, y⃗ ∈?Γ, {x_{1}, …, x_{n}} ∈ !A}.

References

[1] J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987.

[2] J.-Y. Girard. Linear Logic: Its Syntax and Semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, Cambridge University Press, 1995. Proceedings of the Workshop in Linear Logic, Ithaca, New York, June 1993.