BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:The dual of pattern matching - copattern matching
- Anton Setzer\, Swansea University
DTSTART:20131122T160000Z
DTEND:20131122T170000Z
UID:TALK1248AT
URL:/talk/index/1248
DESCRIPTION:Because of the importance of interactive programs\
, which \nresult in potentially infinite computati
on traces\,\ncoalgebraic data types play an \nimpo
rtant role in computer science.\nCoalgebraic data
types are often represented in functional\nprogram
ming as codata types.\nImplicit in the formulation
of codata types is that \nevery element of the co
algebra is introduced by a constructor.\n\nThe fir
st result demonstrated in this talk will be to sho
w that assuming that every element of the coalgebr
a is introduced\nby a constructor results in an un
decidable equality.\n\nIn order to have a decidabl
e equality modifications were \nadded to the rules
in Agda and Coq. \nThis results in lack of subjec
t reduction in the\ntheorem prover Coq and a formu
lation of coalgebraic types\nin Agda which is seve
rely restricted. \n\nIn our joint article with And
reas Abel\, Brigitte Pientka and David Thibodeau w
e \ndemonstrated how\, when following the well kno
wn fact in category theory that\nfinal coalgebras
are the dual of initial algebras\, we obtain \na
formulation of final and weakly final coalgebras t
hat is \ncompletely symmetrical to that\nof initia
l or weakly initial algebras. Introduction rules f
or algebras are\ngiven by the constructors\, where
as elimination rules\ncorrespond to recursive patt
ern matching.\nElimination rules for coalgebras ar
e given by destructors\,\nwhereas introduction rul
es are given by recursive\ncopattern matching. The
resulting theory was shown to fulfil subject redu
ction\,\nwhile allowing nested pattern and copatte
rn matching and even mixing of the \ntwo. In our a
pproach full recursion was allowed.\n\nIn our talk
we will introduce this approach in detail and how
to program\nusing this approach. Then we will sho
w how to to \nunfold nested (co)pattern matching\,
reduce it to (co)recursion operators\, and\, \nin
the case that should be accepted by a termination
checker\, to primitive \n(co)recursion operators.
\n
LOCATION:UG10 Learning Centre
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR