git @ Cat's Eye Technologies The-Glosscubator / f7b5ff1
Rate and add commentary on another paper. Chris Pressey 1 year, 13 days ago
4 changed file(s) with 68 addition(s) and 7 deletion(s). Raw diff Collapse all Expand all
+1
-1
README.md less more
2121 Of these, [**109** have the highest rating](by-rating/Top-rated.md),
2222 [**28** are considered classics](by-rating/Classic.md),
2323 [**51** are considered very interesting](by-rating/Very%20Interesting.md),
24 while [**70** are yet to be rated](by-rating/Unrated.md).
24 while [**69** are yet to be rated](by-rating/Unrated.md).
2525
2626 <!-- /TOTALS -->
2727
+0
-1
by-rating/Unrated.md less more
154154
155155 ### Name Binding
156156
157 * Abstract Syntax for Variable Binders ([web.archive.org](https://web.archive.org/web/20240415115853/http://www.lix.polytechnique.fr/~dale/papers/cl2000.pdf))
158157 * [I am not a Number, I am a Free Variable](http://www.e-pig.org/downloads/notanum.pdf)
159158 * [A Type and Scope Safe Universe of Syntaxes with Binding](https://pure.strath.ac.uk/ws/portalfiles/portal/114903157/Allais_etal_ICFP2018_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf)
160159
+2
-1
by-topic/Modal Logic/commentary/Chris Pressey.md less more
3030
3131 * rating: 1
3232
33 Dynamic logic is a kind of modal logic. Inside this book there is a good exposition on equational logic as well.
33 Dynamic logic is a kind of modal logic. Inside this book, in Section 3.3 to be
34 precise, there is a very good introductory exposition on equational logic as well.
3435
3536 ### Modal Logic for Open Minds
3637
+65
-4
by-topic/Name Binding/commentary/Chris Pressey.md less more
6060 anyway, you want to move the name-binding abstraction to the meta-level.
6161 In most cases I imagine you could do the very same thing with binding
6262 abstractions in the object language. Perhaps lifting them to the
63 meta-level makes the transformations tidier in some way.
63 meta-level makes the transformations tidier in some way. (The conclusion
64 of "Abstract Syntax for Variable Binders" seems to be addressing this
65 concern: apparently this view is "impatient" and these issues are
66 foundational enough that they need to be addressed in a principled
67 fashion, like this.)
6468
6569 How to recurse into these lambda abstractions? Define some inference
6670 rules at the meta-level, then
7680
7781 ### Abstract Syntax for Variable Binders
7882
79 * rating: TODO
80
81 .
83 * rating: 1
84
85 (These are older notes, and if I read the paper again today, I might
86 write them differently.)
87
88 Sometimes we want to write programs that manipulate other programs.
89 Other programs have variables in them that have scopes and stuff.
90 It would behoove us to have a representation of these other programs
91 that would allow us to reason about them modulo those variables.
92 e.g. compare two functions without regard to the names used for
93 their formal parameters.
94
95 Programs have concrete syntax and abstract syntax. But what we're
96 talking about here is even more abstract than abstract syntax is
97 usually considered. It abstracts away name bindings.
98
99 The second section starts talking about Church's STT (as a logical
100 system). Then starts talking about "equality modulo alpha, beta,
101 eta equivalence". This is higher-order abstract syntax (HOAS).
102
103 Miller proposes HOAS to be an _equational theory_ at the
104 meta level that does not distinguish between object level forms
105 if they are alpha, beta, eta convertible. This is different from
106 how HOAS is conceived in Haskell, which is "merely" using the
107 meta-level (Haskell-level) lambda to implement object-level lambda,
108 but this is mainly because Haskell is "merely" a programming language.
109
110 Pfenning and Elliott have already coined the term "HOAS" and
111 have proposed using a lambda calculus with product type and
112 polymorphism. But Miller says
113
114 > In practice, higher-order abstract syntax has generally come to refer
115 > to the encoding and manipulating of syntax using either simply or dependently
116 > typed λ-calculus modulo α, β, and η-conversion.
117
118 Then he starts talking about big-L-sub-lambda, and unification
119 therein, which is basically unification of lambda terms in
120 Lambda Prolog (which is where Miller has applied HOAS.)
121
122 big-L-sub-lambda uses a weaker version of beta-conversion that
123 is called "beta-0 conversion".
124
125 Finally Miller gets to lambda-tree syntax:
126
127 > In contrast to concrete syntax and parse tree syntax, a third level of syntax
128 > representation, named λ-tree syntax was introduced in \[Foundational Aspects of Syntax\]
129
130 Note that Harper's abstract binding trees are also described (by Harper) as a third level
131 of syntax, more abstract than abstract syntax.
132
133 Miller prefers the term "lambda-tree syntax" over "higher-order abstract syntax"
134 because:
135
136 * it has only beta-0 reduction (not full beta reduction -- Pfenning is quoted as
137 saying "higher-order abstract syntax supports substitution through λ-reduction
138 in the meta-language")
139 * it doesn't rely on types (he regards "higher order" as referring to types.)
140
141 (I would agree that "higher-order" is not greatly stable nomenclature, and often
142 refers to things in ways that I don't expect it to refer to them in!)
82143
83144 ### A Simple Take on Typed Abstract Syntax in Haskell-like Languages
84145