Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
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.


[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