Logical Approaches to Computational Barriers

A Sequent Calculus for Intersection and Union Logic

Speaker:
| Anastasia Veneti |

Author(s): |
Anastasia Veneti and Yiorgos Stavrinos |

Slot: |
Array, 11:00-11:20, col. 4 |

We present a logical formalism for the
*intersection and union type assignment system* IUT [1]. A
first attempt to this end is the
intersection and union logic IUL, a logic whose main structures are binary
trees called *kits* [3,4]. The rules of IUL are in natural
deduction style and are categorized as *global* or
*local* according to whether they affect all leaves of the
kits involved or not. While rules for the intersection and union are meant to
be local, the complex notation of kits conceals a certain kind of globality
inherent in the union elimination rule. This becomes explicit if we abandon
kits and resort to the linear structures employed in [2]. These structures are
multisets of judgements (*atoms*) called
*molecules*. A logic for IUT using molecules, but still in
natural deduction style, incorporates a *union elimination
rule*

[(Γ_{i} ⊢
φ_{i})]_{i}
∪
[(Γ ⊢ σ ∪ τ)]
[(Γ_{i}, φ_{i}
⊢ ψ_{i})]_{i}
∪
[(Γ, σ ⊢ ρ),(Γ,
τ ⊢ ρ)]

-----------------------------------------------------------------------------------------
(∪E)

[(Γ_{i} ⊢
ψ_{i})]_{i} ∪
[(Γ ⊢ ρ)]

which has both a global and a local behaviour. Here globality and locality
refer to the number of atoms modified by the rule in the premise molecules.

In the present work we describe IUL with molecules
in sequent calculus style. The main advantage of this formulation is that
globality and locality of the union elimination rule are separated in the
*cut rule*
and *left union rule*, respectively.

[(Γ_{i} ⊢
φ_{i})]_{i}
[(Γ_{i}, φ_{i}
⊢
ψ_{i})]_{i}

-------------------------------------
(cut)

[(Γ_{i} ⊢
ψ_{i})]_{i}

M ∪ [(Γ, σ ⊢
ρ),(Γ,
τ ⊢ ρ)]

----------------------------------
(L∪)

M ∪ [(Γ, σ ∪
τ ⊢ ρ)]

These improvements lead the way in yielding the
relation of IUT to the logic IUL.

**References**

[1] Barbanera F., Dezani-Ciancaglini M., and de'Liguoro U., Intersection and Union Types: Syntax and Semantics, Information and Computation 119, 202--230 (1995)

[2] Pimentel E., Ronchi Della Rocca S., and Roversi L., Intersection Types from a proof-theoretic perspective, 4th Workshop on Intersection Types and Related Systems, Torino (2008)

[3] Ronchi Della Rocca S. and Roversi L., Intersection Logic, Proceedings of CSL'01, LNCS 2142, 414--428 (2001)

[4] Veneti A. and Stavrinos Y., Towards an intersection and union logic, 4th Workshop on Intersection Types and Related Systems, Torino (2008)

websites: Arnold Beckmann | 2008-06-15 |