Sorting and searching by distribution: from generic discrimination to generic tries

Fritz Henglein; Ralf Hinze

doi:10.1007/978-3-319-03542-0_23

Sorting and searching by distribution: from generic discrimination to generic tries

Fritz Henglein, Ralf Hinze

Datalogisk Institut

1 Citationer (Scopus)

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.

Originalsprog	Engelsk
Titel	Programming Languages and Systems : 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings
Redaktører	Chung-chieh Shan
Antal sider	18
Forlag	Springer
Publikationsdato	2013
Sider	315-332
ISBN (Trykt)	978-3-319-03542-0
ISBN (Elektronisk)	978-3-319-03542-0
DOI	https://doi.org/10.1007/978-3-319-03542-0_23
Status	Udgivet - 2013
Begivenhed	11th Asian Symposium on Programming Languages and Systems - Melbourne, Australien Varighed: 9 dec. 2013 → 11 dec. 2013 Konferencens nummer: 11

Konference

Konference	11th Asian Symposium on Programming Languages and Systems
Nummer	11
Land/Område	Australien
By	Melbourne
Periode	09/12/2013 → 11/12/2013

Navn	Lecture notes in computer science
Vol/bind	8301
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-319-03542-0_23

Citationsformater

Sorting and searching by distribution: from generic discrimination to generic tries. / Henglein, Fritz; Hinze, Ralf.
Programming Languages and Systems: 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. red. / Chung-chieh Shan. Springer, 2013. s. 315-332 (Lecture notes in computer science, Bind 8301).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Henglein, F & Hinze, R 2013, Sorting and searching by distribution: from generic discrimination to generic tries. i C Shan (red.), Programming Languages and Systems: 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. Springer, Lecture notes in computer science, bind 8301, s. 315-332, 11th Asian Symposium on Programming Languages and Systems, Melbourne, Australien, 09/12/2013. https://doi.org/10.1007/978-3-319-03542-0_23

@inproceedings{e0d77191027a498d9190e6fe944ca10d,

title = "Sorting and searching by distribution: from generic discrimination to generic tries",

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.",

author = "Fritz Henglein and Ralf Hinze",

year = "2013",

doi = "10.1007/978-3-319-03542-0_23",

language = "English",

isbn = "978-3-319-03542-0",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "315--332",

editor = "Chung-chieh Shan",

booktitle = "Programming Languages and Systems",

note = "11th Asian Symposium on Programming Languages and Systems, APLAS 2013 ; Conference date: 09-12-2013 Through 11-12-2013",

}

TY - GEN

T1 - Sorting and searching by distribution

T2 - 11th Asian Symposium on Programming Languages and Systems

AU - Henglein, Fritz

AU - Hinze, Ralf

N1 - Conference code: 11

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-03542-0_23

DO - 10.1007/978-3-319-03542-0_23

M3 - Article in proceedings

SN - 978-3-319-03542-0

T3 - Lecture notes in computer science

SP - 315

EP - 332

BT - Programming Languages and Systems

A2 - Shan, Chung-chieh

PB - Springer

Y2 - 9 December 2013 through 11 December 2013

ER -

Sorting and searching by distribution: from generic discrimination to generic tries

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater