-
Notifications
You must be signed in to change notification settings - Fork 1
/
meta.yml
208 lines (193 loc) · 6.95 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
---
fullname: Stable sort algorithms in Coq
shortname: stablesort
organization: pi8027
action: true
dune: false
synopsis: >-
Stable sort algorithms and their stability proofs in Coq
description: |-
This library provides a generic and modular way to prove the correctness,
including stability, of several mergesort functions. The correctness lemmas in
this library are overloaded using a canonical structure
(`StableSort.function`). This structure characterizes stable mergesort
functions, say `sort`, by its abstract version `asort` parameterized over the
type of sorted lists and its operators such as merge, the relational
parametricity of `asort`, and two equational properties that `asort`
instantiated with merge and concatenation are `sort` and the identity
function, respectively, which intuitively mean that replacing merge with
concatenation turns `sort` into the identity function.
From this characterization, we derive an induction principle over
traces—binary trees reflecting the underlying divide-and-conquer structure of
mergesort—to reason about the relation between the input and output of
`sort`, and the naturality of `sort`. These two properties are sufficient to
deduce several correctness results of mergesort, including stability. Thus,
one may prove the stability of a new sorting function by defining its abstract
version, proving the relational parametricity of the latter using the
parametricity translation (the Paramcoq plugin), and manually providing the
equational properties.
As an application of the above proof methodology, this library provides two
kinds of optimized mergesorts.
The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
they allow us to compute the first k smallest elements of a list of length n
in the optimal O(n + k log k) time complexity of the partial and incremental
sorting problems. However, the non-tail-recursive merge function linearly
consumes the call stack and triggers a stack overflow in call-by-value
evaluation.
The second kind is tail-recursive mergesorts and thus solves the above issue
in call-by-value evaluation. However, it does not allow us to compute the
output incrementally regardless of the evaluation strategy.
Therefore, there is a performance trade-off between non-tail-recursive and
tail-recursive mergesorts, and the best mergesort function for lists depends
on the situation, in particular, the evaluation strategy and whether it should
be incremental or not.
In addition, each of the above two kinds of mergesort functions has a smooth
(also called natural) variant of mergesort, which takes advantage of sorted
slices in the input.
publications:
- pub_url: https://arxiv.org/abs/2403.08173
pub_title: A bargain for mergesorts (functional pearl) — How to prove your mergesort correct and stable, almost for free
pub_doi: 10.48550/arXiv.2403.08173
authors:
- name: Kazuhiko Sakaguchi
initial: true
- name: Cyril Cohen
initial: false
opam-file-maintainer: kazuhiko.sakaguchi@inria.fr
license:
fullname: CeCILL-B Free Software License Agreement
identifier: CECILL-B
file: CeCILL-B
supported_coq_versions:
text: 8.13 or later
opam: '{>= "8.13"}'
tested_coq_nix_versions:
tested_coq_opam_versions:
- version: '1.13.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.18.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.18.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.18.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.19.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.19.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.19.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.19.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.20'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "1.13.0"}'
description: |-
[MathComp](https://math-comp.github.io) 1.13.0 or later
- opam:
name: coq-paramcoq
version: '{>= "1.1.3"}'
description: |-
[Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
- opam:
name: coq-mathcomp-zify
version: '{with-test}'
description: |-
[Mczify](https://github.com/math-comp/mczify) (required only for the test suite)
- opam:
name: coq-equations
version: '{with-test}'
description: |-
[Equations](https://github.com/mattam82/Coq-Equations) (required only for the test suite)
test_target: build-misc
namespace: stablesort
action_appendix: |2-
export: 'OPAMWITHTEST'
env:
OPAMWITHTEST: true
build: |-
## Building and installation instructions
The easiest way to install the development version of Stable sort algorithms in Coq
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
``` shell
git clone https://github.com/pi8027/stablesort.git
cd stablesort
opam repo add coq-released https://coq.inria.fr/opam/released
opam install ./coq-stablesort.opam
```
documentation: |-
## Credits
The mergesort functions and the stability proofs provided in this library are
mostly based on ones in the `path` library of Mathematical Components.
---