28 mai 2015, 11:00 : Séminaire

Olivier Laurent (LIP, ÉNS Lyon), Treillis et extensions de la logique linéaire additive

Certaines structures ordonnées libres peuvent être représentées à l'aide de la relation de déduction du calcul des séquents. En particulier, Withman a montré par anticipation en 1941 que la relation de déduction en logique linéaire additive (ALL) bilatère correspond au treillis libre. Nous regarderons diverses extensions de ce résultat en définissant des variantes de ALL qui capturent : treillis borné, treillis distributif, treillis avec involution, ortho-treillis, algèbre de Boole, etc. Si la plupart de ces résultats semblent bien connus dans le folklore, il est amusant de les ranger dans ce cadre commun éclairé par le projecteur de la logique linéaire. Dans le même esprit, nous regarderons comment représenter en calcul des séquents la relation d'ordre sous-jacente à des systèmes de types avec intersection.

Du 8 au 12 juin 2015

Rencontre du GT GéoCal du GDR-IM (voir le programme).

18 juin 2015, 11:00 : Séminaire

Fabio Zanasi (LIP, ÉNS Lyon), Interacting Hopf algebras: the string diagrammatic theory of linear subspaces

We introduce the theory IH of interacting Hopf algebras, parametrised over a principal ideal domain R. The axioms of IH are derived using Lack’s approach to composing PROPs: they feature two Hopf algebras and two Frobenius algebras. This construction is instrumental in showing that IH is a presentation by generators and equations of the PROP of linear relations (i.e. subspaces) over the field of fractions of R.

The equational theory IH turns out to be useful in various contexts. For R=Z, it expresses rational subspaces. The case R=Z_2 is of importance for describing quantum computation. In this talk we will focus on the case R=k[x], in which IH yields a compositional stream semantics for linear dynamical systems (signal flow graphs).