Abstract
A discriminator partitions values associated with keys into groups listed in ascending order. Discriminators can be defined generically by structural recursion on representations of ordering relations. Employing type-indexed families we demonstrate how tries with an optimaltime lookup function can be constructed generically in worst-case linear time. We provide generic implementations of comparison, sorting, discrimination and trie building functions and give equational proofs of correctness that highlight core relations between these algorithms.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems : 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings |
Editors | Chung-chieh Shan |
Number of pages | 18 |
Publisher | Springer |
Publication date | 2013 |
Pages | 315-332 |
ISBN (Print) | 978-3-319-03542-0 |
ISBN (Electronic) | 978-3-319-03542-0 |
DOIs | |
Publication status | Published - 2013 |
Event | 11th Asian Symposium on Programming Languages and Systems - Melbourne, Australia Duration: 9 Dec 2013 → 11 Dec 2013 Conference number: 11 |
Conference
Conference | 11th Asian Symposium on Programming Languages and Systems |
---|---|
Number | 11 |
Country/Territory | Australia |
City | Melbourne |
Period | 09/12/2013 → 11/12/2013 |
Series | Lecture notes in computer science |
---|---|
Volume | 8301 |
ISSN | 0302-9743 |