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

Department of Computer Science

1 Citation (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.

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	https://doi.org/10.1007/978-3-319-03542-0_23
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

Access to Document

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

Cite this

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. ed. / Chung-chieh Shan. Springer, 2013. p. 315-332 (Lecture notes in computer science, Vol. 8301).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Henglein, F & Hinze, R 2013, Sorting and searching by distribution: from generic discrimination to generic tries. in C Shan (ed.), Programming Languages and Systems: 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. Springer, Lecture notes in computer science, vol. 8301, pp. 315-332, 11th Asian Symposium on Programming Languages and Systems, Melbourne, Australia, 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

Conference

Access to Document

Fingerprint

Cite this