git @ Cat's Eye Technologies The-Glosscubator / 9f35aed
Split commentary file into smaller commentary files. Chris Pressey 1 year, 28 days ago
10 changed file(s) with 392 addition(s) and 316 deletion(s). Raw diff Collapse all Expand all
+28
-0
Compiler Construction/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Compiler Construction
13 ---------------------
14
15 ### The essence of compiling with continuations
16
17 * rating: 3
18
19 This is the paper that introduces "A-normal form".
20
21 This paper can sometimes be found attached to a newer paper which is a retrospective on the original paper.
22
23 ### An Introduction to Operational Semantics
24
25 * rating: 2
26
27 Actually a book chapter. future-topics: Formal Semantics
+37
-0
Coq/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Coq
13 ---
14
15 ### Pragmatic Quotient Types in Coq
16
17 * rating: 1
18
19 It has more detail than I need on the implementation and how the
20 implementation fits into how Coq sees the world (that's the
21 "pragmatic" part I suppose) but the explanation of quotienting
22 in the intro, it's worth reading just for that.
23
24 ### Interaction Trees
25
26 * rating: 2
27
28 I thought this was very intruiging.
29 The ITree described in the paper is basically the so-called
30 "freer monad". They add a "Tau" to it to make it compatible
31 with Coq (where all expressions must terminate). Tau is
32 weirdly reminiscent of "stuttering" in TLA+, but that might
33 be a coincidence.
34
35 But many of the equations presented in the paper seem surprisingly
36 equational, too. I don't know what I mean by that.
+60
-0
Modal Logic/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Modal Logic
13 -----------
14
15 ### Mathematical Modal Logic: A View of its Evolution
16
17 * rating: 1
18
19 Only skimmed. Historical overview. Not bad but more information than I probably need.
20
21 ### Topological semantics of modal logic
22
23 * rating: TODO
24
25 Like some beaches I've been at, this starts out really fine and then gets deep, QUICK.
26
27 ### Topology, Connectedness, and Modal Logic
28
29 * rating: TODO
30
31 I should take some notes here.
32
33 ### A Modal Walk Through Space
34
35 * rating: TODO
36
37 I should take some notes here.
38
39 ### The Situation Calculus: A Case for Modal Logic
40
41 * rating: 0
42
43 So the idea is that if you use modal logic in the situation calculus, it becomes more
44 useful for stating some things. No doubt, but in the longer view I'm skeptical. One
45 of the strengths of the situation calculus is that it can be stated in a bog-standard
46 logic (FOL) and that it has an efficient "resolution algorithm" for planning. While
47 I can definitely see why one might be tempted to use modal logic here, I'm not
48 convinced that it's an improvement, at least not for the use cases that interest me.
49
50 ### Modal Mu-Calculi
51
52 * rating: TODO
53
54 mu-Calculus can express CTL and related temporal logics.
55
56 This PDF of a book chapter is available
57 [on the first author's website](https://www.julianbradfield.org/Research/pubs.html#mlh-chapter).
58 I like how it's described as
59 "a chapter for the (very expensive) Handbook of Modal Logic, published by Elsevier in 2006".
+35
-0
Model Checking/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Model Checking
13 --------------
14
15 ### Model Checking CTL is Almost Always Inherently Sequential
16
17 * rating: 0
18
19 By "inherently sequential" they mean P-complete. Model checking for CTL is already known
20 to be P-complete, but they show it for a whole bunch of different fragments too.
21
22 ### Cycle Detection in Computation Tree Logic
23
24 * rating: 1
25
26 A variation of CTL* which is aware of cycles is defined; it is called Cycle-CTL*. Various
27 things are proven about Cycle-CTL*. It is a very expressive language for statements
28 about the temporal behaviour of a system.
29
30 ### Direct Model-checking of SysML Models
31
32 * rating: TODO
33
34 .
+50
-0
PLDI/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 PLDI
13 ----
14
15 ### Fundamental Concepts in Programming Languages
16
17 * rating: classic
18
19 Strachey notes, among many other things, that mathematicians seem to have problems seeing functions
20 as first-class objects. (This is a sentiment I've seen repeated in a number of places, including
21 Wouter van Oortmerssen's thesis on the term-rewriting language Aardappel.) This coincides, in an
22 oblique way, with defunctionalization.
23
24 ### Definitional interpreters for higher-order programming languages
25
26 * rating: classic
27
28 This is the paper where the term "meta-circular" is introduced (while discussing the
29 wisdom of trying to define the meaning of a language using an interpreter written in
30 another language, or possibly even that same language) as well as the term "defunctionalization".
31 Reynolds notes a connection between defunctionalized interpreters and state machines,
32 and also gives us this pithy statement:
33
34 > Although the basic concept of assignment is well understood by any competent programmer,
35 > a surprising degree of care is needed to combine this concept with the language features
36 > we have discussed previously.
37
38 This paper was republished in Higher-Order and Symbolic Computation, issue 11, in 1998
39 (pages 363–397). There is another paper
40 "[Definitional interpreters revisited](http://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-revisited.pdf)"
41 (PDF) where Reynolds recollects on this paper.
42
43 ### Trampolined style
44
45 * rating: 3
46
47 This is my own slogan: Trampolines are just defunctionalized continuations. The `cont`
48 function in Interpreter III in Reynolds' "Definitional interpreters for higher-order programming languages"
49 is an example of a trampoline.
+68
-0
Reactive Systems/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Reactive Systems
13 ----------------
14
15 ### Synchronous Programming of Reactive Systems
16
17 * rating: 1
18
19 A good point in here is when they make the distinction between the "reactive kernel"
20 and the rest of the system, the interface and data mangement components.
21
22 ### Statecharts
23
24 * rating: 3
25
26 I would rate this as "classic" except that, unlike most classics, it is easy to
27 understand even on the first reading.
28
29 Even if you're not sold on the visual formalism Harel presents, it's worth thinking about
30 what it means to have a formal description of the reactive behaviour of a system, and what
31 it means to combine such formal descriptions hierarchically and in parallel.
32
33 For motivating why one should care about the reactive behaviour of their app
34 (or other system) in the first place, see "State Machines for Event-Driven Systems" by
35 Miro Samek.
36
37 ### State Machines for Event-Driven Systems
38
39 * rating: 3
40
41 Samek makes a very persuasive case for using state machines to describe the
42 reactive behaviour of software. Ad-hoc introduction of state variables
43 (especially boolean flags), as opposed to stepping back and thinking about
44 the thing as a finite state-transition system, is a common beginner mistake
45 that leads to "spaghetti state" and, quite often, bugs (where a state that
46 simply shouldn't exist, is entered, with undefined behaviour).
47
48 It seems that most of this article was originally published as
49 "[Who Moved my State?](https://web.archive.org/web/20160207112615/http://www.drdobbs.com/who-moved-my-state/184401643)"
50 in the "The Embedded Angle" column of Dr Dobbs Journal in 2003. There were a couple of followup articles,
51 including "[Back to Basics](https://web.archive.org/web/20090906195311/http://www.ddj.com/cpp/184401737?pgno=5)"
52 and "[Dj Vu](https://web.archive.org/web/20120930224548/http://www.drdobbs.com/dj-vu/184401665)".
53 Nowadays these seem to only be available in archive.org's WayBack machine.
54
55 ### Misunderstandings about state machines
56
57 * rating: 3
58
59 A very unusual whitepaper. Not many whitepapers contain this much polemic.
60 However, underneath it there are a number of keen observations.
61
62 ### Embedded State Machine Implementation, 12/2000
63
64 * rating: 1
65
66 A very straightforward and easy-to-understand article on some methods
67 for developing a state machine-based control program.
+59
-0
Term Rewriting/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Term Rewriting
13 --------------
14
15 ### Advanced Topics in Term Rewriting
16
17 * rating: 2
18
19 .
20
21 ### Reflection in Rewriting Logic
22
23 * rating: 0
24
25 .
26
27 ### Combinatory Reduction Systems
28
29 * rating: 2
30
31 Ahh, it is a poorly-written paper, but, it is also covering a very interesting
32 subject matter, and, it does give a formal definition of CRS'es. CRS'es are
33 term rewriting systems that support name binding, like the lambda calculus does.
34
35 ### Matching Power
36
37 * rating: 1
38
39 A simple (mostly) exposition of the rho-calculus, a lambda calculus-like
40 calculus for term rewriting systems, or for lambda calculus with matching.
41
42 ### The Rho Cube
43
44 * rating: TODO
45
46 .
47
48 ### A Constructive Semantics for Rewriting Logic
49
50 * rating: 2
51
52 PhD thesis. Has a few good things in it.
53
54 ### Rewriting Logic as a Logical and Semantic Framework
55
56 * rating: 0
57
58 .
+51
-0
Topology/commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Topology
13 --------
14
15 ### Introduction to topology
16
17 * rating: 1
18
19 .
20
21 ### Counterexamples in Topology
22
23 * rating: 3
24
25 .
26
27 ### The Lattice of Topologies: Structure and Complementation
28
29 * rating: classic
30
31 The set of all topologies on a set forms a lattice where the discrete
32 topology is the supremum and the trivial topology is the infimum.
33
34 ### Finite Topological Spaces
35
36 * rating: TODO
37
38 Lecture notes.
39
40 ### A Short Study of Alexandroff Spaces
41
42 * rating: TODO
43
44 .
45
46 ### general topology - Topological matroids? - Mathematics Stack Exchange
47
48 * rating: 1
49
50 .
+0
-311
commentary/Chris Pressey.md less more
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Compiler Construction
13 ---------------------
14
15 ### The essence of compiling with continuations
16
17 * rating: 3
18
19 This is the paper that introduces "A-normal form".
20
21 This paper can sometimes be found attached to a newer paper which is a retrospective on the original paper.
22
23 ### An Introduction to Operational Semantics
24
25 * rating: 2
26
27 Actually a book chapter. future-topics: Formal Semantics
28
29 Coq
30 ---
31
32 ### Pragmatic Quotient Types in Coq
33
34 * rating: 1
35
36 It has more detail than I need on the implementation and how the
37 implementation fits into how Coq sees the world (that's the
38 "pragmatic" part I suppose) but the explanation of quotienting
39 in the intro, it's worth reading just for that.
40
41 ### Interaction Trees
42
43 * rating: 2
44
45 I thought this was very intruiging.
46 The ITree described in the paper is basically the so-called
47 "freer monad". They add a "Tau" to it to make it compatible
48 with Coq (where all expressions must terminate). Tau is
49 weirdly reminiscent of "stuttering" in TLA+, but that might
50 be a coincidence.
51
52 But many of the equations presented in the paper seem surprisingly
53 equational, too. I don't know what I mean by that.
54
55 Modal Logic
56 -----------
57
58 ### Mathematical Modal Logic: A View of its Evolution
59
60 * rating: 1
61
62 Only skimmed. Historical overview. Not bad but more information than I probably need.
63
64 ### Topological semantics of modal logic
65
66 * rating: TODO
67
68 Like some beaches I've been at, this starts out really fine and then gets deep, QUICK.
69
70 ### Topology, Connectedness, and Modal Logic
71
72 * rating: TODO
73
74 I should take some notes here.
75
76 ### A Modal Walk Through Space
77
78 * rating: TODO
79
80 I should take some notes here.
81
82 ### The Situation Calculus: A Case for Modal Logic
83
84 * rating: 0
85
86 So the idea is that if you use modal logic in the situation calculus, it becomes more
87 useful for stating some things. No doubt, but in the longer view I'm skeptical. One
88 of the strengths of the situation calculus is that it can be stated in a bog-standard
89 logic (FOL) and that it has an efficient "resolution algorithm" for planning. While
90 I can definitely see why one might be tempted to use modal logic here, I'm not
91 convinced that it's an improvement, at least not for the use cases that interest me.
92
93 ### Modal Mu-Calculi
94
95 * rating: TODO
96
97 mu-Calculus can express CTL and related temporal logics.
98
99 This PDF of a book chapter is available
100 [on the first author's website](https://www.julianbradfield.org/Research/pubs.html#mlh-chapter).
101 I like how it's described as
102 "a chapter for the (very expensive) Handbook of Modal Logic, published by Elsevier in 2006".
103
104 Model Checking
105 --------------
106
107 ### Model Checking CTL is Almost Always Inherently Sequential
108
109 * rating: 0
110
111 By "inherently sequential" they mean P-complete. Model checking for CTL is already known
112 to be P-complete, but they show it for a whole bunch of different fragments too.
113
114 ### Cycle Detection in Computation Tree Logic
115
116 * rating: 1
117
118 A variation of CTL* which is aware of cycles is defined; it is called Cycle-CTL*. Various
119 things are proven about Cycle-CTL*. It is a very expressive language for statements
120 about the temporal behaviour of a system.
121
122 ### Direct Model-checking of SysML Models
123
124 * rating: TODO
125
126 .
127
128 PLDI
129 ----
130
131 ### Fundamental Concepts in Programming Languages
132
133 * rating: classic
134
135 Strachey notes, among many other things, that mathematicians seem to have problems seeing functions
136 as first-class objects. (This is a sentiment I've seen repeated in a number of places, including
137 Wouter van Oortmerssen's thesis on the term-rewriting language Aardappel.) This coincides, in an
138 oblique way, with defunctionalization.
139
140 ### Definitional interpreters for higher-order programming languages
141
142 * rating: classic
143
144 This is the paper where the term "meta-circular" is introduced (while discussing the
145 wisdom of trying to define the meaning of a language using an interpreter written in
146 another language, or possibly even that same language) as well as the term "defunctionalization".
147 Reynolds notes a connection between defunctionalized interpreters and state machines,
148 and also gives us this pithy statement:
149
150 > Although the basic concept of assignment is well understood by any competent programmer,
151 > a surprising degree of care is needed to combine this concept with the language features
152 > we have discussed previously.
153
154 This paper was republished in Higher-Order and Symbolic Computation, issue 11, in 1998
155 (pages 363–397). There is another paper
156 "[Definitional interpreters revisited](http://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-revisited.pdf)"
157 (PDF) where Reynolds recollects on this paper.
158
159 ### Trampolined style
160
161 * rating: 3
162
163 This is my own slogan: Trampolines are just defunctionalized continuations. The `cont`
164 function in Interpreter III in Reynolds' "Definitional interpreters for higher-order programming languages"
165 is an example of a trampoline.
166
167 Reactive Systems
168 ----------------
169
170 ### Synchronous Programming of Reactive Systems
171
172 * rating: 1
173
174 A good point in here is when they make the distinction between the "reactive kernel"
175 and the rest of the system, the interface and data mangement components.
176
177 ### Statecharts
178
179 * rating: 3
180
181 I would rate this as "classic" except that, unlike most classics, it is easy to
182 understand even on the first reading.
183
184 Even if you're not sold on the visual formalism Harel presents, it's worth thinking about
185 what it means to have a formal description of the reactive behaviour of a system, and what
186 it means to combine such formal descriptions hierarchically and in parallel.
187
188 For motivating why one should care about the reactive behaviour of their app
189 (or other system) in the first place, see "State Machines for Event-Driven Systems" by
190 Miro Samek.
191
192 ### State Machines for Event-Driven Systems
193
194 * rating: 3
195
196 Samek makes a very persuasive case for using state machines to describe the
197 reactive behaviour of software. Ad-hoc introduction of state variables
198 (especially boolean flags), as opposed to stepping back and thinking about
199 the thing as a finite state-transition system, is a common beginner mistake
200 that leads to "spaghetti state" and, quite often, bugs (where a state that
201 simply shouldn't exist, is entered, with undefined behaviour).
202
203 It seems that most of this article was originally published as
204 "[Who Moved my State?](https://web.archive.org/web/20160207112615/http://www.drdobbs.com/who-moved-my-state/184401643)"
205 in the "The Embedded Angle" column of Dr Dobbs Journal in 2003. There were a couple of followup articles,
206 including "[Back to Basics](https://web.archive.org/web/20090906195311/http://www.ddj.com/cpp/184401737?pgno=5)"
207 and "[Dj Vu](https://web.archive.org/web/20120930224548/http://www.drdobbs.com/dj-vu/184401665)".
208 Nowadays these seem to only be available in archive.org's WayBack machine.
209
210 ### Misunderstandings about state machines
211
212 * rating: 3
213
214 A very unusual whitepaper. Not many whitepapers contain this much polemic.
215 However, underneath it there are a number of keen observations.
216
217 ### Embedded State Machine Implementation, 12/2000
218
219 * rating: 1
220
221 A very straightforward and easy-to-understand article on some methods
222 for developing a state machine-based control program.
223
224 Term Rewriting
225 --------------
226
227 ### Advanced Topics in Term Rewriting
228
229 * rating: 2
230
231 .
232
233 ### Reflection in Rewriting Logic
234
235 * rating: 0
236
237 .
238
239 ### Combinatory Reduction Systems
240
241 * rating: 2
242
243 Ahh, it is a poorly-written paper, but, it is also covering a very interesting
244 subject matter, and, it does give a formal definition of CRS'es. CRS'es are
245 term rewriting systems that support name binding, like the lambda calculus does.
246
247 ### Matching Power
248
249 * rating: 1
250
251 A simple (mostly) exposition of the rho-calculus, a lambda calculus-like
252 calculus for term rewriting systems, or for lambda calculus with matching.
253
254 ### The Rho Cube
255
256 * rating: TODO
257
258 .
259
260 ### A Constructive Semantics for Rewriting Logic
261
262 * rating: 2
263
264 PhD thesis. Has a few good things in it.
265
266 ### Rewriting Logic as a Logical and Semantic Framework
267
268 * rating: 0
269
270 .
271
272 Topology
273 --------
274
275 ### Introduction to topology
276
277 * rating: 1
278
279 .
280
281 ### Counterexamples in Topology
282
283 * rating: 3
284
285 .
286
287 ### The Lattice of Topologies: Structure and Complementation
288
289 * rating: classic
290
291 The set of all topologies on a set forms a lattice where the discrete
292 topology is the supremum and the trivial topology is the infimum.
293
294 ### Finite Topological Spaces
295
296 * rating: TODO
297
298 Lecture notes.
299
300 ### A Short Study of Alexandroff Spaces
301
302 * rating: TODO
303
304 .
305
306 ### general topology - Topological matroids? - Mathematics Stack Exchange
307
308 * rating: 1
309
310 .
+4
-5
scripts/build_readmes.py less more
120120 self.repos = repos
121121 self.books = books
122122 self.papers = papers
123 self.commentary = {}
123124 self.topics = read_document_from(os.path.join(base_dir, "TOPICS.md")).to_json_data()
124125 self.topic_dirs = set([f for f in os.listdir(self.base_dir) if self.is_bookmark_dir(f)])
125126 self.seen_dirs = set()
179180 for entry in self.papers.get(topic, []):
180181 check_entry(topic, entry)
181182
182 def load_commentary(self):
183 path = os.path.join(self.base_dir, "commentary", "Chris Pressey.md")
183 def load_commentary(self, topic):
184 path = os.path.join(self.base_dir, topic, "commentary", "Chris Pressey.md")
184185 sections = []
185186 if os.path.isfile(path):
186187 sections = read_document_from(path).to_json_data()["sections"]
187 self.commentary = {}
188188 for item in sections:
189189 assert item["title"] not in self.commentary
190190 self.commentary[item["title"]] = item
258258
259259 c = Collector(options.base_dir, webpages, repos, books, papers)
260260
261 c.load_commentary()
262
263261 topic_sections = {}
264262 seen_dirs = set()
265263 for section in sorted(c.topics["sections"], key=lambda s: s["title"]):
268266 used_in = section["properties"]["used-in"]
269267 if "bookmarks" not in used_in:
270268 continue
269 c.load_commentary(topic)
271270 c.load_topic(topic)
272271 topic_sections[topic] = section
273272