categories - Category Theory list
 help / color / mirror / Atom feed
* Proof nets
@ 2004-07-19 12:05 Robin Houston
  0 siblings, 0 replies; only message in thread
From: Robin Houston @ 2004-07-19 12:05 UTC (permalink / raw)
  To: categories

Dear categorists,

The category of ordinary MLL proof nets (where an object is a term,
and a morphism X -> Y is a cut-free proof net for |- X^, Y) is the
free unitless *-autonomous category generated by the literals.

Does the corresponding result hold for MALL? The Hughes-van Glabeek
notion of MALL proof net has the ring of truth about it, and indeed
they claim to have proven (theorem 4.22) that "two cut-free MALL
proofs translate to the same proof net iff they can be converted into
each other by a series of rule commutations". Of course the category
of MALL proof nets is a unitless *-autonomous category with binary
products and coproducts, but nowhere (to my knowledge) is it described
as the *free* such category.

Is that because it isn't, or merely because it isn't (yet) known to be?
Enlightenment will be much appreciated.

Yours,
Robin




^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2004-07-19 12:05 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2004-07-19 12:05 Proof nets Robin Houston

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).