![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > The dual of pattern matching - copattern matching
The dual of pattern matching - copattern matchingAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Paul Levy. Because of the importance of interactive programs, which result in potentially infinite computation traces, coalgebraic data types play an important role in computer science. Coalgebraic data types are often represented in functional programming as codata types. Implicit in the formulation of codata types is that every element of the coalgebra is introduced by a constructor. The first result demonstrated in this talk will be to show that assuming that every element of the coalgebra is introduced by a constructor results in an undecidable equality. In order to have a decidable equality modifications were added to the rules in Agda and Coq. This results in lack of subject reduction in the theorem prover Coq and a formulation of coalgebraic types in Agda which is severely restricted. In our joint article with Andreas Abel, Brigitte Pientka and David Thibodeau we demonstrated how, when following the well known fact in category theory that final coalgebras are the dual of initial algebras, we obtain a formulation of final and weakly final coalgebras that is completely symmetrical to that of initial or weakly initial algebras. Introduction rules for algebras are given by the constructors, whereas elimination rules correspond to recursive pattern matching. Elimination rules for coalgebras are given by destructors, whereas introduction rules are given by recursive copattern matching. The resulting theory was shown to fulfil subject reduction, while allowing nested pattern and copattern matching and even mixing of the two. In our approach full recursion was allowed. In our talk we will introduce this approach in detail and how to program using this approach. Then we will show how to to unfold nested (co)pattern matching, reduce it to (co)recursion operators, and, in the case that should be accepted by a termination checker, to primitive (co)recursion operators. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsAnalysis Reading Seminar 2019/2020 PIPS - Postgraduate Informal Physics Seminars BritGrav 15Other talksTBA TBA Ultrafast Spectroscopy and Microscopy as probes of Energy Materials The tragic destiny of Mileva Marić Einstein Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Quantum Sensing in Space |